Encyclopedia Gravity Gravity Seven Gaps Ledger Energy Bridge Coboundary Total Cost Quadratic Matching

ARTICLE 5 claims 5 theorems

Gravity Seven Gaps Ledger Energy Bridge Coboundary Total Cost Quadratic Matching

A machine-checked theorem shows that a ledger of recognition costs and a geometric curvature energy agree to fourth order, with the exact conditions and limits spelled out.

Verify this page

The matching theorem

The declaration coboundary_totalCost_quadratic_matching is a theorem in the Recognition Science framework's machine-checked library of formal theorems. It establishes a precise quantitative link between two seemingly unrelated objects: the total cost of a recognition ledger, which is a discrete record of events with an associated cost, and a geometric energy defined from hinge data, which are the areas and angle deficits of a discrete geometry. The theorem proves that, for a specific class of strain fields, the ledger's total cost is approximately equal to the quadratic curvature energy, with the error bounded by a fourth-order term.

The class of strain fields is the key restriction. The theorem applies only to coboundary strains, meaning strains that can be written as the difference of a cell potential: s(i,j) = f(i) - f(j). For such strains, the theorem proves that the ledger's total cost, which is a sum of J-costs, is within a specific bound of the quadratic energy. The bound is: |totalCost - (ε²/2)·S₂| ≤ (ε⁴/2)·S₄, where S₂ and S₄ are sums of squared and fourth-power potential differences, and ε is a small deformation parameter. This holds under the explicit hypothesis that |ε·(f₀i - f₀j)| ≤ 1 for all i, j.

This matching theorem is significant because it shows that the ledger's cost, which is derived from the J-cost function, behaves like a curvature energy in the small-deformation limit. The theorem is proved in Lean 4 with no axioms beyond the standard ones, and it is part of a larger effort to bridge the ledger formalism to geometry. However, the theorem does not claim that the ledger's cost is exactly equal to the geometric energy, only that they agree to second order with a controlled error. It also does not claim that the bridge works for all strains; the proof explicitly shows that general antisymmetric strains can violate the required gate condition.

The theorem's scope is further clarified by the status structure LedgerEnergyBridgeStatus, which records which parts of the bridge are proved and which remain open. The matching theorem itself is proved, as is the shear-visibility gate, which shows that a pure shear pattern carries nonzero ledger energy. But the Hessian-symbol comparison, which would certify a match against independently derived Regge geometry, is marked as open, and the tensor multichannel escalation is also open. These are targets for future work, not claims of the current theorem.

THEOREM coboundary_totalCost_quadratic_matching · IndisputableMonolith/Gravity/SevenGaps/LedgerEnergyBridge.lean
coboundary_totalCost_quadratic_matching · IndisputableMonolith/Gravity/SevenGaps/LedgerEnergyBridge.lean:339 
/-- **THEOREM (quadratic matching, explicit constants).** For the
one-parameter coboundary strain family ε·f₀ with all scaled strains in
[−1, 1], the total ledger cost matches the quadratic strain energy
(ε²/2)·S₂ to fourth order with explicit remainder constant 1/2:

  |totalCost(ε·f₀) − (ε²/2)·Σ_{i,j}(f₀ i − f₀ j)²|
      ≤ (ε⁴/2)·Σ_{i,j}(f₀ i − f₀ j)⁴.

