theorem
proved
three_almost_prime_fiftytwo
show as:
view math explainer →
open explainer
Read the cached plain-language explainer.
open lean source
IndisputableMonolith.NumberTheory.Primes.ArithmeticFunctions on GitHub at line 2071.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
formal source
2068theorem three_almost_prime_fifty : isThreeAlmostPrime 50 = true := by native_decide
2069
2070/-- 52 = 2² × 13 is 3-almost prime. -/
2071theorem three_almost_prime_fiftytwo : isThreeAlmostPrime 52 = true := by native_decide
2072
2073/-- 63 = 3² × 7 is 3-almost prime. -/
2074theorem three_almost_prime_sixtythree : isThreeAlmostPrime 63 = true := by native_decide
2075
2076/-- 66 = 2 × 3 × 11 is 3-almost prime (RS-relevant: 11). -/
2077theorem three_almost_prime_sixtysix : isThreeAlmostPrime 66 = true := by native_decide
2078
2079/-- 68 = 2² × 17 is 3-almost prime (RS-relevant: 17). -/
2080theorem three_almost_prime_sixtyeight : isThreeAlmostPrime 68 = true := by native_decide
2081
2082/-- 70 = 2 × 5 × 7 is 3-almost prime. -/
2083theorem three_almost_prime_seventy : isThreeAlmostPrime 70 = true := by native_decide
2084
2085/-- 75 = 3 × 5² is 3-almost prime. -/
2086theorem three_almost_prime_seventyfive : isThreeAlmostPrime 75 = true := by native_decide
2087
2088/-- 76 = 2² × 19 is 3-almost prime. -/
2089theorem three_almost_prime_seventysix : isThreeAlmostPrime 76 = true := by native_decide
2090
2091/-! ### σ_2 and σ_3 for RS constants -/
2092
2093/-- σ_2(45) (RS constant). -/
2094theorem sigma_two_fortyfive : sigma 2 45 = 2366 := by native_decide
2095
2096-- Note: σ_2(360) and σ_3 values for large numbers require careful computation
2097-- Leaving those for future sessions when we can verify the exact values
2098
2099/-! ### Balanced primes ((p_{n-1} + p_{n+1})/2 = p_n) -/
2100
2101/-- 5 is a balanced prime: (3 + 7)/2 = 5. -/