D_quad2_not_axisAdditive
plain-language theorem explainer
The map sending dimension d to d²/6 fails axis additivity on the naturals. Researchers deriving the tau generation coefficient in Recognition Science cite the result to rule out quadratic alternatives to the linear D/2 term. The proof assumes additivity, specializes the functional equation to 1+1, unfolds the correction, and obtains an immediate numerical contradiction.
Claim. The function $f(d) = d^2/6$ is not axis-additive: it violates either $f(0)=0$ or $f(a+b)=f(a)+f(b)$ for natural numbers $a,b$.
background
The Tau Step Coefficient Exclusivity module establishes that the coefficient in the tau generation step must be exactly W + D/2 once an admissible class of dimension-dependent corrections is fixed. AxisAdditive requires a map f : ℕ → ℝ to obey f(0)=0 together with f(a+b)=f(a)+f(b) for all a,b; any such map is necessarily linear. The alternatives D²/6, D(D-1)/4 and E/8 all evaluate to the same number at D=3 yet differ algebraically from D/2 in other dimensions, so axis additivity eliminates them.
proof idea
Assume AxisAdditive correction_D_quad2. Extract the additivity clause and instantiate at 1+1 to obtain correction_D_quad2(2) = 2·correction_D_quad2(1). Unfold the definition of correction_D_quad2 and apply norm_num; the resulting equality is false.
why it matters
The theorem removes D²/6 from the admissible corrections for the tau step, thereby supporting the module's main claim that only the linear term D/2 survives. It directly implements the axis-additivity principle required by the Recognition Science forcing chain (T5–T8) to keep the coefficient independent of the choice of quadratic or edge-based representatives.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.