Encyclopedia Gravity Gravity Seven Gaps Ledger Energy Bridge
ARTICLE 4 claims 4 theorems
Gravity Seven Gaps Ledger Energy Bridge
A machine-checked proof shows how a discrete record of strain costs can match a geometric energy, after an earlier guess failed.
The corrected bridge
The gravity seven gaps ledger energy bridge is a formal result inside Recognition Science, a framework that derives physical structure from the idea that reality keeps a ledger, a discrete record of events, and that the cost of each recognition event is forced by a proved equation. The bridge connects two separate descriptions of a strained lattice: one side measures the cost of deformation using the framework's cost function, and the other side measures a geometric energy built from hinge areas and squared deficits. The central theorem proves that, for a specific class of small deformations, these two sides agree to within a computable error bound.
The path to this result began with a failed guess. An earlier attempt assumed the ledger deficit directly equaled a signed geometric hinge deficit, but the proof shows this is impossible: ledger costs are nonnegative and even in the deformation size, while the signed geometric response is odd. The corrected bridge instead matches the ledger cost against a nonnegative, curvature-quadratic geometric energy, a discrete form of the Isaacson energy used in general relativity. This is a genuine correction, not a repackaging, and the result states it plainly.
The bridge is scoped to a specific class of strains. The ledger is well-defined when the strain between two cells is the difference of a single potential value, a condition called a coboundary. For this class, the matching theorem holds. The proof also shows the scope is necessary: it exhibits a general antisymmetric strain on three cells that violates the required gate condition, so the construction cannot be extended carelessly. This scoping is a theorem-backed necessity, not a convenience.
The key quantitative result is a matching bound. For a small deformation parameter ε and a base potential f₀, the theorem states that the absolute difference between the ledger's total cost and ε²/2 times a sum of squared potential differences is at most ε⁴/2 times a sum of fourth powers. This says the ledger cost is quadratic in the deformation to leading order, with a quartic error term. The proof uses the expansion J(exp t) = cosh t − 1, which is between t²/2 and (t²/2) cosh t, and bounds the remainder using cosh 1 < 2.
The result also shows the bridge sees a sector that a previous ansatz missed. A pure shear pattern on a rectangle, with horizontal strain h and vertical strain −h, carries strictly positive ledger energy for any nonzero h, and its quadratic hinge energy is also strictly positive. This shear-visibility result is a concrete payoff: the corrected bridge detects exactly the deformation that a conformal-average ansatz was blind to. The status flags confirm the proved theorems and mark the remaining open items, such as a tensor multichannel escalation, as targets for future work.
THEOREM general_antisymmetric_strain_can_violate_rcl · IndisputableMonolith/Gravity/SevenGaps/LedgerEnergyBridge.lean
/-- **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
THEOREM coboundary_totalCost_quadratic_matching · IndisputableMonolith/Gravity/SevenGaps/LedgerEnergyBridge.lean
/-- **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
/-- **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
THEOREM rectangleShear_ledgerEnergy_pos · rectangleShear_quadraticEnergy_pos · IndisputableMonolith/Gravity/SevenGaps/LedgerEnergyBridge.lean
/-- **THEOREM (shear-visibility gate).** The pure-shear rectangle strain
carries strictly positive ledger energy for every h ≠ 0. Shear is VISIBLE
to the corrected J-ledger bridge: the cell cost on the horizontal edge is
J(exp h) = cosh h − 1 > 0, and all cell costs are nonnegative. This is
exactly the transverse-traceless sector on which the conformal-average
ansatz was proved blind
(`Gravity.conformal_ansatz_cannot_recover_gravitational_waves`). -/
theorem rectangleShear_ledgerEnergy_pos (h : ℝ) (hh : h ≠ 0) :
0 < RecognitionLedger.totalCost
(coboundaryStrainLedger (rectangleShearPotential h)) := by
classical
unfold RecognitionLedger.totalCost
have hval : rectangleShearPotential h 0 - rectangleShearPotential h 1
= h := (rectangleShearPotential_strains h).1
have hterm :
0 < (coboundaryStrainLedger (rectangleShearPotential h)).cost 0 1 := by
show 0 < Cost.Jcost (Real.exp
(rectangleShearPotential h 0 - rectangleShearPotential h 1))
rw [hval, Cost.Jcost_exp_cosh]
have hcosh : 1 < Real.cosh h := Real.one_lt_cosh.mpr hh
linarith
have hinner :
0 < ∑ j, (coboundaryStrainLedger (rectangleShearPotential h)).cost 0 j := by
have hle := Finset.single_le_sum
(f := fun j => (coboundaryStrainLedger (rectangleShearPotential h)).cost 0 j)
(fun j _ => (coboundaryStrainLedger (rectangleShearPotential h)).nonneg 0 j)
(Finset.mem_univ 1)
linarith
have houter := Finset.single_le_sum
(f := fun i => ∑ j, (coboundaryStrainLedger (rectangleShearPotential h)).cost i j)
(fun i _ => Finset.sum_nonneg fun j _ =>
(coboundaryStrainLedger (rectangleShearPotential h)).nonneg i j)
(Finset.mem_univ 0)
exact lt_of_lt_of_le hinner houter
/-- **THEOREM.** The geometric side sees the same shear: the quadratic
hinge energy of the rectangle shear data is strictly positive for h ≠ 0. -/
theorem rectangleShear_quadraticEnergy_pos (h : ℝ) (hh : h ≠ 0) :
0 < quadraticCurvatureEnergy (strainHingeAreas (Fin 4))
(strainHingeDeficits (rectangleShearPotential h)) := by
refine quadraticCurvatureEnergy_pos
(fun p => by unfold strainHingeAreas; norm_num)
((0 : Fin 4), (1 : Fin 4))
(by unfold strainHingeAreas; norm_num) ?_
show rectangleShearPotential h 0 - rectangleShearPotential h 1 ≠ 0
rw [(rectangleShearPotential_strains h).1]
exact hh
What this page does not claim
The bridge does not prove a match against independently derived Regge geometry, only shape-compatibility of two functionals. The module does not derive the fine-structure constant or any other specific coupling constant. The bridge does not apply to general antisymmetric strains, only to coboundary strains.
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:
- What is the physical interpretation of the coboundary condition in terms of a continuous potential?
- Can the matching bound be extended from scalar potentials to tensor fields?
- How does the quadratic curvature energy relate to the Regge action in discrete gravity?
- What is the status of the Hessian-symbol comparison between the ledger and independent Regge geometry?
- Does the shear-visibility result generalize to higher-dimensional lattices?
MACHINE LAYER · GROUNDED CLAIM TABLE · CLICK TO EXPAND
THEOREM general_antisymmetric_strain_can_violate_rcl · IndisputableMonolith/Gravity/SevenGaps/LedgerEnergyBridge.lean
/-- **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) linarithThe module proves that the previously assumed bridge form, where a ledger deficit equals a raw signed geometric hinge deficit, is unsatisfiable on two-sided weak-field classes. general_antisymmetric_strain_can_violate_rcl · IndisputableMonolith/Gravity/SevenGaps/LedgerEnergyBridge.leanTHEOREM coboundary_totalCost_quadratic_matching · IndisputableMonolith/Gravity/SevenGaps/LedgerEnergyBridge.lean
/-- **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) linarithThe matching theorem proves that the ledger's total cost for a coboundary strain equals ε²/2 times a sum of squared potential differences, up to an error bounded by ε⁴/2 times a sum of fourth powers. coboundary_totalCost_quadratic_matching · IndisputableMonolith/Gravity/SevenGaps/LedgerEnergyBridge.leanTHEOREM general_antisymmetric_strain_can_violate_rcl · IndisputableMonolith/Gravity/SevenGaps/LedgerEnergyBridge.lean
/-- **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) linarithThe module exhibits an antisymmetric strain on three cells that violates the required gate condition, proving the construction is scoped to coboundary strains as a theorem-backed necessity. general_antisymmetric_strain_can_violate_rcl · IndisputableMonolith/Gravity/SevenGaps/LedgerEnergyBridge.leanTHEOREM rectangleShear_ledgerEnergy_pos · rectangleShear_quadraticEnergy_pos · IndisputableMonolith/Gravity/SevenGaps/LedgerEnergyBridge.lean
/-- **THEOREM (shear-visibility gate).** The pure-shear rectangle strain carries strictly positive ledger energy for every h ≠ 0. Shear is VISIBLE to the corrected J-ledger bridge: the cell cost on the horizontal edge is J(exp h) = cosh h − 1 > 0, and all cell costs are nonnegative. This is exactly the transverse-traceless sector on which the conformal-average ansatz was proved blind (`Gravity.conformal_ansatz_cannot_recover_gravitational_waves`). -/ theorem rectangleShear_ledgerEnergy_pos (h : ℝ) (hh : h ≠ 0) : 0 < RecognitionLedger.totalCost (coboundaryStrainLedger (rectangleShearPotential h)) := by classical unfold RecognitionLedger.totalCost have hval : rectangleShearPotential h 0 - rectangleShearPotential h 1 = h := (rectangleShearPotential_strains h).1 have hterm : 0 < (coboundaryStrainLedger (rectangleShearPotential h)).cost 0 1 := by show 0 < Cost.Jcost (Real.exp (rectangleShearPotential h 0 - rectangleShearPotential h 1)) rw [hval, Cost.Jcost_exp_cosh] have hcosh : 1 < Real.cosh h := Real.one_lt_cosh.mpr hh linarith have hinner : 0 < ∑ j, (coboundaryStrainLedger (rectangleShearPotential h)).cost 0 j := by have hle := Finset.single_le_sum (f := fun j => (coboundaryStrainLedger (rectangleShearPotential h)).cost 0 j) (fun j _ => (coboundaryStrainLedger (rectangleShearPotential h)).nonneg 0 j) (Finset.mem_univ 1) linarith have houter := Finset.single_le_sum (f := fun i => ∑ j, (coboundaryStrainLedger (rectangleShearPotential h)).cost i j) (fun i _ => Finset.sum_nonneg fun j _ => (coboundaryStrainLedger (rectangleShearPotential h)).nonneg i j) (Finset.mem_univ 0) exact lt_of_lt_of_le hinner houter/-- **THEOREM.** The geometric side sees the same shear: the quadratic hinge energy of the rectangle shear data is strictly positive for h ≠ 0. -/ theorem rectangleShear_quadraticEnergy_pos (h : ℝ) (hh : h ≠ 0) : 0 < quadraticCurvatureEnergy (strainHingeAreas (Fin 4)) (strainHingeDeficits (rectangleShearPotential h)) := by refine quadraticCurvatureEnergy_pos (fun p => by unfold strainHingeAreas; norm_num) ((0 : Fin 4), (1 : Fin 4)) (by unfold strainHingeAreas; norm_num) ?_ show rectangleShearPotential h 0 - rectangleShearPotential h 1 ≠ 0 rw [(rectangleShearPotential_strains h).1] exact hhThe pure-shear rectangle pattern carries strictly positive ledger energy for every nonzero h, as does its quadratic hinge energy. rectangleShear_ledgerEnergy_pos · rectangleShear_quadraticEnergy_pos · IndisputableMonolith/Gravity/SevenGaps/LedgerEnergyBridge.lean