axisAdditive_linear
plain-language theorem explainer
Any function f from naturals to reals obeying axis additivity (f(0)=0 and f(a+b)=f(a)+f(b)) is necessarily linear, f(d)=d*f(1). Researchers deriving the unique D/2 coefficient in the tau generation step of lepton masses would cite this to exclude algebraically distinct alternatives that only match numerically at D=3. The proof runs by induction on d, applying the additivity axiom at each successor and simplifying via ring and cast lemmas.
Claim. If $f : ℕ → ℝ$ satisfies $f(0)=0$ and $f(a+b)=f(a)+f(b)$ for all $a,b ∈ ℕ$, then $f(d)=(d:ℝ)·f(1)$ for every $d ∈ ℕ$.
background
The Tau Step Coefficient Exclusivity module shows that the α-correction term in step_μ→τ = F - (W + D/2)·α must be exactly D/2. AxisAdditive encodes the physical requirement that independent axes contribute additively with no constant term: f(0)=0 ∧ ∀ a b, f(a+b)=f(a)+f(b). This rules out candidates such as E/8 or D(D-1)/4 that agree with D/2 only when D=3 but differ elsewhere.
proof idea
Induction on d. The zero case uses the f(0)=0 clause directly. The successor step invokes additivity to obtain f(d+1)=f(d)+f(1), substitutes the induction hypothesis, and closes with ring plus Nat.cast_succ, add_assoc, add_comm, and add_left_comm from the arithmetic foundation.
why it matters
This result supplies the linearity needed for admissible_unique, which then calibrates at d=3 to conclude every admissible correction equals d/2 and thereby forces the tau coefficient. It implements the axis-additivity exclusivity principle stated in the module, closing one branch of the forcing chain that selects D=3 and the observed lepton mass ratios.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.