IndisputableMonolith.Gravity.SevenGaps.RecognitionRatioBridge

   1import Mathlib
   2import IndisputableMonolith.Cost
   3import IndisputableMonolith.Gravity.RecognitionLedger
   4import IndisputableMonolith.Gravity.SevenGaps.LedgerBridgeNoGo
   5import IndisputableMonolith.Gravity.SevenGaps.LedgerEnergyBridge
   6
   7/-!
   8# Seven Gaps, Phase 0a: the recognition-ratio bridge (the paper's odd form)
   9
  10## Status: the structure `RecognitionRatioBridge` is MODEL tier (an explicit
  11admissibility HYPOTHESIS, the paper's Def 6.2 clause, not yet derived); the
  12named theorems below are THEOREM tier (0 sorry, 0 admit, 0 new axiom;
  13`decide` is used only for `Fin 2` literal disequalities; no `native_decide`).
  14The status record at the end is documentation, not mathematics.
  15
  16`SevenGaps.LedgerBridgeNoGo` refuted the OLD bridge form
  17(`LedgerToHingeBridge.bridge_assumed`: ledger deficit = signed geometric
  18hinge deficit): ledger deficits are nonnegative
  19(`bridge_forces_nonneg_geometricDeficit`, the sign no-go) and J-ratio
  20deficits are EVEN in the deformation parameter
  21(`ledger_family_deficit_even_of_ratio_parity` and its corollaries), while
  22the signed Regge deficit response is odd.
  23
  24The physics paper does NOT assert that refuted form. Its substrate-to-
  25geometry bridge is the ODD relation on a positive comparison ratio x_sigma
  26at each hinge sigma:
  27
  28  log x_sigma = kappa_sigma * delta_sigma + remainder,
  29  |remainder| <= remBound * meshScale ^ 3,
  30
  31an admissibility clause on log x, not an equality of nonnegative deficits.
  32This module encodes that relation (`RecognitionRatioBridge`) and reconciles
  33it with the no-gos by KERNEL-CHECKED statements, not prose:
  34
  35* `ratioBridge_admits_negative_deficit`: for EVERY d there is an exact
  36  (remBound = 0), unit-coupled (kappa = 1) bridge on two hinges with
  37  geometric deficits d and -d. No free field absorbs the content: exactness
  38  and unit coupling are exported in the statement.
  39* `ratioBridgeLedger` and `ratioBridge_separates_deficit_observables`: every
  40  bridge induces a genuine `RecognitionLedger` (cost = J-cost of the ratio
  41  quotient, realized through the proved `coboundaryStrainLedger`), and on
  42  the witness family the induced LEDGER deficit is nonnegative
  43  (`RecognitionLedger.deficit_nonneg`, the engine of the sign no-go) and
  44  even under d -> -d (via `ledger_family_deficit_even_of_ratio_parity`),
  45  WHILE the GEOMETRIC deficit stays signed. The no-gos constrain the ledger
  46  deficit; the odd bridge keeps the signed information in log x: two
  47  different observables, no contradiction.
  48* `jcost_of_ratioBridge_cosh`, `jcost_of_ratioBridge_even_in_deficit`:
  49  J(x) = cosh(log x) - 1, so the J-cost sees only the even part of the
  50  relation and is invariant under a deficit sign flip.
  51* `ratioBridge_jcost_quadratic` (exact) and
  52  `ratioBridge_jcost_quadratic_inexact` (any remBound): the J-cost of the
  53  ratio matches (kappa * delta)^2 / 2 up to the quartic term, plus, in the
  54  inexact case, an explicit perturbation term in remBound * meshScale ^ 3.
  55  Both use the same numeric lemma `Jcost_exp_sub_half_sq_abs_le` (and the
  56  cosh bounds) proved in `LedgerEnergyBridge`.
  57
  58OPEN (wave 1b): deriving the ratio relation from stationarity of the ledger
  59action, rather than positing it as an admissibility hypothesis. OPEN
  60(lane 2): the h -> 0 asymptotic family; this module records the remainder
  61clause at one fixed mesh only.
  62-/
  63
  64namespace IndisputableMonolith
  65namespace Gravity
  66namespace SevenGaps
  67
  68/-! ## §1. The recognition-ratio bridge structure (MODEL tier) -/
  69
  70/-- **MODEL (explicit hypothesis, the paper's Def 6.2 recognition-ratio
  71admissibility clause; NOT yet derived, derivation target is wave 1b).**
  72
  73A recognition-ratio bridge on a hinge type `H` assigns to each hinge
  74`sigma` a positive comparison ratio `xRatio sigma`, a coupling
  75`kappa sigma`, and a SIGNED geometric deficit `geometricDeficit sigma`,
  76together with a mesh scale `meshScale` and a remainder constant `remBound`,
  77subject to the odd admissibility relation
  78
  79  |log (xRatio sigma) - kappa sigma * geometricDeficit sigma|
  80    <= remBound * meshScale ^ 3.
  81
  82Scope note: this records the paper's remainder clause AT A FIXED MESH; the
  83h -> 0 asymptotic family behind the O(h^3) notation is not yet formalized
  84(open, lane 2). Contrast with the REFUTED
  85`LedgerToHingeBridge.bridge_assumed` (ledger deficit = geometric deficit):
  86here the relation is carried by log x, which can take either sign, and the
  87reconciliation with the sign and parity no-gos is proved below
  88(`ratioBridge_admits_negative_deficit`,
  89`ratioBridge_separates_deficit_observables`). -/
  90structure RecognitionRatioBridge (H : Type*) where
  91  /-- The positive comparison ratio x_sigma at each hinge. -/
  92  xRatio : H → ℝ
  93  /-- Positivity of the comparison ratio. -/
  94  xRatio_pos : ∀ σ, 0 < xRatio σ
  95  /-- The hinge coupling kappa_sigma. -/
  96  kappa : H → ℝ
  97  /-- The SIGNED geometric deficit delta_sigma at each hinge. -/
  98  geometricDeficit : H → ℝ
  99  /-- The mesh scale h. -/
 100  meshScale : ℝ
 101  /-- The mesh scale is positive. -/
 102  meshScale_pos : 0 < meshScale
 103  /-- The remainder constant of the cubic-mesh clause. -/
 104  remBound : ℝ
 105  /-- The remainder constant is nonnegative. -/
 106  remBound_nonneg : 0 ≤ remBound
 107  /-- The odd admissibility relation: log x_sigma matches
 108  kappa_sigma * delta_sigma up to the cubic mesh remainder. -/
 109  ratio_relation : ∀ σ,
 110    |Real.log (xRatio σ) - kappa σ * geometricDeficit σ|
 111      ≤ remBound * meshScale ^ 3
 112
 113/-! ## §2. Exactness specializations (THEOREM tier, one-step)
 114
 115These are one-step specializations of `ratio_relation` at remBound = 0,
 116recorded once so later proofs can cite them; they carry no independent
 117content. -/
 118
 119/-- **THEOREM (one-step specialization).** For an exact bridge (remainder
 120constant 0) the relation is an equality: log (xRatio sigma) = kappa sigma *
 121geometricDeficit sigma. -/
 122theorem log_xRatio_eq_of_exact {H : Type*}
 123    (B : RecognitionRatioBridge H) (hB : B.remBound = 0) (σ : H) :
 124    Real.log (B.xRatio σ) = B.kappa σ * B.geometricDeficit σ := by
 125  have h := B.ratio_relation σ
 126  rw [hB, zero_mul] at h
 127  have habs : |Real.log (B.xRatio σ) - B.kappa σ * B.geometricDeficit σ|
 128      = 0 :=
 129    le_antisymm h (abs_nonneg _)
 130  exact sub_eq_zero.mp (abs_eq_zero.mp habs)
 131
 132/-- **THEOREM (one-step specialization).** For an exact bridge the
 133comparison ratio is the exponential of the linear deficit response. -/
 134theorem xRatio_eq_exp_of_exact {H : Type*}
 135    (B : RecognitionRatioBridge H) (hB : B.remBound = 0) (σ : H) :
 136    B.xRatio σ = Real.exp (B.kappa σ * B.geometricDeficit σ) := by
 137  rw [← log_xRatio_eq_of_exact B hB σ, Real.exp_log (B.xRatio_pos σ)]
 138
 139/-! ## §3. Escape from the sign no-go: the strong witness (THEOREM tier)
 140
 141`bridge_forces_nonneg_geometricDeficit` (in `LedgerBridgeNoGo`) shows the
 142OLD form forces every reached geometric deficit to be nonnegative. The odd
 143form does not, and the witness exports its full strength: exact relation,
 144unit coupling, prescribed signed deficits. -/
 145
 146/-- The explicit two-hinge witness: deficits d at hinge 0 and -d at hinge 1,
 147kappa = 1, xRatio sigma = exp(deficit sigma), mesh scale 1, remainder 0.
 148The ratio relation holds exactly. -/
 149noncomputable def twoHingeWitnessBridge (d : ℝ) :
 150    RecognitionRatioBridge (Fin 2) where
 151  xRatio := fun σ => Real.exp (if σ = 0 then d else -d)
 152  xRatio_pos := fun _ => Real.exp_pos _
 153  kappa := fun _ => 1
 154  geometricDeficit := fun σ => if σ = 0 then d else -d
 155  meshScale := 1
 156  meshScale_pos := one_pos
 157  remBound := 0
 158  remBound_nonneg := le_refl 0
 159  ratio_relation := by
 160    intro σ
 161    simp only [Real.log_exp, one_mul, sub_self, abs_zero, zero_mul, le_refl]
 162
 163/-- **THEOREM.** Evaluation of the witness deficits: d at hinge 0 and -d at
 164hinge 1. (Uses `decide` only for the `Fin 2` literal disequality 1 ≠ 0.) -/
 165theorem twoHingeWitnessBridge_deficit (d : ℝ) :
 166    (twoHingeWitnessBridge d).geometricDeficit 0 = d ∧
 167      (twoHingeWitnessBridge d).geometricDeficit 1 = -d := by
 168  constructor
 169  · show (if (0 : Fin 2) = 0 then d else -d) = d
 170    rw [if_pos rfl]
 171  · show (if (1 : Fin 2) = 0 then d else -d) = -d
 172    have h10 : ¬((1 : Fin 2) = 0) := by decide
 173    rw [if_neg h10]
 174
 175/-- **THEOREM (escape from the sign no-go, strong universal form).** For
 176EVERY d there is an EXACT (remBound = 0), UNIT-COUPLED (kappa = 1)
 177recognition-ratio bridge on two hinges whose geometric deficit takes the
 178prescribed values d at hinge 0 and -d at hinge 1. For d > 0 the deficit at
 179hinge 1 is strictly negative, which
 180`bridge_forces_nonneg_geometricDeficit` proves impossible for the old
 181deficit-equality form: the odd log-ratio form escapes the sign obstruction
 182with no free field absorbing the content. -/
 183theorem ratioBridge_admits_negative_deficit (d : ℝ) :
 184    ∃ B : RecognitionRatioBridge (Fin 2),
 185      B.remBound = 0 ∧ (∀ σ, B.kappa σ = 1) ∧
 186      B.geometricDeficit 0 = d ∧ B.geometricDeficit 1 = -d :=
 187  ⟨twoHingeWitnessBridge d, rfl, fun _ => rfl,
 188    (twoHingeWitnessBridge_deficit d).1, (twoHingeWitnessBridge_deficit d).2⟩
 189
 190/-! ## §4. The induced recognition ledger and the reconciliation theorem
 191
 192Engagement with the no-go on its own ground: every bridge induces a genuine
 193`RecognitionLedger`, and the no-go's constraints (nonnegative, parity-even
 194deficit) hold for THAT object while the bridge's geometric deficit stays
 195signed. -/
 196
 197/-- The recognition ledger induced by a recognition-ratio bridge: the cost
 198of the pair (sigma, tau) is the J-cost of the comparison-ratio quotient
 199xRatio sigma / xRatio tau. Realized as `coboundaryStrainLedger` with cell
 200potential log (xRatio sigma), so symmetry, diagonal zero, nonnegativity,
 201and RCL subadditivity are all inherited from the proved construction in
 202`LedgerEnergyBridge`. -/
 203noncomputable def ratioBridgeLedger {H : Type*} [Fintype H] [DecidableEq H]
 204    (B : RecognitionRatioBridge H) :
 205    RecognitionLedger.RecognitionLedger H :=
 206  coboundaryStrainLedger (fun σ => Real.log (B.xRatio σ))
 207
 208/-- **THEOREM.** The induced ledger cost is the J-cost of the ratio
 209quotient: cost sigma tau = J(xRatio sigma / xRatio tau). -/
 210theorem ratioBridgeLedger_cost {H : Type*} [Fintype H] [DecidableEq H]
 211    (B : RecognitionRatioBridge H) (σ τ : H) :
 212    (ratioBridgeLedger B).cost σ τ
 213      = Cost.Jcost (B.xRatio σ / B.xRatio τ) := by
 214  show Cost.Jcost
 215      (Real.exp (Real.log (B.xRatio σ) - Real.log (B.xRatio τ))) = _
 216  rw [Real.exp_sub, Real.exp_log (B.xRatio_pos σ),
 217    Real.exp_log (B.xRatio_pos τ)]
 218
 219/-- **THEOREM.** Ratio parity of the witness family: flipping the sign of d
 220inverts every comparison ratio. -/
 221theorem twoHingeWitnessBridge_xRatio_neg (d : ℝ) (σ : Fin 2) :
 222    (twoHingeWitnessBridge (-d)).xRatio σ
 223      = ((twoHingeWitnessBridge d).xRatio σ)⁻¹ := by
 224  show Real.exp (if σ = 0 then -d else -(-d))
 225      = (Real.exp (if σ = 0 then d else -d))⁻¹
 226  rw [← Real.exp_neg]
 227  congr 1
 228  by_cases h : σ = 0
 229  · rw [if_pos h, if_pos h]
 230  · rw [if_neg h, if_neg h]
 231
 232/-- **THEOREM.** The ledger deficit induced by the witness family is EVEN
 233under d -> -d, by direct application of the no-go's own family theorem
 234`ledger_family_deficit_even_of_ratio_parity` (with ratios r d sigma tau =
 235xRatio sigma / xRatio tau, parity-covariant by
 236`twoHingeWitnessBridge_xRatio_neg`). -/
 237theorem twoHingeWitness_ledger_deficit_even (d : ℝ) (σ : Fin 2) :
 238    RecognitionLedger.deficit
 239        (ratioBridgeLedger (twoHingeWitnessBridge (-d))) σ
 240      = RecognitionLedger.deficit
 241        (ratioBridgeLedger (twoHingeWitnessBridge d)) σ := by
 242  exact ledger_family_deficit_even_of_ratio_parity
 243    (fun ε => ratioBridgeLedger (twoHingeWitnessBridge ε))
 244    (fun ε i j =>
 245      (twoHingeWitnessBridge ε).xRatio i / (twoHingeWitnessBridge ε).xRatio j)
 246    (fun ε i j => div_pos ((twoHingeWitnessBridge ε).xRatio_pos i)
 247      ((twoHingeWitnessBridge ε).xRatio_pos j))
 248    (fun ε i j => ratioBridgeLedger_cost (twoHingeWitnessBridge ε) i j)
 249    (fun ε i j => by
 250      show (twoHingeWitnessBridge (-ε)).xRatio i
 251            / (twoHingeWitnessBridge (-ε)).xRatio j
 252          = ((twoHingeWitnessBridge ε).xRatio i
 253            / (twoHingeWitnessBridge ε).xRatio j)⁻¹
 254      rw [twoHingeWitnessBridge_xRatio_neg ε i,
 255        twoHingeWitnessBridge_xRatio_neg ε j, inv_div_inv, inv_div])
 256    d σ
 257
 258/-- **THEOREM (deficit-observable separation: the reconciliation).** For
 259every d > 0 the exact, unit-coupled two-hinge witness simultaneously has:
 260
 261* a SIGNED geometric deficit (value d at hinge 0, strictly negative value
 262  -d at hinge 1), which the sign no-go forbids for the LEDGER deficit; and
 263* an induced genuine `RecognitionLedger` whose deficit is NONNEGATIVE at
 264  every cell (`RecognitionLedger.deficit_nonneg`, the engine behind
 265  `bridge_forces_nonneg_geometricDeficit`) and EVEN under the sign flip
 266  d -> -d (`ledger_family_deficit_even_of_ratio_parity`, via
 267  `twoHingeWitness_ledger_deficit_even`).
 268
 269The no-gos constrain the ledger deficit; the paper's odd bridge stores the
 270signed information in log x, hence in the geometric deficit. The two
 271observables are separated by this witness, so the no-gos and the paper's
 272bridge are jointly consistent. -/
 273theorem ratioBridge_separates_deficit_observables (d : ℝ) (hd : 0 < d) :
 274    (twoHingeWitnessBridge d).remBound = 0 ∧
 275    (∀ σ, (twoHingeWitnessBridge d).kappa σ = 1) ∧
 276    (twoHingeWitnessBridge d).geometricDeficit 0 = d ∧
 277    (twoHingeWitnessBridge d).geometricDeficit 1 < 0 ∧
 278    (∀ σ, 0 ≤ RecognitionLedger.deficit
 279        (ratioBridgeLedger (twoHingeWitnessBridge d)) σ) ∧
 280    (∀ σ, RecognitionLedger.deficit
 281          (ratioBridgeLedger (twoHingeWitnessBridge (-d))) σ
 282        = RecognitionLedger.deficit
 283          (ratioBridgeLedger (twoHingeWitnessBridge d)) σ) := by
 284  refine ⟨rfl, fun _ => rfl, (twoHingeWitnessBridge_deficit d).1, ?_,
 285    fun σ => RecognitionLedger.deficit_nonneg _ σ,
 286    fun σ => twoHingeWitness_ledger_deficit_even d σ⟩
 287  rw [(twoHingeWitnessBridge_deficit d).2]
 288  linarith
 289
 290/-! ## §5. Parity of the J-cost (THEOREM tier)
 291
 292The ledger cost of the comparison ratio sees only the EVEN part of the
 293relation: J(x) = cosh(log x) - 1. The signed information lives in log x. -/
 294
 295/-- **THEOREM.** For any bridge and hinge, the J-cost of the comparison
 296ratio is cosh of its logarithm minus one. Since cosh is even, the ledger
 297cost is blind to the sign of log x_sigma. -/
 298theorem jcost_of_ratioBridge_cosh {H : Type*}
 299    (B : RecognitionRatioBridge H) (σ : H) :
 300    Cost.Jcost (B.xRatio σ)
 301      = Real.cosh (Real.log (B.xRatio σ)) - 1 := by
 302  conv_lhs => rw [← Real.exp_log (B.xRatio_pos σ)]
 303  exact Cost.Jcost_exp_cosh _
 304
 305/-- **THEOREM.** For an exact bridge the J-cost of the comparison ratio is
 306cosh(kappa sigma * delta sigma) - 1, an EVEN function of the deficit. -/
 307theorem jcost_of_exact_ratioBridge {H : Type*}
 308    (B : RecognitionRatioBridge H) (hB : B.remBound = 0) (σ : H) :
 309    Cost.Jcost (B.xRatio σ)
 310      = Real.cosh (B.kappa σ * B.geometricDeficit σ) - 1 := by
 311  rw [jcost_of_ratioBridge_cosh B σ, log_xRatio_eq_of_exact B hB σ]
 312
 313/-- **THEOREM (J-cost parity).** For two exact bridges whose deficits at a
 314hinge differ by a sign flip while the couplings agree, the J-costs of the
 315comparison ratios are EQUAL: the per-hinge ledger cost is parity-blind,
 316exactly as the parity no-gos require, while the signed deficit information
 317survives in log x_sigma. -/
 318theorem jcost_of_ratioBridge_even_in_deficit {H : Type*}
 319    (B₁ B₂ : RecognitionRatioBridge H)
 320    (h₁ : B₁.remBound = 0) (h₂ : B₂.remBound = 0) (σ : H)
 321    (hκ : B₂.kappa σ = B₁.kappa σ)
 322    (hδ : B₂.geometricDeficit σ = - B₁.geometricDeficit σ) :
 323    Cost.Jcost (B₂.xRatio σ) = Cost.Jcost (B₁.xRatio σ) := by
 324  rw [jcost_of_exact_ratioBridge B₁ h₁ σ, jcost_of_exact_ratioBridge B₂ h₂ σ,
 325    hκ, hδ, mul_neg, Real.cosh_neg]
 326
 327/-! ## §6. Quadratic expansion: exact and inexact (THEOREM tier)
 328
 329Both statements use the numeric expansion lemmas of `LedgerEnergyBridge`
 330(`Jcost_exp_sub_half_sq_abs_le`, `cosh_sub_one_le_half_sq_mul_cosh`,
 331`abs_sinh_le_abs_mul_cosh`, `cosh_one_lt_two`). The inexact form is the one
 332that actually consumes the remainder clause of the structure. -/
 333
 334/-- **THEOREM (exact quadratic expansion).** For an exact bridge with small
 335response |kappa sigma * delta sigma| <= 1:
 336
 337  |J(x_sigma) - (kappa sigma * delta sigma)^2 / 2|
 338    <= (kappa sigma * delta sigma)^4 / 2.
 339
 340Same numeric lemma `Jcost_exp_sub_half_sq_abs_le` as the quadratic-energy
 341matching of `LedgerEnergyBridge`. -/
 342theorem ratioBridge_jcost_quadratic {H : Type*}
 343    (B : RecognitionRatioBridge H) (hB : B.remBound = 0) (σ : H)
 344    (hsmall : |B.kappa σ * B.geometricDeficit σ| ≤ 1) :
 345    |Cost.Jcost (B.xRatio σ)
 346        - (B.kappa σ * B.geometricDeficit σ) ^ 2 / 2|
 347      ≤ (B.kappa σ * B.geometricDeficit σ) ^ 4 / 2 := by
 348  rw [xRatio_eq_exp_of_exact B hB σ]
 349  exact Jcost_exp_sub_half_sq_abs_le _ hsmall
 350
 351/-- **THEOREM.** |sinh a| <= cosh a for all a (from the exponential forms:
 352cosh a - sinh a = exp(-a) > 0 and cosh a + sinh a = exp a > 0). -/
 353theorem abs_sinh_le_cosh (a : ℝ) : |Real.sinh a| ≤ Real.cosh a := by
 354  rw [abs_le]
 355  constructor
 356  · rw [Real.sinh_eq, Real.cosh_eq]
 357    nlinarith [Real.exp_pos a, Real.exp_pos (-a)]
 358  · rw [Real.sinh_eq, Real.cosh_eq]
 359    nlinarith [Real.exp_pos a, Real.exp_pos (-a)]
 360
 361/-- **THEOREM (cosh perturbation bound).** For all a, r:
 362
 363  |cosh (a + r) - cosh a| <= cosh a * cosh r * (|r| + r^2 / 2),
 364
 365from cosh(a + r) = cosh a * cosh r + sinh a * sinh r together with
 366cosh r - 1 <= (r^2/2) * cosh r and |sinh| bounds. -/
 367theorem abs_cosh_add_sub_cosh_le (a r : ℝ) :
 368    |Real.cosh (a + r) - Real.cosh a|
 369      ≤ Real.cosh a * Real.cosh r * (|r| + r ^ 2 / 2) := by
 370  have hsplit : Real.cosh (a + r) - Real.cosh a
 371      = Real.cosh a * (Real.cosh r - 1) + Real.sinh a * Real.sinh r := by
 372    rw [Real.cosh_add]
 373    ring
 374  rw [hsplit]
 375  have hcosh_r1 : 0 ≤ Real.cosh r - 1 := by linarith [Real.one_le_cosh r]
 376  have hca : 0 ≤ Real.cosh a := le_of_lt (Real.cosh_pos a)
 377  have h2 : |Real.cosh a * (Real.cosh r - 1)|
 378      = Real.cosh a * (Real.cosh r - 1) :=
 379    abs_of_nonneg (mul_nonneg hca hcosh_r1)
 380  have h4 : Real.cosh a * (Real.cosh r - 1)
 381      ≤ Real.cosh a * (r ^ 2 / 2 * Real.cosh r) :=
 382    mul_le_mul_of_nonneg_left (cosh_sub_one_le_half_sq_mul_cosh r) hca
 383  have h5 : |Real.sinh a| * |Real.sinh r|
 384      ≤ Real.cosh a * (|r| * Real.cosh r) :=
 385    mul_le_mul (abs_sinh_le_cosh a) (abs_sinh_le_abs_mul_cosh r)
 386      (abs_nonneg _) hca
 387  calc |Real.cosh a * (Real.cosh r - 1) + Real.sinh a * Real.sinh r|
 388      ≤ |Real.cosh a * (Real.cosh r - 1)| + |Real.sinh a * Real.sinh r| :=
 389        abs_add_le _ _
 390    _ = Real.cosh a * (Real.cosh r - 1) + |Real.sinh a| * |Real.sinh r| := by
 391        rw [h2, abs_mul]
 392    _ ≤ Real.cosh a * (r ^ 2 / 2 * Real.cosh r)
 393          + Real.cosh a * (|r| * Real.cosh r) := add_le_add h4 h5
 394    _ = Real.cosh a * Real.cosh r * (|r| + r ^ 2 / 2) := by ring
 395
 396/-- **THEOREM (inexact quadratic expansion, generic form).** If
 397|t - a| <= R with 0 <= R and |a| <= 1, then
 398
 399  |cosh t - 1 - a^2/2| <= a^4/2 + 2 * cosh R * (R + R^2/2).
 400
 401The first term is the exact quartic remainder; the second is the explicit
 402perturbation cost of the inexactness. -/
 403theorem cosh_sub_one_sub_half_sq_abs_le_of_near (a t R : ℝ)
 404    (hsmall : |a| ≤ 1) (hR0 : 0 ≤ R) (hnear : |t - a| ≤ R) :
 405    |Real.cosh t - 1 - a ^ 2 / 2|
 406      ≤ a ^ 4 / 2 + 2 * Real.cosh R * (R + R ^ 2 / 2) := by
 407  have hexact : |Real.cosh a - 1 - a ^ 2 / 2| ≤ a ^ 4 / 2 := by
 408    have h := Jcost_exp_sub_half_sq_abs_le a hsmall
 409    rwa [Cost.Jcost_exp_cosh] at h
 410  have hpert := abs_cosh_add_sub_cosh_le a (t - a)
 411  rw [show a + (t - a) = t from by ring] at hpert
 412  have hcosha : Real.cosh a ≤ 2 := by
 413    have hmono : Real.cosh a ≤ Real.cosh 1 := by
 414      rw [Real.cosh_le_cosh]
 415      simpa using hsmall
 416    linarith [cosh_one_lt_two]
 417  have hcoshr : Real.cosh (t - a) ≤ Real.cosh R := by
 418    rw [Real.cosh_le_cosh, abs_of_nonneg hR0]
 419    exact hnear
 420  have hr2 : (t - a) ^ 2 ≤ R ^ 2 := by
 421    nlinarith [hnear, abs_nonneg (t - a), sq_abs (t - a)]
 422  have hnn : (0 : ℝ) ≤ |t - a| + (t - a) ^ 2 / 2 :=
 423    add_nonneg (abs_nonneg _) (by positivity)
 424  have hchain : Real.cosh a * Real.cosh (t - a) * (|t - a| + (t - a) ^ 2 / 2)
 425      ≤ 2 * Real.cosh R * (R + R ^ 2 / 2) := by
 426    have h1 : Real.cosh a * Real.cosh (t - a) ≤ 2 * Real.cosh R :=
 427      mul_le_mul hcosha hcoshr (le_of_lt (Real.cosh_pos _)) (by norm_num)
 428    have h2 : |t - a| + (t - a) ^ 2 / 2 ≤ R + R ^ 2 / 2 := by
 429      linarith [hnear, hr2]
 430    have h3 : (0 : ℝ) ≤ 2 * Real.cosh R :=
 431      mul_nonneg (by norm_num) (le_of_lt (Real.cosh_pos R))
 432    calc Real.cosh a * Real.cosh (t - a) * (|t - a| + (t - a) ^ 2 / 2)
 433        ≤ 2 * Real.cosh R * (|t - a| + (t - a) ^ 2 / 2) :=
 434          mul_le_mul_of_nonneg_right h1 hnn
 435      _ ≤ 2 * Real.cosh R * (R + R ^ 2 / 2) :=
 436          mul_le_mul_of_nonneg_left h2 h3
 437  have htri : |Real.cosh t - 1 - a ^ 2 / 2|
 438      ≤ |Real.cosh t - Real.cosh a| + |Real.cosh a - 1 - a ^ 2 / 2| := by
 439    have hsplit : Real.cosh t - 1 - a ^ 2 / 2
 440        = (Real.cosh t - Real.cosh a) + (Real.cosh a - 1 - a ^ 2 / 2) := by
 441      ring
 442    rw [hsplit]
 443    exact abs_add_le _ _
 444  linarith [htri, hpert, hexact, hchain]
 445
 446/-- **THEOREM (inexact quadratic expansion of the bridge).** For ANY
 447recognition-ratio bridge (no exactness assumed) with small response
 448|kappa sigma * delta sigma| <= 1, writing R = remBound * meshScale^3 for
 449the remainder budget of `ratio_relation`:
 450
 451  |J(x_sigma) - (kappa sigma * delta sigma)^2 / 2|
 452    <= (kappa sigma * delta sigma)^4 / 2 + 2 * cosh R * (R + R^2 / 2).
 453
 454At remBound = 0 the perturbation term vanishes (cosh 0 * 0 = 0) and the
 455bound reduces to the exact statement `ratioBridge_jcost_quadratic`. This is
 456the theorem that actually consumes the remainder clause of the structure. -/
 457theorem ratioBridge_jcost_quadratic_inexact {H : Type*}
 458    (B : RecognitionRatioBridge H) (σ : H)
 459    (hsmall : |B.kappa σ * B.geometricDeficit σ| ≤ 1) :
 460    |Cost.Jcost (B.xRatio σ)
 461        - (B.kappa σ * B.geometricDeficit σ) ^ 2 / 2|
 462      ≤ (B.kappa σ * B.geometricDeficit σ) ^ 4 / 2
 463        + 2 * Real.cosh (B.remBound * B.meshScale ^ 3)
 464            * (B.remBound * B.meshScale ^ 3
 465                + (B.remBound * B.meshScale ^ 3) ^ 2 / 2) := by
 466  have hR0 : 0 ≤ B.remBound * B.meshScale ^ 3 :=
 467    mul_nonneg B.remBound_nonneg (pow_nonneg (le_of_lt B.meshScale_pos) 3)
 468  rw [jcost_of_ratioBridge_cosh B σ]
 469  exact cosh_sub_one_sub_half_sq_abs_le_of_near
 470    (B.kappa σ * B.geometricDeficit σ) (Real.log (B.xRatio σ))
 471    (B.remBound * B.meshScale ^ 3) hsmall hR0 (B.ratio_relation σ)
 472
 473/-! ## §7. Status record (documentation, not mathematics) -/
 474
 475/-- Status flags for the recognition-ratio bridge (documentation record;
 476the mathematics lives in the theorems above, not in these booleans).
 477
 478**MODEL** (explicit hypothesis, this module): the structure
 479`RecognitionRatioBridge` itself, encoding the paper's Def 6.2
 480recognition-ratio admissibility clause at a fixed mesh.
 481
 482**THEOREM** (kernel-checked, this module): the strong sign-no-go escape
 483witness (`ratioBridge_admits_negative_deficit`); the induced-ledger
 484reconciliation (`ratioBridgeLedger`,
 485`ratioBridge_separates_deficit_observables`); the J-cost parity statements
 486(`jcost_of_ratioBridge_cosh`, `jcost_of_ratioBridge_even_in_deficit`); the
 487exact and inexact quadratic expansions (`ratioBridge_jcost_quadratic`,
 488`ratioBridge_jcost_quadratic_inexact`).
 489
 490**OPEN**: derivation of the ratio relation from stationarity (wave 1b);
 491the h -> 0 asymptotic family behind the O(h^3) notation (lane 2).
 492
 493UPDATE (2026-07-15, `StationarityBridgeClosure`): the CONSTITUTIVE form of
 494wave 1b is now closed — `recognitionRatioBridge_ofStationarity` inhabits
 495this structure with `ratio_relation` PROVED from sourced J-stationarity
 496(`sourced_ratio_cubic_error`). The flag below stays `true` because its
 497honest reading is the residual: the deficit-source coupling inside
 498`sourcedAction` is itself a MODEL premise, so derivation from the BARE
 499`RecognitionLedger` (no constitutive action) remains open. See
 500`stationarityBridgeClosureStatus` for the split record. -/
 501structure RecognitionRatioBridgeStatus where
 502  /-- MODEL tier: the paper's odd ratio relation is encoded as an explicit
 503  hypothesis structure. -/
 504  paper_relation_encoded : Bool
 505  /-- THEOREM tier: strong witness with exactness and unit coupling
 506  exported and a strictly negative geometric deficit for d > 0. -/
 507  negative_deficit_witness : Bool
 508  /-- OPEN residual: derivation from the BARE ledger. The constitutive
 509  form is closed by `StationarityBridgeClosure.recognitionRatioBridge_ofStationarity`
 510  (2026-07-15); the deficit-source coupling remains a MODEL premise. -/
 511  derivation_from_stationarity_open : Bool
 512  /-- THEOREM tier (in `LedgerBridgeNoGo`): the old even/nonneg
 513  deficit-equality form is refuted. -/
 514  old_even_form_refuted : Bool
 515
 516/-- The canonical status record (documentation, not new mathematics). -/
 517def recognitionRatioBridgeStatus : RecognitionRatioBridgeStatus where
 518  paper_relation_encoded := true
 519  negative_deficit_witness := true
 520  derivation_from_stationarity_open := true
 521  old_even_form_refuted := true
 522
 523/-- Status flags record (rfl-forced; documentation, not new mathematics). -/
 524theorem recognitionRatioBridgeStatus_flags :
 525    recognitionRatioBridgeStatus.paper_relation_encoded = true ∧
 526    recognitionRatioBridgeStatus.negative_deficit_witness = true ∧
 527    recognitionRatioBridgeStatus.derivation_from_stationarity_open = true ∧
 528    recognitionRatioBridgeStatus.old_even_form_refuted = true :=
 529  ⟨rfl, rfl, rfl, rfl⟩
 530
 531end SevenGaps
 532end Gravity
 533end IndisputableMonolith
 534