rung_strict_ordering
plain-language theorem explainer
The theorem asserts the strict ordering of atmospheric boundary rungs on the phi-ladder, with the tropopause at 0 below the stratopause at 3, the latter below the mesopause interval 4-5, and that interval below the thermosphere at 7. Recognition Science climate analyses cite it to confirm consistency between the phi-derived altitude sequence and observed layer boundaries. The proof reduces the conjunction to three independent numerical inequalities via unfolding and direct computation.
Claim. $0 < 3 land 3 < 4 land 5 < 7$, where these integers are the rung indices assigned to the tropopause, stratopause, lower mesopause, and thermosphere boundaries on the $phi$-altitude ladder.
background
The module develops atmospheric layering as a consequence of the phi-ladder in Recognition Science. Layer boundaries receive integer rung labels such that altitude at rung k equals base altitude times phi to the k. The tropopause sits at rung 0 as the recognition base, the stratopause at rung 3, mesopause between 4 and 5, and thermosphere at rung 7. These numeric assignments appear in the sibling definitions of the module and feed the master certificate that packages the full layering claim. Upstream results supply the individual rung constants, each a fixed natural number chosen to match empirical altitude ratios within the phi scaling.
proof idea
The proof employs a term-mode refinement that decomposes the three-way conjunction into separate goals. Each goal unfolds the pair of rung constants involved and invokes norm_num to confirm the inequality by arithmetic evaluation.
why it matters
This ordering clause is required by the AtmosphericLayeringFromPhiLadderCert structure, which assembles the complete set of rung equalities and inequalities for Track P4. It appears in the one-statement theorem that summarizes the phi-ladder derivation of atmospheric layers. The result anchors the claim that J-cost minima on the recognition lattice produce the observed sequence of lapse-rate reversals, aligning with the self-similar fixed point of the J-function.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.