radical_twelve'
plain-language theorem explainer
The declaration establishes that the radical of twelve equals six. Number theorists working with arithmetic functions and prime factor products would cite this as a basic verification step. The proof is a direct computational evaluation of the radical definition on the input twelve.
Claim. Let $r(n)$ denote the product of the distinct prime factors of the natural number $n$. Then $r(12) = 6$.
background
The radical function is defined as the product of the distinct prime factors of a natural number. This module supplies lightweight wrappers around arithmetic functions, beginning with the Möbius function and related constructs such as the radical, keeping statements minimal until deeper Dirichlet algebra is added.
proof idea
The proof is a one-line term that applies native_decide to evaluate the radical definition directly on the concrete input twelve.
why it matters
This equality provides a basic sanity check for the radical definition inside the arithmetic functions module. It supports the broader number-theoretic scaffolding that includes Möbius inversion and square-free properties, though no downstream uses are recorded. In the Recognition Science framework it aligns with the prime-related structures needed for the forcing chain steps from T5 onward.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.