IndisputableMonolith.Geometry.ReggeHessian3D

   1import Mathlib.Data.Real.Basic
   2import Mathlib.Algebra.BigOperators.Group.Finset.Basic
   3import IndisputableMonolith.Geometry.SchlaefliTriangulation3D
   4
   5/-!
   6# Regge Hessian Under the 3D Conformal Ansatz
   7
   8This module provides the Hessian interface for the genuine Regge action on
   9a finite 3D triangulation.  The analytic/geometric inputs are kept
  10explicit: a concrete implementation supplies `action`, its Hessian matrix,
  11and the theorem that the quadratic Taylor coefficient is represented by
  12that matrix.
  13-/
  14
  15namespace IndisputableMonolith
  16namespace Geometry
  17namespace ReggeHessian3D
  18
  19open ReggeTriangulation3D SchlaefliTriangulation3D
  20
  21noncomputable section
  22
  23/-- Vertex conformal potentials on a finite 3D triangulation. -/
  24abbrev VertexPotential (K : Triangulation3D) := Fin K.nV → ℝ
  25
  26/-- The zero conformal potential. -/
  27def zeroPotential (K : Triangulation3D) : VertexPotential K := fun _ => 0
  28
  29/-- Quadratic form associated to a Hessian matrix. -/
  30def hessianQuadratic {n : ℕ} (H : Fin n → Fin n → ℝ) (ξ : Fin n → ℝ) : ℝ :=
  31  ∑ i : Fin n, ∑ j : Fin n, H i j * ξ i * ξ j
  32
  33/-- Genuine Regge Hessian data for a triangulation.  `action` is the
  34Regge action under the conformal ansatz, and `hessian` is the matrix of
  35its second variation at `ξ = 0`. -/
  36structure ReggeHessianData (K : Triangulation3D) where
  37  action : VertexPotential K → ℝ
  38  hessian : Fin K.nV → Fin K.nV → ℝ
  39  hessian_symm : ∀ i j, hessian i j = hessian j i
  40  flat_firstVariation_zero : Prop
  41  secondVariation :
  42    ∀ ξ : VertexPotential K,
  43      action ξ - action (zeroPotential K) =
  44        (1 / 2) * hessianQuadratic hessian ξ
  45
  46/-- Swap the order of summation in the Hessian quadratic form. -/
  47theorem hessianQuadratic_sum_comm {n : ℕ} (H : Fin n → Fin n → ℝ)
  48    (ξ : Fin n → ℝ) :
  49    hessianQuadratic H ξ =
  50      ∑ j : Fin n, ∑ i : Fin n, H i j * ξ i * ξ j := by
  51  unfold hessianQuadratic
  52  rw [Finset.sum_comm]
  53
  54/-- Extract the second-variation formula from a concrete Hessian package. -/
  55theorem regge_secondVariation_eq_hessian
  56    (K : Triangulation3D) (D : ReggeHessianData K) (ξ : VertexPotential K) :
  57    D.action ξ - D.action (zeroPotential K) =
  58      (1 / 2) * hessianQuadratic D.hessian ξ :=
  59  D.secondVariation ξ
  60
  61end
  62
  63end ReggeHessian3D
  64end Geometry
  65end IndisputableMonolith
  66