threeSixty_is_tick_gap
plain-language theorem explainer
The identity 360 equals 8 times 45 is recorded in the RS cross-domain cardinality spectrum, expressing a full angular turn as the product of the eight-tick factor and the gap45 parameter. Workers verifying numerical decompositions across RS domains cite this when confirming that spectrum members factor into the primitives 2, 3, 5 and gap45. The proof is a direct decision procedure that checks the arithmetic equality in one step.
Claim. $360 = 8 × 45$, where 8 is the eight-tick octave $2^{D_3}$ and 45 is the gap parameter whose product recovers the full turn.
background
The module shows that cardinalities of canonical RS types belong to the structured set {2, 3, 4, 5, 6, 7, 8, 10, 12, 15, 16, 45, 70, 125, 216, 256, 3125, …}. Each entry decomposes via multiplication or powering of the cube generators {2, 3}, the configuration dimension 5, and the gap45. eightTick is the definition eightTick : ℕ := 8, carrying the comment 2^Dspatial and arising from the spatial dimension fixed at 3 by the forcing chain.
proof idea
The proof is a one-line wrapper that applies the decide tactic to the numerical equality 360 = 8 * 45.
why it matters
The result supplies a concrete witness inside cardinalitySpectrumCert, the top-level certificate that records Dspatial_is_3, Dconfig_is_5, gap_as_D and eightTick_as_D. It instantiates the eight-tick octave (T7) and the claim that every spectrum member admits an RS-primitive decomposition, closing one link in the cross-domain consistency argument.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.