OceanLayer
plain-language theorem explainer
The OceanLayer inductive type enumerates the five radial ocean strata in the Recognition Science cross-domain model. Researchers assembling planet-wide stratification sums cite it to supply the oceanic summand in the total fifteen-element PlanetStratum. The definition is a direct inductive enumeration equipped with deriving clauses for decidable equality and finite cardinality.
Claim. Let OceanLayer be the inductive type with constructors surface, thermocline, intermediate, deep, and abyssal.
background
The Planet Stratification module models Earth via three nested five-layer stratifications whose disjoint sum yields fifteen strata total. Unlike a product, the sum reflects that the strata occupy distinct radial shells. OceanLayer supplies the oceanic component and is imported from the upstream OceanographyFromRS module, where the same five constructors appear.
proof idea
The declaration is the inductive definition itself, introducing the five constructors and deriving DecidableEq, Repr, BEq, and Fintype instances.
why it matters
OceanLayer supplies one of the three summands in the 5+5+5=15 claim of the C2 cross-domain wave. It is used by oceanCount, ocean_is_proper_subset, PlanetStratificationCert, and the PlanetStratum abbrev. The module proves only the combinatorial structure; the predicted phi-ladder ratios for wave speeds remain outside the Lean file.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.