E_eighth_not_axisAdditive
plain-language theorem explainer
Correction term E/8 fails axis additivity on natural numbers. Lepton generation derivations cite it to discard edge-based alpha corrections in favor of the linear D/2 term. The term-mode proof assumes the additivity axioms, instantiates them at 2+2, unfolds via cube_edges, and reaches a numerical falsehood by normalization.
Claim. Let $f(d) = d · 2^{d-1}/8$. It is not the case that $f(0)=0$ and $f(a+b)=f(a)+f(b)$ for all natural numbers $a,b$.
background
AxisAdditive encodes the requirement that independent axes contribute additively with no offset: a function $f$ on natural numbers satisfies $f(0)=0$ and $f(a+b)=f(a)+f(b)$ for all $a,b$. Any such $f$ must be linear, $f(d)=d·f(1)$. The correction_E_eighth is the map $d ↦$ cube_edges$(d)/8$, where cube_edges$(d)=d·2^{d-1}$ counts the edges of the $d$-dimensional hypercube.
proof idea
Assume AxisAdditive correction_E_eighth. Specialize the additivity clause to obtain correction_E_eighth$(2+2)=$ correction_E_eighth$(2)+$ correction_E_eighth$(2)$. Unfold the definition of correction_E_eighth and simplify using the cube_edges formula. Normalization then produces the contradictory equation $4=1$.
why it matters
This declaration eliminates the edge-count correction E/8 from contention in the tau generation step. It supports the parent claim that only the axis-additive linear term D/2 survives among the numerically equivalent candidates at D=3. The result fits the Recognition Science program of deriving lepton masses from the phi-ladder and the eight-tick structure without additional hypotheses.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.