rsTriple_card
plain-language theorem explainer
The finite cardinality of the product space Fin 5 × Fin 5 × Fin 5 equals 125. Cross-domain recognition lattice work in Recognition Science cites this base count when sizing single 5³ state spaces for cognitive or oncological models before scaling to joint products. The proof is a direct term-mode simplification that unfolds the product definition and applies the standard cardinality rule for finite types.
Claim. The cardinality of the finite type $Fin 5 × Fin 5 × Fin 5$ equals 125.
background
The Product Recognition Lattice module models cross-domain recognition states as finite products under Recognition Science bounds. RSTriple is defined as the Cartesian product Fin 5 × Fin 5 × Fin 5 and documented as a generic 5³ recognition state (D-cubed). The module sets out an explicit hierarchy: 5³ = 125 for a single triple, 5⁴ = 625 for four-fold products, up to 5⁶ = 15625 for the joint cognitive-oncology state, all required to satisfy 5⁶ < 2¹⁴.
proof idea
The proof is a one-line term-mode wrapper that applies simp to the definition of RSTriple together with Fintype.card_prod, reducing the product cardinality directly to 5 × 5 × 5 = 125.
why it matters
This cardinality anchors the single-triple entry in the lattice hierarchy and is invoked by rsJoint_card to obtain the joint size 15625. It supplies the five_cubed component required by the ProductRecognitionLatticeCert structure and the productRecognitionLatticeCert definition. The result fills the 5³ slot in the module's information-theoretic bound on clinical state spaces.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.