theorem proved term proof

`D5_fails_sync`

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

formal statement (Lean)

 417theorem D5_fails_sync : Nat.lcm (2 ^ 5) 45 ≠ 360 := by native_decide

Term-mode proof.

 418
 419/-- **THEOREM**: Only D = 3 gives lcm(2^D, 45) = 360 for D ∈ {1,...,8}. -/

Lean names referenced from this declaration's body.

for in IndisputableMonolith.Foundation.UniversalForcingSelfReference decl_use