fortyfive_dvd_360
plain-language theorem explainer
The declaration establishes that 45 divides 360 as an integer divisibility fact. Researchers working on the Recognition Science constants would cite it to anchor repeated arithmetic steps involving 360 and its factors. The proof proceeds via a single decide tactic that computationally confirms the relation without manual calculation.
Claim. $45$ divides $360$
background
The RSConstants module gathers small decidable arithmetic facts about integers that recur in the reality repo, including 8, 45, 360, 840, and primes such as 11, 17, 37, 103, 137. These facts function as stable anchors that prevent repeated arithmetic proofs in bridge lemmas. The local setting emphasizes boring but reliable number-theoretic building blocks for the Recognition Science framework.
proof idea
The proof is a one-line wrapper that invokes the decide tactic to verify the divisibility statement computationally.
why it matters
This theorem provides a foundational arithmetic fact in the NumberTheory.Primes.RSConstants module, supporting factorizations and prime-related lemmas such as those involving 360 and 8. It aligns with the eight-tick octave (T7) in the forcing chain by stabilizing the period-8 structure. No open questions are directly addressed here, but it ensures readability in downstream Recognition Science derivations.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.