CoupledAxis
plain-language theorem explainer
CoupledAxis packages a finite type of exact cardinality n with one of the five RS primitives that assigns its domain meaning. Researchers combining strata from different physical layers cite it to enforce that same-size axes remain distinguishable only through distinct primitives. The entry is a bare structure definition with four fields and no further computation.
Claim. A structure consisting of a type $Ix$ equipped with a Fintype instance such that its cardinality equals $n$, together with a tag from the inductive type of RS primitives (jCost, phiLadder, sigmaCharge, q3Lattice, gap45).
background
The RS-CoupledAxis module builds infrastructure for theorems that combine axes across domains. Its central convention is that two axes of equal cardinality are independent precisely when their RSPrimitive tags differ. The five primitives are jCost, phiLadder, sigmaCharge, q3Lattice and gap45. An upstream result from the algebra layer shows how cardinalities such as powers of two arise for vector spaces over F2.
proof idea
The declaration is a structure definition. It directly records the index type, the Fintype instance, the cardinality equality, and the primitive tag without invoking any lemmas.
why it matters
CoupledAxis supplies the carrier for the independent predicate and for the triple structures RSIndependentTriple and RSDisjointSum3. These feed the concrete axis definitions in PlanetStrataC2, where atmosphere, Earth and ocean layers receive distinct primitives. The construction encodes the Recognition Science rule that independence of same-cardinality axes requires different primitives, a prerequisite for cross-domain composition theorems.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.