theorem proved term proof

`D4_fails_sync`

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

formal statement (Lean)

 414theorem D4_fails_sync : Nat.lcm (2 ^ 4) 45 ≠ 360 := by native_decide

Term-mode proof.

 415
 416/-- **THEOREM**: D = 5 fails (lcm(32,45) = 1440 ≠ 360). -/