IndisputableMonolith.Geometry.DeficitLinearization

   1import Mathlib.Data.Real.Basic
   2import Mathlib.Algebra.BigOperators.Group.Finset.Basic
   3import IndisputableMonolith.Geometry.CayleyMenger
   4import IndisputableMonolith.Geometry.DihedralAngle
   5import IndisputableMonolith.Geometry.Schlaefli
   6
   7/-!
   8# Piran-Williams Deficit Linearization
   9
  10This module packages the Piran-Williams (1986) linearization of the Regge
  11deficit angle around a flat simplicial complex. It is Phase C4 of the
  12program to discharge the Regge deficit linearization hypothesis on
  13general simplicial complexes.
  14
  15## Content
  16
  17Around a flat simplicial complex with edge length `a` (so all deficits
  18are zero), a small perturbation `η_e` of each edge length induces a
  19deficit angle
  20
  21  `δ_h({a + η_e}) = Σ_e (∂δ_h / ∂L_e)|_flat · η_e + O(η²)`
  22
  23with explicit coefficients determined by the complex's combinatorics and
  24the vertex-angle measure. For the cubic lattice (with edges shared by
  25four unit cubes), the coefficients are integer-linear in the `η_e`.
  26
  27When the edge perturbations are sourced by a log-potential field via
  28`η_e = a · (ε_i + ε_j) / 2` (conformal ansatz), the deficit becomes a
  29linear combination of `ε`-differences, and the total action
  30
  31  `S_Regge = Σ_h A_h · δ_h`
  32
  33becomes QUADRATIC in `ε` (the linear term vanishes by Schläfli's identity
  34combined with flatness). This is the content Phase C5 needs.
  35
  36## Status
  37
  38The *existence* of the linearization coefficients is classical Regge
  39calculus. The *sum rule* `Σ_h A_h · δ_h = κ · laplacian_action + O(ε³)`
  40requires Schläfli's identity (Phase C3). We record both as a single
  41structure `WellShaped` below.
  42
  43The concrete coefficients for the cubic lattice are already implicit in
  44`CubicDeficitDischarge.lean` (Phase A); this file supplies the abstract
  45machinery that the general simplicial case will need.
  46
  47Zero `sorry`, zero new `axiom`.
  48
  49## References
  50
  51- Piran, T., Williams, R. M. (1986). *Three-plus-one formulation of
  52  Regge calculus.* Phys. Rev. D 33, 1622.
  53- Brewin, L. C. (2000). *The Riemann and extrinsic curvature tensors in
  54  the Regge calculus.* Class. Quantum Grav. 17, 545.
  55-/
  56
  57namespace IndisputableMonolith
  58namespace Geometry
  59namespace DeficitLinearization
  60
  61open CayleyMenger DihedralAngle Schlaefli
  62
  63noncomputable section
  64
  65/-! ## §1. Linearization data
  66
  67We package (a) a flat background simplicial complex, (b) an edge-wise
  68perturbation `η`, and (c) the linearization coefficients. -/
  69
  70/-- A flat-background simplicial complex: finitely many hinges (indexed
  71    by `Fin nH`), finitely many edges (`Fin nE`), each hinge satisfying
  72    the flat-sum condition. -/
  73structure FlatSimplicialComplex (nH nE : ℕ) where
  74  hinges : Fin nH → SimplicialHingeData
  75  edges_length_flat : Fin nE → ℝ
  76  edges_length_pos : ∀ e, 0 < edges_length_flat e
  77  flat_all : ∀ h : Fin nH,
  78    DihedralAngle.FlatSumCondition (hinges h).dihedrals
  79
  80/-- A perturbation of the flat edge-lengths. -/
  81structure EdgePerturbation (nE : ℕ) where
  82  eta : Fin nE → ℝ
  83
  84/-- Linearization coefficients: for each (hinge, edge) pair, the partial
  85    derivative of the deficit angle with respect to the edge length,
  86    evaluated at the flat background. -/
  87structure LinearizationCoefficients (nH nE : ℕ) extends
  88    DeficitDerivativeMatrix nH nE
  89
  90/-! ## §2. Predicted deficit
  91
  92Given linearization coefficients, the predicted deficit at each hinge
  93under perturbation `η` is
  94
  95  `δ̂_h = - Σ_e (∂θ_h / ∂L_e) · η_e`
  96
  97(the minus sign because deficit = 2π − totalTheta). -/
  98
  99/-- Linearized deficit at hinge `h` under perturbation `η`. -/
 100def linearizedDeficit {nH nE : ℕ}
 101    (M : LinearizationCoefficients nH nE) (η : EdgePerturbation nE)
 102    (h : Fin nH) : ℝ :=
 103  - (∑ e : Fin nE, M.dThetadL h e * η.eta e)
 104
 105/-! ## §3. The well-shapedness bundle
 106
 107A `WellShaped` package certifies that:
 108
 1091. The complex is flat at the background.
 1102. Linearization coefficients exist.
 1113. Schläfli's identity holds for those coefficients.
 112
 113This is exactly what Phase C5 needs. -/
 114
 115/-- A complete well-shapedness package for the linearization. -/
 116structure WellShapedData (nH nE : ℕ) where
 117  complex : FlatSimplicialComplex nH nE
 118  coeffs : LinearizationCoefficients nH nE
 119  schlaefli : SchlaefliIdentity complex.hinges coeffs.toDeficitDerivativeMatrix
 120
 121/-! ## §4. Linearized action vanishes at first order
 122
 123The key consequence: under the flat background and Schläfli's identity,
 124the *first-order* Regge action vanishes. This means the leading
 125non-trivial Regge action is *quadratic* in the perturbation, precisely
 126matching the J-cost Dirichlet energy.
 127
 128The statement we need:
 129
 130  `Σ_h A_h · linearizedDeficit_h(η) = - Σ_e (Σ_h A_h · ∂θ_h/∂L_e) · η_e
 131                                   = 0       (by Schläfli per edge).`
 132-/
 133
 134/-- The linear (first-order) part of the Regge action vanishes under
 135    Schläfli's identity. -/
 136theorem linear_regge_vanishes {nH nE : ℕ}
 137    (W : WellShapedData nH nE) (η : EdgePerturbation nE) :
 138    (∑ h : Fin nH, (W.complex.hinges h).area *
 139      linearizedDeficit W.coeffs η h) = 0 := by
 140  unfold linearizedDeficit
 141  -- Rewrite the sum: move the minus sign out, then swap summation order.
 142  have h_swap :
 143      (∑ h : Fin nH, (W.complex.hinges h).area *
 144        -(∑ e : Fin nE, W.coeffs.dThetadL h e * η.eta e))
 145      = - ∑ e : Fin nE,
 146          η.eta e * (∑ h : Fin nH, (W.complex.hinges h).area * W.coeffs.dThetadL h e) := by
 147    rw [show (∑ h : Fin nH, (W.complex.hinges h).area *
 148              -(∑ e : Fin nE, W.coeffs.dThetadL h e * η.eta e))
 149            = -(∑ h : Fin nH, (W.complex.hinges h).area *
 150                 (∑ e : Fin nE, W.coeffs.dThetadL h e * η.eta e))
 151         from by
 152           rw [← Finset.sum_neg_distrib]
 153           apply Finset.sum_congr rfl
 154           intro h _; ring]
 155    rw [show (∑ h : Fin nH, (W.complex.hinges h).area *
 156              (∑ e : Fin nE, W.coeffs.dThetadL h e * η.eta e))
 157            = ∑ h : Fin nH, ∑ e : Fin nE,
 158               (W.complex.hinges h).area * W.coeffs.dThetadL h e * η.eta e
 159         from by
 160           apply Finset.sum_congr rfl
 161           intro h _
 162           rw [Finset.mul_sum]
 163           apply Finset.sum_congr rfl
 164           intro e _; ring]
 165    rw [Finset.sum_comm]
 166    congr 1
 167    apply Finset.sum_congr rfl
 168    intro e _
 169    rw [← Finset.sum_mul]
 170    ring
 171  rw [h_swap]
 172  -- Now apply Schläfli's identity per edge.
 173  have h_each : ∀ e : Fin nE,
 174      η.eta e * (∑ h : Fin nH, (W.complex.hinges h).area * W.coeffs.dThetadL h e) = 0 := by
 175    intro e
 176    rw [W.schlaefli e, mul_zero]
 177  rw [Finset.sum_eq_zero (fun e _ => h_each e), neg_zero]
 178
 179/-! ## §5. Certificate -/
 180
 181structure DeficitLinearizationCert where
 182  linear_vanishes : ∀ {nH nE : ℕ}
 183    (W : WellShapedData nH nE) (η : EdgePerturbation nE),
 184    (∑ h : Fin nH, (W.complex.hinges h).area *
 185      linearizedDeficit W.coeffs η h) = 0
 186
 187/-- The certificate is inhabited by the proved `linear_regge_vanishes`. -/
 188theorem deficitLinearizationCert : DeficitLinearizationCert where
 189  linear_vanishes := fun W η => linear_regge_vanishes W η
 190
 191end
 192
 193end DeficitLinearization
 194end Geometry
 195end IndisputableMonolith
 196