pith. machine review for the scientific record. sign in
theorem proved tactic proof high

phi_cubed_eq

show as:
view Lean formalization →

The algebraic identity φ³ = 2φ + 1 holds for the golden ratio φ. Atmospheric modelers using the φ-ladder for layer boundaries cite this to obtain the stratopause-to-tropopause ratio near 4.2. The proof substitutes the quadratic φ² = φ + 1 into φ³ = φ · φ² and reduces with ring arithmetic.

claim$φ^3 = 2φ + 1$, where $φ$ is the positive root of $x^2 - x - 1 = 0$ (hence $φ^2 = φ + 1$).

background

The module derives canonical Earth atmospheric layer altitudes from the φ-ladder in Recognition Science. Each boundary corresponds to a rung step on the altitude ladder $z(k) = z_0 · φ^k$, with $z_0$ the recognition-base altitude set by J-cost minimum on radiative balance. The empirical stratopause/tropopause ratio ≈ 4.17 is recovered as the three-rung jump φ³.

proof idea

The proof obtains φ² = φ + 1 from phi_sq_eq. It rewrites φ³ as φ² · φ via ring, substitutes the quadratic, applies ring_nf, then rewrites again with phi_sq_eq and finishes with ring to reach 2φ + 1.

why it matters in Recognition Science

This supplies the closed-form ratio for the stratopause/tropopause boundary. It feeds directly into stratopause_tropopause_ratio_band and stratopause_tropopause_ratio_gt_4 in the same module, and into phi_cubed_band and TidalLockingFromPhiResonanceCert in Astrophysics. Within the framework it instantiates the self-similar fixed point φ from T6 of the forcing chain, enabling prediction of layer spacings via the eight-tick octave.

scope and limits

Lean usage

rw [phi_cubed_eq]

formal statement (Lean)

 153theorem phi_cubed_eq : phi ^ 3 = 2 * phi + 1 := by

proof body

Tactic-mode proof.

 154  have h : phi ^ 2 = phi + 1 := phi_sq_eq
 155  have h_step : phi ^ 3 = phi ^ 2 * phi := by ring
 156  rw [h_step, h]
 157  ring_nf
 158  rw [h]
 159  ring
 160
 161/-- The ratio is strictly above 4. -/

used by (20)

From the project-wide theorem graph. These declarations reference this one in their body.

depends on (9)

Lean names referenced from this declaration's body.