AtmosphericLayer
plain-language theorem explainer
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.
Claim. Let $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
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.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.