meshGeometricDeficit_sign
plain-language theorem explainer
The mesh geometric deficit preserves sign of the real deformation parameter: positive hinge stretch gives positive deficit, negative gives negative. Gravity analysts cite it when extracting dual-entry sources as κ·δ. Proof is a one-line transfer of the four-tetrahedra star deficit sign lemma.
Claim. For every real deformation parameter $h$, if $h>0$ then the mesh geometric deficit at $h$ is strictly positive, and if $h<0$ then the mesh geometric deficit at $h$ is strictly negative.
background
This module closes Wave B residual R1 for quantum-gravity completion: identify the mesh geometric deficit with signed Regge-convention hinge geometry on the recognition Freudenthal mesh, without any $x$-ratio or log-ratio carrier.
The deformation carrier is a real parameter $h$. The geometric object is the four-tetrahedra star deficit (signed angle deficit around a hinge from squared-edge lengths). Sibling facts already record that the mesh geometric deficit equals that star deficit, is odd, vanishes on the flat seed, and matches the arcsin/Regge conventions used downstream.
Upstream, fourTet_deficit_sign certifies the same strict sign law for the abstract star deficit. The mesh context is supplied by the exact-$J$ equals true-Regge Hessian identity on the canonical recognition mesh, together with Freudenthal seed flatness (star angle sum $2\pi$).
proof idea
One-line term proof: apply the upstream four-tetrahedra star deficit sign theorem at the same real parameter $h$. Because the mesh geometric deficit is definitionally (or already equated to) that star deficit, the conjunction of the two implications transfers verbatim.
why it matters
Sign certification is part of the R1 package that inhabits the typed residual "mesh geometric deficit identified from exact-$J$/Regge star geometry." Downstream, meshDualEntrySource_eq multiplies hinge stiffness $\kappa$ by this deficit $\delta$ to recover the dual-entry source; the trichotomy on $h$ needs the deficit to keep the correct sign so the constitutive product is oriented.
In the broader Recognition gravity stack this is local geometry bookkeeping on the recognition mesh, not a forcing-chain step (T5–T8). It does not flip the gap-1 bridge flag and does not claim a constitutive deficit-source coupling or a derived recognition ratio. The recorded open remainder is lifting star deficit onto a concrete deficitAngle field of an encoded Freudenthal triangulation.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.