offDiagEntries_eq
plain-language theorem explainer
The theorem establishes that the off-diagonal entries in the cross-pattern matrix total 16. Researchers verifying the Wave-62 meta-theorem on RS pattern interactions would cite this count. The equality is confirmed by direct computational evaluation of the matrix dimension definition.
Claim. In the cross-pattern matrix of the five Recognition Science patterns, the number of off-diagonal entries equals 16.
background
The module constructs a matrix whose rows and columns are indexed by the patterns D=5, 2³=8, J(1)=0, the φ-ladder, and gap-45/cube-faces. The module doc states that each pair of patterns produces a distinct integer or relation, with n/a entries appearing in the J=0 row and column. offDiagEntries is the square of the effective off-diagonal size, so the count is the number of non-trivial off-diagonal positions in this structure.
proof idea
The proof is a one-line wrapper that applies the decide tactic to evaluate the definition of offDiagEntries and confirm equality to 16.
why it matters
This theorem supplies the entry count required by the C26 structural meta-claim that the five RS patterns form a non-degenerate matrix of cross-products. It aligns with the framework landmark that off-diagonal counts are powers of 2 (T7 eight-tick octave). The listed matrix entries include 25=D², 40=D·2³, and 64=2⁶, all of which presuppose this cardinality. No downstream theorems yet depend on it.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.