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)
78theorem sync_counts :
79 Nat.lcm 8 45 = 360 ∧ Nat.lcm 8 45 / 8 = 45 ∧ Nat.lcm 8 45 / 45 = 8 := by
proof body
Term-mode proof.
80 exact ⟨lcm_8_45_eq_360, lcm_8_45_div_8, lcm_8_45_div_45⟩
81
82/-- The beat-level clock-lag fraction implied by the 45-gap arithmetic: δ_time = 45/960 = 3/64. -/
depends on (10)
Lean names referenced from this declaration's body.
-
lcm_8_45_div_45
in IndisputableMonolith.Gap45
decl_use
-
lcm_8_45_div_8
in IndisputableMonolith.Gap45
decl_use
-
lcm_8_45_eq_360
in IndisputableMonolith.Gap45
decl_use
-
lcm_8_45_div_45
in IndisputableMonolith.Gap45.Beat
decl_use
-
lcm_8_45_div_8
in IndisputableMonolith.Gap45.Beat
decl_use
-
lcm_8_45_eq_360
in IndisputableMonolith.Gap45.Beat
decl_use
-
gap
in IndisputableMonolith.Gap45.Derivation
decl_use
-
gap
in IndisputableMonolith.Masses.AnchorPolicy
decl_use
-
gap
in IndisputableMonolith.Masses.RSBridge.Anchor
decl_use
-
gap
in IndisputableMonolith.RSBridge.Anchor
decl_use