twoCube_squared
plain-language theorem explainer
The arithmetic identity 8 times 8 equals 64 holds in the natural numbers. Cross-domain matrix constructions in Recognition Science cite this fact when populating the certificate that records distinct products among the five core patterns. The proof is a direct computation via the decide tactic.
Claim. $2^3 · 2^3 = 64$
background
The CrossPatternMatrix module defines a 5-by-5 matrix whose rows and columns are indexed by the patterns D=5, 2³=8, J(1)=0, the φ-ladder, and gap-45. Each off-diagonal entry is required to be a distinct integer or relation that matches a known RS quantity. The cell for 2³ squared is recorded as 64 and labeled 2^6 (DFT × DFT, double cube).
proof idea
One-line wrapper that applies the decide tactic to the concrete natural-number equality.
why it matters
Supplies the twoCube_squared field of the CrossPatternMatrixCert structure, which is then packaged into crossPatternMatrixCert. The value 64 completes the matrix row for 2³ and is identified with the double cube. This step supports the C26 meta-claim that the five patterns produce a non-degenerate set of cross-products and aligns with the eight-tick octave (period 2^3) in the forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.