twoCube_times_gap
plain-language theorem explainer
The arithmetic identity eight times forty-five equals three hundred sixty is verified by direct computation. Recognition Science researchers cite it to populate the cross-pattern matrix entry linking the eight-tick pattern to the gap-45 quantity. The proof consists of a single decide tactic that confirms the equality without external lemmas.
Claim. $2^3 times 45 equals 360$.
background
The Cross-Pattern Matrix module establishes a structural meta-claim for five RS patterns: D=5, 2^3=8, J(1)=0, the phi-ladder, and gap-45. These form a non-degenerate matrix of cross-products, with each non-trivial entry matching a known RS quantity. The entry for the product of the eight-tick pattern and gap-45 is listed as 360 and interpreted as the full turn.
proof idea
The proof is a one-line wrapper that applies the decide tactic to verify the arithmetic identity by direct computation.
why it matters
This supplies the value used by the full_turn theorem, which states that 2^3 times 45 equals 360 degrees. It populates one cell in the wave-64 cross-domain matrix and aligns with the eight-tick octave structure in the Recognition framework. The module notes that each matrix entry corresponds to a distinct integer or relation with no two non-trivial entries coinciding.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.