`forty_five_factorization`

proved

show as: view math explainer →

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

open explainer

Read the cached plain-language explainer.

open lean source

IndisputableMonolith.Gap45.Derivation on GitHub at line 124.

browse module

All declarations in this module, on Recognition.

explainer page

A cached Ask Recognition explainer exists for this declaration.

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.