Encyclopedia Gravity Gravity Seven Gaps Ledger Energy Bridge Quadratic Curvature Energy Strain Hinges

ARTICLE 4 claims 2 theorems 2 models

Gravity Seven Gaps Ledger Energy Bridge Quadratic Curvature Energy Strain Hinges

A machine-checked proof shows that a certain discrete curvature energy, built from hinge areas and angle deficits, is exactly half the sum of squared potential differences across all cell pairs.

Verify this page

The hinge energy identity

In discrete geometry, a common way to measure curvature is to look at hinges: the edges where two flat faces meet. Each hinge has an area and a deficit angle, the amount by which the sum of the surrounding angles falls short of a full circle. The quadratic curvature energy is the sum over all hinges of the area times the square of the deficit. The declaration quadraticCurvatureEnergy_strainHinges proves that, for a strain field that comes from a cell potential (a function assigning a number to each cell), this hinge-based energy equals exactly half the sum of the squared differences of that potential over all ordered pairs of cells.

The proof is a theorem in the framework's machine-checked library of formal theorems. It is a purely algebraic identity: given a potential f, the hinge areas are all set to 1/2 and the deficits are the differences f(i) - f(j). The theorem then shows the two sides match with no approximation. This is not a physical claim about real spacetime; it is a statement about two mathematical definitions being equal under a specific construction.

The identity matters because it connects two sides of a bridge. On one side, the ledger energy, a cost computed from a recognition ledger, uses the J-cost function. On the other side, the geometric energy uses hinge data. The matching theorem coboundary_totalCost_quadratic_matching shows that, for small strains, the ledger energy is close to the quadratic curvature energy, with an error bounded by a fourth-order term. The identity quadraticCurvatureEnergy_strainHinges is the exact, zero-error version of that match for the specific hinge construction.

What the declaration does not claim is equally important. It does not claim that this hinge construction is the unique or physically correct one. The canonical bridge instance instantiates the hinge data from the ledger's own potential, so it certifies shape compatibility, not a match against independently derived Regge geometry. The comparison of Hessian symbols closed on 2026-07-22 under amended intent, but the status flag for that comparison is false, and tensor multichannel escalation remains open. The identity is a proved algebraic fact, not a physical law.

In Recognition Science, this identity is a step toward showing that a discrete ledger of recognition events can produce geometric curvature. The framework models a ledger as a discrete record of events with a forced cost. The theorem shows that, for a restricted class of strain fields, the ledger's cost matches a standard geometric energy. That match is the bridge, and the identity is its exact hinge-based foundation.

THEOREM quadraticCurvatureEnergy_strainHinges · IndisputableMonolith/Gravity/SevenGaps/LedgerEnergyBridge.lean
quadraticCurvatureEnergy_strainHinges · IndisputableMonolith/Gravity/SevenGaps/LedgerEnergyBridge.lean:419 
/-- **THEOREM.** The quadratic curvature energy of the strain hinge data is
half the ordered-pair sum of squared potential differences. -/
theorem quadraticCurvatureEnergy_strainHinges {Λ : Type*} [Fintype Λ]
    (f₀ : Λ → ℝ) :
    quadraticCurvatureEnergy (strainHingeAreas Λ) (strainHingeDeficits f₀)
      = (∑ i, ∑ j, (f₀ i - f₀ j) ^ 2) / 2 := by
  unfold quadraticCurvatureEnergy strainHingeAreas strainHingeDeficits
  rw [Fintype.sum_prod_type]
  rw [Finset.sum_div]
  refine Finset.sum_congr rfl fun i _ => ?_
  rw [Finset.sum_div]
  refine Finset.sum_congr rfl fun j _ => ?_
  show (1 : ℝ) / 2 * (f₀ i - f₀ j) ^ 2 = (f₀ i - f₀ j) ^ 2 / 2
  ring
MODEL strainHingeAreas · strainHingeDeficits · IndisputableMonolith/Gravity/SevenGaps/LedgerEnergyBridge.lean
strainHingeAreas · IndisputableMonolith/Gravity/SevenGaps/LedgerEnergyBridge.lean:407 
/-- Uniform hinge areas for the ordered-pair hinge set Λ × Λ: each ordered
pair carries area 1/2, so that summing over ordered pairs matches the
per-unordered-pair weight 1. Purely geometric bookkeeping. -/
noncomputable def strainHingeAreas (Λ : Type*) : Λ × Λ → ℝ := fun _ => 1 / 2
strainHingeDeficits · IndisputableMonolith/Gravity/SevenGaps/LedgerEnergyBridge.lean:412 
/-- Hinge deficits induced by a cell potential: the hinge (i, j) carries
deficit f i − f j. This is hinge DATA (a signed deficit assignment); it is
consumed quadratically by `quadraticCurvatureEnergy`, so its sign is
invisible to the energy, exactly as the parity no-go requires. -/
noncomputable def strainHingeDeficits {Λ : Type*} (f : Λ → ℝ) :
    Λ × Λ → ℝ := fun p => f p.1 - f p.2
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
MODEL canonicalQuadraticEnergyBridge · IndisputableMonolith/Gravity/SevenGaps/LedgerEnergyBridge.lean
canonicalQuadraticEnergyBridge · IndisputableMonolith/Gravity/SevenGaps/LedgerEnergyBridge.lean:465 
/-- **THEOREM (canonical instance).** Every coboundary strain configuration
with small scaled strains yields a `LedgerToQuadraticEnergyBridge`: hinge
areas 1/2 on ordered pairs, hinge deficits f₀ i − f₀ j, matching proved by
`coboundary_totalCost_quadratic_matching`. No assumed fields. -/
noncomputable def canonicalQuadraticEnergyBridge {Λ : Type*} [Fintype Λ]
    [DecidableEq Λ] (f₀ : Λ → ℝ) (ε : ℝ)
    (hsmall : ∀ i j, |ε * (f₀ i - f₀ j)| ≤ 1) :
    LedgerToQuadraticEnergyBridge Λ where
  basePotential := f₀
  eps := ε
  small_strain := hsmall
  hingeArea := strainHingeAreas Λ
  hingeArea_nonneg := fun _ => by
    unfold strainHingeAreas
    norm_num
  hingeDeficit := strainHingeDeficits f₀
  matching := by
    rw [quadraticCurvatureEnergy_strainHinges f₀]
    have harg : ε ^ 2 * ((∑ i, ∑ j, (f₀ i - f₀ j) ^ 2) / 2)
        = ε ^ 2 / 2 * ∑ i, ∑ j, (f₀ i - f₀ j) ^ 2 := by ring
    rw [harg]
    exact coboundary_totalCost_quadratic_matching f₀ ε hsmall

What this page does not claim

The identity does not prove that the hinge construction is the unique or physically correct discrete curvature. The identity does not establish a match against independently derived Regge geometry. The identity does not make any claim about real spacetime physics.

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