oceanCount
plain-language theorem explainer
oceanCount asserts that the ocean stratification type has exactly five elements. Cross-domain Recognition Science modelers cite it when assembling the total planetary stratum count of fifteen. The proof is a one-line wrapper that applies the decide tactic to the Fintype instance of the five-constructor inductive type.
Claim. The cardinality of the ocean layer type is five: $|OceanLayer| = 5$, where $OceanLayer$ is the inductive type whose constructors are surface, thermocline, intermediate, deep, and abyssal.
background
The module CrossDomain.PlanetStratification presents three nested radial stratifications of Earth as a disjoint sum: AtmosphericLayer, EarthLayer, and OceanLayer, each carrying five elements for a total of fifteen. This structure is combinatorial rather than dynamical; the module notes that the strata occupy distinct radial shells and therefore form a sum type. OceanLayer is introduced as an inductive type with exactly those five constructors, deriving Fintype (among other instances) so that its cardinality is computable. The upstream result supplying this definition appears in both the local module and the OceanographyFromRS import.
proof idea
The proof is a one-line wrapper that invokes the decide tactic. This tactic directly evaluates the equality Fintype.card OceanLayer = 5 by enumerating the five constructors of the inductive definition.
why it matters
oceanCount supplies one summand in planetStratumCount, which establishes the total of fifteen strata, and is referenced by ocean_is_proper_subset to show that the full PlanetStratum properly contains the ocean subset. The module doc frames the 5+5+5 structure as the combinatorial skeleton for Wave 62 cross-domain claims, with the parent theorems closing the count and the subset relation. It touches the Recognition Science pattern of D = 5 stratifications in this domain while leaving open the empirical test that wave speeds should obey phi-ladder ratios.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.