D_quad2_not_axisAdditive
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.
claimThe 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 in Recognition Science
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.
scope and limits
- Does not claim D²/6 fails additivity outside the naturals.
- Does not compare D²/6 with the admissible linear term beyond the contradiction.
- Does not derive the explicit closed form of correction_D_quad2.
- Does not address empirical constraints or the value of alpha.
formal statement (Lean)
216theorem D_quad2_not_axisAdditive : ¬ AxisAdditive correction_D_quad2 := by
proof body
Term-mode proof.
217 intro h
218 rcases h with ⟨h0, hadd⟩
219 have h11 : correction_D_quad2 (1 + 1) = correction_D_quad2 1 + correction_D_quad2 1 := hadd 1 1
220 unfold correction_D_quad2 at h11
221 norm_num at h11
222
223/-! ## Part 7: Main statement (uniqueness within the admissible class) -/
224
225/-- **Main theorem**: any admissible correction is exactly `D/2`. -/