atmosphericLayerCount
plain-language theorem explainer
The declaration fixes the finite cardinality of atmospheric layers at five, matching the canonical sequence from troposphere to exosphere. Workers on Recognition Science planetary stratification cite it to set the atmospheric dimension in coupled-axis constructions and total-strata sums. The proof is a one-line decision procedure that enumerates the five inductive constructors via their derived Fintype instance.
Claim. The finite cardinality of the type of atmospheric layers equals five, where the layers are enumerated as troposphere, stratosphere, mesosphere, thermosphere, and exosphere: $ |L| = 5 $ with $ L = $ {troposphere, stratosphere, mesosphere, thermosphere, exosphere}.
background
The module sets atmospheric physics inside Recognition Science by equating five canonical layers to configDim D = 5. Atmospheric stability is expressed as J-cost balance: convective instability occurs for J > 0 while inversion layers remain stable at J = 0. The inductive type AtmosphericLayer is defined with exactly those five constructors and carries DecidableEq, Repr, BEq, and Fintype instances.
proof idea
The proof is a one-line wrapper that applies the decide tactic. The tactic succeeds because the inductive type supplies a decidable Fintype instance whose cardinality is computed by enumerating the five constructors.
why it matters
The result supplies the layer count to atmosphericPhysicsCert, to the CoupledAxis 5 definition in atmosphereAxis, and to the total-strata sum planet_strata_total_15. It anchors the atmospheric component of the five-layer stratification that the framework equates with configDim D = 5, feeding directly into the 15-layer planetary total and the RSPrimitive.phiLadder construction.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.