AxisAdditive
plain-language theorem explainer
AxisAdditive defines the property that a function f from naturals to reals satisfies f(0)=0 and f(a+b)=f(a)+f(b) for all a,b. Physicists deriving the unique coefficient in the tau lepton generation step cite it to enforce additive contributions from independent axes. The definition directly encodes the two axioms as a Prop for use in admissibility structures.
Claim. A function $f : ℕ → ℝ$ is axis-additive if $f(0) = 0$ and $f(a + b) = f(a) + f(b)$ for all $a, b ∈ ℕ$.
background
The TauStepExclusivity module introduces axis additivity to select admissible corrections in the tau generation step formula step_μ→τ = F - (W + D/2) · α. It distinguishes algebraically equivalent forms such as F/4 = D/2 from numerically coincident but distinct alternatives like E/8 or D(D-1)/4 that match at D=3 yet violate the additivity requirement in other dimensions.
proof idea
This is the direct definition of the Prop. It packages the zero-offset condition together with the additive functional equation on ℕ.
why it matters
AxisAdditive supplies the first-principles filter used by AdmissibleCorrection to combine axis additivity with calibration f(3)=3/2, which then feeds axisAdditive_linear to obtain uniqueness of the D/2 term. In the Recognition framework it implements the requirement that corrections respect independent axes, thereby excluding the non-additive alternatives shown in D_quad1_not_axisAdditive, D_quad2_not_axisAdditive and E_eighth_not_axisAdditive while aligning with the eight-tick octave and D=3 spatial dimensions.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.