offDiagEntries
plain-language theorem explainer
The definition sets the off-diagonal entry count in the cross-pattern matrix to the square of the size parameter four. A researcher certifying the wave-64 meta-theorem would cite this count when confirming sixteen positions in the five-pattern matrix. The definition is a direct arithmetic product of the size parameter with itself.
Claim. Let $N = 4$. The off-diagonal entry count is defined as $N^2$.
background
The module presents the cross-pattern matrix for five Recognition Science patterns (D=5, 2^3=8, J(1)=0, φ, gap-45) whose pairwise products yield distinct integers or relations such as 25=D^2, 40=D·2^3, 64=2^6, and 360=2^3·45. The size parameter is fixed at four, reflecting a structural reduction that excludes the trivial J=0 row or column while preserving the non-degenerate off-diagonal block. This definition supplies the total count of those off-diagonal positions as the square of the size parameter.
proof idea
The declaration is a one-line definition that multiplies the size parameter by itself.
why it matters
The count feeds the structure CrossPatternMatrixCert that records the matrix equalities and the theorems establishing the value sixteen (equivalently 2^4). It supports the meta-claim that the five patterns produce a non-degenerate matrix of distinct RS quantities, consistent with the power-of-two structures and the eight-tick octave in the framework.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.