CrossPatternMatrixCert
plain-language theorem explainer
The structure collects eight arithmetic identities that encode the cross-products among the five core patterns of the Wave-62 report. Researchers formalizing the cross-domain meta-theorem cite this bundle to confirm that the matrix entries remain distinct. Each identity is supplied by a one-line decide proof in a sibling declaration.
Claim. A record type whose fields assert the following arithmetic facts: $5^2=25$, $5*2^3=40$, $(2^3)^2=64$, $2^3*45=360$, $45^2=2025$, $6^2=36$, $45-6^2=9$, and the number of off-diagonal entries equals $2^4$.
background
The module presents C26 as a structural meta-claim that the patterns D=5, 2^3=8, J(1)=0, the phi-ladder, and gap=45 produce a non-degenerate matrix of cross-products. Each non-trivial entry matches a known Recognition Science quantity such as 25 for cognitive pair states or 360 for the full turn. Upstream results supply the individual identities, for example the theorem establishing 55=25 and the one establishing 2^345=360.
proof idea
The declaration is a structure definition that lists the required fields. Each field is populated in the downstream construction by the corresponding decide-proved theorem.
why it matters
It provides the certificate type consumed by the crossPatternMatrixCert definition that realizes the C26 claim. The construction ties the matrix directly to the eight-tick octave and the gap-45 structure within the Recognition Science framework. The module reports zero sorry or axiom.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.