IndisputableMonolith.Geometry.Schlaefli

   1import Mathlib.Data.Real.Basic
   2import Mathlib.Algebra.BigOperators.Group.Finset.Basic
   3import IndisputableMonolith.Geometry.CayleyMenger
   4import IndisputableMonolith.Geometry.DihedralAngle
   5
   6/-!
   7# Schläfli's Identity
   8
   9This module formalizes Schläfli's identity for piecewise-flat simplicial
  10complexes. It is Phase C3 of the program to discharge the Regge deficit
  11linearization hypothesis on general simplicial complexes.
  12
  13## Content
  14
  15For a simplicial `n`-complex `K` with vertex-edge structure fixed, let
  16`L_e` denote the edge length of edge `e` and `A_h` the area (or
  17`(n−2)`-volume) of hinge `h`. The dihedral angle of a top simplex `σ`
  18at a hinge `h ⊂ σ` depends on the edge lengths via Cayley-Menger.
  19
  20**Schläfli's identity** (Schläfli 1858; see Regge 1961 for the
  21piecewise-flat version):
  22
  23  for every edge `e` of `K`,
  24    `Σ_{σ} Σ_{h ⊂ σ} A_h · (∂θ_σ,h / ∂L_e) = 0`.
  25
  26Summing only over hinges `h` that meet edge `e`, the classical form is:
  27
  28  `Σ_h A_h · (∂θ_h / ∂L_e) = 0`
  29
  30where `θ_h` is the *total* dihedral angle at hinge `h` (sum over the
  31simplices meeting `h`). This is the identity that makes the Regge
  32equations reduce from two terms to one:
  33
  34  δS_Regge / δL_e = Σ_h (∂A_h / ∂L_e) · δ_h + Σ_h A_h · (∂δ_h / ∂L_e)
  35                  = Σ_h (∂A_h / ∂L_e) · δ_h             ( by Schläfli )
  36                  = 0                                     ( Regge eqns )
  37
  38## Status
  39
  40This identity is *not* trivial; in the Regge literature it is proved
  41via local integration by parts on each simplex's boundary (see Regge's
  42original paper or Hartle-Sorkin 1981). Mathlib does not yet have the
  43ambient geometric-calculus infrastructure to reproduce this proof.
  44
  45We therefore record Schläfli's identity as a *named hypothesis*, matching
  46the pattern of `NonlinearConvergence.regge_to_eh_convergence_axiom` and
  47`CayleyMenger.TetVolumeIdentity`. Downstream consumers (Phase C4 and
  48Phase C5) thread it explicitly, so that callers can see exactly which
  49classical fact is being used.
  50
  51Zero `sorry`, zero new `axiom`.
  52
  53## References
  54
  55- Schläfli, L. (1858). *On the multiple integral ∫^n d x d y · · · d z.*
  56  Quarterly Journal of Pure and Applied Mathematics.
  57- Regge, T. (1961). *General relativity without coordinates.*
  58  Nuovo Cimento 19, 558–571.
  59- Hartle, J. B., Sorkin, R. (1981). *Boundary terms in the action for
  60  the Regge calculus.* General Relativity and Gravitation 13, 541–549.
  61- Brewin, L. C. (2000). *The Riemann and extrinsic curvature tensors in
  62  the Regge calculus.* Class. Quantum Grav. 17, 545.
  63-/
  64
  65namespace IndisputableMonolith
  66namespace Geometry
  67namespace Schlaefli
  68
  69open CayleyMenger DihedralAngle
  70
  71noncomputable section
  72
  73/-! ## §1. Edge / hinge book-keeping -/
  74
  75/-- Abstract edge-length data for a simplicial complex with finitely many
  76    edges indexed by `Fin nE`. -/
  77structure SimplicialEdgeData (nE : ℕ) where
  78  len : Fin nE → ℝ
  79  len_pos : ∀ e, 0 < len e
  80
  81/-- Abstract hinge data: each hinge knows its area and the collection of
  82    dihedral angles of the top simplices meeting it. The *total* dihedral
  83    at the hinge is `Σ θ_σ`; the deficit is `2π − Σ θ_σ`. -/
  84structure SimplicialHingeData where
  85  area : ℝ
  86  area_nonneg : 0 ≤ area
  87  dihedrals : List DihedralAngleData
  88
  89namespace SimplicialHingeData
  90
  91/-- Sum of the dihedral angles at the hinge. -/
  92def totalTheta (h : SimplicialHingeData) : ℝ :=
  93  DihedralAngle.sumThetas h.dihedrals
  94
  95/-- Deficit at the hinge: `2π − Σ θ`. -/
  96def deficit (h : SimplicialHingeData) : ℝ :=
  97  DihedralAngle.deficit h.dihedrals
  98
  99theorem deficit_eq (h : SimplicialHingeData) :
 100    h.deficit = 2 * Real.pi - h.totalTheta := rfl
 101
 102end SimplicialHingeData
 103
 104/-! ## §2. Variational data
 105
 106For Schläfli's identity we need derivatives of `θ_h` with respect to each
 107edge length `L_e`. We package these as a matrix of real numbers, one per
 108(hinge, edge) pair. The identity below constrains this matrix. -/
 109
 110/-- A matrix of deficit-angle derivatives: `dThetadL h e` is intended
 111    to be `∂(totalTheta h) / ∂(len e)`. -/
 112structure DeficitDerivativeMatrix (nH nE : ℕ) where
 113  dThetadL : Fin nH → Fin nE → ℝ
 114
 115/-! ## §3. Schläfli's identity as a hypothesis -/
 116
 117/-- **SCHLÄFLI'S IDENTITY** (piecewise-flat form).
 118
 119    For a finite collection of hinges (indexed by `Fin nH`) with areas
 120    `A_h` and a matrix `dThetadL` of dihedral-angle derivatives with
 121    respect to edge lengths, the weighted sum vanishes:
 122
 123    `∀ e, Σ_h A_h · (∂θ_h / ∂L_e) = 0`.
 124
 125    This is the classical local identity; see Regge (1961, eq. 2.8) and
 126    Brewin (2000). We record it as a hypothesis structure because the
 127    full proof requires boundary-integration machinery not yet in
 128    Mathlib. -/
 129def SchlaefliIdentity {nH nE : ℕ}
 130    (hinges : Fin nH → SimplicialHingeData)
 131    (M : DeficitDerivativeMatrix nH nE) : Prop :=
 132  ∀ e : Fin nE,
 133    (∑ h : Fin nH, (hinges h).area * M.dThetadL h e) = 0
 134
 135/-! ## §4. Consequences of Schläfli's identity
 136
 137Schläfli's identity makes the second term of the Regge variation vanish,
 138leaving only the `∂A/∂L · δ` piece. This is what the Regge equations of
 139motion look like. -/
 140
 141/-- Under Schläfli, the `Σ A · dθ/dL` term in the Regge variation is
 142    identically zero. -/
 143theorem schlaefli_kills_dtheta {nH nE : ℕ}
 144    (hinges : Fin nH → SimplicialHingeData)
 145    (M : DeficitDerivativeMatrix nH nE)
 146    (hS : SchlaefliIdentity hinges M) (e : Fin nE) :
 147    (∑ h : Fin nH, (hinges h).area * M.dThetadL h e) = 0 := hS e
 148
 149/-- Total deficit functional: `Σ_h A_h · δ_h = Σ_h A_h · (2π − totalTheta h)`. -/
 150def totalDeficit {nH : ℕ} (hinges : Fin nH → SimplicialHingeData) : ℝ :=
 151  ∑ h : Fin nH, (hinges h).area * (hinges h).deficit
 152
 153/-! ## §5. Flat baseline -/
 154
 155/-- If every hinge satisfies the flat-sum condition, the total deficit
 156    vanishes. -/
 157theorem totalDeficit_flat {nH : ℕ}
 158    (hinges : Fin nH → SimplicialHingeData)
 159    (hFlat : ∀ h : Fin nH,
 160      DihedralAngle.FlatSumCondition (hinges h).dihedrals) :
 161    totalDeficit hinges = 0 := by
 162  unfold totalDeficit
 163  apply Finset.sum_eq_zero
 164  intro h _
 165  have : (hinges h).deficit = 0 := by
 166    unfold SimplicialHingeData.deficit
 167    exact DihedralAngle.deficit_eq_zero_of_flat _ (hFlat h)
 168  rw [this]; ring
 169
 170/-! ## §6. Certificate -/
 171
 172/-- Phase C3 certificate. -/
 173structure SchlaefliCert where
 174  flat_total_zero : ∀ {nH : ℕ} (hinges : Fin nH → SimplicialHingeData),
 175    (∀ h, DihedralAngle.FlatSumCondition (hinges h).dihedrals) →
 176    totalDeficit hinges = 0
 177  schlaefli_kills_sum : ∀ {nH nE : ℕ}
 178    (hinges : Fin nH → SimplicialHingeData)
 179    (M : DeficitDerivativeMatrix nH nE),
 180    SchlaefliIdentity hinges M →
 181    ∀ e : Fin nE,
 182      (∑ h : Fin nH, (hinges h).area * M.dThetadL h e) = 0
 183
 184theorem schlaefliCert : SchlaefliCert where
 185  flat_total_zero := fun hinges hFlat => totalDeficit_flat hinges hFlat
 186  schlaefli_kills_sum := fun hinges M hS e => schlaefli_kills_dtheta hinges M hS e
 187
 188end
 189
 190end Schlaefli
 191end Geometry
 192end IndisputableMonolith
 193