Sums run over ORDERED pairs (each unordered pair counted twice). The
hypothesis |ε·(f₀ i − f₀ j)| ≤ 1 is the explicit small-strain premise; no
hidden assumptions. -/
theorem coboundary_totalCost_quadratic_matching {Λ : Type*} [Fintype Λ]
    [DecidableEq Λ] (f₀ : Λ → ℝ) (ε : ℝ)
    (hsmall : ∀ i j, |ε * (f₀ i - f₀ j)| ≤ 1) :
    |RecognitionLedger.totalCost
        (coboundaryStrainLedger (fun i => ε * f₀ i))
      - ε ^ 2 / 2 * ∑ i, ∑ j, (f₀ i - f₀ j) ^ 2|
      ≤ ε ^ 4 / 2 * ∑ i, ∑ j, (f₀ i - f₀ j) ^ 4 := by
  classical
  have hcost : ∀ i j : Λ,
      (coboundaryStrainLedger (fun i => ε * f₀ i)).cost i j
        = Cost.Jcost (Real.exp (ε * (f₀ i - f₀ j))) := by
    intro i j
    show Cost.Jcost (Real.exp (ε * f₀ i - ε * f₀ j)) = _
    have harg : ε * f₀ i - ε * f₀ j = ε * (f₀ i - f₀ j) := by ring
    rw [harg]
  have hexpand : RecognitionLedger.totalCost
      (coboundaryStrainLedger (fun i => ε * f₀ i))
      = ∑ i, ∑ j, Cost.Jcost (Real.exp (ε * (f₀ i - f₀ j))) := by
    unfold RecognitionLedger.totalCost
    exact Finset.sum_congr rfl fun i _ =>
      Finset.sum_congr rfl fun j _ => hcost i j
  have hquad : ε ^ 2 / 2 * ∑ i, ∑ j, (f₀ i - f₀ j) ^ 2
      = ∑ i, ∑ j, (ε * (f₀ i - f₀ j)) ^ 2 / 2 := by
    rw [Finset.mul_sum]
    refine Finset.sum_congr rfl fun i _ => ?_
    rw [Finset.mul_sum]
    exact Finset.sum_congr rfl fun j _ => by ring
  have hquart : ε ^ 4 / 2 * ∑ i, ∑ j, (f₀ i - f₀ j) ^ 4
      = ∑ i, ∑ j, (ε * (f₀ i - f₀ j)) ^ 4 / 2 := by
    rw [Finset.mul_sum]
    refine Finset.sum_congr rfl fun i _ => ?_
    rw [Finset.mul_sum]
    exact Finset.sum_congr rfl fun j _ => by ring
  rw [hexpand, hquad, hquart]
  have hcombine : ∑ i, ∑ j, Cost.Jcost (Real.exp (ε * (f₀ i - f₀ j)))
      - ∑ i, ∑ j, (ε * (f₀ i - f₀ j)) ^ 2 / 2
      = ∑ i, ∑ j, (Cost.Jcost (Real.exp (ε * (f₀ i - f₀ j)))
          - (ε * (f₀ i - f₀ j)) ^ 2 / 2) := by
    rw [← Finset.sum_sub_distrib]
    exact Finset.sum_congr rfl fun i _ => (Finset.sum_sub_distrib _ _).symm
  rw [hcombine]
  calc |∑ i, ∑ j, (Cost.Jcost (Real.exp (ε * (f₀ i - f₀ j)))
          - (ε * (f₀ i - f₀ j)) ^ 2 / 2)|
      ≤ ∑ i, |∑ j, (Cost.Jcost (Real.exp (ε * (f₀ i - f₀ j)))
          - (ε * (f₀ i - f₀ j)) ^ 2 / 2)| :=
        Finset.abs_sum_le_sum_abs _ _
    _ ≤ ∑ i, ∑ j, |Cost.Jcost (Real.exp (ε * (f₀ i - f₀ j)))
          - (ε * (f₀ i - f₀ j)) ^ 2 / 2| :=
        Finset.sum_le_sum fun i _ => Finset.abs_sum_le_sum_abs _ _
    _ ≤ ∑ i, ∑ j, (ε * (f₀ i - f₀ j)) ^ 4 / 2 :=
        Finset.sum_le_sum fun i _ => Finset.sum_le_sum fun j _ => by
          have h := Jcost_exp_sub_half_sq_abs_le (ε * (f₀ i - f₀ j))
            (hsmall i j)
          linarith
THEOREM coboundary_totalCost_quadratic_matching · IndisputableMonolith/Gravity/SevenGaps/LedgerEnergyBridge.lean
coboundary_totalCost_quadratic_matching · IndisputableMonolith/Gravity/SevenGaps/LedgerEnergyBridge.lean:339 
/-- **THEOREM (quadratic matching, explicit constants).** For the
one-parameter coboundary strain family ε·f₀ with all scaled strains in
[−1, 1], the total ledger cost matches the quadratic strain energy
(ε²/2)·S₂ to fourth order with explicit remainder constant 1/2:

  |totalCost(ε·f₀) − (ε²/2)·Σ_{i,j}(f₀ i − f₀ j)²|
      ≤ (ε⁴/2)·Σ_{i,j}(f₀ i − f₀ j)⁴.

