IndisputableMonolith.Gravity.SevenGaps.LedgerEnergyBridge

   1import Mathlib
   2import IndisputableMonolith.Cost
   3import IndisputableMonolith.Gravity.RecognitionLedger
   4
   5/-!
   6# Seven Gaps, Lane 1b: the corrected ledger-to-geometry bridge
   7
   8## Status: THEOREM for every proved statement below (0 sorry, 0 RS-internal
   9axiom; `decide` is used ONLY for `Fin 3`/`Fin 4` literal disequalities in
  10the two witness-evaluation lemmas, no `native_decide` anywhere); MODEL and
  11OPEN items are listed in `LedgerEnergyBridgeStatus` at the end.
  12
  13`SevenGaps.LedgerBridgeNoGo` proves that the previously assumed bridge form
  14(ledger deficit = raw SIGNED geometric hinge deficit) is unsatisfiable on
  15two-sided weak-field classes: ledger deficits are nonnegative and even in
  16the deformation parameter, while the signed Regge deficit response is odd.
  17This module builds the corrected bridge to the honest target: the
  18nonnegative curvature-QUADRATIC geometric energy, discrete Isaacson-type
  19form Σ_h A_h · δ_h².
  20
  21**Definitional separation of the two sides (with an honest limit).**
  22* The geometric side `quadraticCurvatureEnergy` is defined purely from
  23  hinge data (areas and deficits); no ledger object appears in its
  24  definition.
  25* The ledger side `coboundaryStrainLedger` and its `totalCost` are defined
  26  purely from the substrate potential and the J-cost; no hinge or geometric
  27  object appears in theirs.
  28The matching theorem `coboundary_totalCost_quadratic_matching` links the two
  29definitionally separate sides. HONEST LIMIT: in the canonical bridge
  30INSTANCE (`canonicalQuadraticEnergyBridge`) the hinge data is instantiated
  31FROM the ledger's own potential (deficits = potential differences, areas =
  321/2 on ordered pairs), so the instance certifies shape-compatibility of the
  33two functionals, not yet a match against independently derived Regge
  34geometry; that comparison is the OPEN Hessian-symbol flag below.
  35
  36**Scoped class (honest scoping).** The J-ratio cost of a strain field
  37`s : Λ → Λ → ℝ` forms a `RecognitionLedger` when `s` is a COBOUNDARY
  38(`s i j = f i - f j` for a cell potential `f`). For coboundary strains the
  39ratios satisfy the cocycle property exp(s i j)·exp(s j k) = exp(s i k), and
  40RCL subadditivity follows from the d'Alembert identity
  41J(xy) + J(x/y) = R(J(x), J(y)) with J(x/y) ≥ 0
  42(`rclGate_Jcost_eq`, `Cost.dalembert_identity`). For GENERAL antisymmetric
  43strains the RCL gate can FAIL: `general_antisymmetric_strain_can_violate_rcl`
  44exhibits an antisymmetric strain on three cells violating the gate. The
  45construction is therefore scoped to coboundary strains, and this scoping is
  46itself a theorem-backed necessity, not a convenience.
  47
  48**Explicit constants.** The per-strain expansion is
  49t²/2 ≤ J(exp t) = cosh t − 1 ≤ (t²/2)·cosh t (all t), whence for |t| ≤ 1:
  50|J(exp t) − t²/2| ≤ (t⁴/4)·cosh 1 ≤ t⁴/2 (using cosh 1 < 2). The summed
  51matching bound is |totalCost − (ε²/2)·S₂| ≤ (ε⁴/2)·S₄ with
  52S₂ = Σ_{i,j} (f₀ i − f₀ j)², S₄ = Σ_{i,j} (f₀ i − f₀ j)⁴, under the explicit
  53hypothesis |ε·(f₀ i − f₀ j)| ≤ 1 for all i, j. Note S₂, S₄ run over ORDERED
  54pairs, so each unordered pair is counted twice.
  55
  56**Shear-visibility gate.** The pure-shear rectangle pattern (horizontal
  57strain h, vertical strain −h: the traceless two-sided class of the no-go)
  58is realized as a coboundary strain by the potential (0, −h, 0, −h), and its
  59ledger energy is strictly positive for every h ≠ 0
  60(`rectangleShear_ledgerEnergy_pos`), as is its quadratic hinge energy
  61(`rectangleShear_quadraticEnergy_pos`). Pure shear carries nonzero ledger
  62energy: the corrected bridge sees exactly the sector on which the
  63conformal-average ansatz was blind.
  64-/
  65
  66namespace IndisputableMonolith
  67namespace Gravity
  68namespace SevenGaps
  69
  70/-! ## §1. The geometric side: discrete quadratic curvature energy
  71
  72Defined purely from hinge data. No ledger objects appear. -/
  73
  74/-- **Discrete quadratic (Isaacson-type) curvature energy.** For hinge data
  75consisting of areas `A : H → ℝ` and deficit angles `δ : H → ℝ`, the energy
  76is Σ_h A_h · δ_h². This is the discrete form of the nonnegative
  77curvature-quadratic energy density; it is EVEN in δ, matching the parity
  78and sign of the ledger side. Purely geometric: no ledger objects. -/
  79noncomputable def quadraticCurvatureEnergy {H : Type*} [Fintype H]
  80    (A δ : H → ℝ) : ℝ :=
  81  ∑ h, A h * δ h ^ 2
  82
  83/-- **THEOREM.** The quadratic curvature energy is nonnegative for
  84nonnegative areas (any deficit signs). -/
  85theorem quadraticCurvatureEnergy_nonneg {H : Type*} [Fintype H]
  86    {A : H → ℝ} (hA : ∀ h, 0 ≤ A h) (δ : H → ℝ) :
  87    0 ≤ quadraticCurvatureEnergy A δ := by
  88  unfold quadraticCurvatureEnergy
  89  exact Finset.sum_nonneg fun h _ => mul_nonneg (hA h) (sq_nonneg _)
  90
  91/-- **THEOREM.** The quadratic curvature energy is strictly positive as
  92soon as one hinge has positive area and nonzero deficit. -/
  93theorem quadraticCurvatureEnergy_pos {H : Type*} [Fintype H]
  94    {A δ : H → ℝ} (hA : ∀ h, 0 ≤ A h) (h₀ : H)
  95    (hA₀ : 0 < A h₀) (hδ₀ : δ h₀ ≠ 0) :
  96    0 < quadraticCurvatureEnergy A δ := by
  97  have hsq : 0 < δ h₀ ^ 2 :=
  98    (sq_nonneg (δ h₀)).lt_of_ne (Ne.symm (pow_ne_zero 2 hδ₀))
  99  have hterm : 0 < A h₀ * δ h₀ ^ 2 := mul_pos hA₀ hsq
 100  have hle : A h₀ * δ h₀ ^ 2 ≤ quadraticCurvatureEnergy A δ :=
 101    Finset.single_le_sum (fun h _ => mul_nonneg (hA h) (sq_nonneg _))
 102      (Finset.mem_univ h₀)
 103  linarith
 104
 105/-! ## §2. Per-strain expansion lemmas (THEOREM tier)
 106
 107J(exp t) = cosh t − 1. The two-sided quadratic bounds and the quartic
 108remainder bound, with explicit constants. -/
 109
 110/-- **THEOREM.** sinh t ≤ t·cosh t for t ≥ 0, by termwise comparison of the
 111power series: t^(2n+1)/(2n+1)! ≤ t^(2n+1)/(2n)!. -/
 112theorem sinh_le_self_mul_cosh {t : ℝ} (ht : 0 ≤ t) :
 113    Real.sinh t ≤ t * Real.cosh t := by
 114  refine hasSum_le (fun n => ?_) (Real.hasSum_sinh t)
 115    ((Real.hasSum_cosh t).mul_left t)
 116  have hfact_le : ((2 * n).factorial : ℝ) ≤ ((2 * n + 1).factorial : ℝ) := by
 117    exact_mod_cast Nat.factorial_le (by omega : 2 * n ≤ 2 * n + 1)
 118  have hfact_pos : (0 : ℝ) < ((2 * n).factorial : ℝ) := by
 119    exact_mod_cast Nat.factorial_pos (2 * n)
 120  have hpow : (0 : ℝ) ≤ t ^ (2 * n + 1) := pow_nonneg ht _
 121  calc t ^ (2 * n + 1) / ((2 * n + 1).factorial : ℝ)
 122      ≤ t ^ (2 * n + 1) / ((2 * n).factorial : ℝ) :=
 123        div_le_div_of_nonneg_left hpow hfact_pos hfact_le
 124    _ = t * (t ^ (2 * n) / ((2 * n).factorial : ℝ)) := by
 125        rw [pow_succ]; ring
 126
 127/-- **THEOREM.** |sinh t| ≤ |t|·cosh t for all t. -/
 128theorem abs_sinh_le_abs_mul_cosh (t : ℝ) :
 129    |Real.sinh t| ≤ |t| * Real.cosh t := by
 130  rw [Real.abs_sinh, ← Real.cosh_abs]
 131  exact sinh_le_self_mul_cosh (abs_nonneg t)
 132
 133/-- **THEOREM (two-sided quadratic upper bound).**
 134cosh t − 1 ≤ (t²/2)·cosh t for ALL t. Combined with
 135`Cost.cosh_quadratic_lower_bound` (t²/2 ≤ cosh t − 1) this brackets the
 136ledger cell cost between two quadratic forms. -/
 137theorem cosh_sub_one_le_half_sq_mul_cosh (t : ℝ) :
 138    Real.cosh t - 1 ≤ t ^ 2 / 2 * Real.cosh t := by
 139  have hkey := Cost.cosh_minus_one_eq t
 140  have hs := abs_sinh_le_abs_mul_cosh (t / 2)
 141  have h1 : |Real.sinh (t / 2)| ^ 2 ≤ (|t / 2| * Real.cosh (t / 2)) ^ 2 := by
 142    have := mul_self_le_mul_self (abs_nonneg _) hs
 143    simpa [pow_two] using this
 144  have h2 : Real.sinh (t / 2) ^ 2 ≤ (t / 2) ^ 2 * Real.cosh (t / 2) ^ 2 := by
 145    rw [sq_abs] at h1
 146    rw [mul_pow, sq_abs] at h1
 147    exact h1
 148  have hC : Real.cosh (t / 2) ^ 2 ≤ Real.cosh t := by
 149    have h2m := Real.cosh_two_mul (t / 2)
 150    have harg : (2 : ℝ) * (t / 2) = t := by ring
 151    rw [harg] at h2m
 152    have hpyth := Real.cosh_sq_sub_sinh_sq (t / 2)
 153    nlinarith [sq_nonneg (Real.cosh (t / 2) - 1), Real.one_le_cosh (t / 2)]
 154  have hS_le : Real.sinh (t / 2) ^ 2 ≤ (t / 2) ^ 2 * Real.cosh t :=
 155    le_trans h2 (mul_le_mul_of_nonneg_left hC (sq_nonneg _))
 156  nlinarith [hkey, hS_le]
 157
 158/-- **THEOREM.** The quadratic remainder of the ledger cell cost is
 159nonnegative: 0 ≤ cosh t − 1 − t²/2. -/
 160theorem cosh_remainder_nonneg (t : ℝ) : 0 ≤ Real.cosh t - 1 - t ^ 2 / 2 := by
 161  have h := Cost.cosh_quadratic_lower_bound t
 162  linarith
 163
 164/-- **THEOREM (explicit quartic remainder).**
 165cosh t − 1 − t²/2 ≤ (t⁴/4)·cosh t for ALL t, by iterating the quadratic
 166upper bound: cosh t − 1 − t²/2 ≤ (t²/2)(cosh t − 1) ≤ (t⁴/4)·cosh t. -/
 167theorem cosh_remainder_le (t : ℝ) :
 168    Real.cosh t - 1 - t ^ 2 / 2 ≤ t ^ 4 / 4 * Real.cosh t := by
 169  have h1 := cosh_sub_one_le_half_sq_mul_cosh t
 170  have h3 : t ^ 2 / 2 * (Real.cosh t - 1)
 171      ≤ t ^ 2 / 2 * (t ^ 2 / 2 * Real.cosh t) :=
 172    mul_le_mul_of_nonneg_left h1 (by positivity)
 173  nlinarith [h1, h3]
 174
 175/-- **THEOREM.** cosh 1 < 2 (explicit numeric bound for the remainder
 176constant), from exp 1 < 2.7182818286 and exp(−1)·exp(1) = 1. -/
 177theorem cosh_one_lt_two : Real.cosh 1 < 2 := by
 178  have he : (2 : ℝ) < Real.exp 1 :=
 179    lt_trans (by norm_num) Real.exp_one_gt_d9
 180  have hlt : Real.exp 1 < 2.7182818286 := Real.exp_one_lt_d9
 181  have hprod : Real.exp (-1) * Real.exp 1 = 1 := by
 182    rw [← Real.exp_add]
 183    norm_num [Real.exp_zero]
 184  have hpos : 0 < Real.exp (-1 : ℝ) := Real.exp_pos _
 185  rw [Real.cosh_eq]
 186  nlinarith [hprod, he, hpos, hlt]
 187
 188/-- **THEOREM (per-strain quadratic expansion, explicit constant 1/2).**
 189For |t| ≤ 1: |J(exp t) − t²/2| ≤ t⁴/2. The constant comes from
 190(1/4)·cosh 1 ≤ 1/2 via `cosh_one_lt_two`. -/
 191theorem Jcost_exp_sub_half_sq_abs_le (t : ℝ) (ht : |t| ≤ 1) :
 192    |Cost.Jcost (Real.exp t) - t ^ 2 / 2| ≤ t ^ 4 / 2 := by
 193  rw [Cost.Jcost_exp_cosh]
 194  have h0 := cosh_remainder_nonneg t
 195  have h1 := cosh_remainder_le t
 196  have hcosh : Real.cosh t ≤ 2 := by
 197    have hmono : Real.cosh t ≤ Real.cosh 1 := by
 198      rw [Real.cosh_le_cosh]
 199      simpa using ht
 200    linarith [cosh_one_lt_two]
 201  rw [abs_of_nonneg h0]
 202  have h2 : t ^ 4 / 4 * Real.cosh t ≤ t ^ 4 / 4 * 2 :=
 203    mul_le_mul_of_nonneg_left hcosh (by positivity)
 204  linarith
 205
 206/-! ## §3. The ledger side: the coboundary-strain J-ledger
 207
 208Defined purely from the substrate potential and the J-cost. No hinge or
 209geometric object appears. -/
 210
 211/-- A strain field is a coboundary if it is the difference field of a cell
 212potential: s i j = f i − f j. Coboundary strains are automatically
 213antisymmetric and satisfy the ratio cocycle property. -/
 214def IsCoboundary {Λ : Type*} (s : Λ → Λ → ℝ) : Prop :=
 215  ∃ f : Λ → ℝ, ∀ i j, s i j = f i - f j
 216
 217/-- Coboundary strains are antisymmetric. -/
 218theorem IsCoboundary.antisymm {Λ : Type*} {s : Λ → Λ → ℝ}
 219    (hs : IsCoboundary s) : ∀ i j, s i j = - s j i := by
 220  obtain ⟨f, hf⟩ := hs
 221  intro i j
 222  rw [hf i j, hf j i]
 223  ring
 224
 225/-- **THEOREM (the panel's key identity).** The RCL gate evaluated on two
 226J-costs is EXACTLY the J-cost of the product ratio plus the J-cost of the
 227quotient ratio: R(J(x), J(y)) = J(xy) + J(x/y) for x, y > 0. Since
 228J(x/y) ≥ 0, the gate inequality J(xy) ≤ R(J(x), J(y)) follows with
 229identified slack J(x/y). Pure algebra from `Cost.dalembert_identity`. -/
 230theorem rclGate_Jcost_eq {x y : ℝ} (hx : 0 < x) (hy : 0 < y) :
 231    RecognitionLedger.rclGate (Cost.Jcost x) (Cost.Jcost y)
 232      = Cost.Jcost (x * y) + Cost.Jcost (x / y) := by
 233  have h := Cost.dalembert_identity hx hy
 234  unfold RecognitionLedger.rclGate
 235  linarith
 236
 237/-- **THEOREM (the corrected ledger construction, coboundary scope).**
 238The J-ratio costs of a coboundary strain field form a genuine
 239`RecognitionLedger`: cost i j = J(exp(f i − f j)).
 240* symmetry from J(x) = J(1/x) (`Cost.Jcost_symm`),
 241* diagonal zero from J(1) = 0,
 242* nonnegativity from J ≥ 0 on positives,
 243* RCL subadditivity from the cocycle property
 244  exp(f i − f j)·exp(f j − f k) = exp(f i − f k) plus J-submultiplicativity
 245  (`Cost.Jcost_submult` in the proof; equivalently the d'Alembert identity
 246  `rclGate_Jcost_eq` with J(x/y) ≥ 0).
 247Scoped to coboundary strains: for general antisymmetric strains the gate
 248can fail (`general_antisymmetric_strain_can_violate_rcl`). -/
 249noncomputable def coboundaryStrainLedger {Λ : Type*} [Fintype Λ]
 250    [DecidableEq Λ] (f : Λ → ℝ) :
 251    RecognitionLedger.RecognitionLedger Λ where
 252  cost i j := Cost.Jcost (Real.exp (f i - f j))
 253  symmetric := by
 254    intro i j
 255    show Cost.Jcost (Real.exp (f i - f j)) = Cost.Jcost (Real.exp (f j - f i))
 256    have h : Real.exp (f j - f i) = (Real.exp (f i - f j))⁻¹ := by
 257      rw [← Real.exp_neg]
 258      congr 1
 259      ring
 260    rw [h]
 261    exact Cost.Jcost_symm (Real.exp_pos _)
 262  diagonal_zero := by
 263    intro i
 264    show Cost.Jcost (Real.exp (f i - f i)) = 0
 265    rw [sub_self, Real.exp_zero, Cost.Jcost_unit0]
 266  nonneg := fun i j => Cost.Jcost_nonneg (Real.exp_pos _)
 267  rcl_subadditive := by
 268    intro i j k
 269    show Cost.Jcost (Real.exp (f i - f k))
 270      ≤ RecognitionLedger.rclGate (Cost.Jcost (Real.exp (f i - f j)))
 271          (Cost.Jcost (Real.exp (f j - f k)))
 272    have hcomp : Real.exp (f i - f k)
 273        = Real.exp (f i - f j) * Real.exp (f j - f k) := by
 274      rw [← Real.exp_add]
 275      congr 1
 276      ring
 277    have hsub := Cost.Jcost_submult (Real.exp_pos (f i - f j))
 278      (Real.exp_pos (f j - f k))
 279    rw [hcomp]
 280    unfold RecognitionLedger.rclGate
 281    linarith
 282
 283/-- The gate-violating antisymmetric strain on three cells: strain 1 from
 284cell 0 to cell 2 but zero strain on both legs through cell 1. Antisymmetric
 285by construction; NOT a coboundary (a coboundary would force
 286s 0 2 = s 0 1 + s 1 2 = 0). -/
 287noncomputable def gateViolatingStrain : Fin 3 → Fin 3 → ℝ := fun i j =>
 288  (if i = 0 ∧ j = 2 then (1 : ℝ) else 0)
 289    - (if j = 0 ∧ i = 2 then (1 : ℝ) else 0)
 290
 291/-- **THEOREM.** The gate-violating strain is antisymmetric. -/
 292theorem gateViolatingStrain_antisymm :
 293    ∀ i j, gateViolatingStrain i j = - gateViolatingStrain j i := by
 294  intro i j
 295  unfold gateViolatingStrain
 296  ring
 297
 298/-- **THEOREM.** Values of the gate-violating strain on the relevant pairs.
 299(Uses `decide` only for `Fin 3` literal disequalities.) -/
 300theorem gateViolatingStrain_vals :
 301    gateViolatingStrain 0 2 = 1 ∧ gateViolatingStrain 0 1 = 0 ∧
 302      gateViolatingStrain 1 2 = 0 := by
 303  have h20 : ¬((2 : Fin 3) = 0) := by decide
 304  have h02 : ¬((0 : Fin 3) = 2) := by decide
 305  have h12 : ¬((1 : Fin 3) = 2) := by decide
 306  have h10 : ¬((1 : Fin 3) = 0) := by decide
 307  refine ⟨?_, ?_, ?_⟩ <;>
 308    · unfold gateViolatingStrain
 309      norm_num [h20, h02, h12, h10]
 310
 311/-- **THEOREM (honest scoping witness).** A general ANTISYMMETRIC strain
 312field need not yield an RCL-subadditive cost: on three cells, the
 313antisymmetric strain with s 0 2 = 1 but s 0 1 = s 1 2 = 0 gives
 314J(exp(s 0 2)) > 0 = R(J(exp(s 0 1)), J(exp(s 1 2))). This is why
 315`coboundaryStrainLedger` is scoped to coboundary strains: the scoping is
 316forced, not chosen. -/
 317theorem general_antisymmetric_strain_can_violate_rcl :
 318    ∃ s : Fin 3 → Fin 3 → ℝ, (∀ i j, s i j = - s j i) ∧
 319      ¬ (Cost.Jcost (Real.exp (s 0 2)) ≤
 320          RecognitionLedger.rclGate (Cost.Jcost (Real.exp (s 0 1)))
 321            (Cost.Jcost (Real.exp (s 1 2)))) := by
 322  refine ⟨gateViolatingStrain, gateViolatingStrain_antisymm, ?_⟩
 323  obtain ⟨h02, h01, h12⟩ := gateViolatingStrain_vals
 324  rw [h02, h01, h12, Real.exp_zero, Cost.Jcost_unit0]
 325  have hgate : RecognitionLedger.rclGate 0 0 = 0 := by
 326    unfold RecognitionLedger.rclGate
 327    ring
 328  rw [hgate]
 329  have hone : (1 : ℝ) < Real.exp 1 :=
 330    lt_trans (by norm_num) Real.exp_one_gt_d9
 331  have hpos : 0 < Cost.Jcost (Real.exp 1) :=
 332    Cost.Jcost_pos_of_ne_one _ (Real.exp_pos 1) (ne_of_gt hone)
 333  linarith
 334
 335/-! ## §4. The matching theorem (the corrected bridge) -/
 336
 337/-- **THEOREM (quadratic matching, explicit constants).** For the
 338one-parameter coboundary strain family ε·f₀ with all scaled strains in
 339[−1, 1], the total ledger cost matches the quadratic strain energy
 340(ε²/2)·S₂ to fourth order with explicit remainder constant 1/2:
 341
 342  |totalCost(ε·f₀) − (ε²/2)·Σ_{i,j}(f₀ i − f₀ j)²|
 343      ≤ (ε⁴/2)·Σ_{i,j}(f₀ i − f₀ j)⁴.
 344
 345Sums run over ORDERED pairs (each unordered pair counted twice). The
 346hypothesis |ε·(f₀ i − f₀ j)| ≤ 1 is the explicit small-strain premise; no
 347hidden assumptions. -/
 348theorem coboundary_totalCost_quadratic_matching {Λ : Type*} [Fintype Λ]
 349    [DecidableEq Λ] (f₀ : Λ → ℝ) (ε : ℝ)
 350    (hsmall : ∀ i j, |ε * (f₀ i - f₀ j)| ≤ 1) :
 351    |RecognitionLedger.totalCost
 352        (coboundaryStrainLedger (fun i => ε * f₀ i))
 353      - ε ^ 2 / 2 * ∑ i, ∑ j, (f₀ i - f₀ j) ^ 2|
 354      ≤ ε ^ 4 / 2 * ∑ i, ∑ j, (f₀ i - f₀ j) ^ 4 := by
 355  classical
 356  have hcost : ∀ i j : Λ,
 357      (coboundaryStrainLedger (fun i => ε * f₀ i)).cost i j
 358        = Cost.Jcost (Real.exp (ε * (f₀ i - f₀ j))) := by
 359    intro i j
 360    show Cost.Jcost (Real.exp (ε * f₀ i - ε * f₀ j)) = _
 361    have harg : ε * f₀ i - ε * f₀ j = ε * (f₀ i - f₀ j) := by ring
 362    rw [harg]
 363  have hexpand : RecognitionLedger.totalCost
 364      (coboundaryStrainLedger (fun i => ε * f₀ i))
 365      = ∑ i, ∑ j, Cost.Jcost (Real.exp (ε * (f₀ i - f₀ j))) := by
 366    unfold RecognitionLedger.totalCost
 367    exact Finset.sum_congr rfl fun i _ =>
 368      Finset.sum_congr rfl fun j _ => hcost i j
 369  have hquad : ε ^ 2 / 2 * ∑ i, ∑ j, (f₀ i - f₀ j) ^ 2
 370      = ∑ i, ∑ j, (ε * (f₀ i - f₀ j)) ^ 2 / 2 := by
 371    rw [Finset.mul_sum]
 372    refine Finset.sum_congr rfl fun i _ => ?_
 373    rw [Finset.mul_sum]
 374    exact Finset.sum_congr rfl fun j _ => by ring
 375  have hquart : ε ^ 4 / 2 * ∑ i, ∑ j, (f₀ i - f₀ j) ^ 4
 376      = ∑ i, ∑ j, (ε * (f₀ i - f₀ j)) ^ 4 / 2 := by
 377    rw [Finset.mul_sum]
 378    refine Finset.sum_congr rfl fun i _ => ?_
 379    rw [Finset.mul_sum]
 380    exact Finset.sum_congr rfl fun j _ => by ring
 381  rw [hexpand, hquad, hquart]
 382  have hcombine : ∑ i, ∑ j, Cost.Jcost (Real.exp (ε * (f₀ i - f₀ j)))
 383      - ∑ i, ∑ j, (ε * (f₀ i - f₀ j)) ^ 2 / 2
 384      = ∑ i, ∑ j, (Cost.Jcost (Real.exp (ε * (f₀ i - f₀ j)))
 385          - (ε * (f₀ i - f₀ j)) ^ 2 / 2) := by
 386    rw [← Finset.sum_sub_distrib]
 387    exact Finset.sum_congr rfl fun i _ => (Finset.sum_sub_distrib _ _).symm
 388  rw [hcombine]
 389  calc |∑ i, ∑ j, (Cost.Jcost (Real.exp (ε * (f₀ i - f₀ j)))
 390          - (ε * (f₀ i - f₀ j)) ^ 2 / 2)|
 391      ≤ ∑ i, |∑ j, (Cost.Jcost (Real.exp (ε * (f₀ i - f₀ j)))
 392          - (ε * (f₀ i - f₀ j)) ^ 2 / 2)| :=
 393        Finset.abs_sum_le_sum_abs _ _
 394    _ ≤ ∑ i, ∑ j, |Cost.Jcost (Real.exp (ε * (f₀ i - f₀ j)))
 395          - (ε * (f₀ i - f₀ j)) ^ 2 / 2| :=
 396        Finset.sum_le_sum fun i _ => Finset.abs_sum_le_sum_abs _ _
 397    _ ≤ ∑ i, ∑ j, (ε * (f₀ i - f₀ j)) ^ 4 / 2 :=
 398        Finset.sum_le_sum fun i _ => Finset.sum_le_sum fun j _ => by
 399          have h := Jcost_exp_sub_half_sq_abs_le (ε * (f₀ i - f₀ j))
 400            (hsmall i j)
 401          linarith
 402
 403/-! ## §5. The corrected bridge structure and its canonical instance -/
 404
 405/-- Uniform hinge areas for the ordered-pair hinge set Λ × Λ: each ordered
 406pair carries area 1/2, so that summing over ordered pairs matches the
 407per-unordered-pair weight 1. Purely geometric bookkeeping. -/
 408noncomputable def strainHingeAreas (Λ : Type*) : Λ × Λ → ℝ := fun _ => 1 / 2
 409
 410/-- Hinge deficits induced by a cell potential: the hinge (i, j) carries
 411deficit f i − f j. This is hinge DATA (a signed deficit assignment); it is
 412consumed quadratically by `quadraticCurvatureEnergy`, so its sign is
 413invisible to the energy, exactly as the parity no-go requires. -/
 414noncomputable def strainHingeDeficits {Λ : Type*} (f : Λ → ℝ) :
 415    Λ × Λ → ℝ := fun p => f p.1 - f p.2
 416
 417/-- **THEOREM.** The quadratic curvature energy of the strain hinge data is
 418half the ordered-pair sum of squared potential differences. -/
 419theorem quadraticCurvatureEnergy_strainHinges {Λ : Type*} [Fintype Λ]
 420    (f₀ : Λ → ℝ) :
 421    quadraticCurvatureEnergy (strainHingeAreas Λ) (strainHingeDeficits f₀)
 422      = (∑ i, ∑ j, (f₀ i - f₀ j) ^ 2) / 2 := by
 423  unfold quadraticCurvatureEnergy strainHingeAreas strainHingeDeficits
 424  rw [Fintype.sum_prod_type]
 425  rw [Finset.sum_div]
 426  refine Finset.sum_congr rfl fun i _ => ?_
 427  rw [Finset.sum_div]
 428  refine Finset.sum_congr rfl fun j _ => ?_
 429  show (1 : ℝ) / 2 * (f₀ i - f₀ j) ^ 2 = (f₀ i - f₀ j) ^ 2 / 2
 430  ring
 431
 432/-- **The corrected bridge (deliverable B).** From a coboundary strain
 433configuration (base potential f₀, deformation parameter ε, explicit
 434small-strain hypothesis) to quadratic hinge energy data (areas, deficits),
 435with the PROVED two-sided matching bound as a field: the total ledger cost
 436of the scaled strain equals ε² times the quadratic hinge energy up to the
 437explicit quartic remainder (ε⁴/2)·S₄. There are NO assumed fields: every
 438Prop field of the canonical instance `canonicalQuadraticEnergyBridge` is
 439discharged by a kernel-checked proof. Contrast with the refuted
 440`LedgerToHingeBridge.bridge_assumed`. -/
 441structure LedgerToQuadraticEnergyBridge
 442    (Λ : Type*) [Fintype Λ] [DecidableEq Λ] where
 443  /-- The base cell potential f₀ (strain generator). -/
 444  basePotential : Λ → ℝ
 445  /-- The deformation parameter ε. -/
 446  eps : ℝ
 447  /-- Explicit small-strain premise: every scaled strain lies in [−1, 1]. -/
 448  small_strain : ∀ i j, |eps * (basePotential i - basePotential j)| ≤ 1
 449  /-- Hinge areas (geometric side). -/
 450  hingeArea : Λ × Λ → ℝ
 451  /-- Areas are nonnegative. -/
 452  hingeArea_nonneg : ∀ p, 0 ≤ hingeArea p
 453  /-- Hinge deficits (geometric side). -/
 454  hingeDeficit : Λ × Λ → ℝ
 455  /-- PROVED two-sided matching (both bounds, via absolute value): ledger
 456  energy = ε²·(quadratic hinge energy) + O(ε⁴) with explicit constant. -/
 457  matching : |RecognitionLedger.totalCost
 458      (coboundaryStrainLedger (fun i => eps * basePotential i))
 459    - eps ^ 2 * quadraticCurvatureEnergy hingeArea hingeDeficit|
 460    ≤ eps ^ 4 / 2 *
 461        ∑ i, ∑ j, (basePotential i - basePotential j) ^ 4
 462
 463/-- **THEOREM (canonical instance).** Every coboundary strain configuration
 464with small scaled strains yields a `LedgerToQuadraticEnergyBridge`: hinge
 465areas 1/2 on ordered pairs, hinge deficits f₀ i − f₀ j, matching proved by
 466`coboundary_totalCost_quadratic_matching`. No assumed fields. -/
 467noncomputable def canonicalQuadraticEnergyBridge {Λ : Type*} [Fintype Λ]
 468    [DecidableEq Λ] (f₀ : Λ → ℝ) (ε : ℝ)
 469    (hsmall : ∀ i j, |ε * (f₀ i - f₀ j)| ≤ 1) :
 470    LedgerToQuadraticEnergyBridge Λ where
 471  basePotential := f₀
 472  eps := ε
 473  small_strain := hsmall
 474  hingeArea := strainHingeAreas Λ
 475  hingeArea_nonneg := fun _ => by
 476    unfold strainHingeAreas
 477    norm_num
 478  hingeDeficit := strainHingeDeficits f₀
 479  matching := by
 480    rw [quadraticCurvatureEnergy_strainHinges f₀]
 481    have harg : ε ^ 2 * ((∑ i, ∑ j, (f₀ i - f₀ j) ^ 2) / 2)
 482        = ε ^ 2 / 2 * ∑ i, ∑ j, (f₀ i - f₀ j) ^ 2 := by ring
 483    rw [harg]
 484    exact coboundary_totalCost_quadratic_matching f₀ ε hsmall
 485
 486/-! ## §6. The shear-visibility gate (nonflat witness) -/
 487
 488/-- The rectangle pure-shear potential: cells 0 and 2 at potential 0, cells
 4891 and 3 at potential −h. The induced coboundary strains carry strain h on
 490the two horizontal edges (0→1, 2→3) and −h on the two vertical edges
 491(1→2, 3→0): the traceless rectangle shear pattern (horizontal strain h,
 492vertical strain v = −h, h ≠ v for h ≠ 0). This is the rectangle shear mode
 493of `TensorShearSector` re-expressed as antisymmetric pair strains; as an
 494edge pattern with h ≠ v it has NO vertex-conformal (averaging) realization,
 495but as a difference field it IS a coboundary, so the corrected ledger
 496bridge applies to it. -/
 497noncomputable def rectangleShearPotential (h : ℝ) : Fin 4 → ℝ :=
 498  fun i => if i = 1 ∨ i = 3 then -h else 0
 499
 500/-- **THEOREM.** The rectangle shear potential realizes the pure-shear
 501strain pattern: horizontal strains h, vertical strains −h.
 502(Uses `decide` only for `Fin 4` literal disequalities.) -/
 503theorem rectangleShearPotential_strains (h : ℝ) :
 504    rectangleShearPotential h 0 - rectangleShearPotential h 1 = h ∧
 505    rectangleShearPotential h 2 - rectangleShearPotential h 3 = h ∧
 506    rectangleShearPotential h 1 - rectangleShearPotential h 2 = -h ∧
 507    rectangleShearPotential h 3 - rectangleShearPotential h 0 = -h := by
 508  have h01 : ¬((0 : Fin 4) = 1) := by decide
 509  have h03 : ¬((0 : Fin 4) = 3) := by decide
 510  have h21 : ¬((2 : Fin 4) = 1) := by decide
 511  have h23 : ¬((2 : Fin 4) = 3) := by decide
 512  have h13 : ¬((1 : Fin 4) = 3) := by decide
 513  have h31 : ¬((3 : Fin 4) = 1) := by decide
 514  unfold rectangleShearPotential
 515  norm_num [h01, h03, h21, h23, h13, h31]
 516
 517/-- **THEOREM (shear-visibility gate).** The pure-shear rectangle strain
 518carries strictly positive ledger energy for every h ≠ 0. Shear is VISIBLE
 519to the corrected J-ledger bridge: the cell cost on the horizontal edge is
 520J(exp h) = cosh h − 1 > 0, and all cell costs are nonnegative. This is
 521exactly the transverse-traceless sector on which the conformal-average
 522ansatz was proved blind
 523(`Gravity.conformal_ansatz_cannot_recover_gravitational_waves`). -/
 524theorem rectangleShear_ledgerEnergy_pos (h : ℝ) (hh : h ≠ 0) :
 525    0 < RecognitionLedger.totalCost
 526      (coboundaryStrainLedger (rectangleShearPotential h)) := by
 527  classical
 528  unfold RecognitionLedger.totalCost
 529  have hval : rectangleShearPotential h 0 - rectangleShearPotential h 1
 530      = h := (rectangleShearPotential_strains h).1
 531  have hterm :
 532      0 < (coboundaryStrainLedger (rectangleShearPotential h)).cost 0 1 := by
 533    show 0 < Cost.Jcost (Real.exp
 534      (rectangleShearPotential h 0 - rectangleShearPotential h 1))
 535    rw [hval, Cost.Jcost_exp_cosh]
 536    have hcosh : 1 < Real.cosh h := Real.one_lt_cosh.mpr hh
 537    linarith
 538  have hinner :
 539      0 < ∑ j, (coboundaryStrainLedger (rectangleShearPotential h)).cost 0 j := by
 540    have hle := Finset.single_le_sum
 541      (f := fun j => (coboundaryStrainLedger (rectangleShearPotential h)).cost 0 j)
 542      (fun j _ => (coboundaryStrainLedger (rectangleShearPotential h)).nonneg 0 j)
 543      (Finset.mem_univ 1)
 544    linarith
 545  have houter := Finset.single_le_sum
 546    (f := fun i => ∑ j, (coboundaryStrainLedger (rectangleShearPotential h)).cost i j)
 547    (fun i _ => Finset.sum_nonneg fun j _ =>
 548      (coboundaryStrainLedger (rectangleShearPotential h)).nonneg i j)
 549    (Finset.mem_univ 0)
 550  exact lt_of_lt_of_le hinner houter
 551
 552/-- **THEOREM.** The geometric side sees the same shear: the quadratic
 553hinge energy of the rectangle shear data is strictly positive for h ≠ 0. -/
 554theorem rectangleShear_quadraticEnergy_pos (h : ℝ) (hh : h ≠ 0) :
 555    0 < quadraticCurvatureEnergy (strainHingeAreas (Fin 4))
 556      (strainHingeDeficits (rectangleShearPotential h)) := by
 557  refine quadraticCurvatureEnergy_pos
 558    (fun p => by unfold strainHingeAreas; norm_num)
 559    ((0 : Fin 4), (1 : Fin 4))
 560    (by unfold strainHingeAreas; norm_num) ?_
 561  show rectangleShearPotential h 0 - rectangleShearPotential h 1 ≠ 0
 562  rw [(rectangleShearPotential_strains h).1]
 563  exact hh
 564
 565/-- **THEOREM (canonical shear bridge witness).** Under the explicit
 566small-strain premise (every scaled pair strain in [−1, 1]; the pair strains
 567of the rectangle shear potential are 0 and ±h, so |ε·h| ≤ 1 suffices), the
 568pure-shear rectangle configuration instantiates the corrected bridge. -/
 569noncomputable def rectangleShearBridge (h ε : ℝ)
 570    (hsmall : ∀ i j : Fin 4, |ε * (rectangleShearPotential h i
 571      - rectangleShearPotential h j)| ≤ 1) :
 572    LedgerToQuadraticEnergyBridge (Fin 4) :=
 573  canonicalQuadraticEnergyBridge (rectangleShearPotential h) ε hsmall
 574
 575/-! ## §7. Status: honest tier accounting -/
 576
 577/-- Status flags for the corrected ledger-energy bridge, by honesty tier.
 578
 579**THEOREM** (kernel-checked, this module):
 580* the per-strain expansion t²/2 ≤ J(exp t) = cosh t − 1 ≤ (t²/2)·cosh t
 581  and the quartic remainder |J(exp t) − t²/2| ≤ t⁴/2 on |t| ≤ 1
 582  (`cosh_sub_one_le_half_sq_mul_cosh`, `Jcost_exp_sub_half_sq_abs_le`);
 583* the coboundary-strain J-ledger is a `RecognitionLedger`
 584  (`coboundaryStrainLedger`), with the gate identity
 585  R(J(x), J(y)) = J(xy) + J(x/y) (`rclGate_Jcost_eq`) and the failure of
 586  the gate for general antisymmetric strain
 587  (`general_antisymmetric_strain_can_violate_rcl`);
 588* the quadratic matching |totalCost − (ε²/2)S₂| ≤ (ε⁴/2)S₄
 589  (`coboundary_totalCost_quadratic_matching`) and the canonical bridge
 590  instance (`canonicalQuadraticEnergyBridge`);
 591* the shear-visibility gate: pure rectangle shear carries strictly
 592  positive ledger AND quadratic hinge energy
 593  (`rectangleShear_ledgerEnergy_pos`, `rectangleShear_quadraticEnergy_pos`).
 594
 595**MODEL** (definitional identification, not derived here): reading
 596Σ_h A_h · δ_h² (`quadraticCurvatureEnergy`) as the discrete Isaacson-type
 597transverse-traceless energy, i.e. as the continuum partner of the ledger
 598energy. The parity and sign structure force a curvature-QUADRATIC target
 599(that much is THEOREM, from the no-go); WHICH quadratic functional is the
 600Regge/Isaacson one is the modeling identification.
 601
 602**OPEN**: the full Hessian-symbol comparison of the ledger quadratic form
 603against the frozen Regge quadratic functional on the periodic Freudenthal
 604mesh; the tensor multichannel escalation beyond the single coboundary
 605channel. -/
 606structure LedgerEnergyBridgeStatus where
 607  /-- THEOREM tier: two-sided quadratic expansion with explicit constants. -/
 608  jcost_expansion_theorem : Bool
 609  /-- THEOREM tier: coboundary-strain J-costs form a RecognitionLedger. -/
 610  coboundary_ledger_instance_theorem : Bool
 611  /-- THEOREM tier: RCL gate can fail for general antisymmetric strain
 612  (the scoping to coboundary strains is forced). -/
 613  general_antisymmetric_gate_failure_theorem : Bool
 614  /-- THEOREM tier: quadratic matching with explicit quartic remainder. -/
 615  quadratic_matching_theorem : Bool
 616  /-- THEOREM tier: pure shear carries strictly positive ledger energy. -/
 617  shear_visibility_theorem : Bool
 618  /-- MODEL tier: identifying Σ A_h δ_h² as the Isaacson-type continuum
 619  partner (definitional identification, not a derivation). -/
 620  isaacson_identification_model : Bool
 621  /-- OPEN: Hessian-symbol comparison against the frozen Regge quadratic
 622  functional on the periodic Freudenthal mesh. -/
 623  hessian_symbol_comparison_open : Bool
 624  /-- OPEN: tensor multichannel escalation. -/
 625  tensor_multichannel_open : Bool
 626
 627/-- The canonical status record. -/
 628def ledgerEnergyBridgeStatus : LedgerEnergyBridgeStatus where
 629  jcost_expansion_theorem := true
 630  coboundary_ledger_instance_theorem := true
 631  general_antisymmetric_gate_failure_theorem := true
 632  quadratic_matching_theorem := true
 633  shear_visibility_theorem := true
 634  isaacson_identification_model := true
 635  hessian_symbol_comparison_open := true
 636  tensor_multichannel_open := true
 637
 638/-- **Status flags theorem (rfl-forced).** -/
 639theorem ledgerEnergyBridgeStatus_flags :
 640    ledgerEnergyBridgeStatus.jcost_expansion_theorem = true ∧
 641    ledgerEnergyBridgeStatus.coboundary_ledger_instance_theorem = true ∧
 642    ledgerEnergyBridgeStatus.general_antisymmetric_gate_failure_theorem
 643      = true ∧
 644    ledgerEnergyBridgeStatus.quadratic_matching_theorem = true ∧
 645    ledgerEnergyBridgeStatus.shear_visibility_theorem = true ∧
 646    ledgerEnergyBridgeStatus.isaacson_identification_model = true ∧
 647    ledgerEnergyBridgeStatus.hessian_symbol_comparison_open = true ∧
 648    ledgerEnergyBridgeStatus.tensor_multichannel_open = true :=
 649  ⟨rfl, rfl, rfl, rfl, rfl, rfl, rfl, rfl⟩
 650
 651end SevenGaps
 652end Gravity
 653end IndisputableMonolith
 654