meshGeometricDeficit_odd
plain-language theorem explainer
The mesh geometric deficit is odd in the hinge deformation: flipping the sign of h flips the sign of the deficit. Gravity analysts in the Wave B residual program cite it to kill even decoys (magnitude-only extracts and log-ratio couplings). Proof is a one-line wrapper: the mesh deficit is definitionally the banked star deficit, which is already odd.
Claim. For every real deformation parameter $h$, the mesh geometric deficit satisfies $\delta_{\mathrm{mesh}}(-h)=-\delta_{\mathrm{mesh}}(h)$.
background
In this module the mesh geometric deficit is the banked signed Regge-convention star deficit, viewed as a real function of a single deformation parameter. It is built from squared-edge and dihedral geometry (starSq, dihedralAngle3Sq); no recognition ratio and no logarithm enter the definition. Definitionally it is just starDeficit from the four-tetrahedron signed-deficit library.
The local setting is Wave B residual R1: identify a signed Regge-convention hinge deficit for the recognition Freudenthal mesh carrier, free of xRatio. Lean has no HingeCarrier type yet, so the honest binding uses a real deformation parameter with the abstract-star deficit, mesh context via the exact-J / true-Regge Hessian bridge on the canonical recognition mesh, and the banked Freudenthal seed flatness (star angle sum $2\pi$).
Upstream, starDeficit_odd already records that the star deficit is odd: $\mathrm{deficit}(-h)=-\mathrm{deficit}(h)$, proved by rewriting to arcsin and using $\arcsin(-x)=-\arcsin(x)$.
proof idea
One-line wrapper. Because meshGeometricDeficit is defined to be starDeficit, the claim is exactly starDeficit_odd applied to $h$. No extra algebra.
why it matters
Oddness is the structural fact that separates the signed mesh geometric deficit from even decoys in the dual-entry and hinge-kappa analyses. Downstream, the magnitude-only decoy theorem uses it to show $|\delta|$ is even and cannot equal the signed deficit on a punctured interval. The log-ratio-over-deficit decoy uses it to force an odd quotient while the named constitutive unit coupling meshHingeKappa is the nonzero constant $1$.
In the QG Wave B residual DAG this sits inside residual R1 (mesh geometric deficit identified, no xRatio). It does not flip gap1_bridge_derived, does not inhabit constitutive coupling, and does not claim recognition-ratio derivation. The recorded open remainder remains: lift the star deficit onto ReggeActionConcrete.deficitAngle on an encoded triangulation of the recognition Freudenthal mesh (encodedFreudenthalLiftOpen).
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.