rsJoint_fits_14_bits
plain-language theorem explainer
The joint recognition state formed as the Cartesian product of two RS triples has cardinality exactly 15625, hence strictly less than 16384. Researchers constructing cross-domain lattices that combine cognitive and oncological recognition spaces cite this bound to confirm the full patient state remains inside a 14-bit clinical envelope. The proof is a one-line wrapper that rewrites via the product cardinality theorem and decides the numerical comparison.
Claim. Let $RSJoint$ denote the product of two recognition triples. Then the cardinality satisfies $|RSJoint| < 2^{14}$.
background
The module defines the joint state as the Cartesian product of two RS triples, each triple encoding a recognition domain such as a cognitive or oncological state space. The upstream theorem rsJoint_card computes the exact cardinality of this product as 15625 by applying the Fintype product formula to the known cardinality of a single triple. This places the result inside the module's hierarchy of 5-powers: 5^6 equals the joint cognitive-oncology space and is required to lie below 2^14.
proof idea
One-line wrapper that applies the rsJoint_card theorem to replace the goal with the concrete equality 15625 = 15625, then invokes decide to confirm the inequality 15625 < 16384 holds.
why it matters
The theorem supplies the 5^6 < 2^14 bound that appears inside the productRecognitionLatticeCert definition, closing the information-theoretic constraint on the combined cognitive-oncology lattice. It directly instantiates the module's structural claim that cross-domain products remain inside the 14-bit clinical bandwidth while respecting the Recognition Science lattice hierarchy of successive 5-powers.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.