even_and_odd_forces_zero
plain-language theorem explainer
An even real function and an odd real function that agree pointwise must both vanish at every point. Gravity and discrete-geometry workers cite it when a J-cost (even) ledger deficit is forced to match a signed Regge (odd) linear response. The proof is a four-line calc reducing agreement to d(ε)=-d(ε), then linarith.
Claim. Let $g,d:\mathbb{R}\to\mathbb{R}$. If $g$ is even ($g(-\varepsilon)=g(\varepsilon)$ for all $\varepsilon$), $d$ is odd ($d(-\varepsilon)=-d(\varepsilon)$ for all $\varepsilon$), and $g(\varepsilon)=d(\varepsilon)$ for all $\varepsilon$, then for every $\varepsilon\in\mathbb{R}$ one has $g(\varepsilon)=0$ and $d(\varepsilon)=0$.
background
Lane 1a of the Seven Gaps program obstructs the assumed ledger-to-hinge bridge that equates recognition-ledger cell deficit with raw geometric hinge deficit. Ledger deficit is a sum of J-costs, hence nonnegative and, under natural ratio parity $r(-\varepsilon)=r(\varepsilon)^{-1}$, an even function of the deformation parameter (via $J(x)=J(1/x)$). Weak-field Regge hinge deficit is signed and odd at leading order.
The present lemma is the pure parity exclusion that closes that comparison: even and odd functions can agree only by vanishing. Upstream geometry supplies the signed deficit $2\pi-\sum\theta$ at a hinge; the recognition ledger supplies the nonnegative cell cost sum. No deeper RS constants enter the argument.
proof idea
Tactic proof, no external lemmas. From pointwise agreement and evenness of $g$, rewrite $d(\varepsilon)=g(\varepsilon)=g(-\varepsilon)=d(-\varepsilon)$, then apply oddness of $d$ to obtain $d(\varepsilon)=-d(\varepsilon)$. linarith yields $d(\varepsilon)=0$; agreement transfers the zero to $g(\varepsilon)$. The conjunction is immediate.
why it matters
This is the algebraic engine of the parity no-go in LedgerBridgeNoGo. The module doc routes it into the linear-response corollaries: a signed assignment $\delta(\varepsilon)=c\cdot\varepsilon$ with $c\neq 0$ admits no J-ratio realization on any symmetric interval, and no parity-covariant J-ratio ledger family has a deficit with signed linear response. Together with the sign no-go (ledger deficit nonnegative vs. two-sided negative geometric hinges), it blocks the assumed form of the substrate-to-triangulation bridge on two-sided weak-field deformation classes. The geometric premise that such classes contain negative-deficit hinges remains prose-tier, outside this formalization.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.