squarefree_fortytwo
plain-language theorem explainer
42 factors as the product of three distinct primes, confirming it carries no squared prime factors. Number theorists applying Möbius inversion to small composite inputs would cite this fact to validate the domain of the inversion formula. The proof is a one-line wrapper that applies native_decide to verify the factorization by direct computation.
Claim. The positive integer 42 is squarefree: its prime factorization $42=2×3×7$ contains no repeated prime factors.
background
The module supplies lightweight wrappers around Mathlib arithmetic functions, beginning with the Möbius function μ. Squarefree is the predicate asserting that a natural number is not divisible by p² for any prime p. Sibling declarations such as mobius_ne_zero_iff_squarefree connect this predicate directly to the non-vanishing of μ(n). The local setting is the construction of basic Möbius footholds before layering Dirichlet inversion; upstream interface markers from OptionAEmpiricalProgram, SimplicialLedger, MechanismDesignFromSigma and RamanujanBridge appear only as dependency placeholders and supply no arithmetic content here.
proof idea
The proof is a one-line wrapper that invokes native_decide. This tactic evaluates the definition of Squarefree on the concrete numeral 42 by computing its prime factorization and confirming all exponents equal one.
why it matters
The declaration supplies a verified base case inside the arithmetic-functions layer that supports later Möbius-based calculations in the Recognition framework. No downstream theorems currently reference it, yet it aligns with the module's stated goal of stabilizing lightweight interfaces before deeper algebra. It touches the same number-theoretic substrate used for phi-ladder rung assignments and mass formulas, though it remains isolated from the T0–T8 forcing chain and the Recognition Composition Law.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.