productRecognitionLatticeCert
plain-language theorem explainer
The declaration assembles a certificate for the product recognition lattice by collecting precomputed facts on powers of five that arise when cognitive and oncology domains are multiplied. Cross-domain modelers in Recognition Science cite it to confirm that the joint state space of size 15625 fits inside a 14-bit register. The construction is a direct structure instantiation that references the supporting theorems for each field.
Claim. A certificate for the product recognition lattice consists of the equalities $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 $|RSTriple|=125$, $|RSJoint|=15625$, $|RSJoint|<2^{14}$.
background
The module treats cross-domain products of recognition state spaces. Cognitive processes and oncology each contribute a triple of size $5^3=125$, so their product yields a joint space of size $5^6=15625$. The hierarchy runs from $5^2=25$ (pairs of domains) through $5^8=390625$, with the explicit constraint that the joint space must fit inside 14 bits. This bound is presented as an information-theoretic limit derived from the Recognition Science framework.
proof idea
The definition builds the required structure by assigning each field to an upstream theorem: five_cubed receives the result of five_pow_3, five_to_six receives five_pow_6, joint_size receives cognitive_oncology_size, five_six_under_14_bits receives five_six_lt_two_fourteen, and the remaining cardinality and inequality fields receive their matching pre-proved statements. No further tactics are applied.
why it matters
The definition packages the numerical facts that realize the C23 structural claim for the product recognition lattice. It supplies the concrete bounds needed to close the Lean formalization of the 5^6 joint state without axioms or sorrys. The construction sits inside the broader Recognition Science derivation of state-space hierarchies from the forcing chain and supplies the information-theoretic ceiling used in cross-domain applications.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.