radical_sixty
plain-language theorem explainer
The statement asserts that the radical of 60 equals 30. Number theorists referencing concrete evaluations of the square-free kernel in arithmetic function libraries would cite this result. The proof is a one-line wrapper that invokes native_decide on the prime-factor product definition.
Claim. $rad(60) = 30$, where $rad(n)$ denotes the product of the distinct prime factors of the natural number $n$.
background
The module supplies lightweight wrappers around Mathlib arithmetic functions, beginning with the Möbius function and the radical. The radical is defined as the product of the distinct prime factors of its argument. This evaluation sits inside the NumberTheory.Primes.ArithmeticFunctions development that prepares Dirichlet-algebra tools.
proof idea
The proof is a one-line wrapper that applies native_decide to the definition radical n := n.primeFactors.prod id evaluated at 60.
why it matters
This concrete check anchors the radical definition inside the arithmetic-functions module. It supplies a verified base case that later Möbius and square-free lemmas can reference, consistent with the Recognition Science emphasis on explicit number-theoretic footholds before inversion formulas are layered on.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.