planetStratumCount
plain-language theorem explainer
The theorem establishes that the cardinality of the planet stratum type equals 15 by summing the sizes of its three disjoint components. Cross-domain researchers applying Recognition Science to planetary models cite this result when confirming the additive structure of nested radial shells. The proof is a one-line simplification that unfolds the sum-type definition and substitutes the precomputed cardinalities of five elements per layer.
Claim. Let $S = A_5 + E_5 + O_5$ be the disjoint union of the atmospheric, earth, and ocean layer types, each of cardinality 5. Then $|S| = 15$.
background
The CrossDomain.PlanetStratification module models Earth as three nested stratifications at distinct radial shells, formalized as the sum type PlanetStratum := AtmosphericLayer ⊕ EarthLayer ⊕ OceanLayer. Because the layers occupy mutually exclusive radii, the structure is a disjoint sum rather than a product; the module documentation states that this yields the combinatorial identity 5 + 5 + 5 = 15. Each component cardinality is supplied by the sibling theorems atmoCount, earthCount, and oceanCount, each proved by decide.
proof idea
The proof is a one-line wrapper that applies simp to the definition of PlanetStratum together with Fintype.card_sum and the three layer-count theorems. It therefore reduces the claim directly to the arithmetic identity 5 + 5 + 5 = 15 without further case analysis.
why it matters
The result supplies the stratum_count field inside planetStratificationCert and is invoked by the three proper-subset theorems that follow. It realizes the C2 structural claim of the module that three nested D = 5 stratifications cover the planet, consistent with the framework's preference for additive compositions on nested domains. No open scaffolding remains in the supplied material.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.