radical_fortyfive
plain-language theorem explainer
The declaration shows that the product of the distinct prime factors of 45 equals 15. Researchers maintaining the Recognition Science constant table cite it to keep later bridge lemmas free of repeated arithmetic. The proof is a one-line native_decide wrapper that evaluates the factorization directly.
Claim. The product of the distinct prime factors of 45 equals 15, i.e., $3·5=15$.
background
The module collects small, decidable arithmetic facts about integers that recur in the reality repo, such as the numbers 8, 45, 360, and 840 together with selected primes. These anchors keep bridge lemmas readable by avoiding repeated factorization proofs. The upstream identity morphisms from CostAlgebra, ArithmeticOf, UniversalForcingSelfReference, and Octave supply only the trivial maps needed for the native decision procedure.
proof idea
One-line wrapper that applies native_decide to the expression (45 : ℕ).primeFactors.prod id.
why it matters
It supplies a stable arithmetic anchor inside the RSConstants module, whose purpose is to hold the small facts that appear repeatedly when constructing the phi-ladder and octave structures. The declaration fills the concrete factorization slot for 45 that later lemmas on wheel numbers and gcd relations rely upon. No open question is touched; the result is fully discharged.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.