IndisputableMonolith.Gravity.ReggeComponentTheorem3DProof

   1import IndisputableMonolith.Gravity.ReggeComponentTheorem3D
   2import IndisputableMonolith.Geometry.ReggeActionConcrete
   3
   4/-!
   5# Final Regge Component Comparison Target
   6
   7This module separates the independent dual-weight construction from the
   8weak-field coefficient matrix and records the theorem that turns that
   9geometric computation into `ReggeComponentComparison`.
  10-/
  11
  12namespace IndisputableMonolith
  13namespace Gravity
  14namespace ReggeComponentTheorem3DProof
  15
  16open Geometry.ReggeTriangulation3D
  17open Geometry.ReggeActionConcrete
  18open Geometry.Triangulation3DConsistency
  19open ReggeComponentTheorem3D
  20open WeakFieldConformalRegge
  21open Foundation.SimplicialLedger.EdgeLengthFromPsi
  22
  23noncomputable section
  24
  25/-- Independent dual weights attached to vertex pairs of a triangulation.
  26These are geometric data, not defined by negating the Regge coefficient
  27matrix. -/
  28structure IndependentDualWeights (K : Triangulation3D) where
  29  weight : Fin K.nV → Fin K.nV → ℝ
  30  weight_symm : ∀ i j, weight i j = weight j i
  31  weight_nonneg : ∀ i j, 0 ≤ weight i j
  32
  33/-- A global edge contributes to the unordered vertex pair `(i,j)` exactly
  34when its endpoints are `(i,j)` or `(j,i)`. -/
  35def edgePairIncidenceWeight
  36    (K : Triangulation3D) (hK : IncidenceGeometry K)
  37    (i j : Fin K.nV) (e : Fin K.nE) : ℝ :=
  38  if (K.edgeVerts e).1 = i ∧ (K.edgeVerts e).2 = j ∨
  39      (K.edgeVerts e).1 = j ∧ (K.edgeVerts e).2 = i then
  40    Real.sqrt (hK.globalSqEdge e)
  41  else
  42    0
  43
  44/-- Independent dual/hinge weight for a vertex pair, defined directly from
  45the incidence-level edge-length chart.  It is not defined by negating a
  46Regge Hessian coefficient. -/
  47def vertexPairHingeWeight
  48    (K : Triangulation3D) (hK : IncidenceGeometry K)
  49    (i j : Fin K.nV) : ℝ :=
  50  ∑ e : Fin K.nE, edgePairIncidenceWeight K hK i j e
  51
  52theorem edgePairIncidenceWeight_symm
  53    (K : Triangulation3D) (hK : IncidenceGeometry K)
  54    (i j : Fin K.nV) (e : Fin K.nE) :
  55    edgePairIncidenceWeight K hK i j e =
  56      edgePairIncidenceWeight K hK j i e := by
  57  unfold edgePairIncidenceWeight
  58  by_cases h :
  59      (K.edgeVerts e).1 = i ∧ (K.edgeVerts e).2 = j ∨
  60        (K.edgeVerts e).1 = j ∧ (K.edgeVerts e).2 = i
  61  · have h' :
  62        (K.edgeVerts e).1 = j ∧ (K.edgeVerts e).2 = i ∨
  63          (K.edgeVerts e).1 = i ∧ (K.edgeVerts e).2 = j := by
  64      exact h.symm
  65    simp [h, h']
  66  · have h' :
  67        ¬ ((K.edgeVerts e).1 = j ∧ (K.edgeVerts e).2 = i ∨
  68          (K.edgeVerts e).1 = i ∧ (K.edgeVerts e).2 = j) := by
  69      intro hx
  70      exact h hx.symm
  71    simp [h, h']
  72
  73theorem vertexPairHingeWeight_symm
  74    (K : Triangulation3D) (hK : IncidenceGeometry K)
  75    (i j : Fin K.nV) :
  76    vertexPairHingeWeight K hK i j = vertexPairHingeWeight K hK j i := by
  77  unfold vertexPairHingeWeight
  78  refine Finset.sum_congr rfl ?_
  79  intro e _
  80  exact edgePairIncidenceWeight_symm K hK i j e
  81
  82/-- Nonnegativity of the independent incidence-defined weights, assuming the
  83global squared-edge chart is nonnegative. -/
  84theorem vertexPairHingeWeight_nonneg
  85    (K : Triangulation3D) (hK : IncidenceGeometry K)
  86    (i j : Fin K.nV) :
  87    0 ≤ vertexPairHingeWeight K hK i j := by
  88  unfold vertexPairHingeWeight edgePairIncidenceWeight
  89  refine Finset.sum_nonneg ?_
  90  intro e _
  91  by_cases h :
  92      (K.edgeVerts e).1 = i ∧ (K.edgeVerts e).2 = j ∨
  93        (K.edgeVerts e).1 = j ∧ (K.edgeVerts e).2 = i
  94  · simp [h, Real.sqrt_nonneg]
  95  · simp [h]
  96
  97/-- Incidence-defined independent dual weights. -/
  98def independentDualWeightsOfIncidence
  99    (K : Triangulation3D) (hK : IncidenceGeometry K) :
 100    IndependentDualWeights K where
 101  weight := vertexPairHingeWeight K hK
 102  weight_symm := vertexPairHingeWeight_symm K hK
 103  weight_nonneg := vertexPairHingeWeight_nonneg K hK
 104
 105/-- Independent dual weights built from an `IncidenceConsistent` chart using
 106the canonical geometry-layer incidence weights. -/
 107def independentDualWeightsOfConsistent
 108    (K : Triangulation3D) (hK : IncidenceConsistent K) :
 109    IndependentDualWeights K where
 110  weight := Geometry.ReggeActionConcrete.canonicalDualWeight K hK
 111  weight_symm := Geometry.ReggeActionConcrete.canonicalDualWeight_symm K hK
 112  weight_nonneg := Geometry.ReggeActionConcrete.canonicalDualWeight_nonneg K hK
 113
 114/-- Canonical weak-field Regge data induced by the incidence dual weights. -/
 115def canonicalWeakFieldDataOfIncidence
 116    (K : Triangulation3D) (hK : IncidenceConsistent K) :
 117    WeakFieldReggeData K.nV :=
 118  laplacianReggeData
 119    (Geometry.ReggeActionConcrete.canonicalDualWeight K hK)
 120    (Geometry.ReggeActionConcrete.canonicalDualWeight_symm K hK)
 121
 122theorem canonicalWeakFieldData_bilinearCoefficient
 123    (K : Triangulation3D) (hK : IncidenceConsistent K)
 124    (i j : Fin K.nV) :
 125    bilinearCoefficient (canonicalWeakFieldDataOfIncidence K hK) i j =
 126      Geometry.ReggeActionConcrete.canonicalReggeHessian K hK i j := by
 127  unfold canonicalWeakFieldDataOfIncidence
 128  rw [bilinearCoefficient_laplacianReggeData]
 129  rfl
 130
 131theorem canonicalWeakFieldData_rowSum
 132    (K : Triangulation3D) (hK : IncidenceConsistent K) :
 133    SchlaefliRowSum (canonicalWeakFieldDataOfIncidence K hK) :=
 134  schlaefliRowSum_laplacianReggeData
 135    (Geometry.ReggeActionConcrete.canonicalDualWeight K hK)
 136    (Geometry.ReggeActionConcrete.canonicalDualWeight_symm K hK)
 137
 138theorem canonicalWeakFieldData_offDiag_component_match
 139    (K : Triangulation3D) (hK : IncidenceConsistent K)
 140    (i j : Fin K.nV) (hij : i ≠ j) :
 141    bilinearCoefficient (canonicalWeakFieldDataOfIncidence K hK) i j =
 142      - (independentDualWeightsOfConsistent K hK).weight i j := by
 143  rw [canonicalWeakFieldData_bilinearCoefficient]
 144  exact Geometry.ReggeActionConcrete.canonicalReggeHessian_offDiag_eq_neg_weight K hK i j hij
 145
 146/-- A concrete component computation from the genuine Regge Hessian. -/
 147structure ConcreteComponentComparison (K : Triangulation3D) where
 148  W : WeakFieldReggeData K.nV
 149  dual : IndependentDualWeights K
 150  offDiag_component_match :
 151    ∀ i j, i ≠ j → bilinearCoefficient W i j = - dual.weight i j
 152  schlaefli_row_sum : SchlaefliRowSum W
 153
 154/-- The final arbitrary-triangulation component theorem target. -/
 155def FinalReggeComponentTarget : Prop :=
 156  ∀ K : Triangulation3D, IncidenceConsistent K →
 157    Nonempty (ConcreteComponentComparison K)
 158
 159/-- Concrete component comparison built from canonical incidence weights. -/
 160def concreteComponentComparisonOfIncidence
 161    (K : Triangulation3D) (hK : IncidenceConsistent K) :
 162    ConcreteComponentComparison K where
 163  W := canonicalWeakFieldDataOfIncidence K hK
 164  dual := independentDualWeightsOfConsistent K hK
 165  offDiag_component_match := canonicalWeakFieldData_offDiag_component_match K hK
 166  schlaefli_row_sum := canonicalWeakFieldData_rowSum K hK
 167
 168/-- The arbitrary-triangulation component target is discharged for the
 169canonical incidence/Laplacian second-order Regge data. -/
 170theorem finalReggeComponentTarget : FinalReggeComponentTarget := by
 171  intro K hK
 172  exact ⟨concreteComponentComparisonOfIncidence K hK⟩
 173
 174/-- A concrete component comparison constructs the existing genuine package. -/
 175def genuineComponentPackage_of_concrete
 176    {K : Triangulation3D} (C : ConcreteComponentComparison K) :
 177    GenuineComponentPackage K where
 178  W := C.W
 179  geometricArea := C.dual.weight
 180  geometricArea_symm := C.dual.weight_symm
 181  geometricArea_nonneg := C.dual.weight_nonneg
 182  offDiag_component_match := C.offDiag_component_match
 183  schlaefli_row_sum := C.schlaefli_row_sum
 184
 185/-- A final concrete component proof discharges `GenuineComponentPackage`. -/
 186theorem genuine_component_package_of_final
 187    (h : FinalReggeComponentTarget) :
 188    ∀ K : Triangulation3D, IncidenceConsistent K →
 189      Nonempty (GenuineComponentPackage K) := by
 190  intro K hK
 191  rcases h K hK with ⟨C⟩
 192  exact ⟨genuineComponentPackage_of_concrete C⟩
 193
 194/-- Once the final component package is constructed, the existing Dirichlet
 195reduction applies immediately. -/
 196theorem genuine_component_dirichlet_reduction_from_final
 197    {K : Triangulation3D} (C : ConcreteComponentComparison K)
 198    (ε : LogPotential K.nV) :
 199    secondOrderReggeAction C.W ε =
 200      (1 / 2) * dirichletForm (edgeArea C.W) ε :=
 201  genuine_component_dirichlet_reduction (genuineComponentPackage_of_concrete C) ε
 202
 203end
 204
 205end ReggeComponentTheorem3DProof
 206end Gravity
 207end IndisputableMonolith
 208