ocean_is_proper_subset
plain-language theorem explainer
The declaration establishes that the total cardinality of planetary strata exceeds the ocean layer cardinality alone. Researchers formalizing nested planetary structure in Recognition Science cite it to confirm the 15-element sum from three disjoint 5-element layers. The proof rewrites the inequality to the precomputed cardinalities of the sum type and the ocean layer then decides the numerical comparison.
Claim. $|AtmosphericLayer ⊕ EarthLayer ⊕ OceanLayer| > |OceanLayer|$
background
The module formalizes C2 planet stratification as three nested D=5 layers whose disjoint sum yields fifteen strata total. PlanetStratum is defined as the sum type AtmosphericLayer ⊕ EarthLayer ⊕ OceanLayer, while OceanLayer is the inductive type with five constructors (surface, thermocline, intermediate, deep, abyssal). The module documentation states that the layers occupy distinct radial shells, making the structure a sum rather than a product.
proof idea
The proof is a one-line wrapper that rewrites the goal using planetStratumCount and oceanCount then applies decide to confirm the resulting inequality 15 > 5.
why it matters
The result supplies the ocean subset relation inside planetStratificationCert, which collects all cardinality and proper-subset facts for the full stratification. It fills the combinatorial claim that 5 + 5 + 5 = 15 in the C2 cross-domain section, consistent with the framework's use of layer counts scaled by D = 5. No open scaffolding questions are touched.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.