offDiagEntries
The definition computes the count of off-diagonal entries in the cross-pattern matrix as the square of the off-diagonal dimension. Cross-domain researchers cite this when verifying the 16 distinct cross-product relations in the Wave-62 meta-theorem. The definition is a direct multiplication of the fixed off-diagonal size by itself.
claimLet $k=4$ be the off-diagonal size. The number of off-diagonal entries in the cross-pattern matrix is $k^2$.
background
The cross-pattern matrix organizes products of five RS patterns: D=5, the eight-tick octave 2^3, J(1)=0, the phi-ladder, and gap-45. Off-diagonal size is fixed at 4 to exclude the trivial J=0 self-product, so the off-diagonal block is 4 by 4. This definition supplies the dimension for counting the 16 non-trivial cross terms that the module later certifies as distinct integers or relations such as 25=D squared and 40=D times 2 cubed.
proof idea
The definition is a one-line arithmetic expression that multiplies the upstream off-diagonal size by itself. It applies the constant value 4 supplied by the sibling definition offDiagSize.
why it matters in Recognition Science
This definition supplies the dimension used by the CrossPatternMatrixCert structure and by the theorems offDiagEntries_eq and offDiag_is_two_fourth that establish the count equals 16, or equivalently 2 to the fourth. It fills the counting step in the C26 cross-pattern matrix meta-claim, confirming that the off-diagonal block is a power of two consistent with the eight-tick octave landmark.
scope and limits
- Does not assign values to any matrix entries.
- Does not prove relations among the five patterns.
- Does not invoke the J-cost function or the phi-ladder.
formal statement (Lean)
94def offDiagEntries : ℕ := offDiagSize * offDiagSize
proof body
Definition body.
95