210theorem refinement_calibrated {n : ℕ} 211 (a : ℝ) (ha : 0 < a) (G : WeightedLedgerGraph n) 212 (R_at : ∀ ε : LogPotential n, 213 SimplicialRefinement (cubicDeficitFunctional n) 214 (conformal_edge_length_field a ha ε) (cubicHinges G)) : 215 ∀ ε : LogPotential n, 216 regge_sum (cubicDeficitFunctional n) 217 (conformal_edge_length_field a ha ε) (R_at ε).hinges 218 = jcost_to_regge_factor * laplacian_action G ε :=
proof body
Term-mode proof.
219 refinement_discharge_inherits a ha G R_at 220 221/-! ## §5. Diagnostic: the equivalence is fully invariant -/ 222 223/-- **MASTER DIAGNOSTIC.** The cubic and simplicial presentations 224 of the same ledger data produce the **same** J-cost ↔ Regge 225 identification, under the only physically reasonable hypothesis 226 that internal (diagonal) hinges of the simplicial refinement 227 carry zero deficit on the conformal field. 228 229 This is the Lean-level answer to Philip's §5 concern: one can 230 work on cubes or on simplices; the J-cost ↔ Regge identity is 231 the same equation, with the same coupling `κ = 8 φ⁵`. The 232 triangulation is a choice of *presentation*, not of physics. -/
depends on (37)
Lean names referenced from this declaration's body.