D_quad2_not_axisAdditive

formal source

 213  norm_num at h11
 214
 215/-- D²/6 is not axis-additive (witness: 1+1). -/
 216theorem D_quad2_not_axisAdditive : ¬ AxisAdditive correction_D_quad2 := by
 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`. -/
 226theorem tau_correction_unique_admissible (f : ℕ → ℝ) (h : AdmissibleCorrection f) :
 227    ∀ d : ℕ, f d = correction_D_half d := by
 228  intro d
 229  have := admissible_unique f h d
 230  simpa [correction_D_half] using this
 231
 232/-! ## Summary
 233
 234**The Exclusivity Proof**:
 235
 2361. Among the proposed alternatives {D/2, F/4, E/8, D(D-1)/4, D²/6}:
 237   - F/4 = D/2 algebraically (not a distinct alternative)
 238   - E/8, D(D-1)/4, D²/6 violate axis additivity (they are not sums of per-axis contributions)
 239
 2402. Under the admissible class (axis-additive + calibrated at D=3), the correction term is unique:
 241   `f(D) = D/2`.
 242
 243**Conclusion**: the dimension contribution in the tau step coefficient is uniquely `D/2`
 244within the stated admissible correction class.
 245-/
 246