OceanographyCert
plain-language theorem explainer
OceanographyCert is the structure type whose single field records that the ocean layer enumeration has cardinality five. A physicist modeling planetary stratification in Recognition Science would cite it to confirm the five-layer decomposition matches configDim D = 5. The definition is a direct record whose field is discharged by the Fintype instance on the inductive type OceanLayer.
Claim. Let $O$ be the inductive type with constructors surface, thermocline, intermediate, deep, and abyssal. OceanographyCert is the structure whose sole field is the assertion that the cardinality of $O$ equals 5.
background
The module develops oceanographic consequences inside Recognition Science. It states that five canonical layers—surface, thermocline, intermediate, deep, abyssal—equal configDim D = 5, with ocean depth following the phi-ladder of recognition density and surface wave periods in the 5φ/φ range. OceanLayer is the inductive type enumerating these layers and carries DecidableEq, Repr, BEq, and Fintype instances. The same inductive type appears upstream in PlanetStratification, supplying the Fintype cardinality fact used here.
proof idea
OceanographyCert is a structure definition. Its field is filled by the cardinality computation supplied by the Fintype instance on OceanLayer; no tactics or lemmas beyond that instance are applied.
why it matters
The structure is instantiated by the downstream oceanographyCert definition in the same module. It supplies the five-layer count required to embed oceanography into the Recognition Science framework, aligning with the module's claim that thermohaline circulation involves five canonical gyres and that depth follows the phi-ladder. The declaration closes the local configDim D = 5 statement without further hypotheses.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.