AtmosphericLayer
plain-language theorem explainer
AtmosphericLayer enumerates the five canonical atmospheric layers as an inductive type realizing configDim D = 5 in the Recognition Science model. Atmospheric physicists working inside the RS framework cite it to fix the layer set for J-cost stability calculations and stratification certificates. The declaration is a pure inductive enumeration that derives DecidableEq, Repr, BEq and Fintype instances with no separate proof body.
Claim. Let $L$ be the finite set of atmospheric layers defined inductively by the five constructors troposphere, stratosphere, mesosphere, thermosphere, exosphere. Then $|L| = 5$ and $L$ carries decidable equality together with the standard type-class instances for representation and finiteness.
background
Recognition Science models atmospheric stability via J-cost balance on the forcing chain, where convective instability requires J > 0 for a rising parcel and stable layers satisfy J = 0. The module AtmosphericPhysicsFromRS sets the five canonical layers equal to configDim D = 5, matching the five weather phenomena treated in the same file. This inductive definition is the same object imported from PlanetStratification to keep cross-domain strata consistent.
proof idea
The declaration is an inductive definition with zero proof lines. The deriving clause directly installs DecidableEq, Repr, BEq and Fintype; no lemmas are applied.
why it matters
AtmosphericLayer supplies the atmospheric summand for PlanetStratum and the cardinality hypothesis in PlanetStratificationCert (15 = 3 * 5 with atmosphere a proper subset). It anchors the claim that atmospheric stability equals J-cost balance and feeds atmosphericLayerCount, atmoCount, atmo_is_proper_subset and atmosphereAxis. The definition closes the D = 5 scaffolding for the C/E4 climate model without axioms.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.