planet_strata_disjoint_sum_15
plain-language theorem explainer
The theorem establishes that the three 5-stratum axes for atmosphere, Earth, and ocean form an RS disjoint sum whose total cardinality is exactly 15. A physicist building Recognition Science planetary models would cite this to fix the structural count before any dynamics. The proof is a one-line rewrite that instantiates the general disjoint-sum cardinality lemma on the planetStrataSum definition.
Claim. Let $S$ be the RS disjoint sum of three independent 5-element strata stacks (atmosphere, solid Earth, ocean). Then $|S_1| + |S_2| + |S_3| = 15$.
background
Module C2 models the planet as three independent 5-stratum stacks whose cardinalities add directly rather than tensor. RSDisjointSum3 n is the structure carrying three axes, each of size n, together with independence proofs. planetStrataSum instantiates this at n=5 by setting axis1 to atmosphereAxis, axis2 to earthAxis, and axis3 to oceanAxis. The upstream disjoint_sum_card theorem states that any RSDisjointSum3 n satisfies the sum of its three Fintype.card values equals 3*n.
proof idea
One-line wrapper that applies disjoint_sum_card to the planetStrataSum instance.
why it matters
This supplies the rs_sum_15 field inside the PlanetStrataCert definition, closing the finite structural claim for the C2 module. It directly instantiates the general RSDisjointSum3 cardinality result at n=5, matching the three-stack planetary model described in the module header. The module notes that wave-speed phi-ratio predictions remain empirical and outside this proof.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.