even_ledger_cannot_match_signed_regge
plain-language theorem explainer
No even real function of a deformation parameter can coincide with a signed deficit family on a punctured neighborhood of the flat point. Anyone arguing that ledger J-deficits cannot reproduce signed Regge star deficits cites this parity obstruction. The proof is a two-point evaluation at ±h₀/2 plus evenness and the sign hypothesis, closed by linarith.
Claim. Let $\delta,g:\mathbb{R}\to\mathbb{R}$ and $h_0>0$. Suppose that for every $h$ with $0<h<h_0$ one has $\delta(h)>0$ and $\delta(-h)<0$, and that $g$ is even: $g(-h)=g(h)$ for all $h$. Then it is false that $g(h)=\delta(h)$ for all $h$ with $0<|h|<h_0$.
background
The ambient module builds an abstract four-tetrahedron hinge star from squared-edge data: four congruent tets around a common hinge AB, certified nondegenerate by Cayley-Menger ($\mathrm{cm}_3>0$). On the slice $\ell=m=1$ the flat equatorial edge is $p_0=3/2$; the deformation $p(h)=(3/2)(1-h)$ yields dihedral cosine $q=h$ and star deficit $\delta(h)=2\pi-4\arccos(h)=4\arcsin(h)$, so $\mathrm{sign}(\delta)=\mathrm{sign}(h)$ without evaluating arccos in the kernel.
Upstream, hinge deficit is the classical Regge quantity $2\pi-\sum\theta$ (DihedralAngle / Schlaefli). Ledger deficit is a separate non-negative cost sum on a recognition ledger; this lemma never mentions either object. The doc-comment states the intended composition with the seven-gaps parity no-go (ledger J-deficits are even in the deformation), but the import firewall keeps that composition outside this lane.
proof idea
Assume for contradiction a pointwise match $g=\delta$ on $0<|h|<h_0$. Take the interior test point $h_0/2$ (positive by half_pos, strictly below $h_0$ by half_lt_self). The sign hypothesis supplies $\delta(h_0/2)>0$ and $\delta(-(h_0/2))<0$. Absolute-value rewrites put both $\pm h_0/2$ inside the match domain, so $g(h_0/2)=\delta(h_0/2)$ and $g(-(h_0/2))=\delta(-(h_0/2))$. Evenness rewrites the second equality to $g(h_0/2)=\delta(-(h_0/2))$. Then $\delta(h_0/2)>0$ and $\delta(-(h_0/2))<0$ contradict equality by linarith. No geometric lemmas are invoked.
why it matters
This is the pure algebraic half of the parity no-go separating even ledger J-costs from signed Regge star deficits. Downstream, even_cannot_match_starDeficit instantiates it on the explicit starDeficit family with $h_0=1$, using fourTet_deficit_sign for the sign hypothesis. The module's goal is the first kernel-checked signed Regge-convention deficits on an abstract four-tet star; this lemma shows no even deformation response can track that signed family near flatness.
In the Recognition framework it supports the seven-gaps campaign's LedgerBridgeNoGo story: ledger J-deficits are even, signed star deficits are odd in sign, so they cannot match. The composition is deliberately not performed here (import firewall). It does not touch T0–T8 forcing, RCL, or the mass ladder; it is a local geometry/ledger interface fact.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.