disjoint_sum_card
plain-language theorem explainer
The theorem shows that any RSDisjointSum3 structure S of parameter n has the sum of cardinalities of its three axes equal to 3n. Researchers modeling multi-domain state counting in Recognition Science would cite this when verifying totals for pairwise independent coupled axes. The proof is a direct rewriting of each axis cardinality followed by algebraic simplification.
Claim. Let $S$ be a pairwise independent disjoint sum of three coupled axes each of cardinality $n$. Then the sum of the three axis cardinalities equals $3n$.
background
The RS-Coupled Axes module supplies infrastructure for cross-domain combination theorems. Two finite axes of equal cardinality count as independent only when tagged by distinct recognition primitives. The structure RSDisjointSum3 n packages three CoupledAxis n together with explicit pairwise independence proofs between each pair.
proof idea
The proof is a term-mode reduction that rewrites each of the three Fintype.card terms using the card_eq property of the respective axis inside S, then applies the ring tactic to obtain equality with 3n.
why it matters
This cardinality identity is invoked directly by planet_strata_disjoint_sum_15 to obtain a concrete total of 15. It supplies a basic counting tool for three-axis combinations inside the Recognition Science framework, aligning with the eight-tick octave and the emergence of three spatial dimensions.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.