twoCube_times_gap
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 in Recognition Science
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.
scope and limits
- Does not assign physical units or interpret the result as degrees.
- Does not prove that all matrix entries are distinct.
- Does not derive the equality from deeper RS axioms or forcing chain steps.
- Does not address connections to the phi-ladder or J-cost beyond this single product.
Lean usage
theorem full_turn : (2 : ℕ)^3 * 45 = 360 := twoCube_times_gapformal statement (Lean)
44theorem twoCube_times_gap : (2 : ℕ)^3 * 45 = 360 := by decide
proof body
45