radical_360
plain-language theorem explainer
The radical of 360, the product of its distinct prime factors, equals 30. Researchers maintaining bridge lemmas in Recognition Science cite this to avoid recomputing the factorization of 360 each time it appears with 8 or 45. The proof reduces the equality to a single native decision procedure on natural-number arithmetic.
Claim. The product of the distinct prime factors of 360 equals 30, i.e., $2·3·5=30$.
background
The RSConstants module assembles small, decidable arithmetic facts about integers that recur in the reality repo, including 8, 45, 360 and 840 together with selected primes. These facts function as stable anchors so that later lemmas remain readable without repeated arithmetic proofs. The radical of a natural number is defined as the product of its distinct prime factors; the present declaration records the value for 360.
proof idea
The proof is a one-line wrapper that invokes the native_decide tactic, which evaluates the left-hand side (360).primeFactors.prod id directly inside the kernel and confirms equality with 30.
why it matters
The declaration supplies a concrete numerical anchor inside NumberTheory.Primes.RSConstants, supporting the surrounding collection of facts for 8, 45, 360 and 840. It keeps factorizations involving the eight-tick octave (period 2^3) and the lcm of 8 and 45 readable when these quantities appear in phi-ladder or J-cost calculations. No downstream theorems are recorded yet, but the fact closes a small computational gap that would otherwise be re-proved in multiple bridge lemmas.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.