not_squarefree_840
plain-language theorem explainer
840 is divisible by 4 and therefore not squarefree. Researchers maintaining Recognition Science constant tables cite this fact to keep later bridge lemmas free of repeated divisibility checks. The proof is a short term-mode script that assumes squarefreeness, instantiates the definition at the prime 2 with explicit quotient 210, and obtains an immediate contradiction by simplification.
Claim. $840$ is not square-free.
background
The RSConstants module collects small decidable arithmetic facts about integers that recur throughout the Recognition Science development, including factorizations involving 8, 45, 360, 840 and selected primes such as 5, 11, 17, 37, 103 and 137. Squarefree n asserts that no integer d > 1 satisfies d² | n. These anchors prevent re-proving the same elementary divisibility statements across many later lemmas.
proof idea
The proof is a short term-mode script. It introduces the assumption that 840 is squarefree, instantiates the universal quantifier at the prime 2 together with the explicit divisor pair 210 (verified by norm_num), and simplifies the resulting statement to falsehood.
why it matters
This theorem supplies one of the stable arithmetic anchors listed in the module documentation for RS constants. It supports later factorization lemmas such as wheel840_factorization and threehundredsixty_factorization among the siblings. Within the Recognition Science framework it contributes to the collection of decidable facts needed for prime markers and ladder calculations without introducing new hypotheses.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.