not_squarefree_eight
plain-language theorem explainer
Eight fails to be squarefree because 4 divides it. Researchers handling the eight-tick octave and related factorizations in Recognition Science cite this arithmetic anchor when building bridge lemmas. The proof assumes squarefreeness of 8, applies the predicate to the divisor 2, and obtains an immediate contradiction by simplification.
Claim. $8$ is not square-free, i.e., $4$ divides $8$.
background
The module collects small decidable arithmetic facts about integers that recur across the Recognition Science development, such as powers of 2 and the primes 11, 17, 37, 103, and 137. These facts function as stable anchors that keep later bridge lemmas readable without repeated arithmetic. Squarefree is the standard predicate asserting that no integer square greater than 1 divides the number.
proof idea
Assume Squarefree 8. Apply the predicate to the prime divisor 2 to obtain that 4 does not divide 8. Simplification yields false.
why it matters
The result anchors the eight-tick octave (period 2^3) in the forcing chain T7 and supports factorizations such as those of 840 used in ledger and mechanism-design constructions. It supplies a concrete instance of the 8 = 2^3 structure without introducing new hypotheses.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.