starDeficit_odd
plain-language theorem explainer
The signed star deficit on the abstract four-tetrahedron hinge family is an odd function of the deformation parameter: flipping h flips the sign of the deficit. Anyone working signed Regge deficits, the weak-field pair certificate, or the 4D mesh geometric residual cites this. The proof rewrites the deficit as four times arcsin and applies the classical oddness of arcsin, then closes by ring.
Claim. For every real $h$, the signed four-tet star deficit satisfies $\mathrm{deficit}(-h)=-\mathrm{deficit}(h)$.
background
The module builds signed Regge-convention deficit angles on an abstract four-tetrahedron hinge star: four congruent tets share an interior hinge AB in a closed 4-cycle link, given as squared-edge data and certified nondegenerate by the Cayley-Menger sign. On the kernel-checked slice with hinge and leg squares equal to 1, the common dihedral cosine at the hinge is the rational parameter $q=h$, and the star-local deficit collapses to
$$\mathrm{deficit}(h)=2\pi-4\arccos(h)=4\arcsin(h).$$
The geometric reading is for $|h|<1$ (nondegenerate); the algebraic identity is stated for all real $h$ because arcsin is constant outside $[-1,1]$. The deformation family is chosen so that the sign of the deficit is exactly the sign of the rational hinge cosine, with no interval arithmetic required.
proof idea
Term-mode rewrite proof. Both sides are rewritten by the characterization that identifies the star deficit with four times arcsin of the deformation parameter. Classical oddness of real arcsin (Real.arcsin_neg) turns the left-hand side into a negated arcsin; a final ring equates the two sides. No geometric nondegeneracy hypothesis is needed.
why it matters
This is the algebraic half of the signed-deficit contact certificate for the four-tet star. Downstream, fourTet_weak_pair quotes the exact antisymmetry clause $\mathrm{deficit}(-h^2)=-\mathrm{deficit}(+h^2)$ as item 3 of the weak-field Test B pair. The gravity analysis layer lifts it verbatim to mesh geometric deficit oddness, and the typed residual package includes the oddness witness when it closes residual R1 (mesh geometric deficit identified). In the broader Recognition geometry stack it supplies the sign-reversal needed so that positive and negative curvature sources can be paired without ad-hoc sign conventions.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.