`forty_five_factorization`

proved

show as: view math explainer →

module: IndisputableMonolith.Gap45.Derivation
domain: Gap45
line: 124 · github
papers citing: none yet

open explainer

Generate a durable explainer page for this declaration.

open lean source

IndisputableMonolith.Gap45.Derivation on GitHub at line 124.

browse module

All declarations in this module, on Recognition.

explainer page

Tracked in the explainer inventory; generation is lazy so crawlers do not trigger LLM jobs.

open explainer

depends on

formal source

 121theorem forty_five_eq_nine_times_five : (45 : ℕ) = 9 * 5 := rfl
 122
 123/-- 45's prime factorization: 3² × 5. -/
 124theorem forty_five_factorization : (45 : ℕ) = 3^2 * 5 := by decide
 125
 126/-! ## LCM with Eight-Tick -/
 127
 128/-- The full synchronization period. -/
 129def full_period : ℕ := Nat.lcm eight_tick_period gap
 130
 131/-- **Key Result**: lcm(8, 45) = 360. -/
 132@[simp] theorem full_period_eq_360 : full_period = 360 := by
 133  simp [full_period, eight_tick_period, gap]
 134  decide
 135
 136/-- 360 = 8 × 45 (since gcd(8, 45) = 1). -/
 137theorem full_period_is_product : full_period = eight_tick_period * gap := by
 138  native_decide
 139
 140/-- The number of eight-tick cycles in a full period. -/
 141theorem cycles_of_eight : full_period / eight_tick_period = gap := by
 142  native_decide
 143
 144/-- The number of gap cycles in a full period. -/
 145theorem cycles_of_gap : full_period / gap = eight_tick_period := by
 146  native_decide
 147
 148/-! ## D=3 Forcing -/
 149
 150/-- For D dimensions, the power of 2 is 2^D. -/
 151def power_of_two (D : ℕ) : ℕ := 2^D
 152
 153/-- lcm(2^D, 45) = 360 only when D = 3. -/
 154theorem lcm_360_forces_D_eq_3 :

papers checked against this theorem

No papers in the current corpus map onto this theorem yet.