phi5_gt
plain-language theorem explainer
φ^5 exceeds 11.05 when φ > 1.61. Hubble tension analyses cite the bound to fix the lower edge of the Z-aging amplitude interval that produces the predicted H0 ratio band. The argument substitutes the Fibonacci identity φ^5 = 5φ + 3 and applies linear arithmetic to the upstream lower bound on φ.
Claim. $11.05 < φ^5$, where $φ$ is the golden ratio obeying the Fibonacci identity $φ^5 = 5φ + 3$.
background
The module constructs the Hubble tension pipeline from Z-complexity aging of the recognition field. The amplitude formula is $r_H = 1 + (1/φ^5) · c$ with the closed form $φ^5 = 5φ + 3$ supplied by the Fibonacci identity. Numerics at $φ ∈ (1.61, 1.62)$ place $φ^5 ∈ (11.05, 11.1)$ and $1/φ^5 ∈ (0.0900, 0.0906)$, so that $c ≈ 0.91$ yields a ratio near the empirical value 1.083 inside the target band (1.075, 1.091).
proof idea
The term proof first rewrites the goal via the sibling theorem phi5_eq, replacing $φ^5$ by $5φ + 3$. It then invokes linarith on the upstream lemma phi_gt_onePointSixOne that supplies the strict inequality $φ > 1.61$, producing the numerical claim directly.
why it matters
The result supplies the lower bound phi5_lower inside the hubbleTensionCert definition that certifies the RS-predicted H0 ratio band contains the observed SH0ES/Planck value. It closes the A5 precision step of the Z-aging pipeline, confirming consistency with the recognition composition law and the eight-tick octave. The bound touches the open question whether the five Z-aging channels (D = 5) reproduce the exact tension amplitude without extra parameters.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.