atmosphereAxis
plain-language theorem explainer
The definition equips the five atmospheric layers with the structure of a coupled axis of length 5 tagged by the phi-ladder primitive. Researchers assembling the planetary 15-stratum direct sum cite this when forming the atmosphere component of the three-stack decomposition. The construction is a direct record instantiation that pulls finiteness from the typeclass, cardinality from the layer-count theorem, and the primitive tag from RSPrimitive.
Claim. Let $L$ be the inductive type with five constructors for the atmospheric layers. Define the coupled axis of size 5 by the record with index set $L$, cardinality equality $Fintype.card(L)=5$, and primitive tag the phi-ladder constructor.
background
A CoupledAxis of size $n$ is a finite type $Ix$ equipped with a cardinality proof equal to $n$ and a tag drawn from the five RSPrimitive constructors. The index type here is AtmosphericLayer, the inductive type whose constructors are troposphere, stratosphere, mesosphere, thermosphere, and exosphere. The module C2 realizes the planetary 15-stratum direct sum as an RS disjoint sum of three independent 5-strata stacks (atmosphere, solid Earth, ocean); this definition supplies the atmosphere stack. The upstream atmosphericLayerCount theorem states that $Fintype.card(AtmosphericLayer)=5$.
proof idea
The definition populates the CoupledAxis 5 record by setting the index type to AtmosphericLayer, obtaining the Fintype instance by inference, setting the cardinality field to the atmosphericLayerCount theorem, and selecting the phiLadder constructor of RSPrimitive.
why it matters
This supplies the atmosphere axis inside planetStrataSum, which assembles the full RSDisjointSum3 5 realizing the 15-stratum decomposition. It implements the phi-ladder primitive for one of the three 5-layer stacks in the C2 module; the framework uses such tagged axes to organize strata before the direct-sum step, with no dynamical content derived here.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.