planetStratumCount
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.
claimLet $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 in Recognition Science
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.
scope and limits
- Does not derive the five-layer division from the phi-ladder or J-cost function.
- Does not assert empirical match to observed geological boundaries.
- Does not predict wave speeds or phase velocities at stratum interfaces.
- Does not claim this stratification is the unique model permitted by Recognition Science.
Lean usage
rw [planetStratumCount]formal statement (Lean)
43theorem planetStratumCount : Fintype.card PlanetStratum = 15 := by
proof body
Term-mode proof.
44 simp only [PlanetStratum, Fintype.card_sum, atmoCount, earthCount, oceanCount]
45
46/-- The three injections are not surjective: each covers only 5 of 15. -/