mesopause_rung_lower
plain-language theorem explainer
The definition assigns natural number 4 as the lower rung index for the mesopause on the phi-ladder of atmospheric boundaries. Climate modelers working from Recognition Science would cite it when checking predicted altitude ratios against observed lapse-rate reversals. It is introduced by direct constant assignment with no computation or lemmas.
Claim. The lower rung index for the mesopause layer on the phi-altitude ladder is defined to be the natural number $4$.
background
Recognition Science places Earth's atmospheric boundaries on the phi-ladder via z_layer(k) = z_0 · phi^k, where z_0 is the recognition-base altitude fixed by J-cost minimum on radiative-convective balance. The module treats the five canonical layers as successive rung steps, with empirical ratios (stratopause/tropopause ≈ 4.17, mesopause/stratopause ≈ 1.70) recovered from phi-powers once rung skips are allowed. Upstream rung definitions appear in mass-anchor and particle contexts but are reused here only as integer indices for layer boundaries.
proof idea
Direct definition that assigns the constant 4.
why it matters
The definition supplies the lower mesopause rung required by AtmosphericLayeringFromPhiLadderCert and by the one-statement theorem atmospheric_layering_one_statement, which together close Track P4. It completes the sequence 0-3-4/5-7 that yields the phi^3 and phi^7 altitude ratios inside empirical bands, consistent with the self-similar fixed point phi and the eight-tick octave of the forcing chain. It leaves open the precise placement of the upper mesopause rung relative to observed 85 km data.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.