AtmosphericLayer
AtmosphericLayer enumerates five atmospheric strata as a finite inductive type with decidable equality. Cross-domain proofs in Recognition Science cite it to form the first summand of the 15-element PlanetStratum via disjoint union with EarthLayer and OceanLayer. The declaration is a direct inductive definition that derives Fintype and related instances automatically.
claimLet $L$ be the inductive type with constructors troposphere, stratosphere, mesosphere, thermosphere, exosphere, equipped with decidable equality, representation, boolean equality, and finite cardinality structure.
background
The module establishes a cross-domain claim that Earth comprises three nested D=5 stratifications whose disjoint sum yields 15 elements. AtmosphericLayer supplies the atmospheric summand; the strata occupy distinct radial shells, so the total PlanetStratum is a sum type rather than a product. The definition is imported verbatim from AtmosphericPhysicsFromRS to maintain consistency between the physics and cross-domain modules.
proof idea
The declaration is the base inductive definition with five constructors, automatically deriving DecidableEq, Repr, BEq, and Fintype via the deriving clause.
why it matters in Recognition Science
This supplies the atmospheric component for PlanetStratum and is used in PlanetStratificationCert to certify the 15-element count together with the three proper-subset relations. It fills the combinatorial half of the C2 claim (5+5+5=15) while the module doc notes that phi-ladder wave-speed predictions remain unproved here. The structure aligns with the framework's use of finite sum types for nested radial shells.
scope and limits
- Does not assert physical existence or measured boundaries of the layers.
- Does not derive phi-ladder ratios or wave-speed relations.
- Does not apply to non-Earth bodies or additional strata.
- Does not encode layer thicknesses, densities, or dynamical equations.
formal statement (Lean)
25inductive AtmosphericLayer where
26 | troposphere | stratosphere | mesosphere | thermosphere | exosphere
27 deriving DecidableEq, Repr, BEq, Fintype
28