IndisputableMonolith.Gravity.SevenGaps.LedgerBridgeNoGo

   1import Mathlib
   2import IndisputableMonolith.Cost
   3import IndisputableMonolith.Gravity.RecognitionLedger
   4import IndisputableMonolith.Gravity.LedgerToGeometryBridge
   5
   6/-!
   7# Seven Gaps, Lane 1a: the ledger-to-hinge bridge no-go
   8
   9## Status: THEOREM (0 sorry, 0 RS-internal axiom, no decide/native_decide).
  10
  11This module proves two obstruction theorems against the assumed form of the
  12substrate-to-triangulation bridge (`Gravity.LedgerToHingeBridge.bridge_assumed`,
  13which equates the recognition-ledger deficit at each cell with a raw geometric
  14hinge deficit). PRECISE SCOPE OF WHAT IS FORMALIZED: (1) no bridge exists for
  15any specification that puts a strictly negative deficit in the image of the
  16comparison map; (2) no parity-covariant J-ratio ledger family has a deficit
  17with a signed linear response. The composite reading "hence the assumed form
  18is unsatisfiable on two-sided weak-field deformation classes" additionally
  19uses the GEOMETRIC PREMISE (not formalized here, prose tier) that such
  20classes contain hinges of strictly negative deficit in the image of any
  21faithful comparison map, and that the weak-field Regge response is odd at
  22leading order.
  23
  24**1. Sign no-go.** The ledger deficit is a sum of J-costs, hence provably
  25nonnegative (`RecognitionLedger.deficit_nonneg`). Weak-field Regge deficit
  26angles are signed: a two-sided deformation class contains hinges with
  27strictly negative deficit. Consequently every `LedgerToHingeBridge` forces
  28its geometric deficit to be nonnegative on the image of the comparison map
  29(`bridge_forces_nonneg_geometricDeficit`), and no bridge exists whose
  30specified deficit assignment is negative anywhere on that image
  31(`no_bridge_matches_negative_deficit_spec`).
  32
  33**2. Parity no-go.** Any ledger built from J-costs of comparison ratios
  34inherits the ratio symmetry J(x) = J(1/x) (`Cost.Jcost_symm`). If the
  35one-parameter ratio family satisfies the natural ratio parity
  36r(-ε) = r(ε)⁻¹ (e.g. exponential strain ratios r = exp(ε·s)), the induced
  37deficit is an EVEN function of the deformation parameter ε
  38(`jRatioDeficit_even`, `ledger_family_deficit_even_of_ratio_parity`),
  39with O(ε²) leading term. The signed Regge deficit response is odd, O(ε).
  40An even function can match an odd function only if both vanish identically
  41(`even_and_odd_forces_zero`); in particular a signed linear-response
  42deficit δ(ε) = c·ε with c ≠ 0 admits no J-ratio realization on any
  43symmetric interval (`no_jRatio_deficit_linear_response`,
  44`no_ledger_family_linear_response`).
  45
  46**Reading revision.** The status structure `LedgerBridgeNoGoStatus` records
  47what these theorems change about the reading of
  48`LedgerToHingeBridge.bridge_assumed`: the field is not a neutral assumption
  49awaiting derivation; it carries the two proved obstructions above, and under
  50the stated geometric premise (prose tier) it is unsatisfiable on two-sided
  51weak-field classes. The corrected bridge target is the nonnegative
  52curvature-QUADRATIC geometric energy (discrete Isaacson-type form
  53Σ_h A_h · δ_h²), built in
  54`IndisputableMonolith.Gravity.SevenGaps.LedgerEnergyBridge`.
  55
  56Honest tier split: the sign and parity theorems are THEOREM; the negative
  57deficits and odd leading response of two-sided weak-field Regge classes are
  58the geometric input motivating the hypotheses (MODEL/prose, not formalized
  59in this file).
  60-/
  61
  62namespace IndisputableMonolith
  63namespace Gravity
  64namespace SevenGaps
  65
  66/-! ## §1. Sign no-go -/
  67
  68/-- **THEOREM (sign obstruction, positive form).** Any bridge satisfying the
  69assumed deficit-matching condition forces the geometric deficit to be
  70nonnegative at every hinge in the image of the comparison map `x_sigma`.
  71Direct consequence of `RecognitionLedger.deficit_nonneg`: ledger deficits
  72are sums of nonnegative J-costs. -/
  73theorem bridge_forces_nonneg_geometricDeficit
  74    {Λ : Type*} [Fintype Λ] [DecidableEq Λ] {H : Type*}
  75    (L : RecognitionLedger.RecognitionLedger Λ)
  76    (B : LedgerToHingeBridge H L) (i : Λ) :
  77    0 ≤ B.geometricDeficit (B.x_sigma i) := by
  78  rw [← B.bridge_assumed i]
  79  exact RecognitionLedger.deficit_nonneg L i
  80
  81/-- **THEOREM (sign obstruction, nonexistence form).** Given any hinge
  82specification (comparison map `x` and deficit assignment `δ`) for which some
  83cell `i` sees a strictly negative geometric deficit `δ (x i) < 0`, there is
  84NO `LedgerToHingeBridge` realizing that specification, for any recognition
  85ledger `L` whatsoever. Combined with the geometric premise that two-sided
  86(signed) weak-field deformation classes place negative deficits in the image
  87of any faithful comparison map (prose tier, not formalized here), this
  88excludes the assumed bridge form on such classes. -/
  89theorem no_bridge_matches_negative_deficit_spec
  90    {Λ : Type*} [Fintype Λ] [DecidableEq Λ] {H : Type*}
  91    (L : RecognitionLedger.RecognitionLedger Λ)
  92    (x : Λ → H) (δ : H → ℝ) (i : Λ) (hneg : δ (x i) < 0) :
  93    ¬ ∃ B : LedgerToHingeBridge H L, B.x_sigma = x ∧ B.geometricDeficit = δ := by
  94  rintro ⟨B, hx, hd⟩
  95  have h := bridge_forces_nonneg_geometricDeficit L B i
  96  rw [hx, hd] at h
  97  exact absurd h (not_le.mpr hneg)
  98
  99/-! ## §2. Parity no-go
 100
 101A J-ratio ledger family assigns to each cell pair the J-cost of a
 102one-parameter comparison ratio. The natural ratio parity r(-ε) = r(ε)⁻¹
 103(satisfied by exponential strain ratios r = exp(ε·s)) makes every induced
 104cost, hence every induced deficit, EVEN in the deformation parameter ε. -/
 105
 106/-- **THEOREM (abstract ratio parity).** For any positive one-parameter ratio
 107family with the natural parity r(-ε) = r(ε)⁻¹, the J-cost of the ratio is an
 108even function of ε. This is exactly J(x) = J(1/x) (`Cost.Jcost_symm`). -/
 109theorem Jcost_ratio_parity (r : ℝ → ℝ) (hpos : ∀ ε, 0 < r ε)
 110    (hpar : ∀ ε, r (-ε) = (r ε)⁻¹) (ε : ℝ) :
 111    Cost.Jcost (r (-ε)) = Cost.Jcost (r ε) := by
 112  rw [hpar ε]
 113  exact (Cost.Jcost_symm (hpos ε)).symm
 114
 115/-- The J-cost of the exponential strain ratio exp(ε·s i j) on cell pair
 116(i, j). This is the generic J-ratio ledger cell cost; no antisymmetry of `s`
 117is required for the parity argument. -/
 118noncomputable def jRatioCellCost {Λ : Type*} (s : Λ → Λ → ℝ) (ε : ℝ)
 119    (i j : Λ) : ℝ :=
 120  Cost.Jcost (Real.exp (ε * s i j))
 121
 122/-- The deficit at cell `i` induced by the J-ratio family: the sum over all
 123cells of the cell-pair J-costs (the raw analogue of
 124`RecognitionLedger.deficit`, needing no ledger axioms). -/
 125noncomputable def jRatioDeficit {Λ : Type*} [Fintype Λ] (s : Λ → Λ → ℝ)
 126    (ε : ℝ) (i : Λ) : ℝ :=
 127  ∑ j, jRatioCellCost s ε i j
 128
 129/-- **THEOREM.** Each J-ratio cell cost is even in ε: the exponential strain
 130ratio satisfies exp(-ε·s) = (exp(ε·s))⁻¹ and J(x) = J(1/x). -/
 131theorem jRatioCellCost_even {Λ : Type*} (s : Λ → Λ → ℝ) (ε : ℝ) (i j : Λ) :
 132    jRatioCellCost s (-ε) i j = jRatioCellCost s ε i j := by
 133  unfold jRatioCellCost
 134  have hexp : Real.exp (-ε * s i j) = (Real.exp (ε * s i j))⁻¹ := by
 135    rw [← Real.exp_neg]
 136    congr 1
 137    ring
 138  rw [hexp]
 139  exact (Cost.Jcost_symm (Real.exp_pos _)).symm
 140
 141/-- **THEOREM (parity no-go, deficit form).** The J-ratio deficit at every
 142cell is an EVEN function of the deformation parameter ε. Its response to a
 143deformation therefore has no odd part: the leading term is O(ε²), never the
 144signed O(ε) linear response of a weak-field Regge deficit. -/
 145theorem jRatioDeficit_even {Λ : Type*} [Fintype Λ] (s : Λ → Λ → ℝ) (ε : ℝ)
 146    (i : Λ) :
 147    jRatioDeficit s (-ε) i = jRatioDeficit s ε i := by
 148  unfold jRatioDeficit
 149  exact Finset.sum_congr rfl fun j _ => jRatioCellCost_even s ε i j
 150
 151/-- **THEOREM (even vs. odd exclusion).** An even function of ε can equal an
 152odd function of ε only if both vanish identically. -/
 153theorem even_and_odd_forces_zero (g d : ℝ → ℝ)
 154    (hg : ∀ ε, g (-ε) = g ε) (hd : ∀ ε, d (-ε) = - d ε)
 155    (hmatch : ∀ ε, g ε = d ε) (ε : ℝ) :
 156    g ε = 0 ∧ d ε = 0 := by
 157  have h1 : d ε = - d ε := by
 158    calc d ε = g ε := (hmatch ε).symm
 159      _ = g (-ε) := (hg ε).symm
 160      _ = d (-ε) := hmatch (-ε)
 161      _ = - d ε := hd ε
 162  have h2 : d ε = 0 := by linarith
 163  exact ⟨(hmatch ε).trans h2, h2⟩
 164
 165/-- **THEOREM (parity no-go, linear-response form).** A signed
 166linear-response deficit assignment δ(ε) = c·ε with c ≠ 0 admits no J-ratio
 167realization on any symmetric interval [-a, a] with a > 0: evenness of the
 168J-ratio deficit forces c·a = c·(-a). -/
 169theorem no_jRatio_deficit_linear_response {Λ : Type*} [Fintype Λ]
 170    (s : Λ → Λ → ℝ) (i : Λ) (c a : ℝ) (hc : c ≠ 0) (ha : 0 < a) :
 171    ¬ (∀ ε : ℝ, |ε| ≤ a → jRatioDeficit s ε i = c * ε) := by
 172  intro hmatch
 173  have hpa : jRatioDeficit s a i = c * a :=
 174    hmatch a (le_of_eq (abs_of_pos ha))
 175  have habs : |(-a)| = a := by
 176    rw [abs_neg]
 177    exact abs_of_pos ha
 178  have hna : jRatioDeficit s (-a) i = c * (-a) :=
 179    hmatch (-a) (le_of_eq habs)
 180  rw [jRatioDeficit_even] at hna
 181  have hca : c * a = 0 := by linarith
 182  rcases mul_eq_zero.mp hca with h | h
 183  · exact hc h
 184  · exact absurd h (ne_of_gt ha)
 185
 186/-- **THEOREM (parity no-go, ledger-family form).** For any one-parameter
 187family of recognition ledgers whose costs are J-costs of PARITY-COVARIANT
 188positive ratios (r(-ε) = r(ε)⁻¹), the `RecognitionLedger.deficit` at every
 189cell is even in ε. Scope note: the parity hypothesis is genuine scope, not
 190decoration; ratio families violating it (e.g. r = exp(ε·s + ε²·t) with
 191t ≠ 0) escape this theorem. Exponential strain ratios r = exp(ε·s), the
 192natural first-order substrate deformations, satisfy it. -/
 193theorem ledger_family_deficit_even_of_ratio_parity
 194    {Λ : Type*} [Fintype Λ] [DecidableEq Λ]
 195    (L : ℝ → RecognitionLedger.RecognitionLedger Λ)
 196    (r : ℝ → Λ → Λ → ℝ)
 197    (hpos : ∀ ε i j, 0 < r ε i j)
 198    (hcost : ∀ ε i j, (L ε).cost i j = Cost.Jcost (r ε i j))
 199    (hpar : ∀ ε i j, r (-ε) i j = (r ε i j)⁻¹)
 200    (ε : ℝ) (i : Λ) :
 201    RecognitionLedger.deficit (L (-ε)) i
 202      = RecognitionLedger.deficit (L ε) i := by
 203  unfold RecognitionLedger.deficit
 204  refine Finset.sum_congr rfl fun j _ => ?_
 205  rw [hcost (-ε) i j, hcost ε i j, hpar ε i j]
 206  exact (Cost.Jcost_symm (hpos ε i j)).symm
 207
 208/-- **THEOREM (parity no-go, ledger-family linear-response form).** No
 209one-parameter family of recognition ledgers with parity-covariant J-ratio
 210costs can have a deficit matching a signed linear response c·ε (c ≠ 0) on
 211any symmetric interval. -/
 212theorem no_ledger_family_linear_response
 213    {Λ : Type*} [Fintype Λ] [DecidableEq Λ]
 214    (L : ℝ → RecognitionLedger.RecognitionLedger Λ)
 215    (r : ℝ → Λ → Λ → ℝ)
 216    (hpos : ∀ ε i j, 0 < r ε i j)
 217    (hcost : ∀ ε i j, (L ε).cost i j = Cost.Jcost (r ε i j))
 218    (hpar : ∀ ε i j, r (-ε) i j = (r ε i j)⁻¹)
 219    (i : Λ) (c a : ℝ) (hc : c ≠ 0) (ha : 0 < a) :
 220    ¬ (∀ ε : ℝ, |ε| ≤ a → RecognitionLedger.deficit (L ε) i = c * ε) := by
 221  intro hmatch
 222  have hpa : RecognitionLedger.deficit (L a) i = c * a :=
 223    hmatch a (le_of_eq (abs_of_pos ha))
 224  have habs : |(-a)| = a := by
 225    rw [abs_neg]
 226    exact abs_of_pos ha
 227  have hna : RecognitionLedger.deficit (L (-a)) i = c * (-a) :=
 228    hmatch (-a) (le_of_eq habs)
 229  rw [ledger_family_deficit_even_of_ratio_parity L r hpos hcost hpar a i]
 230    at hna
 231  have hca : c * a = 0 := by linarith
 232  rcases mul_eq_zero.mp hca with h | h
 233  · exact hc h
 234  · exact absurd h (ne_of_gt ha)
 235
 236/-! ### Concrete two-cell instance
 237
 238The minimal substrate exhibiting the parity mechanism: two cells with a
 239single strain σ between them. The induced deficit is cosh(ε·σ) - 1, an
 240explicitly even function of ε with leading term (σ²/2)·ε². -/
 241
 242/-- The two-cell antisymmetric strain: s 0 1 = σ, s 1 0 = -σ, diagonal 0. -/
 243noncomputable def twoCellStrain (σ : ℝ) : Fin 2 → Fin 2 → ℝ :=
 244  fun i j => if i = j then 0 else if i = 0 then σ else -σ
 245
 246/-- **THEOREM (two-cell parity witness).** On the two-cell substrate the
 247J-ratio deficit at cell 0 is exactly cosh(ε·σ) - 1: even in ε, O(ε²) at
 248small ε, and containing no odd (signed linear-response) part. -/
 249theorem twoCell_jRatioDeficit (σ ε : ℝ) :
 250    jRatioDeficit (twoCellStrain σ) ε 0 = Real.cosh (ε * σ) - 1 := by
 251  have h00 : twoCellStrain σ 0 0 = 0 := by norm_num [twoCellStrain]
 252  have h01 : twoCellStrain σ 0 1 = σ := by norm_num [twoCellStrain]
 253  unfold jRatioDeficit jRatioCellCost
 254  rw [Fin.sum_univ_two, h00, h01, mul_zero, Real.exp_zero, Cost.Jcost_unit0,
 255    zero_add, Cost.Jcost_exp_cosh]
 256
 257/-! ## §3. Status: the corrected reading of `bridge_assumed` -/
 258
 259/-- Status flags for the ledger-bridge no-go (documentation record; the
 260mathematics lives in the theorems above, not in these booleans).
 261
 262What is PROVED: (1) sign obstruction, `bridge_forces_nonneg_geometricDeficit`
 263and `no_bridge_matches_negative_deficit_spec` (no bridge for any
 264negative-deficit-in-image specification); (2) parity obstruction,
 265`jRatioDeficit_even` and `no_ledger_family_linear_response` (no signed linear
 266response for parity-covariant J-ratio families). What is GEOMETRIC PREMISE
 267(prose tier): two-sided weak-field Regge classes carry negative image
 268deficits and odd leading response. Under that premise the assumed raw-deficit
 269bridge form is excluded on such classes, and the honest bridge target is the
 270nonnegative curvature-quadratic energy Σ_h A_h · δ_h² built in
 271`SevenGaps.LedgerEnergyBridge` (deliverable B of this lane). -/
 272structure LedgerBridgeNoGoStatus where
 273  /-- PROVED: no bridge exists for any specification with a strictly negative
 274  deficit in the image of the comparison map (sign obstruction). -/
 275  sign_nogo_proved_for_negative_image_specs : Bool
 276  /-- PROVED: parity-covariant J-ratio ledger families admit no signed
 277  linear-response deficit (parity obstruction). -/
 278  parity_nogo_proved_for_parity_covariant_families : Bool
 279  /-- The corrected bridge target is the curvature-quadratic energy
 280  Σ_h A_h · δ_h², not the raw signed deficit Σ_h A_h · δ_h. -/
 281  corrected_target_is_quadratic_energy : Bool
 282
 283/-- The canonical no-go status: all flags true, forced by `rfl`. -/
 284def ledgerBridgeNoGoStatus : LedgerBridgeNoGoStatus where
 285  sign_nogo_proved_for_negative_image_specs := true
 286  parity_nogo_proved_for_parity_covariant_families := true
 287  corrected_target_is_quadratic_energy := true
 288
 289/-- Status flags record (rfl-forced; documentation, not new mathematics). -/
 290theorem ledgerBridgeNoGoStatus_flags :
 291    ledgerBridgeNoGoStatus.sign_nogo_proved_for_negative_image_specs = true ∧
 292    ledgerBridgeNoGoStatus.parity_nogo_proved_for_parity_covariant_families
 293        = true ∧
 294    ledgerBridgeNoGoStatus.corrected_target_is_quadratic_energy = true :=
 295  ⟨rfl, rfl, rfl⟩
 296
 297end SevenGaps
 298end Gravity
 299end IndisputableMonolith
 300