D_times_double_cube
plain-language theorem explainer
The arithmetic identity 5 multiplied by 64 equals 320 records the D times double-cube cell in the cross-pattern matrix. Recognition Science researchers building the Wave-64 meta-claim would cite this to verify one non-trivial product among the five patterns. The proof is a one-line decision procedure that evaluates the natural-number equality directly.
Claim. $5 times 2^6 = 320$
background
The module establishes C26, the cross-pattern matrix for five Recognition Science patterns: D=5, 2^3=8 (cube), J(1)=0, the phi-ladder, and gap-45. The matrix tabulates all pairwise products, with each non-trivial entry tied to an RS quantity such as 40 = D · 2^3 (attention space) and 64 = 2^6 (double cube, DFT × DFT). This declaration supplies the product of D=5 with the double-cube term 2^6.
proof idea
One-line wrapper that applies the decide tactic to the decidable equality on natural numbers.
why it matters
The result populates a cell in the C26 matrix meta-claim that asserts the five patterns produce a non-degenerate set of distinct integers and relations. It anchors the D=5 row against the double-cube column, consistent with the listed 64 = 2^6 entry. No downstream theorems depend on it yet; it closes a basic arithmetic slot inside the structural meta-theorem.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.