even_cannot_match_starDeficit
plain-language theorem explainer
No even real function of the deformation parameter can equal the four-tetrahedron star Regge deficit on the punctured interval 0 < |h| < 1. Gravity analysts cite this when excluding ledger-style (parity-even) deficit candidates against the signed mesh geometric deficit. The proof is a direct specialization of the algebraic parity no-go at radius h₀ = 1, feeding the four-tet sign certificate.
Claim. Let $g:\mathbb{R}\to\mathbb{R}$ be even, i.e. $g(-h)=g(h)$ for all $h$. Then $g$ cannot coincide with the star-local Regge deficit $\delta_\star$ on the punctured interval $0<|h|<1$: it is false that $\forall h$ with $0<|h|<1$ one has $g(h)=\delta_\star(h)$.
background
The module builds an abstract four-tetrahedron hinge star: four congruent tets share an interior edge AB in a closed 4-cycle link, given as squared-edge data certified nondegenerate by Cayley-Menger (cm3 > 0). On the slice l = m = 1 the deformation p(h) = (3/2)(1-h) forces the common hinge cosine to equal h, so the star deficit is $\delta_\star(h) = 2\pi - 4\arccos(h) = 4\arcsin(h)$ in the weak-field window |h| < 1.
By definition the hinge deficit is $2\pi$ minus the sum of incident dihedral angles. The contact certificate fourTet_deficit_sign states that the sign of $\delta_\star(h)$ equals the sign of h: positive h gives positive deficit, negative h gives negative deficit. Upstream, even_ledger_cannot_match_signed_regge is the pure algebraic parity fact: no even g can equal any signed family $\delta$ that flips sign across a punctured interval of radius h₀ > 0.
proof idea
One-line term specialization of even_ledger_cannot_match_signed_regge at h₀ = 1 (via one_pos). The sign hypothesis is discharged by packaging both halves of fourTet_deficit_sign: for 0 < h < 1 one gets 0 < δ_★(h), and for the reflected argument one gets δ_★(-h) < 0. The evenness assumption on g is passed through unchanged. No new geometry is proved here.
why it matters
This is the concrete instantiation of the algebraic parity no-go on the explicit star-deficit family, with mesh bound |h| < 1. Downstream it is banked as the decoy decoy_even_function_ne_mesh_geometricDeficit in RecognitionMeshGeometricDeficit4D (any even-in-h candidate cannot equal the signed mesh geometric deficit) and feeds the closed typed residual TypedResidual_mesh_geometricDeficit_identified_closed.
In the broader Recognition picture it is the geometric half of the intended composition with the seven-gaps ledger parity no-go: ledger J-deficits are even in the deformation parameter, while the Regge star deficit is odd in sign, so no ledger-style even family can match the signed geometric deficit. That composition is disclosed upstream but not discharged in this declaration.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.