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

sync_implies_D3

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)

 346theorem sync_implies_D3 : 2^3 ∣ sync_period := by

proof body

Term-mode proof.

 347  rw [sync_period_eq_360]
 348  use 45; rfl
 349
 350/-! ## Combined Forcing -/
 351
 352/-- A dimension is RS-compatible if it satisfies all forcing conditions:
 353    1. Supports non-trivial linking (ledger conservation)
 354    2. 2^D = 8 (eight-tick synchronization)
 355    3. Compatible with gap-45 sync -/

depends on (22)

Lean names referenced from this declaration's body.