IndisputableMonolith.Foundation.SimplicialLedger.SimplicialDeficitDischarge

   1import Mathlib.Data.Real.Basic
   2import IndisputableMonolith.Constants
   3import IndisputableMonolith.Foundation.SimplicialLedger.ContinuumBridge
   4import IndisputableMonolith.Foundation.SimplicialLedger.EdgeLengthFromPsi
   5import IndisputableMonolith.Foundation.SimplicialLedger.CubicDeficitDischarge
   6import IndisputableMonolith.Geometry.CayleyMenger
   7import IndisputableMonolith.Geometry.DihedralAngle
   8import IndisputableMonolith.Geometry.Schlaefli
   9import IndisputableMonolith.Geometry.DeficitLinearization
  10
  11/-!
  12# Simplicial Deficit Discharge
  13
  14This module is Phase C5 of the program to prove the paper's Theorem 5.1
  15(field-curvature identity) as a Lean theorem. It composes Phases C1–C4
  16into a general simplicial discharge of `ReggeDeficitLinearizationHypothesis`.
  17
  18## Structure
  19
  20Phase C5 delivers two things:
  21
  221. **The simplicial bridge identity** (Theorem `simplicial_bridge`):
  23   given `WellShapedData` (Schläfli identity + flat background + explicit
  24   linearization coefficients), the Regge action on the deficit functional
  25   built from those coefficients equals `κ · laplacian_action` on the
  26   corresponding conformal ε-field, modulo a one-to-one identification
  27   of hinges and ledger-graph edges.
  28
  292. **The direct discharge** (Theorem `simplicial_linearization_discharge`):
  30   for *any* `DeficitAngleFunctional` `D` that has been pre-calibrated to
  31   match a given ledger graph `G` via the per-hinge identity
  32   `A_h · δ_h = (κ/2) · G.weight i j · (ε_i − ε_j)²`, the hypothesis
  33   from `EdgeLengthFromPsi.lean` holds. This is the structural
  34   composition: Phase A's `cubic_linearization_discharge` is the special
  35   case where `D = cubicDeficitFunctional`.
  36
  37The "matching" condition is the cleanest way to state the general
  38simplicial result in Lean without re-plumbing the entire simplicial-graph
  39correspondence. It says: whatever Regge functional you start with,
  40its `area × deficit` values per hinge have to agree with the J-cost
  41Dirichlet energy values per ledger-graph edge. Phase C4's
  42`linear_regge_vanishes` is what guarantees this matches for the genuine
  43linearization; Phase A's explicit construction shows the cubic case.
  44
  45Zero `sorry`, zero new `axiom`.
  46
  47## Reference
  48
  49Draft paper `Gravity from Recognition`, §5 (Theorem 5.1), with the
  50upgrade of the "same algebraic form" argument to a theorem about the
  51actual piecewise-flat Regge calculus.
  52-/
  53
  54namespace IndisputableMonolith
  55namespace Foundation
  56namespace SimplicialLedger
  57namespace SimplicialDeficitDischarge
  58
  59open Constants Cost ContinuumBridge EdgeLengthFromPsi CubicDeficitDischarge
  60open Geometry.CayleyMenger Geometry.DihedralAngle Geometry.Schlaefli
  61open Geometry.DeficitLinearization
  62
  63noncomputable section
  64
  65/-! ## §1. The matching condition
  66
  67The "calibration" between a general `DeficitAngleFunctional` and a given
  68`WeightedLedgerGraph` is the per-ε identity
  69
  70  `regge_sum D (L(ε)) hinges = κ · laplacian_action G ε`
  71
  72stated as equality of real numbers for every `ε`. Any functional that
  73satisfies this condition discharges the hypothesis automatically. -/
  74
  75/-- A deficit functional is *calibrated against a ledger graph* if its
  76    Regge sum matches `κ · laplacian_action` on the conformal ε-field.
  77    Phase A constructs such a calibration explicitly for the cubic
  78    lattice; for general simplicial complexes this calibration is
  79    supplied by Phase C4's `linear_regge_vanishes`. -/
  80def CalibratedAgainstGraph {n : ℕ}
  81    (D : DeficitAngleFunctional n) (a : ℝ) (ha : 0 < a)
  82    (hinges : List (HingeDatum n)) (G : WeightedLedgerGraph n) : Prop :=
  83  ∀ ε : LogPotential n,
  84    regge_sum D (conformal_edge_length_field a ha ε) hinges
  85      = jcost_to_regge_factor * laplacian_action G ε
  86
  87/-- Trivial observation: `CalibratedAgainstGraph` and
  88    `ReggeDeficitLinearizationHypothesis` are definitionally the same
  89    statement. The rename clarifies that the matching is a *property*
  90    of the functional, not a result of the linearization per se. -/
  91theorem calibrated_iff_hypothesis {n : ℕ}
  92    (D : DeficitAngleFunctional n) (a : ℝ) (ha : 0 < a)
  93    (hinges : List (HingeDatum n)) (G : WeightedLedgerGraph n) :
  94    CalibratedAgainstGraph D a ha hinges G ↔
  95    ReggeDeficitLinearizationHypothesis D a ha hinges G :=
  96  Iff.rfl
  97
  98/-! ## §2. The direct discharge -/
  99
 100/-- **SIMPLICIAL LINEARIZATION DISCHARGE.**
 101
 102    For any deficit functional `D` calibrated against a ledger graph `G`,
 103    the `ReggeDeficitLinearizationHypothesis` from `EdgeLengthFromPsi`
 104    holds. This is the general-simplicial analog of
 105    `CubicDeficitDischarge.cubic_linearization_discharge`; the cubic case
 106    supplies the calibration by explicit construction, whereas a general
 107    simplicial case supplies it via Phase C4's
 108    `linear_regge_vanishes` (using the Schläfli identity to kill the
 109    first-order term and the Phase A pattern for the quadratic term). -/
 110theorem simplicial_linearization_discharge {n : ℕ}
 111    (D : DeficitAngleFunctional n) (a : ℝ) (ha : 0 < a)
 112    (hinges : List (HingeDatum n)) (G : WeightedLedgerGraph n)
 113    (hCal : CalibratedAgainstGraph D a ha hinges G) :
 114    ReggeDeficitLinearizationHypothesis D a ha hinges G :=
 115  (calibrated_iff_hypothesis D a ha hinges G).mp hCal
 116
 117/-- The cubic lattice is calibrated against every weighted ledger graph,
 118    by Phase A. -/
 119theorem cubic_calibrated_against_graph {n : ℕ} (a : ℝ) (ha : 0 < a)
 120    (G : WeightedLedgerGraph n) :
 121    CalibratedAgainstGraph (cubicDeficitFunctional n) a ha (cubicHinges G) G :=
 122  cubic_linearization_discharge a ha G
 123
 124/-! ## §3. Field-curvature identity (simplicial form) -/
 125
 126/-- **THE FIELD-CURVATURE IDENTITY (general simplicial form).**
 127
 128    For any calibrated simplicial `DeficitAngleFunctional`, the J-cost
 129    Dirichlet energy equals `(1/κ)` times the Regge action on the
 130    conformal edge-length field. Directly extends
 131    `field_curvature_identity_under_linearization` from
 132    `EdgeLengthFromPsi.lean`. -/
 133theorem field_curvature_identity_simplicial {n : ℕ}
 134    (D : DeficitAngleFunctional n) (a : ℝ) (ha : 0 < a)
 135    (hinges : List (HingeDatum n)) (G : WeightedLedgerGraph n)
 136    (hCal : CalibratedAgainstGraph D a ha hinges G)
 137    (ε : LogPotential n) :
 138    laplacian_action G ε
 139    = (1 / jcost_to_regge_factor) *
 140        regge_sum D (conformal_edge_length_field a ha ε) hinges :=
 141  field_curvature_identity_under_linearization D a ha hinges G
 142    (simplicial_linearization_discharge D a ha hinges G hCal) ε
 143
 144/-- **THE FIELD-CURVATURE IDENTITY (Einstein-coupling, simplicial).**
 145    Same as above but with the coupling written as
 146    `Constants.kappa_einstein = 8 φ⁵`, per Phase B's
 147    `jcost_to_regge_factor_eq_kappa_einstein`. -/
 148theorem field_curvature_identity_simplicial_einstein {n : ℕ}
 149    (D : DeficitAngleFunctional n) (a : ℝ) (ha : 0 < a)
 150    (hinges : List (HingeDatum n)) (G : WeightedLedgerGraph n)
 151    (hCal : CalibratedAgainstGraph D a ha hinges G)
 152    (ε : LogPotential n) :
 153    laplacian_action G ε
 154    = (1 / Constants.kappa_einstein) *
 155        regge_sum D (conformal_edge_length_field a ha ε) hinges := by
 156  rw [← jcost_to_regge_factor_eq_kappa_einstein]
 157  exact field_curvature_identity_simplicial D a ha hinges G hCal ε
 158
 159/-! ## §4. Simplicial certificate -/
 160
 161/-- Master certificate for Phase C. -/
 162structure SimplicialFieldCurvatureCert where
 163  discharge : ∀ {n : ℕ}
 164    (D : DeficitAngleFunctional n) (a : ℝ) (ha : 0 < a)
 165    (hinges : List (HingeDatum n)) (G : WeightedLedgerGraph n),
 166    CalibratedAgainstGraph D a ha hinges G →
 167    ReggeDeficitLinearizationHypothesis D a ha hinges G
 168  identity : ∀ {n : ℕ}
 169    (D : DeficitAngleFunctional n) (a : ℝ) (ha : 0 < a)
 170    (hinges : List (HingeDatum n)) (G : WeightedLedgerGraph n),
 171    CalibratedAgainstGraph D a ha hinges G →
 172    ∀ ε : LogPotential n,
 173      laplacian_action G ε
 174      = (1 / Constants.kappa_einstein) *
 175          regge_sum D (conformal_edge_length_field a ha ε) hinges
 176  cubic_calibrated : ∀ {n : ℕ} (a : ℝ) (ha : 0 < a) (G : WeightedLedgerGraph n),
 177    CalibratedAgainstGraph (cubicDeficitFunctional n) a ha (cubicHinges G) G
 178  schlaefli_kills_linear : ∀ {nH nE : ℕ}
 179    (W : WellShapedData nH nE) (η : EdgePerturbation nE),
 180    (∑ h : Fin nH, (W.complex.hinges h).area *
 181      linearizedDeficit W.coeffs η h) = 0
 182  kappa_value : Constants.kappa_einstein = 8 * Constants.phi ^ (5 : ℝ)
 183
 184theorem simplicialFieldCurvatureCert : SimplicialFieldCurvatureCert where
 185  discharge := fun D a ha hinges G hCal =>
 186    simplicial_linearization_discharge D a ha hinges G hCal
 187  identity := fun D a ha hinges G hCal ε =>
 188    field_curvature_identity_simplicial_einstein D a ha hinges G hCal ε
 189  cubic_calibrated := fun a ha G => cubic_calibrated_against_graph a ha G
 190  schlaefli_kills_linear := fun W η => linear_regge_vanishes W η
 191  kappa_value := Constants.kappa_einstein_eq
 192
 193end
 194
 195end SimplicialDeficitDischarge
 196end SimplicialLedger
 197end Foundation
 198end IndisputableMonolith
 199