tripleProductCard
plain-language theorem explainer
tripleProductCard supplies the cardinality of the combined state space for three pairwise-independent axes of equal size n in the RS framework. It is used in downstream cardinality theorems such as triple_card. The implementation multiplies the individual axis cardinalities obtained from their Fintype instances.
Claim. For an RS-independent triple $T$ consisting of three axes each of size $n$, the triple product cardinality is defined as $|I_1| · |I_2| · |I_3|$, where $I_k$ is the index set of the $k$-th axis.
background
The RS-Coupled Axes module supplies infrastructure for cross-domain combination theorems. Two finite axes of the same cardinality count as independent in RS only when tagged by different recognition primitives. An RSIndependentTriple n is a structure containing three CoupledAxis n together with pairwise independence proofs. The independence predicate is drawn from the LNALSemantics module, where it encodes minimal spatial semantics with no neighbor interactions. Upstream results include the axis definitions from F2Power, which supply the three weight-1 vectors in F2^3.
proof idea
The definition directly multiplies the Fintype.card of each of the three axes using their finite instances. No additional lemmas are applied beyond the structure accessors.
why it matters
This definition is invoked by the theorem triple_card, which proves the product equals n^3. It fills the role of providing the counting mechanism for tensor-product combinations of independent axes in the Recognition Science framework. The construction supports the discrete tier counting central to the phi-ladder and eight-tick octave structures.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.