threehundredsixty_div_eight
plain-language theorem explainer
The equality 360 divided by 8 equals 45 is recorded as a stable arithmetic anchor. Researchers maintaining bridge lemmas in the RS constants collection would cite it to avoid repeating basic divisions. The proof is a single native decision tactic that evaluates the integer equality directly.
Claim. $360 / 8 = 45$
background
The module gathers small decidable arithmetic facts about integers such as 8, 45, 360, and 840 that recur across the Recognition Science development. These facts function as stable anchors that keep later bridge lemmas readable without re-proving the same arithmetic repeatedly. The local setting is a collection of prime markers and factorizations chosen for their repeated appearance rather than for any deeper number-theoretic content.
proof idea
The proof is a one-line wrapper that applies the native_decide tactic to confirm the equality by direct integer computation.
why it matters
This declaration supplies a basic arithmetic anchor inside the RSConstants module that supports the surrounding collection of prime facts and factorizations. It aligns with the framework's need for stable constants tied to the eight-tick octave where the factor 8 appears explicitly. No downstream uses are recorded, so the fact remains a leaf-level readability device rather than a step in any forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.