E_eighth_not_axisAdditive
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.
claimLet $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 in Recognition Science
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.
scope and limits
- Does not verify axis additivity of the D/2 term itself.
- Does not derive the explicit value of the tau mass.
- Does not rule out other functional forms outside the listed alternatives.
- Does not extend the argument to non-integer dimensions.
formal statement (Lean)
197theorem E_eighth_not_axisAdditive : ¬ AxisAdditive correction_E_eighth := by
proof body
Term-mode proof.
198 intro h
199 rcases h with ⟨h0, hadd⟩
200 have h22 : correction_E_eighth (2 + 2) = correction_E_eighth 2 + correction_E_eighth 2 := hadd 2 2
201 -- compute both sides
202 unfold correction_E_eighth at h22
203 simp [cube_edges] at h22
204 -- LHS = 4, RHS = 1
205 norm_num at h22
206
207/-- D(D-1)/4 is not axis-additive (witness: 1+1). -/