oceanCount
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.
claimThe 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 in Recognition Science
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.
scope and limits
- Does not prove the physical existence or stability of the five ocean layers.
- Does not derive the layer count from the phi-ladder or any Recognition Science forcing chain.
- Does not address dynamical properties such as wave propagation or phase velocities.
- Does not claim that the five-layer division is unique or exhaustive across all planets.
formal statement (Lean)
39theorem oceanCount : Fintype.card OceanLayer = 5 := by decide
proof body
40