D_times_double_cube
plain-language theorem explainer
The natural-number identity 5 multiplied by 2 to the sixth power equals 320 is recorded. Cross-domain researchers cite it to fix the D times double-cube entry inside the Wave-64 cross-pattern matrix. The verification is a direct arithmetic decision performed in one step.
Claim. $5 times 2^6 = 320$
background
The CrossPatternMatrix module constructs a 5-by-5 table of products among the RS patterns D=5, the cube 2^3=8, J(1)=0, the golden ratio phi, and gap45. Each non-trivial entry is required to be a distinct integer or algebraic relation; 2^6 is identified as the double cube (DFT squared). The present theorem supplies the concrete value of the D times double-cube product. The module imports only Mathlib and contains no upstream lemmas beyond decidable equality on naturals.
proof idea
The proof is a one-line wrapper that applies the decide tactic to the arithmetic equality.
why it matters
The declaration supplies one concrete integer entry required by the C26 meta-theorem that the five RS patterns form a non-degenerate cross-product matrix. It aligns with the framework landmarks of the eight-tick octave and D=3 spatial structure by confirming the integer 320 that appears alongside 40 = D times 2^3 and 64 = 2^6. No downstream theorem yet depends on it, leaving the matrix entry as a basic computational anchor.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.