deficitOnNonHinge
plain-language theorem explainer
The definition sets the curvature deficit to zero for any non-hinge stratum in a simplicial ledger. Physicists modeling Regge calculus or discrete gravity cite it to localize curvature exclusively to codimension-two hinges. The declaration is a direct assignment of the constant zero.
Claim. For any simplicial ledger $L$ and non-hinge stratum $s$ (a 3-simplex interior or shared 2-face), the deficit is defined by $deficit(s) := 0$.
background
The module establishes flat Euclidean or Minkowski interiors for every 3-simplex, so that loops through codimension-0 or codimension-1 strata acquire no holonomy. NonHingeStratum is the inductive type whose constructors are interior($σ$) for a single 3-simplex and face($σ_1,σ_2$) for a shared 2-face; both are declared curvature-free by the flat-interior axiom. Upstream, the deficit function itself is taken from the dihedral-angle sum $2π - Σ θ$, while SimplicialLedger supplies the underlying collection of simplices.
proof idea
This is a direct definition that assigns the constant zero to the deficit on every non-hinge stratum.
why it matters
It supplies the zero value used by the theorem curvature_only_on_hinges and by the master certificate InteriorFlatCert that closes Beltracchi §7. In the Recognition framework the definition enforces curvature support on codimension-2 hinges, aligning with the eight-tick octave and the forced spatial dimension D=3.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.