crossPatternMatrixCert
plain-language theorem explainer
The crossPatternMatrixCert assembles verified numerical identities for the cross-products of five RS patterns (D=5, 2^3 cube, J=0, phi-ladder, gap-45) into a single certificate structure. Researchers citing the Wave-64 meta-theorem would reference it to confirm matrix entries match known RS quantities such as 25, 40, 64, 360, and 2025. The definition is a direct record construction that pulls each field from a pre-proved decide lemma.
Claim. The declaration supplies an instance of the structure asserting the following equalities: $5^2 = 25$, $5^2^3 = 40$, $(2^3)^2 = 64$, $2^3 times 45 = 360$, $45^2 = 2025$, $6^2 = 36$, $45 - 36 = 9$, and the count of off-diagonal entries equals $2^4$.
background
In the CrossDomain module the cross-pattern matrix is introduced as a structural meta-claim for the Wave-64 report. It organizes the five patterns D=5, the 8-tick cube, J(1)=0, the phi-ladder, and gap-45 into a 5x5 matrix whose non-trivial entries are distinct integers or relations. The structure CrossPatternMatrixCert collects these as a set of equalities including D5_squared for 25, full_turn for 360, and face_pairs_minus_gap_is_D_sq for 9.
proof idea
The definition is a one-line record constructor that populates each field of CrossPatternMatrixCert by direct reference to the corresponding sibling theorem: D5_squared to D5_squared, D5_2cube to D5_times_2cube, full_turn to full_turn, gap_squared to gap_squared, cube_faces_squared to cube_faces_squared, face_pairs_minus_gap_is_D_sq to face_pairs_minus_gap, and off_diag_count to offDiag_is_two_fourth.
why it matters
This definition completes the certificate for the C26 cross-pattern matrix meta-theorem, which asserts that the five RS patterns produce a non-degenerate matrix of distinct cross-products. It supports the claim that each entry corresponds to a known quantity such as 64 for the double cube or 2025 for gap squared. The construction closes the Lean formalization of the Wave-64 structural claim with zero sorrys, linking the numerical identities to the eight-tick octave and phi-ladder relations.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.