squarefree_thirtythree
plain-language theorem explainer
33 factors as the product of distinct primes 3 and 11 and therefore satisfies the squarefree condition. Number theorists using the Möbius function inside the Recognition Science arithmetic-functions layer would cite this instance when checking small cases for inversion identities. The proof reduces the predicate to a decidable computation that native_decide evaluates directly.
Claim. The positive integer $33$ is squarefree.
background
The module supplies lightweight wrappers around Mathlib arithmetic functions, beginning with the Möbius function μ. Squarefree numbers are those whose prime factorization contains no repeated factors; this property determines the support of μ, with μ(n) nonzero precisely when n is squarefree. The local setting is therefore a collection of basic facts that later Dirichlet-algebra layers can invoke without re-proving elementary number-theoretic predicates.
proof idea
The proof is a one-line wrapper that invokes the native_decide tactic. This tactic reduces Squarefree 33 to a decidable proposition on the prime factorization of 33 and confirms the result at compile time.
why it matters
The declaration supplies a verified concrete instance inside the arithmetic-functions module that supports Möbius-function definitions. It sits at the base of the NumberTheory.Primes hierarchy but does not invoke the Recognition Science forcing chain, the J-cost functional, or the phi-ladder. No downstream theorems currently depend on it.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.