ocean_is_proper_subset
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 in Recognition Science
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.
scope and limits
- Does not prove the physical existence or observability of the five-layer divisions.
- Does not derive the layer count from the phi-ladder or Recognition Science forcing chain.
- Does not address wave speeds, phase velocities, or any dynamical predictions.
- Does not connect the stratification to spatial dimension D = 3 or the eight-tick octave.
formal statement (Lean)
55theorem ocean_is_proper_subset :
56 Fintype.card PlanetStratum > Fintype.card OceanLayer := by
proof body
Term-mode proof.
57 rw [planetStratumCount, oceanCount]; decide
58
59/-- 15 = 3 × D (where D = 5). -/