meshGeometricDeficit_flat
plain-language theorem explainer
The mesh geometric deficit vanishes at zero deformation. Anyone identifying the Regge-hinge residual or dual-entry constitutive source on the recognition mesh cites this flat-point normalization. The proof is a one-line wrapper of banked star-deficit flatness, since the mesh deficit is definitionally that signed star deficit.
Claim. The mesh geometric deficit at vanishing deformation is zero: $\delta_{\mathrm{mesh}}(0)=0$, where $\delta_{\mathrm{mesh}}$ is the signed Regge-convention star deficit of the recognition mesh, viewed as a function of the deformation parameter.
background
This module closes Wave B residual R1: identify a mesh geometric deficit free of ratio or log-ratio carriers. The honest binding uses a real deformation parameter and the banked four-tetrahedron signed star deficit (Regge convention from squared-edge and dihedral geometry), not a per-hinge angle family on an encoded Freudenthal triangulation.
The mesh geometric deficit is defined to be exactly that star deficit: an odd, flat-vanishing, sign-certified map built from squared-edge data and three-square dihedral angles. Upstream, star-deficit flatness states that the deficit is zero at the flat value (deformation parameter zero, corresponding to the flat edge-square configuration). Mesh context is supplied by the exact-J versus true-Regge Hessian bridge on the canonical recognition mesh, with Freudenthal seed flatness already banked.
proof idea
One-line wrapper. Unfolding the definition, the mesh geometric deficit is identical to the star deficit, so the claim is exactly the upstream theorem that the star deficit vanishes at zero deformation. That upstream proof rewrites the star deficit via its arcsin closed form and applies $\arcsin 0 = 0$.
why it matters
Flat vanishing is the normalization every residual and constitutive coupling needs: no fictitious source when the mesh is undeformed. Downstream, the dual-entry source equality factors the extracted source as hinge stiffness times this geometric deficit; at zero deformation both factors and the product stay consistent with a pure geometric residual.
In the QG Wave B plan this is part of residual R1 (mesh geometric deficit identified without ratio carriers). It does not close the open lift of the star deficit onto a concrete triangulation deficit angle, nor flip the gap-1 bridge or inhabit a full deficit-source constitutive coupling. It is the elementary flat-point lemma that keeps the Regge-convention residual honest before those larger joins.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.