DeficitAngleFunctional

formal source

 133    deficit angle at each hinge. Abstract — the concrete implementation
 134    is left to downstream modules (via Cayley–Menger or via the
 135    Piran–Williams 3+1 split). -/
 136structure DeficitAngleFunctional (n : ℕ) where
 137  deficit : EdgeLengthField n → HingeDatum n → ℝ
 138  area : EdgeLengthField n → HingeDatum n → ℝ
 139  area_pos : ∀ L h, 0 ≤ area L h
 140
 141/-- The Regge action on a list of hinges, as defined by the functional:
 142    `S_Regge = Σ_h A_h · δ_h`. -/
 143def regge_sum {n : ℕ} (D : DeficitAngleFunctional n) (L : EdgeLengthField n)
 144    (hinges : List (HingeDatum n)) : ℝ :=
 145  (hinges.map (fun h => D.area L h * D.deficit L h)).sum
 146
 147/-! ## §3. The linearization hypothesis
 148
 149The key geometric statement that the draft paper's Theorem 5.1 needs, but
 150does not prove, is that the deficit angle at a hinge is a linear combination
 151of log-potential differences at leading order in ε. This is the statement
 152Piran–Williams / Brewin compute for specific triangulations, and that
 153Cheeger–Müller–Schrader (1984) establish at `O(a²)` for well-shaped
 154simplicial approximations to smooth Riemannian metrics.
 155
 156We package this as a `Prop`-valued hypothesis with explicit coefficient
 157data. When the hypothesis holds, the bridge from J-cost to Regge becomes
 158a genuine equation of independently-defined quantities. -/
 159
 160/-- The linearization hypothesis for a deficit-angle functional `D` around
 161    the flat vacuum `ε ≡ 0`.
 162
 163    **Content.** There exist signed linearization coefficients
 164    `c h i j : ℝ` (one per hinge, per ordered vertex pair) and a Dirichlet
 165    weight `w : Fin n → Fin n → ℝ` such that
 166    `Σ_h A_h · δ_h(L(ε)) = (1/κ) · (1/2) Σ_{i,j} w_{ij} (ε_i - ε_j)²`