RSIndependentTriple
plain-language theorem explainer
RSIndependentTriple n assembles three CoupledAxis records of common cardinality n, each tagged by a distinct RSPrimitive, together with explicit pairwise independence witnesses. Researchers deriving combined state spaces or tensor products in Recognition Science cite it when establishing n^3 cardinalities. The declaration is a pure structure definition carrying no proof obligations or computational content.
Claim. Let $n$ be a natural number. An RS-independent triple of size $n$ consists of three coupled axes $A_1,A_2,A_3$, each a finite type of cardinality exactly $n$ tagged by an RSPrimitive, together with proofs that $A_i$ and $A_j$ are independent for every pair $i<j$.
background
The RS-Coupled Axes module supplies infrastructure for cross-domain combinations of finite axes. A CoupledAxis n is defined as a finite type Ix equipped with a Fintype instance, a proof that its cardinality equals n, and a tag given by an RSPrimitive; two axes count as independent precisely when their primitives differ. The module notes that same-cardinality axes are not automatically independent in RS; independence requires distinct recognition primitives.
proof idea
This declaration is a structure definition. It introduces the record type RSIndependentTriple n with six fields (three axes and three independence conditions) and contains no proof body, tactics, or reduction steps.
why it matters
The structure is the immediate prerequisite for tripleProductCard and triple_card, which conclude that three same-size independent axes produce a combined cardinality of n cubed. It supplies the basic building block for multi-axis tensor constructions inside the Recognition framework and aligns with the derivation of three spatial dimensions from the eight-tick octave. No open scaffolding questions are closed by this definition.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.