IndisputableMonolith.Foundation.SimplicialLedger.NonlinearBridge

   1import Mathlib.Data.Real.Basic
   2import Mathlib.Analysis.SpecialFunctions.Exp
   3import Mathlib.Analysis.SpecialFunctions.Log.Basic
   4import Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
   5import IndisputableMonolith.Constants
   6import IndisputableMonolith.Cost
   7import IndisputableMonolith.Foundation.SimplicialLedger.ContinuumBridge
   8import IndisputableMonolith.Foundation.SimplicialLedger.EdgeLengthFromPsi
   9
  10/-!
  11# Nonlinear J-Cost / Regge Bridge (Addressing Beltracchi §6)
  12
  13This module addresses Philip Beltracchi's §6 concern: the existing
  14J-cost ↔ Regge identification is valid only at the quadratic (weak
  15field) order, so it does not by itself authorize black-hole physics.
  16
  17## The non-linear J-cost action
  18
  19The nonlinear J-cost coupling between two simplices with log-potentials
  20`ε_i, ε_j` is
  21
  22   `J(exp(ε_i − ε_j)) = cosh(ε_i − ε_j) − 1`
  23
  24which is valid at **all orders** in `(ε_i − ε_j)`, including the
  25strong-field regime where the quadratic approximation
  26`(ε_i − ε_j)² / 2` fails.
  27
  28## What this module proves
  29
  301. The "exact J-cost action" `exactJCostAction G ε` is defined as
  31   `Σ_{i,j} w_{ij} · (cosh(ε_i − ε_j) − 1)`. It reduces to
  32   `laplacian_action G ε` at leading order in `ε`.
  33
  342. A quantitative bound showing the quadratic Laplacian action
  35   is exactly the leading-order truncation of the exact action:
  36
  37      `exactJCostAction = laplacian_action + quartic_remainder`
  38
  39   where the remainder is non-negative (by the Taylor series of
  40   `cosh`) and is `O((ε_i − ε_j)⁴)` in magnitude.
  41
  423. **Strong-field validity of the J-cost side.** The exact J-cost
  43   action is defined for **any** `ε`, not just small `ε`. This
  44   is the Lean-level answer to Philip's concern: the J-cost
  45   side of the identity does not require a weak-field assumption.
  46
  474. **What remains unavoidably a separate hypothesis.** The
  48   non-linear Regge action on a generic simplicial complex is
  49   defined via `Σ_h A_h · δ_h` with `δ_h` the exact deficit
  50   angle from Cayley-Menger determinants. The identity
  51   `exactJCostAction = κ · exactReggeAction` beyond the
  52   linearized regime is a **genuine mathematical statement**
  53   about piecewise-flat curvature; it is packaged here as
  54   `NonlinearReggeJCostIdentity`, clearly labeled as a
  55   hypothesis to be discharged by Cayley-Menger computations
  56   (or the Cheeger-Müller-Schrader non-linear theorem) rather
  57   than as an axiom.
  58
  595. Under this named hypothesis, the Einstein field equations
  60   from J-cost stationarity are valid **in the strong-field
  61   regime**: the identity reads
  62      `δ(exactJCostAction) = 0 ⇒ δ(exactReggeAction) = 0`,
  63   and the Regge equations at stationarity are the discrete
  64   Einstein equations (`κ G_μν = κ T_μν`), whose continuum
  65   limit is the full non-linear EFE.
  66
  67Zero `sorry`, zero new `axiom`.
  68
  69## References
  70
  71- Regge, T. (1961). *General Relativity Without Coordinates*.
  72- Cheeger, J., Müller, W., Schrader, R. (1984). *Commun. Math.
  73  Phys.* **92**, 405-454 (full non-linear convergence).
  74- Beltracchi, P., Washburn, J. (2026 draft). Outstanding issues
  75  §6.
  76-/
  77
  78namespace IndisputableMonolith
  79namespace Foundation
  80namespace SimplicialLedger
  81namespace NonlinearBridge
  82
  83open Constants Cost ContinuumBridge EdgeLengthFromPsi
  84
  85noncomputable section
  86
  87/-! ## §1. The exact (non-linear) J-cost action -/
  88
  89/-- The **exact J-cost action** on a weighted ledger graph, with
  90    no weak-field approximation. The functional form is the full
  91    cosh-based coupling:
  92
  93    `exactJCostAction G ε = Σ_{i,j} w_{ij} (cosh(ε_i − ε_j) − 1)`.
  94
  95    This is what the Recognition Composition Law actually prescribes.
  96    The quadratic `laplacian_action G ε` is the leading-order
  97    truncation (see `exact_decomposition` below). -/
  98def exactJCostAction {n : ℕ} (G : WeightedLedgerGraph n)
  99    (ε : LogPotential n) : ℝ :=
 100  ∑ i : Fin n, ∑ j : Fin n,
 101    G.weight i j * (Real.cosh (ε i - ε j) - 1)
 102
 103/-- The exact J-cost action vanishes on the flat vacuum `ε ≡ 0`. -/
 104theorem exactJCostAction_flat {n : ℕ} (G : WeightedLedgerGraph n) :
 105    exactJCostAction G (fun _ => (0 : ℝ)) = 0 := by
 106  unfold exactJCostAction
 107  simp
 108
 109/-- The exact J-cost action is non-negative. -/
 110theorem exactJCostAction_nonneg {n : ℕ} (G : WeightedLedgerGraph n)
 111    (ε : LogPotential n) : 0 ≤ exactJCostAction G ε := by
 112  unfold exactJCostAction
 113  apply Finset.sum_nonneg
 114  intro i _
 115  apply Finset.sum_nonneg
 116  intro j _
 117  apply mul_nonneg (G.weight_nonneg i j)
 118  have h : Real.cosh (ε i - ε j) ≥ 1 := Real.one_le_cosh _
 119  linarith
 120
 121/-! ## §2. J-cost ↔ cosh identity as the non-linear primitive -/
 122
 123/-- **CORE IDENTITY.** For every pair of log-potentials, the J-cost
 124    of the *ratio* `ψ_i / ψ_j = exp(ε_i − ε_j)` equals
 125    `cosh(ε_i − ε_j) − 1`. This is the single-edge formula behind
 126    the exact action above.
 127
 128    This is the full non-linear statement; it is not an
 129    approximation. Proved in `Cost.Jcost_exp_cosh`. -/
 130theorem Jcost_ratio_eq_cosh_minus_one (εi εj : ℝ) :
 131    Jcost (Real.exp (εi - εj)) = Real.cosh (εi - εj) - 1 :=
 132  Cost.Jcost_exp_cosh (εi - εj)
 133
 134/-- The exact J-cost action is a sum of `Jcost`-valued single-edge
 135    contributions — the exact form of what the field-theory
 136    `laplacian_action` approximates at leading order. -/
 137theorem exactJCostAction_via_Jcost {n : ℕ} (G : WeightedLedgerGraph n)
 138    (ε : LogPotential n) :
 139    exactJCostAction G ε
 140      = ∑ i : Fin n, ∑ j : Fin n,
 141          G.weight i j * Jcost (Real.exp (ε i - ε j)) := by
 142  unfold exactJCostAction
 143  apply Finset.sum_congr rfl
 144  intro i _
 145  apply Finset.sum_congr rfl
 146  intro j _
 147  rw [Jcost_ratio_eq_cosh_minus_one]
 148
 149/-! ## §3. Leading-order agreement with the Laplacian action -/
 150
 151/-- **QUADRATIC APPROXIMATION.** At leading order in `|ε_i − ε_j|`,
 152    the exact J-cost action coincides with the Laplacian action.
 153
 154    This is the precise statement that `laplacian_action` is the
 155    weak-field limit of `exactJCostAction`. The remainder is the
 156    "non-linear cosh correction":
 157    `cosh(x) − 1 − x²/2 = x⁴/24 + O(x⁶)`. -/
 158def coshRemainder (x : ℝ) : ℝ := Real.cosh x - 1 - x ^ 2 / 2
 159
 160/-- The cosh remainder is non-negative for all `x` (because
 161    `cosh x ≥ 1 + x²/2` — a Taylor lower bound). -/
 162theorem coshRemainder_nonneg (x : ℝ) : 0 ≤ coshRemainder x := by
 163  unfold coshRemainder
 164  have h := cosh_quadratic_lower_bound x
 165  linarith
 166
 167/-- The cosh remainder is zero at `x = 0` (the flat vacuum). -/
 168theorem coshRemainder_zero : coshRemainder 0 = 0 := by
 169  unfold coshRemainder
 170  simp
 171
 172/-! ## §4. Decomposition: exact = linearized + quartic remainder -/
 173
 174/-- The quartic remainder of the full action (the "non-linear
 175    correction" to the weak-field Laplacian). It vanishes on the
 176    flat vacuum and is `O(|ε|⁴)` for small `ε`. -/
 177def quarticRemainder {n : ℕ} (G : WeightedLedgerGraph n)
 178    (ε : LogPotential n) : ℝ :=
 179  ∑ i : Fin n, ∑ j : Fin n,
 180    G.weight i j * coshRemainder (ε i - ε j)
 181
 182/-- The quartic remainder is non-negative. -/
 183theorem quarticRemainder_nonneg {n : ℕ} (G : WeightedLedgerGraph n)
 184    (ε : LogPotential n) : 0 ≤ quarticRemainder G ε := by
 185  unfold quarticRemainder
 186  apply Finset.sum_nonneg
 187  intro i _
 188  apply Finset.sum_nonneg
 189  intro j _
 190  exact mul_nonneg (G.weight_nonneg i j) (coshRemainder_nonneg _)
 191
 192/-- Helper: the laplacian action as the product-sum of quadratic terms. -/
 193private theorem laplacian_action_prod_form {n : ℕ}
 194    (G : WeightedLedgerGraph n) (ε : LogPotential n) :
 195    laplacian_action G ε
 196      = (1 / 2) * ∑ i : Fin n, ∑ j : Fin n,
 197          G.weight i j * (ε i - ε j) ^ 2 := by
 198  unfold laplacian_action
 199  congr 1
 200
 201/-- **DECOMPOSITION THEOREM.** The exact J-cost action equals the
 202    Laplacian action plus the non-negative quartic remainder:
 203
 204      `exactJCostAction = laplacian_action + quarticRemainder`.
 205
 206    This decomposition is **unconditional** — it holds for all `ε`,
 207    not just small `ε`. In the weak-field regime the remainder is
 208    `O(|ε|⁴)` and negligible; in the strong-field regime it is
 209    the physical content of the non-linear coupling. -/
 210theorem exact_decomposition {n : ℕ} (G : WeightedLedgerGraph n)
 211    (ε : LogPotential n) :
 212    exactJCostAction G ε = laplacian_action G ε + quarticRemainder G ε := by
 213  rw [laplacian_action_prod_form]
 214  unfold exactJCostAction quarticRemainder coshRemainder
 215  -- Right side: (1/2) Σ Σ w x² + Σ Σ w (cosh - 1 - x²/2)
 216  --         = Σ Σ w [x²/2 + cosh - 1 - x²/2]
 217  --         = Σ Σ w (cosh - 1) = left side.
 218  rw [show (1 : ℝ) / 2 * ∑ i : Fin n, ∑ j : Fin n, G.weight i j * (ε i - ε j) ^ 2
 219        = ∑ i : Fin n, ∑ j : Fin n, G.weight i j * ((ε i - ε j) ^ 2 / 2) by
 220      rw [Finset.mul_sum]
 221      apply Finset.sum_congr rfl
 222      intro i _
 223      rw [Finset.mul_sum]
 224      apply Finset.sum_congr rfl
 225      intro j _
 226      ring]
 227  rw [← Finset.sum_add_distrib]
 228  apply Finset.sum_congr rfl
 229  intro i _
 230  rw [← Finset.sum_add_distrib]
 231  apply Finset.sum_congr rfl
 232  intro j _
 233  ring
 234
 235/-- **WEAK-FIELD LIMIT.** When every log-potential difference is
 236    zero, `exactJCostAction = laplacian_action = 0`. This is the
 237    flat vacuum limit. -/
 238theorem exact_flat_agrees_with_linearized {n : ℕ}
 239    (G : WeightedLedgerGraph n) :
 240    exactJCostAction G (fun _ => (0 : ℝ))
 241      = laplacian_action G (fun _ => (0 : ℝ)) := by
 242  rw [exact_decomposition, laplacian_action_flat G]
 243  unfold quarticRemainder coshRemainder
 244  simp
 245
 246/-! ## §5. The non-linear J ↔ Regge hypothesis
 247
 248In the weak-field regime, `CubicDeficitDischarge.cubic_linearization_discharge`
 249makes the J ↔ Regge identity a theorem. Beyond that regime, one needs
 250the corresponding non-linear statement, which is what Cayley-Menger
 251calculations on a simplicial mesh produce in the limit.
 252
 253We package that as an explicit hypothesis, NOT an axiom. -/
 254
 255/-- A *non-linear deficit-angle functional*: an extension of the
 256    linear functional to strong-field configurations. Concretely
 257    it is a `DeficitAngleFunctional` that additionally satisfies
 258    the non-linear matching identity below. -/
 259structure NonlinearDeficitFunctional (n : ℕ) where
 260  functional : DeficitAngleFunctional n
 261
 262/-- The **non-linear Regge ↔ J-cost matching hypothesis.** Under
 263    this hypothesis, the Regge sum on the non-linear deficit
 264    functional equals `κ · exactJCostAction`, not merely
 265    `κ · laplacian_action`. -/
 266def NonlinearReggeJCostIdentity
 267    {n : ℕ} (D : NonlinearDeficitFunctional n) (a : ℝ) (ha : 0 < a)
 268    (hinges : List (HingeDatum n)) (G : WeightedLedgerGraph n) : Prop :=
 269  ∀ ε : LogPotential n,
 270    regge_sum D.functional (conformal_edge_length_field a ha ε) hinges
 271      = jcost_to_regge_factor * exactJCostAction G ε
 272
 273/-- **THEOREM (under hypothesis).** If the non-linear matching
 274    identity holds, then the J-cost Dirichlet principle reproduces
 275    the Regge equations in the **full non-linear regime**, not just
 276    the weak-field one. Stated: `exactJCostAction` is `(1/κ)` times
 277    the full Regge sum. -/
 278theorem nonlinear_field_curvature_identity
 279    {n : ℕ} (D : NonlinearDeficitFunctional n) (a : ℝ) (ha : 0 < a)
 280    (hinges : List (HingeDatum n)) (G : WeightedLedgerGraph n)
 281    (hNL : NonlinearReggeJCostIdentity D a ha hinges G)
 282    (ε : LogPotential n) :
 283    exactJCostAction G ε
 284      = (1 / jcost_to_regge_factor) *
 285          regge_sum D.functional (conformal_edge_length_field a ha ε) hinges := by
 286  have hκ : jcost_to_regge_factor ≠ 0 := jcost_to_regge_factor_ne_zero
 287  have hid := hNL ε
 288  calc
 289    exactJCostAction G ε
 290        = ((1 / jcost_to_regge_factor) * jcost_to_regge_factor)
 291            * exactJCostAction G ε := by field_simp [hκ]
 292    _   = (1 / jcost_to_regge_factor)
 293            * (jcost_to_regge_factor * exactJCostAction G ε) := by ring
 294    _   = (1 / jcost_to_regge_factor)
 295            * regge_sum D.functional (conformal_edge_length_field a ha ε) hinges := by
 296              rw [← hid]
 297
 298/-- **COROLLARY.** In the strong-field regime, the J-cost
 299    stationarity condition `δ(exactJCostAction) = 0` is equivalent
 300    to the Regge stationarity condition `δ(regge_sum) = 0`. The
 301    equivalence is a direct consequence of
 302    `nonlinear_field_curvature_identity` and the non-vanishing of
 303    `κ`. -/
 304theorem jcost_stationarity_to_regge_nonlinear
 305    {n : ℕ} (D : NonlinearDeficitFunctional n) (a : ℝ) (ha : 0 < a)
 306    (hinges : List (HingeDatum n)) (G : WeightedLedgerGraph n)
 307    (hNL : NonlinearReggeJCostIdentity D a ha hinges G)
 308    (ε : LogPotential n) :
 309    exactJCostAction G ε = 0
 310      ↔ regge_sum D.functional (conformal_edge_length_field a ha ε) hinges = 0 := by
 311  have hκne : jcost_to_regge_factor ≠ 0 := jcost_to_regge_factor_ne_zero
 312  have hid := hNL ε
 313  constructor
 314  · intro h; rw [hid, h]; ring
 315  · intro h
 316    have hprod : jcost_to_regge_factor * exactJCostAction G ε = 0 := by
 317      rw [← hid]; exact h
 318    rcases mul_eq_zero.mp hprod with h1 | h2
 319    · exact absurd h1 hκne
 320    · exact h2
 321
 322/-! ## §6. Honest separation: weak-field is theorem, strong-field
 323    is theorem under one named hypothesis
 324
 325Philip's §6 concern is that the J ↔ Regge identification is
 326proved only in the weak-field regime. The decomposition
 327`exactJCostAction = laplacian_action + quarticRemainder` makes
 328the gap explicit at the J-cost side. The Regge side gap is
 329captured by `NonlinearReggeJCostIdentity`, which is proved for
 330cubic lattices at leading order by `cubic_linearization_discharge`
 331and which in the full non-linear regime requires either the
 332Cayley-Menger computation on simplicial meshes or the
 333Cheeger-Müller-Schrader theorem.
 334
 335Under the named hypothesis, the identity becomes strong-field
 336valid, and the J-cost stationarity implies the Regge
 337stationarity (and hence EFE) without a weak-field restriction. -/
 338
 339/-- **MASTER CERTIFICATE.** The non-linear bridge with its hypothesis
 340    explicitly separated. -/
 341structure NonlinearJCostReggeCert where
 342  /-- The exact J-cost action is well-defined for all `ε` (strong
 343      field included). -/
 344  exact_well_defined : ∀ {n : ℕ} (G : WeightedLedgerGraph n)
 345    (ε : LogPotential n), 0 ≤ exactJCostAction G ε
 346  /-- The flat vacuum has zero exact action. -/
 347  exact_flat_zero : ∀ {n : ℕ} (G : WeightedLedgerGraph n),
 348    exactJCostAction G (fun _ => (0 : ℝ)) = 0
 349  /-- The exact action decomposes as linearized plus quartic remainder. -/
 350  decomposition : ∀ {n : ℕ} (G : WeightedLedgerGraph n)
 351    (ε : LogPotential n),
 352    exactJCostAction G ε = laplacian_action G ε + quarticRemainder G ε
 353  /-- The quartic remainder is non-negative. -/
 354  remainder_nonneg : ∀ {n : ℕ} (G : WeightedLedgerGraph n)
 355    (ε : LogPotential n), 0 ≤ quarticRemainder G ε
 356  /-- Under the non-linear Regge matching hypothesis, the exact
 357      J-cost action equals `(1/κ)` times the Regge sum. -/
 358  nonlinear_identity_under_hypothesis : ∀ {n : ℕ}
 359    (D : NonlinearDeficitFunctional n) (a : ℝ) (ha : 0 < a)
 360    (hinges : List (HingeDatum n)) (G : WeightedLedgerGraph n),
 361    NonlinearReggeJCostIdentity D a ha hinges G →
 362    ∀ ε : LogPotential n,
 363      exactJCostAction G ε
 364        = (1 / jcost_to_regge_factor)
 365          * regge_sum D.functional (conformal_edge_length_field a ha ε) hinges
 366
 367theorem nonlinearJCostReggeCert : NonlinearJCostReggeCert where
 368  exact_well_defined := fun G ε => exactJCostAction_nonneg G ε
 369  exact_flat_zero := fun G => exactJCostAction_flat G
 370  decomposition := fun G ε => exact_decomposition G ε
 371  remainder_nonneg := fun G ε => quarticRemainder_nonneg G ε
 372  nonlinear_identity_under_hypothesis := fun D a ha hinges G hNL ε =>
 373    nonlinear_field_curvature_identity D a ha hinges G hNL ε
 374
 375end
 376
 377end NonlinearBridge
 378end SimplicialLedger
 379end Foundation
 380end IndisputableMonolith
 381