not_squarefree_fortyfive
plain-language theorem explainer
The integer 45 is not square-free because 9 divides it. Number theorists maintaining the Recognition Science constant anchors would cite this when handling the cycle-45 gap in factorizations. The proof assumes square-freeness, applies the definition at the prime 3 with witness 5, and simplifies to a contradiction.
Claim. The positive integer 45 is not square-free.
background
The RSConstants module assembles small decidable arithmetic facts about integers such as 8, 45, 360 and 840 that recur across the reality repo. These facts keep later bridge lemmas readable by avoiding repeated arithmetic. Square-freeness is the property that no prime square divides the integer; the present theorem records the elementary observation that 45 = 3² · 5 fails this property.
proof idea
The proof assumes Squarefree 45. It applies the assumption to the prime 3 together with the witness 5 (from 45 = 9 · 5) and simplifies to reach a contradiction.
why it matters
This fact anchors the factorization of 45 inside the RS constants file and supports the sibling lemma fortyfive_eq_three_sq_mul_five. It ensures downstream lemmas that reference the cycle-45 gap correctly track the repeated factor of 3. No parent theorem or open question is touched.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.