offDiag_is_two_fourth
plain-language theorem explainer
The off-diagonal entry count in the cross-pattern matrix equals 16, or 2 to the fourth power. Researchers citing the Wave-64 meta-theorem on RS pattern cross-products would reference this to confirm the matrix dimension. The proof is a direct decidable check on the squared off-diagonal size definition.
Claim. Let $n$ denote the off-diagonal size in the cross-pattern matrix of RS patterns. Then $n^2 = 2^4$.
background
The module develops C26, a structural meta-claim that five RS patterns (D=5, 2^3=8, J(1)=0, phi-ladder, gap-45) form a non-degenerate cross-product matrix whose entries recover known quantities such as 25=D^2, 40=D*2^3, 64=2^6, 5 phi, 8 phi, 45, 360, phi^2, and 2025. offDiagEntries counts the off-diagonal cells of this matrix. The upstream definition states offDiagEntries : Nat := offDiagSize * offDiagSize, so the theorem asserts that this count is exactly 16.
proof idea
One-line wrapper that applies the decide tactic to the definition of offDiagEntries as the square of offDiagSize, confirming equality to 16 by direct computation.
why it matters
The result supplies one certified entry to crossPatternMatrixCert, which assembles the full matrix for the C26 meta-theorem. It aligns with the eight-tick octave (T7) by exhibiting a clean power-of-two count in the off-diagonal block. No open scaffolding questions are closed here.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.