full_turn
plain-language theorem explainer
The equality 2 cubed times 45 equals 360 populates the full-turn cell of the cross-pattern matrix. Wave-64 meta-theorem authors cite it when building the cardinality spectrum certificate from the five RS patterns. Proof is a direct reference to the twoCube_times_gap identity.
Claim. $2^{3} × 45 = 360$
background
The CrossPatternMatrix module states a structural meta-claim: the five RS patterns (D=5, 2³=8, J(1)=0, φ-ladder, gap-45/cube-faces) form a non-degenerate matrix of cross-products, each yielding a distinct integer. The matrix lists the 2³-by-gap45 entry as 360, labeled full turn = tick × gap. This setting is local to C26 with zero sorrys and zero axioms.
proof idea
One-line wrapper that applies twoCube_times_gap.
why it matters
The theorem supplies the full_turn field demanded by CrossPatternMatrixCert, which is referenced by cardinalitySpectrumCert. It completes the matrix entry for the eight-tick octave (T7) times gap-45, consistent with the forcing chain step T7 and D=3 spatial dimensions. The module doc states 360 = 2³ · 45 (full turn = tick × gap).
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.