theorem proved term proof

`D1_fails_sync`

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

formal statement (Lean)

 408theorem D1_fails_sync : Nat.lcm (2 ^ 1) 45 ≠ 360 := by native_decide

Term-mode proof.

 409
 410/-- **THEOREM**: D = 2 fails (lcm(4,45) = 180 ≠ 360). -/