twoCube_times_gap
plain-language theorem explainer
The arithmetic identity eight times forty-five equals three hundred sixty is recorded here. Workers on the cross-pattern matrix cite it to populate the entry linking the eight-tick octave to the gap of forty-five. The proof applies a decision tactic that confirms the numerical equality without further lemmas.
Claim. $2^{3} 45 = 360$
background
The module assembles a matrix of cross-products among five RS patterns: D=5, 2³=8, J=0, φ-ladder, gap-45. The entry at 2³ and gap45 is 360, described as full turn = tick × gap. This identity supplies one cell in that matrix. No upstream results are required.
proof idea
The proof consists of a single decide tactic that evaluates the arithmetic expression directly.
why it matters
This supplies the value for the full_turn theorem, which states that 2³ × 45 = 360 degrees. It completes one non-trivial entry in the cross-pattern matrix of the C26 meta-theorem, corresponding to the eight-tick octave multiplied by the gap. The matrix as a whole demonstrates that the five patterns produce distinct integers.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.