AtmosphericPhysicsCert
plain-language theorem explainer
AtmosphericPhysicsCert is a record bundling the assertions that the set of atmospheric layers has cardinality 5, the set of weather phenomena has cardinality 5, and J-cost at unity equals zero. A researcher deriving climate stability from Recognition Science would cite the record to encode the canonical D=5 counts together with the equilibrium condition. The declaration is a bare structure whose fields are filled by the Fintype cardinalities of two inductive types and an upstream equilibrium lemma.
Claim. Let $L$ be the finite type whose elements are the five atmospheric layers (troposphere through exosphere) and $W$ the finite type whose elements are the five weather phenomena (high pressure through ENSO). The structure AtmosphericPhysicsCert asserts $|L|=5$, $|W|=5$, and $J(1)=0$ where $J$ denotes the J-cost function.
background
The module states that five canonical atmospheric layers equal configDim D=5 and that atmospheric stability is expressed by J-cost balance, with stable layers satisfying J=0 while convective instability requires J>0. The inductive type AtmosphericLayer enumerates troposphere, stratosphere, mesosphere, thermosphere, exosphere; WeatherPhenomenon enumerates highPressure, lowPressure, fronts, jetStreams, enso. Both derive DecidableEq, Repr, BEq, Fintype instances so that their cardinalities are directly 5.
proof idea
This is a structure definition that packages three independent facts. The two cardinality fields are supplied by the Fintype.card instances on the inductive definitions of AtmosphericLayer and WeatherPhenomenon. The equilibrium field is taken directly from the upstream theorem equilibrium, which states At equilibrium: J = 0 and reduces to Jcost_unit0.
why it matters
The structure is the type of the definition atmosphericPhysicsCert that asserts the atmospheric physics facts for the C/E4 Climate section. It instantiates the module claim that five layers and five phenomena equal configDim D together with the J-cost equilibrium property. In the Recognition framework it supplies the concrete D=5 stratification and the equilibrium landmark J=0 without invoking the forcing chain or phi-ladder.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.