OceanLayer
Recognition Science models ocean structure with an inductive enumeration of five layers: surface, thermocline, intermediate, deep, and abyssal. This supplies the ocean component of the PlanetStratum sum type and the count of 5 required for the 15 = 3D stratification certificate. Stratification proofs cite it to establish subset relations and to close the ocean cardinality in the planetary layering structure. The definition is introduced directly as an inductive type carrying standard deriving instances for equality and finiteness.
claimLet OceanLayer be the inductive type whose constructors are surface, thermocline, intermediate, deep, and abyssal.
background
The OceanographyFromRS module states that five canonical ocean layers equal configDim D = 5, with ocean depth following the phi-ladder of recognition density and thermohaline circulation exhibiting five gyres. The same inductive type appears upstream in PlanetStratification, where it is used to form the PlanetStratum abbrev as AtmosphericLayer ⊕ EarthLayer ⊕ OceanLayer. This supplies the ocean cardinality needed for the PlanetStratificationCert structure that records the 15 = 3 × 5 identity and the proper-subset relations among strata.
proof idea
The declaration is a direct inductive definition with five constructors and deriving clauses for DecidableEq, Repr, BEq, and Fintype. No lemmas are invoked and no tactics are applied; the type is primitive.
why it matters in Recognition Science
OceanLayer supplies the cardinality 5 that oceanCount and oceanLayerCount prove by decide, and that PlanetStratificationCert uses to witness ocean_sub and the three_D relation 15 = 3 × 5. It realizes the configDim D = 5 landmark for ocean layers inside the RS stratification chain, consistent with the five-gyre and phi-ladder statements in the module doc.
scope and limits
- Does not assign physical depths or transition criteria to the layers.
- Does not encode rung or gap assignments on the phi-ladder for each layer.
- Does not derive the layer count from the Recognition Composition Law.
- Does not model continuous depth profiles or wave-period dynamics.
formal statement (Lean)
22inductive OceanLayer where
23 | surface | thermocline | intermediate | deep | abyssal
24 deriving DecidableEq, Repr, BEq, Fintype
25