Sums run over ORDERED pairs (each unordered pair counted twice). The
hypothesis |ε·(f₀ i − f₀ j)| ≤ 1 is the explicit small-strain premise; no
hidden assumptions. -/
theorem coboundary_totalCost_quadratic_matching {Λ : Type*} [Fintype Λ]
    [DecidableEq Λ] (f₀ : Λ → ℝ) (ε : ℝ)
    (hsmall : ∀ i j, |ε * (f₀ i - f₀ j)| ≤ 1) :
    |RecognitionLedger.totalCost
        (coboundaryStrainLedger (fun i => ε * f₀ i))
      - ε ^ 2 / 2 * ∑ i, ∑ j, (f₀ i - f₀ j) ^ 2|
      ≤ ε ^ 4 / 2 * ∑ i, ∑ j, (f₀ i - f₀ j) ^ 4 := by
  classical
  have hcost : ∀ i j : Λ,
      (coboundaryStrainLedger (fun i => ε * f₀ i)).cost i j
        = Cost.Jcost (Real.exp (ε * (f₀ i - f₀ j))) := by
    intro i j
    show Cost.Jcost (Real.exp (ε * f₀ i - ε * f₀ j)) = _
    have harg : ε * f₀ i - ε * f₀ j = ε * (f₀ i - f₀ j) := by ring
    rw [harg]
  have hexpand : RecognitionLedger.totalCost
      (coboundaryStrainLedger (fun i => ε * f₀ i))
      = ∑ i, ∑ j, Cost.Jcost (Real.exp (ε * (f₀ i - f₀ j))) := by
    unfold RecognitionLedger.totalCost
    exact Finset.sum_congr rfl fun i _ =>
      Finset.sum_congr rfl fun j _ => hcost i j
  have hquad : ε ^ 2 / 2 * ∑ i, ∑ j, (f₀ i - f₀ j) ^ 2
      = ∑ i, ∑ j, (ε * (f₀ i - f₀ j)) ^ 2 / 2 := by
    rw [Finset.mul_sum]
    refine Finset.sum_congr rfl fun i _ => ?_
    rw [Finset.mul_sum]
    exact Finset.sum_congr rfl fun j _ => by ring
  have hquart : ε ^ 4 / 2 * ∑ i, ∑ j, (f₀ i - f₀ j) ^ 4
      = ∑ i, ∑ j, (ε * (f₀ i - f₀ j)) ^ 4 / 2 := by
    rw [Finset.mul_sum]
    refine Finset.sum_congr rfl fun i _ => ?_
    rw [Finset.mul_sum]
    exact Finset.sum_congr rfl fun j _ => by ring
  rw [hexpand, hquad, hquart]
  have hcombine : ∑ i, ∑ j, Cost.Jcost (Real.exp (ε * (f₀ i - f₀ j)))
      - ∑ i, ∑ j, (ε * (f₀ i - f₀ j)) ^ 2 / 2
      = ∑ i, ∑ j, (Cost.Jcost (Real.exp (ε * (f₀ i - f₀ j)))
          - (ε * (f₀ i - f₀ j)) ^ 2 / 2) := by
    rw [← Finset.sum_sub_distrib]
    exact Finset.sum_congr rfl fun i _ => (Finset.sum_sub_distrib _ _).symm
  rw [hcombine]
  calc |∑ i, ∑ j, (Cost.Jcost (Real.exp (ε * (f₀ i - f₀ j)))
          - (ε * (f₀ i - f₀ j)) ^ 2 / 2)|
      ≤ ∑ i, |∑ j, (Cost.Jcost (Real.exp (ε * (f₀ i - f₀ j)))
          - (ε * (f₀ i - f₀ j)) ^ 2 / 2)| :=
        Finset.abs_sum_le_sum_abs _ _
    _ ≤ ∑ i, ∑ j, |Cost.Jcost (Real.exp (ε * (f₀ i - f₀ j)))
          - (ε * (f₀ i - f₀ j)) ^ 2 / 2| :=
        Finset.sum_le_sum fun i _ => Finset.abs_sum_le_sum_abs _ _
    _ ≤ ∑ i, ∑ j, (ε * (f₀ i - f₀ j)) ^ 4 / 2 :=
        Finset.sum_le_sum fun i _ => Finset.sum_le_sum fun j _ => by
          have h := Jcost_exp_sub_half_sq_abs_le (ε * (f₀ i - f₀ j))
            (hsmall i j)
          linarith
