decoy_even_function_ne_mesh_geometricDeficit
plain-language theorem explainer
Any even real function of the hinge deformation cannot equal the signed mesh geometric deficit on the punctured interval 0 < |h| < 1. Gravity analysts closing Wave B residual R1 cite this to kill ledger-style even deficit families. Proof is a one-line wrapper of the banked star-deficit even-function obstruction.
Claim. For every even map $g:\mathbb{R}\to\mathbb{R}$ (i.e. $g(-h)=g(h)$ for all $h$), it is false that $g(h)$ equals the signed mesh geometric deficit for every $h$ with $0<|h|<1$.
background
Wave B residual R1 identifies the mesh geometric deficit with the banked signed Regge-convention star deficit, free of ratio fields and logarithms. The deformation carrier is a real parameter $h$; the mesh geometric deficit is defined as the star-local hinge deficit $2\pi$ minus four equal dihedral angles of congruent incident tetrahedra, computed from squared-edge geometry.
That star deficit is odd in $h$, vanishes at the flat point, and carries a certified sign. Classical hinge deficit is $2\pi-\sum\theta$; the star family instantiates the same convention on an abstract four-tetrahedron star. Ledger-style candidates that are even in $h$ (magnitude-only extracts, even posited ratios) are the adversarial decoys this module rules out.
Upstream, even_cannot_match_starDeficit already states the obstruction for the explicit star family on $|h|<1$ with $h_0=1$, using the signed-Regge vs even-ledger mismatch.
proof idea
One-line term wrapper: apply the banked theorem that no even $g$ can match the star deficit on the punctured unit interval, then use definitional equality of the mesh geometric deficit with that star deficit. No new algebra; the sign certificate and oddness live upstream in the four-tet signed-deficit development.
why it matters
Closes the first adversarial decoy for Wave B residual R1 (mesh geometric deficit identified, no xRatio). Downstream it feeds the packaged pair of DAG decoys, the magnitude-only even extract obstruction, and the log-of-even-ratio-over-kappa decoy that blocks smuggling a ratio field into the deficit.
In the Recognition gravity stack this protects the claim that the residual is the genuine signed Regge hinge deficit of the recognition mesh carrier, not an even ledger functional. It does not flip the gap-1 bridge flag, inhabit constitutive coupling, or claim recognition-ratio derivation. The remaining open join is lifting the star deficit onto an encoded Freudenthal triangulation deficit angle; that lift is still recorded as open.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.