radical_one_eq
radical(1) equals 1 follows directly from the definition of the radical as the product of distinct prime factors. Number theorists working with arithmetic functions in the Recognition Science layer would cite this identity as the base case for multiplicative calculations and square-free decompositions. The proof is a one-line wrapper that applies native_decide to evaluate the definition at n=1.
claim$rad(1)=1$, where $rad(n)$ denotes the product of the distinct prime factors of the positive integer $n$.
background
The module supplies lightweight wrappers around Mathlib arithmetic functions, beginning with the Möbius function and related objects such as the radical. The radical is defined directly as the product of the distinct prime factors of n via n.primeFactors.prod id. This supplies the value at the unit element under that definition.
proof idea
The proof is a one-line wrapper that applies the native_decide tactic to evaluate the definition of radical at 1.
why it matters in Recognition Science
This identity anchors the arithmetic functions module and supplies the n=1 case required for consistent multiplicative properties. It supports later Möbius and square-free results in the Recognition Science number theory layer, though no downstream theorems are recorded yet. The result closes the base case for radical computations without invoking deeper forcing chain steps.
scope and limits
- Does not prove radical values for any n greater than 1.
- Does not relate radical to the Möbius function or other arithmetic functions.
- Does not extend the definition beyond natural numbers.
formal statement (Lean)
855theorem radical_one_eq : radical 1 = 1 := by native_decide
proof body
Term-mode proof.
856
857/-- rad(n) > 0 for n > 0. -/