threehundredsixty_div_fortyfive
plain-language theorem explainer
The arithmetic identity 360 divided by 45 equals 8 is recorded as a stable anchor inside the RSConstants module. Researchers building bridge lemmas over the phi-ladder or eight-tick octave would cite it to avoid repeating the same division. The proof is a one-line wrapper that invokes native_decide to evaluate the expression directly.
Claim. $360 / 45 = 8$
background
The RSConstants module gathers small, decidable integer facts (8, 45, 360, 840 and selected primes) that recur in Recognition Science derivations. These facts function as fixed reference points so that later lemmas stay compact and do not re-prove elementary arithmetic. The upstream Primes definition supplies the set of prime numbers as a subset of the naturals, providing the ambient number-theoretic context even though the present equality is purely arithmetic.
proof idea
The declaration is a term-mode proof consisting of a single native_decide tactic. Native_decide reduces the concrete integer division to a decidable equality and discharges the goal without further lemmas.
why it matters
This equality supplies one of the explicit numerical anchors listed in the module documentation for keeping bridge lemmas readable. It directly supports the eight-tick octave (period 2^3) that appears in the forcing chain at T7, since the result is exactly 8. No downstream theorems are recorded yet, but the fact closes a scaffolding gap for any later derivation that must manipulate 360 and 45 without inline recomputation.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.