Encyclopedia Gravity Gravity Seven Gaps Ledger Energy Bridge Rectangle Shear Ledger Energy Pos
ARTICLE 4 claims 4 theorems
Gravity Seven Gaps Ledger Energy Bridge Rectangle Shear Ledger Energy Pos
A rectangle that is stretched one way and squeezed the other still carries stored energy, and a machine-checked proof shows why.
Shear carries energy
A flat rectangle drawn on a sheet of rubber. Stretch it horizontally by a small amount h and squeeze it vertically by the same amount h. This deformation, called pure shear, changes the shape but not the area. A rubber sheet resists this change: it stores energy. The declaration rectangleShear_ledgerEnergy_pos proves that a discrete ledger of recognition events also assigns strictly positive energy to this same pure-shear pattern, for any nonzero h.
The proof lives in the framework's machine-checked library of formal theorems. The framework models a physical system as a ledger: a discrete record of events, here the differences of a potential between pairs of cells. The cost of each entry is forced by a proved theorem to be J(x) = (x + 1/x)/2 - 1. For a strain field that comes from a potential, the ledger's total cost is well defined. The theorem rectangleShear_ledgerEnergy_pos states that for the rectangle shear pattern, given by the potential (0, -h, 0, -h) on four cells, this total cost is strictly greater than zero whenever h is not zero.
The result is part of a larger correction. An earlier bridge assumed the ledger deficit equaled the raw signed geometric hinge deficit. That assumption failed: ledger deficits are nonnegative and even in the deformation, while signed hinge deficits are odd. The corrected bridge matches the ledger energy to a nonnegative curvature-quadratic geometric energy. The pure-shear theorem shows the corrected bridge sees exactly the sector on which the older, conformal-average ansatz was blind.
The theorem does not claim that shear energy matches any independently measured physical value. It does not claim the bridge to full Regge geometry is complete; the Hessian-symbol comparison and tensor multichannel escalation remain open. It proves a structural fact: in this discrete ledger model, pure shear carries positive energy.
THEOREM rectangleShear_ledgerEnergy_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 rectangleShearPotential_strains · IndisputableMonolith/Gravity/SevenGaps/LedgerEnergyBridge.lean
/-- **THEOREM.** The rectangle shear potential realizes the pure-shear
strain pattern: horizontal strains h, vertical strains −h.
(Uses `decide` only for `Fin 4` literal disequalities.) -/
theorem rectangleShearPotential_strains (h : ℝ) :
rectangleShearPotential h 0 - rectangleShearPotential h 1 = h ∧
rectangleShearPotential h 2 - rectangleShearPotential h 3 = h ∧
rectangleShearPotential h 1 - rectangleShearPotential h 2 = -h ∧
rectangleShearPotential h 3 - rectangleShearPotential h 0 = -h := by
have h01 : ¬((0 : Fin 4) = 1) := by decide
have h03 : ¬((0 : Fin 4) = 3) := by decide
have h21 : ¬((2 : Fin 4) = 1) := by decide
have h23 : ¬((2 : Fin 4) = 3) := by decide
have h13 : ¬((1 : Fin 4) = 3) := by decide
have h31 : ¬((3 : Fin 4) = 1) := by decide
unfold rectangleShearPotential
norm_num [h01, h03, h21, h23, h13, h31]
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
What this page does not claim
The theorem does not claim that the ledger shear energy matches any measured physical value. The theorem does not claim the bridge to independently derived Regge geometry is complete. The theorem does not claim that all shear deformations in general relativity carry positive energy.
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 physical system, if any, does the discrete ledger of recognition events model?
- How does the discrete quadratic curvature energy relate to the Regge calculus used in loop quantum gravity?
- What would it mean for the tensor multichannel escalation to close, and what new theorems would it require?
- Does the positive shear energy in this discrete model survive in a continuum limit?
MACHINE LAYER · GROUNDED CLAIM TABLE · CLICK TO EXPAND
THEOREM rectangleShear_ledgerEnergy_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 houterThe declaration rectangleShear_ledgerEnergy_pos proves that a discrete ledger of recognition events assigns strictly positive energy to a pure-shear rectangle pattern for any nonzero h. rectangleShear_ledgerEnergy_pos · IndisputableMonolith/Gravity/SevenGaps/LedgerEnergyBridge.leanTHEOREM rectangleShearPotential_strains · IndisputableMonolith/Gravity/SevenGaps/LedgerEnergyBridge.lean
/-- **THEOREM.** The rectangle shear potential realizes the pure-shear strain pattern: horizontal strains h, vertical strains −h. (Uses `decide` only for `Fin 4` literal disequalities.) -/ theorem rectangleShearPotential_strains (h : ℝ) : rectangleShearPotential h 0 - rectangleShearPotential h 1 = h ∧ rectangleShearPotential h 2 - rectangleShearPotential h 3 = h ∧ rectangleShearPotential h 1 - rectangleShearPotential h 2 = -h ∧ rectangleShearPotential h 3 - rectangleShearPotential h 0 = -h := by have h01 : ¬((0 : Fin 4) = 1) := by decide have h03 : ¬((0 : Fin 4) = 3) := by decide have h21 : ¬((2 : Fin 4) = 1) := by decide have h23 : ¬((2 : Fin 4) = 3) := by decide have h13 : ¬((1 : Fin 4) = 3) := by decide have h31 : ¬((3 : Fin 4) = 1) := by decide unfold rectangleShearPotential norm_num [h01, h03, h21, h23, h13, h31]The pure-shear pattern is realized as a coboundary strain by the potential (0, -h, 0, -h). rectangleShearPotential_strains · 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) linarithAn earlier bridge form assuming ledger deficit equals 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 corrected bridge matches the ledger energy to a nonnegative curvature-quadratic geometric energy. coboundary_totalCost_quadratic_matching · IndisputableMonolith/Gravity/SevenGaps/LedgerEnergyBridge.lean