CrossPatternMatrixCert
plain-language theorem explainer
The CrossPatternMatrixCert structure assembles eight arithmetic identities that realize the cross-products among Recognition Science patterns D=5, the 2^3 cube, gap-45, and cube faces into distinct matrix entries. Researchers working on cross-domain meta-theorems cite it to certify non-degeneracy of the pattern matrix described in the module documentation. The definition directly bundles pre-established facts from sibling theorems without further derivation.
Claim. A certificate structure whose fields assert the identities $5^2=25$, $5·2^3=40$, $(2^3)^2=64$, $2^3·45=360$, $45^2=2025$, $6^2=36$, $45-6·6=9$, and off-diagonal entry count equal to $2^4$.
background
The CrossDomain module organizes five core Recognition Science patterns (D=5, 2^3 cube, J(1)=0, phi-ladder, gap-45/cube-faces) into a matrix whose non-trivial products are claimed to be distinct integers. Upstream theorems supply the individual products: cube_faces_squared establishes 6·6=36 and notes the relation 36 = gap45 - 9 = 45 - D^2; full_turn records 2^3·45=360 as the full-turn quantity; gap_squared and twoCube_squared give the squared terms 2025 and 64. The module documentation states that each entry corresponds to a known RS quantity such as 25 = D^2 for cognitive pair states and 360 for tick times gap.
proof idea
The structure definition directly packages the eight arithmetic facts as fields. Each field pulls a pre-proved sibling result (D5_squared, D5_times_2cube, twoCube_squared, full_turn, gap_squared, cube_faces_squared) or the offDiagEntries definition. All component equalities were established by decide tactics in the depends_on theorems.
why it matters
CrossPatternMatrixCert supplies the type for the downstream crossPatternMatrixCert definition that instantiates the certificate. It realizes the C26 meta-claim that the five patterns form a non-degenerate cross-product matrix. Within the Recognition framework the construction encodes interactions among the eight-tick octave (T7), D=3 dimensions (T8), and gap-45, though phi-ladder entries remain outside the present certificate.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.