D_quad1_not_axisAdditive

formal source

 205  norm_num at h22
 206
 207/-- D(D-1)/4 is not axis-additive (witness: 1+1). -/
 208theorem D_quad1_not_axisAdditive : ¬ AxisAdditive correction_D_quad1 := by
 209  intro h
 210  rcases h with ⟨h0, hadd⟩
 211  have h11 : correction_D_quad1 (1 + 1) = correction_D_quad1 1 + correction_D_quad1 1 := hadd 1 1
 212  unfold correction_D_quad1 at h11
 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)