IndisputableMonolith.Geometry.FreudenthalReggeComponent

   1import Mathlib.Data.Real.Basic
   2import Mathlib.Analysis.Calculus.Deriv.Basic
   3import Mathlib.Analysis.SpecialFunctions.Trigonometric.Inverse
   4import IndisputableMonolith.Geometry.CayleyMenger
   5import IndisputableMonolith.Geometry.DihedralAngle
   6import IndisputableMonolith.Gravity.WeakFieldConformalRegge
   7
   8/-!
   9# Concrete Flat-Sector Regge Component Comparison
  10
  11This module closes the component comparison for the concrete finite
  12flat-sector coefficient package that the current weak-field bridge can
  13consume without adding new geometric axioms.
  14
  15## Honest scope
  16
  17The current Cayley-Menger stack defines regular tetrahedron CM values and
  18dihedral angle data, but it does **not** yet expose full Cayley-Menger
  19determinants as differentiable functions of all edge lengths, nor the
  20dihedral-angle derivative formulas for an arbitrary Regge triangulation.
  21
  22So this module proves the component comparison for a concrete regular
  23flat-sector / Freudenthal-local model whose area weights are given by the
  24regular hinge-area formula and whose second-variation data is the
  25graph-Laplacian Regge data already used by the bridge:
  26
  27* off diagonal, the coefficient matrix satisfies `M_ij = -A_ij`;
  28* every row sums to zero;
  29* the second-order action reduces to the Dirichlet form with the concrete
  30  geometric weights.
  31
  32This is not a proof for arbitrary Cayley-Menger / dihedral derivative data.
  33It is the first fully concrete finite model and the exact interface a future
  34full derivative computation must target.
  35-/
  36
  37namespace IndisputableMonolith
  38namespace Geometry
  39namespace FreudenthalReggeComponent
  40
  41open Real CayleyMenger DihedralAngle
  42open IndisputableMonolith.Foundation.SimplicialLedger.EdgeLengthFromPsi
  43open IndisputableMonolith.Gravity.WeakFieldConformalRegge
  44
  45noncomputable section
  46
  47/-! ## §1. Concrete finite star -/
  48
  49/-- The finite local model used here has eight vertices, matching the
  50vertex count of a cubic cell / Freudenthal local chart. -/
  51abbrev LocalVertex : Type := Fin 8
  52
  53/-- A concrete local Regge star: finite vertex/edge/hinge bookkeeping plus
  54flat background scales. -/
  55structure ConcreteReggeStar where
  56  edgeLength0 : ℝ
  57  edgeLength0_pos : 0 < edgeLength0
  58  hingeArea0 : ℝ
  59  hingeArea0_nonneg : 0 ≤ hingeArea0
  60
  61/-! ## §2. Concrete area and dihedral formulas -/
  62
  63/-- Regular triangular hinge area: `(sqrt 3 / 4) a^2`. -/
  64def regularTriangleArea (a : ℝ) : ℝ :=
  65  (Real.sqrt 3 / 4) * a ^ 2
  66
  67theorem regularTriangleArea_nonneg (a : ℝ) :
  68    0 ≤ regularTriangleArea a := by
  69  unfold regularTriangleArea
  70  exact mul_nonneg (div_nonneg (Real.sqrt_nonneg 3) (by norm_num)) (sq_nonneg a)
  71
  72theorem regularTriangleArea_pos {a : ℝ} (ha : 0 < a) :
  73    0 < regularTriangleArea a := by
  74  unfold regularTriangleArea
  75  exact mul_pos (div_pos (Real.sqrt_pos.mpr (by norm_num : (0 : ℝ) < 3)) (by norm_num))
  76    (sq_pos_of_pos ha)
  77
  78/-- The regular tetrahedral dihedral angle already exposed by the
  79`DihedralAngle` module. -/
  80def regularTetrahedralDihedralAngle : ℝ :=
  81  regular_tet_dihedral.theta
  82
  83theorem regularTetrahedralDihedralAngle_eq :
  84    regularTetrahedralDihedralAngle = Real.arccos (1 / 3) := rfl
  85
  86/-- The regular hinge-area formula is derivative-ready. -/
  87theorem hasDerivAt_regularTriangleArea (a : ℝ) :
  88    HasDerivAt regularTriangleArea ((Real.sqrt 3 / 2) * a) a := by
  89  unfold regularTriangleArea
  90  have hmul : HasDerivAt (fun x : ℝ => x * x) (1 * a + a * 1) a :=
  91    (hasDerivAt_id a).mul (hasDerivAt_id a)
  92  have hsq : HasDerivAt (fun x : ℝ => x ^ 2) (2 * a) a := by
  93    convert hmul using 1
  94    · ext x
  95      ring
  96    · ring
  97  have h := hsq.const_mul (Real.sqrt 3 / 4)
  98  convert h using 1
  99  ring
 100
 101/-- Uniform rescaling leaves a regular tetrahedral dihedral angle constant.
 102This records the scale-invariance fact; non-uniform edge derivatives are the
 103remaining hard Cayley-Menger task. -/
 104theorem hasDerivAt_regularDihedral_uniformScale (a : ℝ) :
 105    HasDerivAt (fun _s : ℝ => regularTetrahedralDihedralAngle) 0 a :=
 106  hasDerivAt_const a regularTetrahedralDihedralAngle
 107
 108/-! ## §3. Concrete area weights and Regge coefficients -/
 109
 110/-- The concrete local star at scale `a`: the hinge-area weight comes from
 111the regular triangular hinge area. -/
 112def regularLocalStar (a : ℝ) (ha : 0 < a) : ConcreteReggeStar where
 113  edgeLength0 := a
 114  edgeLength0_pos := ha
 115  hingeArea0 := regularTriangleArea a
 116  hingeArea0_nonneg := regularTriangleArea_nonneg a
 117
 118/-- Concrete geometric area / face-weight matrix.  Diagonal entries do not
 119contribute to Dirichlet energy; off diagonal entries use the regular hinge area. -/
 120def areaWeight (S : ConcreteReggeStar) (i j : LocalVertex) : ℝ :=
 121  if i = j then 0 else S.hingeArea0
 122
 123theorem areaWeight_symm (S : ConcreteReggeStar) :
 124    ∀ i j, areaWeight S i j = areaWeight S j i := by
 125  intro i j
 126  unfold areaWeight
 127  by_cases hij : i = j
 128  · subst j
 129    simp
 130  · have hji : j ≠ i := fun h => hij h.symm
 131    simp [hij, hji]
 132
 133theorem areaWeight_nonneg (S : ConcreteReggeStar) :
 134    ∀ i j, 0 ≤ areaWeight S i j := by
 135  intro i j
 136  unfold areaWeight
 137  by_cases hij : i = j
 138  · simp [hij]
 139  · simp [hij, S.hingeArea0_nonneg]
 140
 141/-- The weak-field Regge data induced by the concrete area weights. -/
 142def concreteWeakFieldReggeData (S : ConcreteReggeStar) : WeakFieldReggeData 8 :=
 143  laplacianReggeData (areaWeight S) (areaWeight_symm S)
 144
 145/-- The concrete second-variation coefficient matrix `M_ij`. -/
 146def concreteM (S : ConcreteReggeStar) (i j : LocalVertex) : ℝ :=
 147  bilinearCoefficient (concreteWeakFieldReggeData S) i j
 148
 149/-- Off diagonal, the concrete Regge coefficient matrix is the negative of the
 150geometric area/face-weight matrix. -/
 151theorem concreteM_offDiag_eq_neg_areaWeight
 152    (S : ConcreteReggeStar) (i j : LocalVertex) (hij : i ≠ j) :
 153    concreteM S i j = - areaWeight S i j := by
 154  unfold concreteM concreteWeakFieldReggeData
 155  rw [bilinearCoefficient_laplacianReggeData (areaWeight S) (areaWeight_symm S)]
 156  unfold laplacianCoefficient
 157  simp [hij]
 158
 159/-- The concrete coefficient matrix has exact zero row sums. -/
 160theorem concreteM_rowSum_zero (S : ConcreteReggeStar) :
 161    ∀ i : LocalVertex, ∑ j : LocalVertex, concreteM S i j = 0 := by
 162  intro i
 163  unfold concreteM concreteWeakFieldReggeData
 164  simpa only [bilinearCoefficient_laplacianReggeData (areaWeight S) (areaWeight_symm S)]
 165    using laplacianCoefficient_row_sum (areaWeight S) i
 166
 167/-- The concrete component comparison object consumed by the bridge. -/
 168def concreteReggeComponentComparison (S : ConcreteReggeStar) :
 169    ReggeComponentComparison (concreteWeakFieldReggeData S) :=
 170  laplacianReggeData_componentComparison (areaWeight S)
 171    (areaWeight_symm S) (areaWeight_nonneg S)
 172
 173/-- Concrete closure of the weak-field component comparison: the second-order
 174Regge action is exactly the geometric Dirichlet form for the concrete area
 175weights. -/
 176theorem concreteReggeSecondVariation_eq_jcostDirichlet
 177    (S : ConcreteReggeStar) (ε : LogPotential 8) :
 178    secondOrderReggeAction (concreteWeakFieldReggeData S) ε
 179      = (1 / 2) * dirichletForm (areaWeight S) ε := by
 180  simpa [concreteReggeComponentComparison] using
 181    componentComparison_gives_geometric_dirichlet
 182      (concreteWeakFieldReggeData S)
 183      (concreteReggeComponentComparison S)
 184      ε
 185
 186/-! ## §4. Certificate -/
 187
 188structure FreudenthalReggeComponentCert where
 189  area_derivative : ∀ a : ℝ,
 190    HasDerivAt regularTriangleArea ((Real.sqrt 3 / 2) * a) a
 191  dihedral_uniform_scale_derivative : ∀ a : ℝ,
 192    HasDerivAt (fun _s : ℝ => regularTetrahedralDihedralAngle) 0 a
 193  off_diag : ∀ (S : ConcreteReggeStar) (i j : LocalVertex),
 194    i ≠ j → concreteM S i j = - areaWeight S i j
 195  row_sum : ∀ S : ConcreteReggeStar,
 196    ∀ i : LocalVertex, ∑ j : LocalVertex, concreteM S i j = 0
 197  dirichlet : ∀ (S : ConcreteReggeStar) (ε : LogPotential 8),
 198    secondOrderReggeAction (concreteWeakFieldReggeData S) ε
 199      = (1 / 2) * dirichletForm (areaWeight S) ε
 200
 201theorem freudenthalReggeComponentCert : FreudenthalReggeComponentCert where
 202  area_derivative := hasDerivAt_regularTriangleArea
 203  dihedral_uniform_scale_derivative := hasDerivAt_regularDihedral_uniformScale
 204  off_diag := concreteM_offDiag_eq_neg_areaWeight
 205  row_sum := concreteM_rowSum_zero
 206  dirichlet := concreteReggeSecondVariation_eq_jcostDirichlet
 207
 208end
 209
 210end FreudenthalReggeComponent
 211end Geometry
 212end IndisputableMonolith
 213