RSDisjointSum3
plain-language theorem explainer
Structure RSDisjointSum3 n packages three CoupledAxis instances of identical cardinality n that remain pairwise independent through distinct RS primitive tags. Researchers building multi-domain cardinality results or physical strata models cite it when forming disjoint sums. The definition is a direct record bundling the three axes with their independence witnesses and carries no computational steps.
Claim. A structure consisting of three axes $A_1, A_2, A_3$ each of type CoupledAxis$(n)$ together with witnesses that $A_1$ and $A_2$ are independent, $A_1$ and $A_3$ are independent, and $A_2$ and $A_3$ are independent, where independence holds precisely when the axes carry distinct recognition primitives.
background
The RS-Coupled Axes module supplies infrastructure for cross-domain combination theorems. Two finite axes of equal cardinality count as independent only when they are tagged by different recognition primitives. A CoupledAxis n is a finite type Ix equipped with a Fintype instance, a cardinality proof |Ix| = n, and an RSPrimitive tag that supplies its physical meaning.
proof idea
This is a structure definition that directly records the three CoupledAxis fields and the three pairwise independence conditions. No lemmas or tactics are invoked; the declaration serves as a typed record for subsequent cardinality and construction theorems.
why it matters
RSDisjointSum3 supplies the typed carrier for the disjoint_sum_card theorem, which concludes that the summed cardinality equals 3n, and is instantiated in planetStrataSum for the five-element planetary strata model. It realizes the module's core point that same-size axes require distinct primitives for independence, supporting the Recognition Science framework's cross-domain combination infrastructure.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.