pith. machine review for the scientific record. sign in
theorem proved term proof

D_quad2_not_axisAdditive

show as:
view Lean formalization →

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

generate prose now

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`. -/

depends on (8)

Lean names referenced from this declaration's body.