IndisputableMonolith.Constants.CurvatureCostForm

   1import Mathlib
   2import IndisputableMonolith.Constants.LambdaRecDerivation
   3import IndisputableMonolith.Foundation.JCostHessianC7
   4import IndisputableMonolith.Geometry.ReggeActionConcrete
   5
   6/-!
   7# Curvature Cost Form
   8
   9This module is the M2B bridge from the living plan
  10`plans/Regge_To_JCurv_CostForm_Closure_Plan_20260617.html`.
  11
  12It records two facts.
  13
  141. The bulk Regge/Dirichlet quadratic cannot be the source of the one-cell
  15   curvature cost under a uniform conformal scale: constant vertex potentials
  16   are graph-Laplacian zero modes.
  172. The boundary angle-defect cost has a theorem-tier quadratic form:
  18   the local J-cost Hessian coefficient is `1`, and the Gauss-Bonnet defect
  19   coefficient is `χ(∂Q₃) = 2`, so the quadratic boundary cost is `2 λ²`.
  20
  21Honest boundary: the theorem below closes the quadratic FORM used by
  22`J_curv`; it does not claim the full nonlinear expression `Jcost (1 + λ)` is
  23exactly `λ²`. In fact `Jcost (1 + λ) = λ² / (2(1+λ))` away from `λ = -1`.
  24The theorem-grade statement is the Hessian/quadratic-form statement.
  25-/
  26
  27namespace IndisputableMonolith
  28namespace Constants
  29namespace CurvatureCostForm
  30
  31open Geometry
  32open Geometry.ReggeActionConcrete
  33open Geometry.ReggeHessian3D
  34open Geometry.ReggeTriangulation3D
  35open Geometry.Triangulation3DConsistency
  36
  37noncomputable section
  38
  39/-! ## M1: bulk Regge uniform-scale zero mode -/
  40
  41/-- Constant vertex potentials are zero modes of the canonical Dirichlet
  42energy. This is the formal reason the bulk Regge Hessian does not carry the
  43single-cell uniform-scale curvature cost: the Dirichlet quadratic only sees
  44differences `ξ i - ξ j`. -/
  45theorem canonicalDirichletEnergy_constant_zero
  46    (K : Triangulation3D) (hK : IncidenceConsistent K) (c : ℝ) :
  47    canonicalDirichletEnergy K hK (fun _ : Fin K.nV => c) = 0 := by
  48  unfold canonicalDirichletEnergy
  49  simp
  50
  51/-! ## M2B: boundary angle-defect J-cost quadratic form -/
  52
  53open LambdaRecDerivation
  54
  55/-- Boundary Gauss-Bonnet coefficient of the one-cell curvature cost:
  56total angular defect in units of one full turn. -/
  57abbrev boundaryDefectCoefficient : ℝ :=
  58  curvatureCoefficient
  59
  60/-- The boundary coefficient is the Euler characteristic of the cube boundary. -/
  61theorem boundaryDefectCoefficient_eq_euler_char :
  62    boundaryDefectCoefficient = (euler_S2 : ℝ) :=
  63  curvatureCoefficient_eq_euler_char
  64
  65/-- The local J-cost Hessian coefficient is `1`. This imports the exact
  66local-algebra theorem `J(1+ε) = ε² / (2(1+ε))` through its standard Hessian
  67normalization. -/
  68theorem localJCostHessianCoefficient_eq_one :
  69    Foundation.JCostHessianC7.jcostHessianCoefficient = 1 :=
  70  Foundation.JCostHessianC7.jcostHessianCoefficient_eq_one
  71
  72/-- Boundary curvature-cost quadratic form: Gauss-Bonnet defect coefficient
  73times the J-cost Hessian coefficient times `λ²`. -/
  74def boundaryCurvatureQuadraticCost (lam : ℝ) : ℝ :=
  75  boundaryDefectCoefficient *
  76    Foundation.JCostHessianC7.jcostHessianCoefficient *
  77      lam ^ (2 : ℕ)
  78
  79/-- The boundary angle-defect J-cost quadratic form is exactly `2 λ²`.
  80
  81This is the form-level closure: the `2` comes from Gauss-Bonnet
  82(`χ(∂Q₃) = 2`) and the quadratic dependence comes from the Hessian of the
  83canonical reciprocal cost at equilibrium. -/
  84theorem boundaryCurvatureQuadraticCost_eq (lam : ℝ) :
  85    boundaryCurvatureQuadraticCost lam = 2 * lam ^ (2 : ℕ) := by
  86  unfold boundaryCurvatureQuadraticCost boundaryDefectCoefficient
  87  rw [curvatureCoefficient_eq_euler_char, localJCostHessianCoefficient_eq_one]
  88  norm_num [euler_S2]
  89
  90/-- The existing `J_curv` definition agrees with the theorem-derived boundary
  91quadratic form. This isolates the only intended meaning of `J_curv`: it is the
  92quadratic boundary angle-defect J-cost, not the bulk Regge Dirichlet energy and
  93not the full nonlinear `Jcost (1+λ)`. -/
  94theorem J_curv_eq_boundaryCurvatureQuadraticCost (lam : ℝ) :
  95    LambdaRecDerivation.J_curv lam = boundaryCurvatureQuadraticCost lam := by
  96  rw [LambdaRecDerivation.J_curv_derivation, boundaryCurvatureQuadraticCost_eq]
  97
  98/-- M2B certificate: bulk uniform scaling is a Regge zero mode, while the
  99boundary angle-defect quadratic cost equals the existing `J_curv`. -/
 100structure CurvatureCostFormCert where
 101  bulk_uniform_scale_zero :
 102    ∀ (K : Triangulation3D) (hK : IncidenceConsistent K) (c : ℝ),
 103      canonicalDirichletEnergy K hK (fun _ : Fin K.nV => c) = 0
 104  boundary_cost_eq :
 105    ∀ lam : ℝ, LambdaRecDerivation.J_curv lam = boundaryCurvatureQuadraticCost lam
 106  boundary_cost_closed :
 107    ∀ lam : ℝ, boundaryCurvatureQuadraticCost lam = 2 * lam ^ (2 : ℕ)
 108  coefficient_is_euler :
 109    boundaryDefectCoefficient = (euler_S2 : ℝ)
 110  j_hessian_one :
 111    Foundation.JCostHessianC7.jcostHessianCoefficient = 1
 112
 113/-- The curvature-cost form certificate is inhabited. -/
 114def curvatureCostFormCert : CurvatureCostFormCert where
 115  bulk_uniform_scale_zero := canonicalDirichletEnergy_constant_zero
 116  boundary_cost_eq := J_curv_eq_boundaryCurvatureQuadraticCost
 117  boundary_cost_closed := boundaryCurvatureQuadraticCost_eq
 118  coefficient_is_euler := boundaryDefectCoefficient_eq_euler_char
 119  j_hessian_one := localJCostHessianCoefficient_eq_one
 120
 121end
 122
 123end CurvatureCostForm
 124end Constants
 125end IndisputableMonolith
 126