ProductRecognitionLatticeCert
plain-language theorem explainer
ProductRecognitionLatticeCert is a record structure that bundles the arithmetic identities and cardinality bounds for the 5^3 and 5^6 recognition state spaces in the cross-domain product lattice. Researchers modeling combined cognitive and oncological recognition spaces cite it to certify that the joint state space occupies 15625 elements and remains below the 14-bit clinical bandwidth. The structure is realized as a plain record type whose fields are later populated by direct evaluation of natural-number powers and Fintype cardinalities.
Claim. Let $R_3$ be the 5-cubed recognition triple $Fin 5 × Fin 5 × Fin 5$ and $R_6$ the joint space $R_3 × R_3$. The certificate asserts the identities $5^3 = 125$, $5^6 = 15625$, $5^3 · 5^3 = 15625$, the inequalities $5^6 < 2^{14}$ and $5^3 < 2^7$, and the cardinality statements $|R_3| = 125$, $|R_6| = 15625$, $|R_6| < 2^{14}$.
background
In the Product Recognition Lattice module, RSTriple is the Cartesian product Fin 5 × Fin 5 × Fin 5, a generic 5³ recognition state (D-cubed). RSJoint is defined as RSTriple × RSTriple, the joint state formed by two such triples. The module places these spaces inside the hierarchy 5² = 25, 5³ = 125, 5⁴ = 625, 5⁵ = 3125, 5⁶ = 15625, with the explicit constraint that the 5⁶ joint space lies below 2¹⁴ = 16384.
proof idea
The declaration is a structure definition with no proof body; it simply declares the record type whose eight fields are the listed equalities and inequalities. Instantiation is performed downstream by supplying concrete values from sibling lemmas such as five_pow_3, five_pow_6, rsTriple_card and rsJoint_card.
why it matters
The structure supplies the certificate for the cross-domain product claim that the combined cognitive-oncology state space occupies exactly 15625 states and satisfies the 14-bit bandwidth bound. It is instantiated by productRecognitionLatticeCert, which feeds higher-level assertions about the recognition lattice hierarchy. The construction aligns with the Recognition Science emphasis on finite state spaces bounded by powers of 5 and information-theoretic limits.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.