rsJoint_card
plain-language theorem explainer
rsJoint_card shows that the finite cardinality of the joint state, defined as the Cartesian product of two recognition triples, equals exactly 15625. Cross-domain modelers in cognitive-oncology applications cite this to fix the 5^6 lattice level. The proof reduces the claim in one simplification step by unfolding the product definition and substituting the triple cardinality.
Claim. The cardinality of the joint recognition state space, defined as the Cartesian product of two recognition triple spaces each of cardinality 125, equals 15625.
background
The Product Recognition Lattice module constructs a hierarchy of state spaces from products of 5-powers. The joint state combines two RSTriples (each a recognition triple of size 125) to produce the 5^6 = 15625 space that represents the full cognitive-oncology state of a patient, as stated in the module: 'Combining C1 (cognitive 5³) with C3 (oncology 5³) gives a 5⁶ = 15625 state space — the full state of a cancer patient (cognitive + oncological).'
proof idea
The proof is a one-line wrapper that applies simp to unfold RSJoint as RSTriple × RSTriple, invoke Fintype.card_prod, and substitute the value from rsTriple_card.
why it matters
This result supplies the joint_size value required by the ProductRecognitionLatticeCert structure and directly enables the rsJoint_fits_14_bits theorem that confirms the state lies under the 2^14 clinical-bandwidth bound. It completes the 5^6 entry in the lattice hierarchy, consistent with the Recognition Science eight-tick octave and holographic constraints on cross-domain products.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.