offDiagSize
offDiagSize sets the off-diagonal dimension of the cross-pattern matrix to the natural number 4. Researchers citing the C26 meta-theorem use this constant to count the 16 non-trivial interactions among the five RS patterns. The definition is a direct constant assignment.
claimThe off-diagonal size of the cross-pattern matrix is defined as $4$.
background
The Cross-Pattern Matrix module constructs a 5-by-5 array whose rows and columns are indexed by the RS patterns D=5, 2³=8, J(1)=0, the phi-ladder, and gap-45. Module documentation records the resulting products, including 25 = D², 40 = D · 2³, 64 = 2⁶, 5φ, 8φ, 45, 360, φ², and 2025. offDiagSize isolates the dimension of the block that excludes the degenerate J=0 row and column, which produces many n/a entries.
proof idea
Direct definition that assigns the constant 4.
why it matters in Recognition Science
offDiagSize supplies the dimension consumed by the sibling definition offDiagEntries, which forms the total count of off-diagonal entries. It implements the structural requirement of the C26 meta-claim that each pair of patterns yields a distinct integer or relation. The definition therefore quantifies cross-domain interactions among the phi-ladder, the eight-tick octave, and gap quantities inside the Recognition Science framework.
scope and limits
- Does not identify which patterns occupy the matrix rows or columns.
- Does not compute any cross-product values.
- Does not prove distinctness or non-degeneracy of the entries.
- Does not reference the spatial dimension D=3 from the forcing chain.
Lean usage
def offDiagEntries : ℕ := offDiagSize * offDiagSizeformal statement (Lean)
93def offDiagSize : ℕ := 4