altitude_geometric
plain-language theorem explainer
Adjacent rungs on the phi-ladder satisfy a strict multiplicative relation with ratio phi. Atmospheric modelers using Recognition Science for layer boundary predictions cite this geometric step. The proof is a one-line algebraic reduction that unfolds the altitude definition, applies the power successor rule, and simplifies via ring.
Claim. Let $z_0$ be a real base altitude and $k$ a natural number. Then the altitude at rung $k+1$ equals the altitude at rung $k$ multiplied by $phi$, where altitude at rung $k$ is defined by $z_0 phi^k$.
background
The module derives canonical altitudes for Earth's atmospheric layers from the phi-ladder in Recognition Science. The altitude at rung $k$ is given by $z_0 phi^k$, with $z_0$ the recognition-base altitude set by the J-cost minimum on radiative balance. The module doc states that each layer boundary corresponds to a phi-rung step on the canonical altitude ladder $z_layer(k) = z_0 phi^k$ and that the sequence is forced by J-cost minima of the radiative-convective recognition lattice.
proof idea
The proof unfolds the definition of altitude_at_rung on both sides of the equality, rewrites the successor power via pow_succ, and closes the resulting polynomial identity with the ring tactic.
why it matters
This theorem supplies the altitude_geometric field to the master certificate AtmosphericLayeringFromPhiLadderCert, which certifies rung assignments tropopause at 0, stratopause at 3, and thermosphere at 7. It thereby closes the structural claim of Track P4 that layer boundaries are phi-rung steps, consistent with the self-similar fixed point phi forced in the T0-T8 chain and the Recognition Composition Law.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.