THEOREM IsCoboundary · IndisputableMonolith/Gravity/SevenGaps/LedgerEnergyBridge.lean
IsCoboundary · IndisputableMonolith/Gravity/SevenGaps/LedgerEnergyBridge.lean:213 
/-- A strain field is a coboundary if it is the difference field of a cell
potential: s i j = f i − f j. Coboundary strains are automatically
antisymmetric and satisfy the ratio cocycle property. -/
def IsCoboundary {Λ : Type*} (s : Λ → Λ → ℝ) : Prop :=
  ∃ f : Λ → ℝ, ∀ i j, s i j = f i - f j
THEOREM coboundary_totalCost_quadratic_matching · IndisputableMonolith/Gravity/SevenGaps/LedgerEnergyBridge.lean
coboundary_totalCost_quadratic_matching · IndisputableMonolith/Gravity/SevenGaps/LedgerEnergyBridge.lean:339 
/-- **THEOREM (quadratic matching, explicit constants).** For the
one-parameter coboundary strain family ε·f₀ with all scaled strains in
[−1, 1], the total ledger cost matches the quadratic strain energy
(ε²/2)·S₂ to fourth order with explicit remainder constant 1/2:

  |totalCost(ε·f₀) − (ε²/2)·Σ_{i,j}(f₀ i − f₀ j)²|
      ≤ (ε⁴/2)·Σ_{i,j}(f₀ i − f₀ j)⁴.

Sums run over ORDERED pairs (each unordered pair counted twice). The
hypothesis |ε·(f₀ i − f₀ j)| ≤ 1 is the explicit small-strain premise; no
hidden assumptions. -/
theorem coboundary_totalCost_quadratic_matching {Λ : Type*} [Fintype Λ]
    [DecidableEq Λ] (f₀ : Λ → ℝ) (ε : ℝ)
    (hsmall : ∀ i j, |ε * (f₀ i - f₀ j)| ≤ 1) :
    |RecognitionLedger.totalCost
        (coboundaryStrainLedger (fun i => ε * f₀ i))
      - ε ^ 2 / 2 * ∑ i, ∑ j, (f₀ i - f₀ j) ^ 2|
      ≤ ε ^ 4 / 2 * ∑ i, ∑ j, (f₀ i - f₀ j) ^ 4 := by
  classical
  have hcost : ∀ i j : Λ,
      (coboundaryStrainLedger (fun i => ε * f₀ i)).cost i j
        = Cost.Jcost (Real.exp (ε * (f₀ i - f₀ j))) := by
    intro i j
    show Cost.Jcost (Real.exp (ε * f₀ i - ε * f₀ j)) = _
    have harg : ε * f₀ i - ε * f₀ j = ε * (f₀ i - f₀ j) := by ring
    rw [harg]
  have hexpand : RecognitionLedger.totalCost
      (coboundaryStrainLedger (fun i => ε * f₀ i))
      = ∑ i, ∑ j, Cost.Jcost (Real.exp (ε * (f₀ i - f₀ j))) := by
    unfold RecognitionLedger.totalCost
    exact Finset.sum_congr rfl fun i _ =>
      Finset.sum_congr rfl fun j _ => hcost i j
  have hquad : ε ^ 2 / 2 * ∑ i, ∑ j, (f₀ i - f₀ j) ^ 2
      = ∑ i, ∑ j, (ε * (f₀ i - f₀ j)) ^ 2 / 2 := by
    rw [Finset.mul_sum]
    refine Finset.sum_congr rfl fun i _ => ?_
    rw [Finset.mul_sum]
    exact Finset.sum_congr rfl fun j _ => by ring
  have hquart : ε ^ 4 / 2 * ∑ i, ∑ j, (f₀ i - f₀ j) ^ 4
      = ∑ i, ∑ j, (ε * (f₀ i - f₀ j)) ^ 4 / 2 := by
    rw [Finset.mul_sum]
    refine Finset.sum_congr rfl fun i _ => ?_
    rw [Finset.mul_sum]
    exact Finset.sum_congr rfl fun j _ => by ring
  rw [hexpand, hquad, hquart]
  have hcombine : ∑ i, ∑ j, Cost.Jcost (Real.exp (ε * (f₀ i - f₀ j)))
      - ∑ i, ∑ j, (ε * (f₀ i - f₀ j)) ^ 2 / 2
      = ∑ i, ∑ j, (Cost.Jcost (Real.exp (ε * (f₀ i - f₀ j)))
          - (ε * (f₀ i - f₀ j)) ^ 2 / 2) := by
    rw [← Finset.sum_sub_distrib]
    exact Finset.sum_congr rfl fun i _ => (Finset.sum_sub_distrib _ _).symm
  rw [hcombine]
  calc |∑ i, ∑ j, (Cost.Jcost (Real.exp (ε * (f₀ i - f₀ j)))
          - (ε * (f₀ i - f₀ j)) ^ 2 / 2)|
      ≤ ∑ i, |∑ j, (Cost.Jcost (Real.exp (ε * (f₀ i - f₀ j)))
          - (ε * (f₀ i - f₀ j)) ^ 2 / 2)| :=
        Finset.abs_sum_le_sum_abs _ _
    _ ≤ ∑ i, ∑ j, |Cost.Jcost (Real.exp (ε * (f₀ i - f₀ j)))
          - (ε * (f₀ i - f₀ j)) ^ 2 / 2| :=
        Finset.sum_le_sum fun i _ => Finset.abs_sum_le_sum_abs _ _
    _ ≤ ∑ i, ∑ j, (ε * (f₀ i - f₀ j)) ^ 4 / 2 :=
        Finset.sum_le_sum fun i _ => Finset.sum_le_sum fun j _ => by
          have h := Jcost_exp_sub_half_sq_abs_le (ε * (f₀ i - f₀ j))
            (hsmall i j)
          linarith
