D_quad1_not_axisAdditive
plain-language theorem explainer
The theorem establishes that the candidate correction f(d) = d(d-1)/4 fails axis additivity on natural numbers. Researchers deriving the unique tau-step coefficient W + D/2 in Recognition Science lepton generations would cite it to exclude this quadratic alternative. The proof is a short term-mode contradiction: assume additivity, specialize to inputs 1 and 1, unfold the definition, and obtain a numerical mismatch via norm_num.
Claim. Let $f : ℕ → ℝ$ be given by $f(d) = d(d-1)/4$. Then $f$ is not axis-additive, i.e., it is not the case that $f(0) = 0$ and $f(a+b) = f(a) + f(b)$ for all natural numbers $a,b$.
background
The module TauStepExclusivity proves that the alpha-correction coefficient in the tau generation step must be exactly W + D/2 once one imposes an admissible class of dimension-dependent corrections. AxisAdditive is the key predicate: a function f : ℕ → ℝ satisfies f(0) = 0 and f(a + b) = f(a) + f(b) for all a, b ∈ ℕ, which forces linearity f(d) = d · f(1). The sibling definition correction_D_quad1 supplies the concrete quadratic candidate f(d) = d(d-1)/4, one of several numerically coincident but algebraically distinct alternatives to D/2 that all evaluate to 1.5 when D = 3.
proof idea
The term proof proceeds by contradiction. Assume AxisAdditive correction_D_quad1. Extract the additivity conjunct and instantiate it at a = 1, b = 1 to obtain correction_D_quad1(2) = 2 · correction_D_quad1(1). Unfold the definition of correction_D_quad1 and apply norm_num to reach the false equality 0.5 = 0.
why it matters
This result belongs to the second category of alternatives in the module (numerically coincident at D = 3 but algebraically distinct). By showing that D(D-1)/4 violates axis additivity, it eliminates one of the non-linear candidates and thereby supports the uniqueness claim for the linear term D/2 inside the tau-step formula. The argument directly implements the exclusivity principles stated in the module doc-comment and is consistent with the Recognition Science requirement that admissible corrections respect independent-axis additivity in D = 3.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.