IndisputableMonolith.Gravity.ReggeComponentTheorem3D

   1import Mathlib.Data.Real.Basic
   2import IndisputableMonolith.Geometry.ReggeHessian3D
   3import IndisputableMonolith.Gravity.WeakFieldConformalRegge
   4
   5/-!
   6# 3D Regge Component Theorem Bridge
   7
   8This module connects the genuine 3D Regge Hessian package to the existing
   9weak-field conformal Regge bridge.  The geometric computation supplies a
  10`GenuineComponentPackage`; this file turns it into the existing
  11`ReggeComponentComparison` interface and therefore into the Dirichlet-form
  12reduction already proved in `WeakFieldConformalRegge`.
  13-/
  14
  15namespace IndisputableMonolith
  16namespace Gravity
  17namespace ReggeComponentTheorem3D
  18
  19open Geometry.ReggeTriangulation3D
  20open Geometry.ReggeHessian3D
  21open WeakFieldConformalRegge
  22open Foundation.SimplicialLedger.EdgeLengthFromPsi
  23
  24noncomputable section
  25
  26/-- The genuine geometric component package produced by the
  27Cayley-Menger/dihedral/Hessian computation. -/
  28structure GenuineComponentPackage (K : Triangulation3D) where
  29  W : WeakFieldReggeData K.nV
  30  geometricArea : Fin K.nV → Fin K.nV → ℝ
  31  geometricArea_symm : ∀ i j, geometricArea i j = geometricArea j i
  32  geometricArea_nonneg : ∀ i j, 0 ≤ geometricArea i j
  33  offDiag_component_match :
  34    ∀ i j, i ≠ j → bilinearCoefficient W i j = - geometricArea i j
  35  schlaefli_row_sum : SchlaefliRowSum W
  36
  37/-- A genuine component package instantiates the existing comparison
  38interface. -/
  39def componentComparison_of_genuine
  40    {K : Triangulation3D} (G : GenuineComponentPackage K) :
  41    ReggeComponentComparison G.W where
  42  geometricArea := G.geometricArea
  43  geometricArea_symm := G.geometricArea_symm
  44  geometricArea_nonneg := G.geometricArea_nonneg
  45  offDiag_component_match := G.offDiag_component_match
  46  schlaefli_row_sum := G.schlaefli_row_sum
  47
  48/-- The existing weak-field reduction applies to the genuine component
  49package. -/
  50theorem genuine_component_dirichlet_reduction
  51    {K : Triangulation3D} (G : GenuineComponentPackage K)
  52    (ε : LogPotential K.nV) :
  53    secondOrderReggeAction G.W ε =
  54      (1 / 2) * dirichletForm (edgeArea G.W) ε :=
  55  weak_field_conformal_reduction G.W G.schlaefli_row_sum ε
  56
  57end
  58
  59end ReggeComponentTheorem3D
  60end Gravity
  61end IndisputableMonolith
  62