deficitOnNonHinge
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.
claimFor 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 in Recognition Science
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.
scope and limits
- Does not compute nonzero deficits at hinges.
- Does not prove existence of flat interior metrics.
- Does not extend the zero-deficit rule beyond 3-simplices.
formal statement (Lean)
175def deficitOnNonHinge {L : SimplicialLedger.SimplicialLedger}
176 (_s : NonHingeStratum L) : ℝ := 0
proof body
Definition body.
177
178/-- Zero-deficit on non-hinge strata is a definitional theorem. -/