IndisputableMonolith.Gravity.DiscreteVacuumEinstein

   1import Mathlib
   2import IndisputableMonolith.Geometry.ReggeActionSecondVariation
   3
   4/-!
   5# Discrete Vacuum Einstein Equation for the Nonlinear Regge Action
   6
   7The Regge vacuum equation is zero deficit at every hinge.  For the conformal
   8nonlinear action, the forward direction follows from zero deficit plus global
   9Schläfli cancellation; the reverse direction needs a rank/nondegeneracy input
  10for the conformal edge-incidence derivative.  This module records the exact
  11equivalence as a named input rather than an axiom.
  12-/
  13
  14namespace IndisputableMonolith
  15namespace Gravity
  16namespace DiscreteVacuumEinstein
  17
  18open Geometry.ReggeTriangulation3D
  19open Geometry.ReggeHessian3D
  20open Geometry.Triangulation3DConsistency
  21open Geometry.ReggeActionConcrete
  22open Geometry.ReggeActionSmoothness
  23open Geometry.ReggeActionFirstVariation
  24
  25noncomputable section
  26
  27/-- Zero Regge deficit at every global edge of the flat potential. -/
  28def ZeroDeficitAtFlat (K : Triangulation3D) : Prop :=
  29  ∀ e : Fin K.nE, deficitAngle K (zeroPotential K) e = 0
  30
  31/-- The nonlinear Regge action is critical at the flat potential. -/
  32def CriticalAtFlat
  33    (K : Triangulation3D) (hK : IncidenceConsistent K) : Prop :=
  34  ReggeActionCriticalAtZero K hK
  35
  36/-- Vertex-edge incidence coefficient for the conformal derivative of a global
  37edge length: each endpoint contributes `1/2`. -/
  38def vertexEdgeIncidenceDerivative
  39    (K : Triangulation3D) (e : Fin K.nE) (i : Fin K.nV) : ℝ :=
  40  if (K.edgeVerts e).1 = i ∨ (K.edgeVerts e).2 = i then (1 / 2 : ℝ) else 0
  41
  42/-- Directional length coefficient for edge `e` in vertex-potential direction
  43`η`, without the constant edge-length factor. -/
  44def directionalLengthCoefficient
  45    (K : Triangulation3D) (η : VertexPotential K) (e : Fin K.nE) : ℝ :=
  46  ∑ i : Fin K.nV, vertexEdgeIncidenceDerivative K e i * η i
  47
  48/-- Compatibility between the geometric hinge derivative and the endpoint
  49incidence coefficient used in the vacuum equation.  This isolates the
  50normalization issue: the geometric derivative includes the flat edge length,
  51whereas the incidence formula is dimensionless. -/
  52def HingeDerivativeMatchesIncidence
  53    (K : Triangulation3D) (hK : IncidenceConsistent K) : Prop :=
  54  ∀ η : VertexPotential K, ∀ e : Fin K.nE,
  55    Geometry.ReggeActionFirstVariation.hingeMeasureDirectionalDeriv K hK η e =
  56      deficitAngle K (zeroPotential K) e * 0 +
  57        Real.sqrt (hK.globalSqEdge e) * directionalLengthCoefficient K η e
  58
  59theorem hingeDerivative_matches_incidence_simplified
  60    (K : Triangulation3D) (hK : IncidenceConsistent K)
  61    (hMatch : HingeDerivativeMatchesIncidence K hK) :
  62    ∀ η : VertexPotential K, ∀ e : Fin K.nE,
  63      Geometry.ReggeActionFirstVariation.hingeMeasureDirectionalDeriv K hK η e =
  64        Real.sqrt (hK.globalSqEdge e) * directionalLengthCoefficient K η e := by
  65  intro η e
  66  simpa using hMatch η e
  67
  68/-- Incidence rank/separation condition: a deficit vector whose pairing with
  69every conformal edge-length direction vanishes is zero.  This is a real
  70condition on the triangulation, not a consequence of local tetrahedron
  71nondegeneracy. -/
  72def IncidenceDeficitSeparating (K : Triangulation3D) : Prop :=
  73  ∀ δ : Fin K.nE → ℝ,
  74    (∀ η : VertexPotential K,
  75      ∑ e : Fin K.nE, δ e * directionalLengthCoefficient K η e = 0) →
  76    δ = 0
  77
  78/-- Concrete recovery/rank certificate for incidence separation.  The scalar
  79observations are the directional pairings against vertex-basis potentials. -/
  80def IncidenceDeficitRecovering (K : Triangulation3D) : Prop :=
  81  ∃ recover : Fin K.nE → Fin K.nV → ℝ,
  82    ∀ δ : Fin K.nE → ℝ, ∀ e : Fin K.nE,
  83      δ e =
  84        ∑ i : Fin K.nV,
  85          recover e i *
  86            (∑ e' : Fin K.nE,
  87              δ e' * directionalLengthCoefficient K
  88                (fun j : Fin K.nV => if j = i then (1 : ℝ) else 0) e')
  89
  90theorem incidenceDeficitSeparating_of_recovering
  91    (K : Triangulation3D)
  92    (hRecover : IncidenceDeficitRecovering K) :
  93    IncidenceDeficitSeparating K := by
  94  rcases hRecover with ⟨recover, hrecover⟩
  95  intro δ hpair
  96  funext e
  97  rw [hrecover δ e]
  98  apply Finset.sum_eq_zero
  99  intro i _
 100  rw [hpair (fun j : Fin K.nV => if j = i then (1 : ℝ) else 0)]
 101  ring
 102
 103/-- Intended triangulation class for the reverse vacuum implication: the
 104vertex-edge incidence observations recover every edge-deficit vector. -/
 105structure RecoveringIncidenceTriangulation (K : Triangulation3D) where
 106  recovery : IncidenceDeficitRecovering K
 107
 108theorem RecoveringIncidenceTriangulation.separating
 109    {K : Triangulation3D} (R : RecoveringIncidenceTriangulation K) :
 110    IncidenceDeficitSeparating K :=
 111  incidenceDeficitSeparating_of_recovering K R.recovery
 112
 113/-- First-variation formula before imposing zero deficit: the derivative of
 114the action pairs the deficit vector with conformal edge-length directions. -/
 115structure ReggeFirstVariationFormula
 116    (K : Triangulation3D) (hK : IncidenceConsistent K) where
 117  variation_formula :
 118    ∀ η : VertexPotential K,
 119      fderiv ℝ (reggeAction K hK) (zeroPotential K) η =
 120        ∑ e : Fin K.nE,
 121          deficitAngle K (zeroPotential K) e *
 122            directionalLengthCoefficient K η e
 123
 124/-- Convert the geometry-layer first-variation formula into the dimensionless
 125vacuum formula when the hinge-length normalization is known to be harmless.
 126The cleanest case is unit flat edge length, encoded as
 127`sqrt (globalSqEdge e) = 1`. -/
 128def ReggeFirstVariationFormula.ofGeometryFormula_unitEdges
 129    (K : Triangulation3D) (hK : IncidenceConsistent K)
 130    (hGeom : Geometry.ReggeActionFirstVariation.ReggeActionFirstVariationFormula K hK)
 131    (hUnit : ∀ e : Fin K.nE, Real.sqrt (hK.globalSqEdge e) = 1)
 132    (hCoeff :
 133      ∀ η : VertexPotential K, ∀ e : Fin K.nE,
 134        Geometry.ReggeActionFirstVariation.hingeMeasureDirectionalDeriv K hK η e =
 135          Real.sqrt (hK.globalSqEdge e) * directionalLengthCoefficient K η e) :
 136    ReggeFirstVariationFormula K hK where
 137  variation_formula := by
 138    intro η
 139    rw [hGeom.firstVariation_formula η]
 140    refine Finset.sum_congr rfl ?_
 141    intro e _
 142    rw [hCoeff η e, hUnit e]
 143    ring
 144
 145theorem zero_deficit_of_flat_configuration
 146    (K : Triangulation3D) (hK : IncidenceConsistent K)
 147    (h_flat : FlatConfiguration K hK) :
 148    ZeroDeficitAtFlat K :=
 149  h_flat.flat_deficit_zero
 150
 151/-- Named discrete-vacuum-Einstein input.  The nontrivial reverse implication
 152is the incidence-rank theorem: if all conformal first variations vanish, then
 153each edge deficit is zero. -/
 154structure DiscreteVacuumEinsteinInput
 155    (K : Triangulation3D) (hK : IncidenceConsistent K)
 156    (_h_flat : FlatConfiguration K hK) where
 157  critical_iff_zero_deficit :
 158    CriticalAtFlat K hK ↔ ZeroDeficitAtFlat K
 159
 160/-- Phase-F discrete vacuum Einstein equivalence. -/
 161theorem reggeAction_critical_iff_zero_deficit
 162    (K : Triangulation3D) (hK : IncidenceConsistent K)
 163    (h_flat : FlatConfiguration K hK)
 164    (h_einstein : DiscreteVacuumEinsteinInput K hK h_flat) :
 165    CriticalAtFlat K hK ↔ ZeroDeficitAtFlat K :=
 166  h_einstein.critical_iff_zero_deficit
 167
 168theorem zero_deficit_of_critical_of_variationFormula_of_separating
 169    (K : Triangulation3D) (hK : IncidenceConsistent K)
 170    (hFormula : ReggeFirstVariationFormula K hK)
 171    (hSep : IncidenceDeficitSeparating K)
 172    (hCrit : CriticalAtFlat K hK) :
 173    ZeroDeficitAtFlat K := by
 174  unfold CriticalAtFlat ReggeActionCriticalAtZero at hCrit
 175  unfold ZeroDeficitAtFlat
 176  have hdelta :
 177      (fun e : Fin K.nE => deficitAngle K (zeroPotential K) e) = 0 := by
 178    apply hSep
 179    intro η
 180    have happly := congrArg (fun L : VertexPotential K →L[ℝ] ℝ => L η) hCrit
 181    have hzero :
 182        (fderiv ℝ (reggeAction K hK) (zeroPotential K)) η = 0 := by
 183      simpa using happly
 184    have hformula := hFormula.variation_formula η
 185    rw [hformula] at hzero
 186    simpa using hzero
 187  intro e
 188  exact congrFun hdelta e
 189
 190/-- Construct the old vacuum-Einstein input from an explicit first-variation
 191formula, a first-variation theorem for zero-deficit flat backgrounds, and the
 192incidence separation/rank condition. -/
 193def discreteVacuumEinsteinInput_of_variationFormula_of_separating
 194    (K : Triangulation3D) (hK : IncidenceConsistent K)
 195    (h_flat : FlatConfiguration K hK)
 196    (hFirst : ReggeActionFirstVariationInput K hK h_flat)
 197    (hFormula : ReggeFirstVariationFormula K hK)
 198    (hSep : IncidenceDeficitSeparating K) :
 199    DiscreteVacuumEinsteinInput K hK h_flat where
 200  critical_iff_zero_deficit := by
 201    constructor
 202    · intro hCrit
 203      exact zero_deficit_of_critical_of_variationFormula_of_separating
 204        K hK hFormula hSep hCrit
 205    · intro _hZero
 206      exact hFirst.firstVariation_zero
 207
 208def discreteVacuumEinsteinInput_of_recoveringIncidence
 209    (K : Triangulation3D) (hK : IncidenceConsistent K)
 210    (h_flat : FlatConfiguration K hK)
 211    (hFirst : ReggeActionFirstVariationInput K hK h_flat)
 212    (hFormula : ReggeFirstVariationFormula K hK)
 213    (R : RecoveringIncidenceTriangulation K) :
 214    DiscreteVacuumEinsteinInput K hK h_flat :=
 215  discreteVacuumEinsteinInput_of_variationFormula_of_separating
 216    K hK h_flat hFirst hFormula R.separating
 217
 218end
 219
 220end DiscreteVacuumEinstein
 221end Gravity
 222end IndisputableMonolith
 223