theorem
proved
threehundredsixty_factorization
show as:
view math explainer →
open explainer
Read the cached plain-language explainer.
open lean source
IndisputableMonolith.NumberTheory.Primes.RSConstants on GitHub at line 54.
browse module
All declarations in this module, on Recognition.
explainer page
formal source
51theorem lcm_eight_fortyfive_eq_360 : Nat.lcm 8 45 = 360 := by
52 native_decide
53
54theorem threehundredsixty_factorization : (360 : ℕ) = 2^3 * 3^2 * 5 := by
55 native_decide
56
57theorem wheel840_factorization : (840 : ℕ) = 2^3 * 3 * 5 * 7 := by
58 native_decide
59
60/-! ### Rational identities (beat-frequency arithmetic) -/
61
62theorem one_div_eight_sub_one_div_fortyfive :
63 (1 : ℚ) / 8 - (1 : ℚ) / 45 = (37 : ℚ) / 360 := by
64 norm_num
65
66theorem aliasing_ratio : (37 : ℚ) / 45 < 1 := by
67 norm_num
68
69/-! ### Integer identities (beat numerator as a difference) -/
70
71/-- The RS beat numerator arises as a simple difference: \(45 - 8 = 37\). -/
72theorem fortyfive_sub_eight_eq_thirtyseven : (45 : ℕ) - 8 = 37 := by
73 native_decide
74
75/-- Convenience wrapper: 8 and 45 are coprime. -/
76theorem coprime_eight_fortyfive : Nat.Coprime 8 45 := by
77 native_decide
78
79/-! ### vp-based characterizations of RS constants -/
80
81/-- The prime spectrum of 8: only has 2-content, with exponent 3. -/
82theorem vp_eight_two : vp 2 8 = 3 := by native_decide
83theorem vp_eight_three : vp 3 8 = 0 := by native_decide
84theorem vp_eight_five : vp 5 8 = 0 := by native_decide