not_squarefree_360
plain-language theorem explainer
360 fails to be square-free because 4 divides it. Researchers anchoring arithmetic facts in the Recognition Science constants file cite this result to stabilize repeated factorizations involving 360 without re-deriving the divisor relation. The proof assumes square-freeness, feeds the predicate the prime 2 together with the explicit witness 90, and simplifies to a contradiction.
Claim. The integer 360 is not square-free.
background
The RSConstants module collects small decidable arithmetic facts about integers such as 8, 45, 360, 840 and selected primes that recur in the reality repo. These facts serve as stable anchors that keep later bridge lemmas readable and prevent repeated arithmetic derivations. Squarefree is the standard predicate asserting that no integer square greater than 1 divides the argument.
proof idea
The term proof assumes Squarefree 360, applies the assumption to the prime 2 with the witness pair 90 that witnesses 4 dividing 360, and simplifies the resulting equality to obtain falsehood.
why it matters
This theorem supplies a basic non-square-freeness anchor inside the RSConstants collection of prime facts and factorizations. It supports the NumberTheory.Primes section by fixing a concrete arithmetic relation that appears in downstream bridge lemmas. No open questions are touched; the result is fully proved arithmetic scaffolding.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.