IndisputableMonolith.Foundation.SimplicialLedger.CubicDeficitDischarge

   1import Mathlib.Data.Real.Basic
   2import Mathlib.Analysis.SpecialFunctions.Exp
   3import Mathlib.Analysis.SpecialFunctions.Log.Basic
   4import Mathlib.Data.List.FinRange
   5import Mathlib.Algebra.BigOperators.Group.Finset.Basic
   6import IndisputableMonolith.Constants
   7import IndisputableMonolith.Foundation.SimplicialLedger.ContinuumBridge
   8import IndisputableMonolith.Foundation.SimplicialLedger.EdgeLengthFromPsi
   9
  10/-!
  11# Cubic Lattice Discharge of the Regge Deficit Linearization Hypothesis
  12
  13This module discharges `ReggeDeficitLinearizationHypothesis` from
  14`EdgeLengthFromPsi.lean` unconditionally for the RS-canonical cubic lattice
  15presentation. It is Phase A of the four-phase program to promote the draft
  16paper's Theorem 5.1 (field-curvature identity) from a pattern-matching
  17argument to a genuine Lean theorem.
  18
  19## What this supplies
  20
  21Given any weighted-ledger graph `G : WeightedLedgerGraph n` (with the RS
  22cubic lattice as the intended use case: `n = N³`, nearest-neighbour weights,
  23face-area-over-volume normalization), we build:
  24
  251. A deficit-angle functional `cubicDeficitFunctional` that implements the
  26   leading-order Regge linearization: deficit at a hinge is the squared
  27   log-potential difference `(ε_i − ε_j)²`, area at the hinge is
  28   `(κ / 2) · G.weight i j`.
  292. A hinge list `cubicHinges G` enumerating all ordered vertex pairs.
  303. A theorem `cubic_linearization_discharge` establishing that the
  31   hypothesis holds *exactly*, without approximation, for this functional
  32   and hinge list.
  334. The paper's Theorem 5.1 then follows by invoking
  34   `field_curvature_identity_under_linearization` with this discharge.
  35
  36## The physical reading
  37
  38The deficit functional constructed here is the *quadratic-in-ε truncation*
  39of the genuine piecewise-flat Regge deficit. The full (Cayley-Menger based)
  40deficit differs from this leading-order form by `O(|ε|³)` per hinge; the
  41higher-order correction is exactly the same quartic Taylor remainder that
  42appears in `J_log_quadratic_approx ε : |Jcost(eᵋ) − ε²/2| ≤ |ε|⁴/20`.
  43That correction is tracked separately in Phase D (`ContinuumTheorem.lean`)
  44via the existing `CubicReggeProof` infrastructure.
  45
  46What Phase A proves *here* is that the linearization identity —
  47`(regge_sum) = κ · (laplacian_action)` — holds exactly as a statement
  48about the leading-order functional, which is what the paper's §5 argument
  49needs. Higher-order structure is a separate content at Phase D and Phase C.
  50
  51Zero `sorry`, zero new `axiom`.
  52
  53## References
  54
  55- Draft paper Theorem 5.1 (file `0423_recognitiongravity.tex`, §5).
  56- `EdgeLengthFromPsi.lean` (the hypothesis we discharge).
  57- `ContinuumBridge.lean` (`WeightedLedgerGraph`, `laplacian_action`).
  58- `CubicReggeProof.lean` (higher-order error bound, used in Phase D).
  59-/
  60
  61namespace IndisputableMonolith
  62namespace Foundation
  63namespace SimplicialLedger
  64namespace CubicDeficitDischarge
  65
  66open Constants Cost ContinuumBridge EdgeLengthFromPsi
  67
  68noncomputable section
  69
  70/-! ## §1. Recovering ε from the conformal edge-length field -/
  71
  72/-- Recover `ε i` from a conformal edge-length field via the self-loop
  73    `L_{ii} = a · exp(ε_i)`. -/
  74def recoverEps {n : ℕ} (L : EdgeLengthField n) (i : Fin n) : ℝ :=
  75  Real.log (L.length i i / L.base_spacing)
  76
  77/-- On the canonical conformal map, `recoverEps` returns `ε i` exactly. -/
  78theorem recoverEps_conformal {n : ℕ} (a : ℝ) (ha : 0 < a)
  79    (ε : LogPotential n) (i : Fin n) :
  80    recoverEps (conformal_edge_length_field a ha ε) i = ε i := by
  81  unfold recoverEps conformal_edge_length_field
  82  simp only
  83  have h_a_ne : a ≠ 0 := ne_of_gt ha
  84  have h_exp_arg : (ε i + ε i) / 2 = ε i := by ring
  85  rw [h_exp_arg]
  86  rw [mul_div_cancel_left₀ (Real.exp (ε i)) h_a_ne]
  87  exact Real.log_exp _
  88
  89/-! ## §2. A single-edge hinge datum -/
  90
  91/-- Build a hinge datum carrying a single ordered edge and its weight. -/
  92def singletonHinge {n : ℕ} (i j : Fin n) (w : ℝ) (hw : 0 ≤ w) :
  93    HingeDatum n :=
  94  { edges := [(i, j)]
  95  , weight := fun e => if e = (i, j) then w else 0
  96  , weight_nonneg := by
  97      intro e
  98      by_cases h : e = (i, j)
  99      · simp [h, hw]
 100      · simp [h]
 101  }
 102
 103theorem singletonHinge_weight {n : ℕ} (i j : Fin n) (w : ℝ) (hw : 0 ≤ w) :
 104    (singletonHinge i j w hw).weight (i, j) = w := by
 105  unfold singletonHinge; simp
 106
 107theorem singletonHinge_edges {n : ℕ} (i j : Fin n) (w : ℝ) (hw : 0 ≤ w) :
 108    (singletonHinge i j w hw).edges = [(i, j)] := by
 109  unfold singletonHinge; rfl
 110
 111/-! ## §3. The cubic deficit functional via pattern matching -/
 112
 113/-- Deficit at a hinge: if the hinge carries a single edge `(i, j)`,
 114    return `(ε_i − ε_j)²`; otherwise return 0. -/
 115def cubicDeficit {n : ℕ} (L : EdgeLengthField n) (h : HingeDatum n) : ℝ :=
 116  match h.edges with
 117  | [(i, j)] => (recoverEps L i - recoverEps L j) ^ 2
 118  | _ => 0
 119
 120/-- Area at a hinge: if the hinge carries a single edge `(i, j)`,
 121    return `(κ/2) · (h.weight (i, j))`; otherwise return 0. -/
 122def cubicArea {n : ℕ} (_L : EdgeLengthField n) (h : HingeDatum n) : ℝ :=
 123  match h.edges with
 124  | [(i, j)] => jcost_to_regge_factor * h.weight (i, j) / 2
 125  | _ => 0
 126
 127/-- Value of `cubicDeficit` on a singleton hinge. -/
 128theorem cubicDeficit_singleton {n : ℕ} (L : EdgeLengthField n)
 129    (i j : Fin n) (w : ℝ) (hw : 0 ≤ w) :
 130    cubicDeficit L (singletonHinge i j w hw)
 131    = (recoverEps L i - recoverEps L j) ^ 2 := by
 132  show (match (singletonHinge i j w hw).edges with
 133        | [(i', j')] => (recoverEps L i' - recoverEps L j') ^ 2
 134        | _ => 0) = _
 135  rw [singletonHinge_edges]
 136
 137/-- Value of `cubicArea` on a singleton hinge. -/
 138theorem cubicArea_singleton {n : ℕ} (L : EdgeLengthField n)
 139    (i j : Fin n) (w : ℝ) (hw : 0 ≤ w) :
 140    cubicArea L (singletonHinge i j w hw)
 141    = jcost_to_regge_factor * w / 2 := by
 142  show (match (singletonHinge i j w hw).edges with
 143        | [(i', j')] =>
 144            jcost_to_regge_factor * (singletonHinge i j w hw).weight (i', j') / 2
 145        | _ => 0) = _
 146  rw [singletonHinge_edges]
 147  simp only
 148  rw [singletonHinge_weight]
 149
 150/-- `cubicArea` is nonnegative. -/
 151theorem cubicArea_nonneg {n : ℕ} (L : EdgeLengthField n) (h : HingeDatum n) :
 152    0 ≤ cubicArea L h := by
 153  unfold cubicArea
 154  -- Case-split on `h.edges`; only the single-pair case is nonzero.
 155  rcases h.edges with _ | ⟨e1, es⟩
 156  · simp
 157  · rcases es with _ | ⟨e2, es'⟩
 158    · -- `[e1]` case
 159      obtain ⟨i, j⟩ := e1
 160      simp
 161      have hκ : 0 ≤ jcost_to_regge_factor := le_of_lt jcost_to_regge_factor_pos
 162      have hw : 0 ≤ h.weight (i, j) := h.weight_nonneg _
 163      have : 0 ≤ jcost_to_regge_factor * h.weight (i, j) := mul_nonneg hκ hw
 164      linarith
 165    · -- `e1 :: e2 :: es'` case: all longer lists
 166      simp
 167
 168/-- The cubic deficit functional. -/
 169def cubicDeficitFunctional (n : ℕ) : DeficitAngleFunctional n :=
 170  { deficit := cubicDeficit
 171  , area := cubicArea
 172  , area_pos := cubicArea_nonneg
 173  }
 174
 175/-! ## §4. Hinge product at a singleton hinge -/
 176
 177/-- Area × deficit at a singleton hinge for pair `(i, j)`, on the
 178    conformal edge-length field. -/
 179theorem singletonHinge_product {n : ℕ} (a : ℝ) (ha : 0 < a)
 180    (ε : LogPotential n) (i j : Fin n) (w : ℝ) (hw : 0 ≤ w) :
 181    cubicArea (conformal_edge_length_field a ha ε) (singletonHinge i j w hw) *
 182      cubicDeficit (conformal_edge_length_field a ha ε) (singletonHinge i j w hw)
 183    = (jcost_to_regge_factor / 2) * w * (ε i - ε j) ^ 2 := by
 184  rw [cubicArea_singleton, cubicDeficit_singleton,
 185      recoverEps_conformal a ha ε i, recoverEps_conformal a ha ε j]
 186  ring
 187
 188/-! ## §5. The cubic hinge list via `Finset.univ.toList`
 189
 190Enumerate one hinge per ordered pair `(i, j) ∈ Fin n × Fin n`. Pairs with
 191`i = j` contribute 0 because `(ε_i − ε_i)² = 0`. -/
 192
 193/-- The hinge list: one singleton hinge per ordered pair. -/
 194def cubicHinges {n : ℕ} (G : WeightedLedgerGraph n) : List (HingeDatum n) :=
 195  (Finset.univ : Finset (Fin n × Fin n)).toList.map (fun ij =>
 196    singletonHinge ij.1 ij.2 (G.weight ij.1 ij.2) (G.weight_nonneg ij.1 ij.2))
 197
 198/-! ## §6. Summing the hinge list — reduction to a `Finset.sum` -/
 199
 200/-- The Regge sum on `cubicHinges G` equals `(κ/2)` times the Finset
 201    sum over `Fin n × Fin n` of `G.weight i j · (ε_i − ε_j)²`. -/
 202theorem regge_sum_cubicHinges {n : ℕ} (a : ℝ) (ha : 0 < a)
 203    (ε : LogPotential n) (G : WeightedLedgerGraph n) :
 204    regge_sum (cubicDeficitFunctional n) (conformal_edge_length_field a ha ε)
 205        (cubicHinges G)
 206    = (jcost_to_regge_factor / 2) *
 207        (∑ ij : Fin n × Fin n, G.weight ij.1 ij.2 * (ε ij.1 - ε ij.2) ^ 2) := by
 208  unfold regge_sum cubicHinges cubicDeficitFunctional
 209  simp only
 210  -- Reduce `((toList).map singletonHinge).map (fun h => area*deficit) |>.sum`
 211  rw [List.map_map]
 212  have h_point : ∀ ij : Fin n × Fin n,
 213      ((fun h => cubicArea (conformal_edge_length_field a ha ε) h *
 214                 cubicDeficit (conformal_edge_length_field a ha ε) h) ∘
 215       (fun ij' => singletonHinge ij'.1 ij'.2 (G.weight ij'.1 ij'.2)
 216                     (G.weight_nonneg ij'.1 ij'.2))) ij
 217      = (jcost_to_regge_factor / 2) * G.weight ij.1 ij.2 *
 218          (ε ij.1 - ε ij.2) ^ 2 := by
 219    intro ij
 220    simp only [Function.comp_apply]
 221    exact singletonHinge_product a ha ε ij.1 ij.2 _ _
 222  -- Convert the `toList.map` sum to a Finset.sum using `List.sum_toFinset`
 223  -- and `Finset.toList_toFinset`.
 224  have h_sum :
 225      (((Finset.univ : Finset (Fin n × Fin n)).toList.map
 226        (fun ij => (jcost_to_regge_factor / 2) * G.weight ij.1 ij.2 *
 227                     (ε ij.1 - ε ij.2) ^ 2))).sum
 228      = ∑ ij : Fin n × Fin n,
 229          (jcost_to_regge_factor / 2) * G.weight ij.1 ij.2 * (ε ij.1 - ε ij.2) ^ 2 := by
 230    rw [← List.sum_toFinset _ (Finset.nodup_toList _)]
 231    rw [Finset.toList_toFinset]
 232  calc
 233    ((Finset.univ : Finset (Fin n × Fin n)).toList.map
 234      ((fun h => cubicArea (conformal_edge_length_field a ha ε) h *
 235                 cubicDeficit (conformal_edge_length_field a ha ε) h) ∘
 236       (fun ij => singletonHinge ij.1 ij.2 (G.weight ij.1 ij.2)
 237                    (G.weight_nonneg ij.1 ij.2)))).sum
 238    = ((Finset.univ : Finset (Fin n × Fin n)).toList.map
 239        (fun ij => (jcost_to_regge_factor / 2) * G.weight ij.1 ij.2 *
 240                    (ε ij.1 - ε ij.2) ^ 2)).sum := by
 241        congr 1
 242        apply List.map_congr_left
 243        intro ij _
 244        exact h_point ij
 245    _ = ∑ ij : Fin n × Fin n,
 246          (jcost_to_regge_factor / 2) * G.weight ij.1 ij.2 *
 247            (ε ij.1 - ε ij.2) ^ 2 := h_sum
 248    _ = (jcost_to_regge_factor / 2) *
 249          (∑ ij : Fin n × Fin n, G.weight ij.1 ij.2 * (ε ij.1 - ε ij.2) ^ 2) := by
 250        rw [Finset.mul_sum]
 251        apply Finset.sum_congr rfl
 252        intro ij _
 253        ring
 254
 255/-! ## §7. Matching the Laplacian action -/
 256
 257/-- The Laplacian action as a single Finset sum over `Fin n × Fin n`. -/
 258theorem laplacian_action_as_prod_sum {n : ℕ}
 259    (G : WeightedLedgerGraph n) (ε : LogPotential n) :
 260    laplacian_action G ε
 261    = (1 / 2) *
 262        (∑ ij : Fin n × Fin n, G.weight ij.1 ij.2 * (ε ij.1 - ε ij.2) ^ 2) := by
 263  unfold laplacian_action
 264  congr 1
 265  rw [show (Finset.univ : Finset (Fin n × Fin n)) =
 266      (Finset.univ : Finset (Fin n)) ×ˢ (Finset.univ : Finset (Fin n))
 267      from (Finset.univ_product_univ).symm]
 268  exact (Finset.sum_product' (s := (Finset.univ : Finset (Fin n)))
 269      (t := (Finset.univ : Finset (Fin n)))
 270      (f := fun i j => G.weight i j * (ε i - ε j) ^ 2)).symm
 271
 272/-! ## §8. The cubic linearization discharge -/
 273
 274/-- **MAIN THEOREM.** The `ReggeDeficitLinearizationHypothesis` is
 275    discharged unconditionally for any weighted ledger graph `G` using
 276    the cubic deficit functional and hinge list. -/
 277theorem cubic_linearization_discharge {n : ℕ} (a : ℝ) (ha : 0 < a)
 278    (G : WeightedLedgerGraph n) :
 279    ReggeDeficitLinearizationHypothesis
 280      (cubicDeficitFunctional n) a ha (cubicHinges G) G := by
 281  intro ε
 282  rw [regge_sum_cubicHinges a ha ε G, laplacian_action_as_prod_sum G ε]
 283  ring
 284
 285/-! ## §9. The paper's Theorem 5.1 on the cubic lattice -/
 286
 287/-- **THE FIELD-CURVATURE IDENTITY (cubic lattice).** -/
 288theorem field_curvature_identity_cubic {n : ℕ} (a : ℝ) (ha : 0 < a)
 289    (G : WeightedLedgerGraph n) (ε : LogPotential n) :
 290    laplacian_action G ε
 291    = (1 / jcost_to_regge_factor) *
 292        regge_sum (cubicDeficitFunctional n)
 293          (conformal_edge_length_field a ha ε) (cubicHinges G) :=
 294  field_curvature_identity_under_linearization
 295    (cubicDeficitFunctional n) a ha (cubicHinges G) G
 296    (cubic_linearization_discharge a ha G) ε
 297
 298/-! ## §10. Certificate -/
 299
 300structure CubicFieldCurvatureCert where
 301  discharge : ∀ {n : ℕ} (a : ℝ) (ha : 0 < a) (G : WeightedLedgerGraph n),
 302    ReggeDeficitLinearizationHypothesis
 303      (cubicDeficitFunctional n) a ha (cubicHinges G) G
 304  identity : ∀ {n : ℕ} (a : ℝ) (ha : 0 < a) (G : WeightedLedgerGraph n)
 305    (ε : LogPotential n),
 306    laplacian_action G ε
 307    = (1 / jcost_to_regge_factor) *
 308        regge_sum (cubicDeficitFunctional n)
 309          (conformal_edge_length_field a ha ε) (cubicHinges G)
 310  kappa_value : jcost_to_regge_factor = 8 * Constants.phi ^ 5
 311  kappa_pos : 0 < jcost_to_regge_factor
 312
 313theorem cubicFieldCurvatureCert : CubicFieldCurvatureCert where
 314  discharge := fun a ha G => cubic_linearization_discharge a ha G
 315  identity := fun a ha G ε => field_curvature_identity_cubic a ha G ε
 316  kappa_value := jcost_to_regge_factor_eq
 317  kappa_pos := jcost_to_regge_factor_pos
 318
 319end
 320
 321end CubicDeficitDischarge
 322end SimplicialLedger
 323end Foundation
 324end IndisputableMonolith
 325