triple_card
plain-language theorem explainer
The theorem states that any RSIndependentTriple T of size n has triple product cardinality exactly n cubed. Researchers building Recognition Science models of coupled discrete axes would cite this when enumerating states in cross-domain combinations. The proof is a one-line wrapper that unfolds the product definition and rewrites each axis cardinality via the F2Power card equality.
Claim. Let $T$ be a pairwise independent triple of coupled axes, each of cardinality $n$. Then the cardinality of the triple product of these axes equals $n^3$.
background
The module supplies infrastructure for RS-Coupled Axes, where two axes of equal cardinality count as independent only when tagged by distinct recognition primitives. RSIndependentTriple is the structure that packages three CoupledAxis n together with explicit independence proofs between every pair. Upstream, the card_eq theorem on F2Power D asserts that this type has exactly 2^D elements, which supplies the concrete cardinality for each axis component.
proof idea
The proof is a one-line wrapper. It unfolds the definition of tripleProductCard, then rewrites using the card_eq field of each of the three axes supplied by T.
why it matters
This declaration supplies the explicit n^3 count for triple products inside the RS-Coupled Axes layer. It directly supports the module's goal of cross-domain combination theorems and sits downstream of the F2Power cardinality result. No downstream uses are recorded yet, leaving it as a foundational counting lemma for later state-enumeration arguments in the Recognition framework.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.