eight_dvd_360
plain-language theorem explainer
The declaration establishes that 8 divides 360. Researchers assembling Recognition Science constants cite it as a stable anchor that keeps repeated arithmetic out of bridge lemmas. The proof is a one-line decision procedure that confirms the relation directly.
Claim. $8$ divides $360$.
background
The module collects small decidable arithmetic facts on integers that recur in the reality repo, such as 8, 45, 360, 840 and the prime markers 11, 17, 37, 103, 137. These serve as boring but stable anchors that keep later bridge lemmas readable and avoid re-proving the same arithmetic in many places. The local setting is RS constants (prime facts and factorizations).
proof idea
The proof is a one-line wrapper that invokes the decide tactic to verify the divisibility statement directly.
why it matters
This fact anchors arithmetic inside the RSConstants module and supports factorizations involving 360 that appear in Recognition Science calculations. It aligns with the eight-tick octave structure (period 2^3) by confirming divisibility by 8. No downstream theorems are listed; the result is fully proved and closed.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.