matrixSize
plain-language theorem explainer
The definition fixes the dimension of the cross-pattern matrix at 5 to match the five core RS patterns (D=5, 2³, J=0, phi-ladder, gap-45). Researchers working on the C26 meta-theorem cite this constant when indexing the 25 total entries or isolating the 16 non-trivial off-diagonal cross-products. It is supplied as a direct constant definition with no further computation.
Claim. The dimension of the cross-pattern matrix is defined to be the natural number 5.
background
The CrossPatternMatrix module encodes the C26 structural meta-claim: the five RS patterns (D=5, 2³=8, J(1)=0, phi-ladder, gap-45/cube-faces) generate a non-degenerate 5 by 5 matrix of pairwise products. The module table lists the resulting quantities (25 = D², 40 = D·2³, 64 = 2⁶, 5φ, 8φ, 45, 360, φ², 2025) and states that each non-trivial entry corresponds to a known RS quantity. Only Mathlib is imported and the file contains zero axioms or sorrys.
proof idea
Direct definition that assigns the constant natural number 5.
why it matters
This constant supplies the row and column count for the 5 by 5 cross-product array that organizes the Wave-62 patterns. It anchors the enumeration of all pairwise relations among D, cube, J, phi and gap, feeding the sibling declarations that compute individual entries such as D5_squared and gap_squared. The definition therefore closes the structural part of the C26 meta-claim while leaving open whether the Recognition Composition Law forces all 16 off-diagonal terms to remain distinct.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.