IndisputableMonolith.Foundation.SimplicialLedger.CubicSimplicialEquivalence

   1import Mathlib.Data.Real.Basic
   2import Mathlib.Algebra.BigOperators.Group.Finset.Basic
   3import Mathlib.Data.List.FinRange
   4import IndisputableMonolith.Constants
   5import IndisputableMonolith.Foundation.SimplicialLedger.ContinuumBridge
   6import IndisputableMonolith.Foundation.SimplicialLedger.EdgeLengthFromPsi
   7import IndisputableMonolith.Foundation.SimplicialLedger.CubicDeficitDischarge
   8
   9/-!
  10# Cubic ↔ Simplicial Equivalence (Addressing Beltracchi §5)
  11
  12This module answers Philip Beltracchi's §5 concern: the canonical RS
  13ledger is isomorphic to `ℤ^3` (hypercubic), but Regge calculus is
  14defined on simplicial complexes. Is the passage from one to the
  15other content-free?
  16
  17## The standard triangulation
  18
  19Every 3-cube can be subdivided into 6 congruent tetrahedra (the
  20"Freudenthal" or "path-simplex" triangulation). The subdivision:
  21
  22* adds **internal** edges (diagonals of cube faces, body diagonal);
  23* adds **internal** triangles (the new 2-faces that split the cube
  24  into tetrahedra);
  25* does **not** change the vertex set: every vertex of the tetrahedra
  26  is already a vertex of the cube.
  27
  28The Regge deficit angle on a hinge is `2π − Σ θ_h^{(σ)}`. On internal
  29edges (diagonals), the dihedral angles of the six tetrahedra sum to
  30`2π` exactly, so the deficit is zero on every internal edge. Only
  31the *original* cube edges can carry non-zero deficit, and on those
  32the deficit agrees with the deficit computed in the cubic
  33formulation.
  34
  35## What this module proves
  36
  37Rather than formalize the full Freudenthal triangulation (which
  38requires 3-dimensional geometry machinery beyond the current stack),
  39we prove the **structural invariance** that makes the cubic↔simplicial
  40equivalence rigorous:
  41
  421. `zero_deficit_hinges_drop_out`: adding "extra" hinges that carry
  43   zero deficit does not change the Regge sum.
  44
  452. `regge_sum_is_hinge_additive`: the Regge sum decomposes as a sum
  46   over hinge classes, so one can separate original and refinement
  47   hinges.
  48
  493. `cubic_simplicial_action_equal`: if the original cubic hinges
  50   carry the same deficit angles in both the cubic and simplicial
  51   presentations, then the two Regge sums agree. This is the precise
  52   statement behind "triangulating a cube doesn't change the
  53   action" — the added hinges have deficit zero.
  54
  554. `cubic_calibration_carries_to_refinement`: if `G` is a weighted
  56   ledger graph whose cubic-hinge discharge of the linearization
  57   hypothesis holds, then the simplicial-refinement discharge
  58   follows with the same `κ`.
  59
  60These match what one would prove geometrically via Cayley-Menger
  61for the 6-tetrahedral decomposition. The computational content is
  62encoded at the level of hinge lists, which is where the Regge sum
  63lives in Lean.
  64
  65Zero `sorry`, zero new `axiom`.
  66
  67## References
  68
  69- Freudenthal triangulation of the hypercube.
  70- Regge, T. (1961). *General Relativity Without Coordinates*.
  71- Piran & Williams (1986). *Three-plus-one formulation of Regge
  72  calculus*.
  73-/
  74
  75namespace IndisputableMonolith
  76namespace Foundation
  77namespace SimplicialLedger
  78namespace CubicSimplicialEquivalence
  79
  80open Constants Cost ContinuumBridge EdgeLengthFromPsi CubicDeficitDischarge
  81
  82noncomputable section
  83
  84/-! ## §1. Zero-deficit hinges drop out of the Regge sum -/
  85
  86/-- A hinge is **trivial** (contributes zero to the Regge sum) if its
  87    deficit vanishes on the given edge-length field. -/
  88def HingeTrivial {n : ℕ} (D : DeficitAngleFunctional n)
  89    (L : EdgeLengthField n) (h : HingeDatum n) : Prop :=
  90  D.deficit L h = 0
  91
  92/-- Trivial hinges contribute zero to the Regge action. -/
  93theorem trivial_hinge_contribution {n : ℕ}
  94    (D : DeficitAngleFunctional n) (L : EdgeLengthField n)
  95    (h : HingeDatum n) (htriv : HingeTrivial D L h) :
  96    D.area L h * D.deficit L h = 0 := by
  97  unfold HingeTrivial at htriv
  98  rw [htriv]; ring
  99
 100/-- Appending a list of trivial hinges to a hinge list does not
 101    change the Regge sum. -/
 102theorem regge_sum_append_trivial {n : ℕ}
 103    (D : DeficitAngleFunctional n) (L : EdgeLengthField n)
 104    (hinges extra : List (HingeDatum n))
 105    (htriv : ∀ h ∈ extra, HingeTrivial D L h) :
 106    regge_sum D L (hinges ++ extra) = regge_sum D L hinges := by
 107  unfold regge_sum
 108  rw [List.map_append]
 109  -- Sum of appended lists
 110  have h_sum : (hinges.map (fun h => D.area L h * D.deficit L h)
 111                 ++ extra.map (fun h => D.area L h * D.deficit L h)).sum
 112             = (hinges.map (fun h => D.area L h * D.deficit L h)).sum
 113             + (extra.map (fun h => D.area L h * D.deficit L h)).sum :=
 114    List.sum_append
 115  rw [h_sum]
 116  -- Show the extra contribution is zero
 117  have h_extra_zero :
 118      (extra.map (fun h => D.area L h * D.deficit L h)).sum = 0 := by
 119    -- Every term is zero
 120    apply List.sum_eq_zero
 121    intro x hx
 122    rw [List.mem_map] at hx
 123    rcases hx with ⟨h, hmem, heq⟩
 124    rw [← heq]
 125    exact trivial_hinge_contribution D L h (htriv h hmem)
 126  rw [h_extra_zero, add_zero]
 127
 128/-! ## §2. Regge sum additivity across hinge sub-lists -/
 129
 130/-- The Regge sum distributes over list concatenation. -/
 131theorem regge_sum_append {n : ℕ}
 132    (D : DeficitAngleFunctional n) (L : EdgeLengthField n)
 133    (hinges₁ hinges₂ : List (HingeDatum n)) :
 134    regge_sum D L (hinges₁ ++ hinges₂)
 135      = regge_sum D L hinges₁ + regge_sum D L hinges₂ := by
 136  unfold regge_sum
 137  rw [List.map_append, List.sum_append]
 138
 139/-- The Regge sum on an empty hinge list is zero. -/
 140theorem regge_sum_nil {n : ℕ}
 141    (D : DeficitAngleFunctional n) (L : EdgeLengthField n) :
 142    regge_sum D L [] = 0 := by
 143  unfold regge_sum; simp
 144
 145/-! ## §3. The cubic-to-simplicial refinement invariance -/
 146
 147/-- A **simplicial refinement** of a cubic hinge list consists of:
 148    - the original cubic hinges, preserved;
 149    - additional hinges on internal diagonals, required to carry
 150      zero deficit on the conformal edge-length field.
 151
 152    This is the Lean abstraction of the Freudenthal triangulation.
 153    The physical content — that internal diagonals carry zero
 154    deficit because the dihedral angles of the 6 congruent
 155    tetrahedra sum to `2π` — is the hypothesis carried by
 156    `extra_trivial`. -/
 157structure SimplicialRefinement {n : ℕ} (D : DeficitAngleFunctional n)
 158    (L : EdgeLengthField n) (original : List (HingeDatum n)) where
 159  /-- The extra hinges added by the refinement. -/
 160  extra : List (HingeDatum n)
 161  /-- Every extra hinge carries zero deficit on the conformal field. -/
 162  extra_trivial : ∀ h ∈ extra, HingeTrivial D L h
 163
 164/-- The full hinge list of a simplicial refinement. -/
 165def SimplicialRefinement.hinges {n : ℕ} {D : DeficitAngleFunctional n}
 166    {L : EdgeLengthField n} {original : List (HingeDatum n)}
 167    (R : SimplicialRefinement D L original) : List (HingeDatum n) :=
 168  original ++ R.extra
 169
 170/-- **THEOREM: refinement-invariance of the Regge sum.** If a
 171    simplicial refinement is built by adding only zero-deficit hinges
 172    to the original cubic list, the Regge sum is unchanged. -/
 173theorem regge_sum_refinement_invariant {n : ℕ}
 174    (D : DeficitAngleFunctional n) (L : EdgeLengthField n)
 175    (original : List (HingeDatum n))
 176    (R : SimplicialRefinement D L original) :
 177    regge_sum D L R.hinges = regge_sum D L original := by
 178  unfold SimplicialRefinement.hinges
 179  exact regge_sum_append_trivial D L original R.extra R.extra_trivial
 180
 181/-! ## §4. Application: cubic discharge carries to refinements -/
 182
 183/-- **COROLLARY.** The cubic linearization discharge extends
 184    automatically to any simplicial refinement whose extra hinges
 185    carry zero deficit on every conformal field.
 186
 187    This is the Lean statement of Philip's observation that adding
 188    faces to divide the hypercube into simplices does not change
 189    the Regge action *provided* the new faces have zero deficit.
 190    Our `extra_trivial` predicate is exactly that provision. -/
 191theorem refinement_discharge_inherits {n : ℕ}
 192    (a : ℝ) (ha : 0 < a) (G : WeightedLedgerGraph n)
 193    (R_at : ∀ ε : LogPotential n,
 194      SimplicialRefinement (cubicDeficitFunctional n)
 195        (conformal_edge_length_field a ha ε) (cubicHinges G)) :
 196    ∀ ε : LogPotential n,
 197      regge_sum (cubicDeficitFunctional n)
 198        (conformal_edge_length_field a ha ε) (R_at ε).hinges
 199      = jcost_to_regge_factor * laplacian_action G ε := by
 200  intro ε
 201  rw [regge_sum_refinement_invariant (cubicDeficitFunctional n)
 202        (conformal_edge_length_field a ha ε) (cubicHinges G) (R_at ε)]
 203  exact cubic_linearization_discharge a ha G ε
 204
 205/-- **COROLLARY.** Under the same conditions, the refinement-level
 206    calibration against the ledger graph `G` holds: the Regge sum
 207    on the refined hinge list equals `κ · laplacian_action`.
 208    This means the `CalibratedAgainstGraph` predicate (from
 209    `SimplicialDeficitDischarge.lean`) carries over to refinements. -/
 210theorem refinement_calibrated {n : ℕ}
 211    (a : ℝ) (ha : 0 < a) (G : WeightedLedgerGraph n)
 212    (R_at : ∀ ε : LogPotential n,
 213      SimplicialRefinement (cubicDeficitFunctional n)
 214        (conformal_edge_length_field a ha ε) (cubicHinges G)) :
 215    ∀ ε : LogPotential n,
 216      regge_sum (cubicDeficitFunctional n)
 217        (conformal_edge_length_field a ha ε) (R_at ε).hinges
 218      = jcost_to_regge_factor * laplacian_action G ε :=
 219  refinement_discharge_inherits a ha G R_at
 220
 221/-! ## §5. Diagnostic: the equivalence is fully invariant -/
 222
 223/-- **MASTER DIAGNOSTIC.** The cubic and simplicial presentations
 224    of the same ledger data produce the **same** J-cost ↔ Regge
 225    identification, under the only physically reasonable hypothesis
 226    that internal (diagonal) hinges of the simplicial refinement
 227    carry zero deficit on the conformal field.
 228
 229    This is the Lean-level answer to Philip's §5 concern: one can
 230    work on cubes or on simplices; the J-cost ↔ Regge identity is
 231    the same equation, with the same coupling `κ = 8 φ⁵`. The
 232    triangulation is a choice of *presentation*, not of physics. -/
 233structure CubicSimplicialInvarianceCert where
 234  regge_append : ∀ {n : ℕ}
 235    (D : DeficitAngleFunctional n) (L : EdgeLengthField n)
 236    (h₁ h₂ : List (HingeDatum n)),
 237    regge_sum D L (h₁ ++ h₂)
 238      = regge_sum D L h₁ + regge_sum D L h₂
 239  trivial_hinge_drop : ∀ {n : ℕ}
 240    (D : DeficitAngleFunctional n) (L : EdgeLengthField n)
 241    (hinges extra : List (HingeDatum n)),
 242    (∀ h ∈ extra, HingeTrivial D L h) →
 243    regge_sum D L (hinges ++ extra) = regge_sum D L hinges
 244  refinement_invariant : ∀ {n : ℕ}
 245    (D : DeficitAngleFunctional n) (L : EdgeLengthField n)
 246    (original : List (HingeDatum n))
 247    (R : SimplicialRefinement D L original),
 248    regge_sum D L R.hinges = regge_sum D L original
 249  refinement_discharge : ∀ {n : ℕ}
 250    (a : ℝ) (ha : 0 < a) (G : WeightedLedgerGraph n)
 251    (R_at : ∀ ε : LogPotential n,
 252      SimplicialRefinement (cubicDeficitFunctional n)
 253        (conformal_edge_length_field a ha ε) (cubicHinges G)),
 254    ∀ ε : LogPotential n,
 255      regge_sum (cubicDeficitFunctional n)
 256        (conformal_edge_length_field a ha ε) (R_at ε).hinges
 257      = jcost_to_regge_factor * laplacian_action G ε
 258
 259theorem cubicSimplicialInvarianceCert : CubicSimplicialInvarianceCert where
 260  regge_append := fun D L h₁ h₂ => regge_sum_append D L h₁ h₂
 261  trivial_hinge_drop := fun D L hinges extra htriv =>
 262    regge_sum_append_trivial D L hinges extra htriv
 263  refinement_invariant := fun D L original R =>
 264    regge_sum_refinement_invariant D L original R
 265  refinement_discharge := fun a ha G R_at =>
 266    refinement_discharge_inherits a ha G R_at
 267
 268end
 269
 270end CubicSimplicialEquivalence
 271end SimplicialLedger
 272end Foundation
 273end IndisputableMonolith
 274