offDiagSize
plain-language theorem explainer
The cross-pattern matrix in Recognition Science fixes the off-diagonal block size at 4. Researchers citing the C26 meta-theorem use this constant to count distinct cross-product relations among the five patterns. The definition is a direct numeric assignment.
Claim. The off-diagonal block size in the cross-pattern matrix of Recognition Science patterns is defined to be $4$.
background
The module formalizes the C26 meta-claim that five RS patterns (D=5, 2³=8, J(1)=0, φ-ladder, gap-45/cube-faces) form a non-degenerate matrix of cross-products. Each non-trivial entry matches a known RS quantity such as 25=D², 40=D·2³, 64=2⁶, 5φ, 8φ, 45, 360, φ², and 2025. This definition supplies the integer 4 that sizes the off-diagonal portion of that matrix.
proof idea
Direct definition that assigns the natural number 4.
why it matters
This constant is used by the sibling definition that computes the total number of off-diagonal entries. It supports the C26 structural meta-claim that each pair of patterns produces a distinct integer or relation. The setting draws on the five patterns identified in the Wave-62 report and the requirement of a non-degenerate matrix with zero axioms or sorrys.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.