DeficitAngleFunctional
plain-language theorem explainer
DeficitAngleFunctional packages an abstract deficit map and area map from conformal edge-length fields to real numbers, together with area positivity, for use on an n-vertex graph. Regge-calculus and discrete-gravity workers cite it when constructing the simplicial side of the J-cost to Regge bridge. The declaration is a pure structure with no proof obligations or computational content.
Claim. A deficit-angle functional on an $n$-vertex simplicial complex consists of maps $L,hmapsto delta(L,h)$ and $L,h mapsto A(L,h)$ from conformal edge-length fields $L$ to hinge data $h$, together with the axiom that $A(L,h)ge0$ for all such $L$ and $h$.
background
The module supplies the missing map from the recognition-potential field psi on simplices to an edge-length field L_e together with the linearization that converts log-potential differences into deficit angles. EdgeLengthField is the structure whose length component satisfies the conformal ansatz L_{ij}=a exp((epsilon_i + epsilon_j)/2) and reduces to constant spacing when all epsilon vanish. HingeDatum collects the list of edges incident to a hinge together with nonnegative weights that become shared-face areas in the continuum limit. Upstream, ContinuumBridge.as records the identification (1/2) sum w_{ij}(epsilon_i - epsilon_j)^2 = (1/kappa) sum delta_h A_h with kappa=8 phi^5.
proof idea
The declaration is a structure definition that introduces the DeficitAngleFunctional type with its three fields; no tactics or lemmas are applied.
why it matters
This structure carries the Regge action S_Regge = sum A_h delta_h inside the simplicial ledger. It is instantiated by cubicDeficitFunctional and supplies the type for the invariance theorems in CubicSimplicialEquivalence, including the master diagnostic CubicSimplicialInvarianceCert that equates the cubic and simplicial presentations of the J-cost to Regge identification. It closes the gap in the Gravity from Recognition draft section 5 by packaging the deficit map required for the field-curvature identity, pending discharge of the ReggeDeficitLinearizationHypothesis.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.