not_squarefree_fifty
plain-language theorem explainer
50 fails to be squarefree because 25 divides it. Researchers using the Möbius function in arithmetic number theory cite this to confirm that μ(50) vanishes. The proof is a one-line wrapper that invokes native_decide to evaluate the predicate directly on the concrete integer.
Claim. The integer 50 is not square-free, i.e., $5^2$ divides 50.
background
The module supplies lightweight wrappers around Mathlib arithmetic functions, beginning with the Möbius function μ. Squarefree(n) holds precisely when n has no squared prime factor. The upstream theorem and from CirclePhaseLift supplies an explicit log-derivative bound M that yields the angular Lipschitz constant logDerivBound = M * r on the circle of radius r.
proof idea
The proof is a one-line wrapper that applies native_decide to the negated Squarefree predicate on 50.
why it matters
This supplies a concrete verified instance supporting sibling equivalences such as mobius_eq_zero_iff_not_squarefree. It anchors the Möbius footholds in the module documentation and provides a basic fact for the arithmetic-functions layer of the Recognition Science number-theory development.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.