radical_eight
plain-language theorem explainer
Radical of 8 equals 2, a fixed arithmetic identity collected as a stable anchor for repeated use in Recognition Science calculations involving powers of 2. Number theorists and framework developers cite it when building bridge lemmas on prime factorizations or phi-ladders to avoid re-deriving the same fact. The proof is a one-line native decision that directly evaluates the product of distinct prime factors.
Claim. The product of the distinct prime factors of the natural number 8 equals 2.
background
The module collects small decidable arithmetic facts about integers such as 8, 45, 360, and 840 together with prime markers 11, 17, 37, 103, and 137. These act as boring but stable anchors that keep later bridge lemmas readable without repeated arithmetic proofs. The radical of a natural number is the product of its distinct prime factors.
proof idea
The proof is a one-line native decision that computes the prime factorization of 8, retains only the distinct primes, and applies the identity map to their product.
why it matters
This theorem supplies a basic anchor inside the RS constants collection used by prime factorization and wheel lemmas in NumberTheory. It fills arithmetic groundwork for structures such as phi-forcing and ledger factorizations, though the current dependency graph records no direct downstream citations.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.