THEOREM general_antisymmetric_strain_can_violate_rcl · IndisputableMonolith/Gravity/SevenGaps/LedgerEnergyBridge.lean
general_antisymmetric_strain_can_violate_rcl · IndisputableMonolith/Gravity/SevenGaps/LedgerEnergyBridge.lean:313 
/-- **THEOREM (honest scoping witness).** A general ANTISYMMETRIC strain
field need not yield an RCL-subadditive cost: on three cells, the
antisymmetric strain with s 0 2 = 1 but s 0 1 = s 1 2 = 0 gives
J(exp(s 0 2)) > 0 = R(J(exp(s 0 1)), J(exp(s 1 2))). This is why
`coboundaryStrainLedger` is scoped to coboundary strains: the scoping is
forced, not chosen. -/
theorem general_antisymmetric_strain_can_violate_rcl :
    ∃ s : Fin 3 → Fin 3 → ℝ, (∀ i j, s i j = - s j i) ∧
      ¬ (Cost.Jcost (Real.exp (s 0 2)) ≤
          RecognitionLedger.rclGate (Cost.Jcost (Real.exp (s 0 1)))
            (Cost.Jcost (Real.exp (s 1 2)))) := by
  refine ⟨gateViolatingStrain, gateViolatingStrain_antisymm, ?_⟩
  obtain ⟨h02, h01, h12⟩ := gateViolatingStrain_vals
  rw [h02, h01, h12, Real.exp_zero, Cost.Jcost_unit0]
  have hgate : RecognitionLedger.rclGate 0 0 = 0 := by
    unfold RecognitionLedger.rclGate
    ring
  rw [hgate]
  have hone : (1 : ℝ) < Real.exp 1 :=
    lt_trans (by norm_num) Real.exp_one_gt_d9
  have hpos : 0 < Cost.Jcost (Real.exp 1) :=
    Cost.Jcost_pos_of_ne_one _ (Real.exp_pos 1) (ne_of_gt hone)
  linarith

What this page does not claim

The theorem does not prove that the ledger's cost is exactly equal to the quadratic curvature energy for all strains. The theorem does not establish a match against independently derived Regge geometry, as the Hessian-symbol comparison remains open. The theorem does not apply to general antisymmetric strains, which can violate the gate condition.

Verify this page

Every tagged claim above names its theorem. To check one yourself rather than trust this page, elaborate the source module with Lean 4 and audit its axiom basis:

$ lake env lean IndisputableMonolith/Gravity/SevenGaps/LedgerEnergyBridge.lean
expected axiom basis: [propext, Classical.choice, Quot.sound] (the Lean kernel's standard three; no RS-specific axioms)

A page whose claims cannot be reproduced this way does not ship. In production, every anchor links to the exact declaration in the public source release, and this block carries the build receipt for the page itself.

Derived articles

This page is generated by a question-recursion engine: the questions its answers raise become the next pages. The current agenda, with open targets marked red:

MACHINE LAYER · GROUNDED CLAIM TABLE · CLICK TO EXPAND