phi5_lt
plain-language theorem explainer
The theorem establishes that φ^5 is strictly less than 11.11 for the golden ratio φ. Cosmologists working on the Hubble tension via Z-aging corrections in Recognition Science cite this bound to fix the upper edge of the amplitude interval. The proof is a one-line term that rewrites φ^5 via the Fibonacci identity and applies linear arithmetic to the upstream bound φ < 1.62.
Claim. Let φ denote the golden ratio. Then φ^5 < 11.11.
background
In Recognition Science the golden ratio φ is the self-similar fixed point forced by the J-uniqueness relation. The Fibonacci identity φ^5 = 5φ + 3 is proved once in Constants and re-exported across cosmology modules; the module doc states that φ^5 lies in (11.05, 11.1) for φ ∈ (1.61, 1.62) and normalizes the Z-aging amplitude c ≈ 0.91. The upstream lemma phi_lt_onePointSixTwo supplies the tighter bound φ < 1.62 obtained from √5 < 2.24.
proof idea
The proof is a one-line wrapper: it rewrites the left-hand side with the Fibonacci identity phi5_eq, then invokes the linarith tactic on the hypothesis phi_lt_onePointSixTwo.
why it matters
The bound supplies the phi5_upper field of the hubbleTensionCert definition, which assembles the full HubbleTensionCert structure for the Z-aging pipeline. It closes the numerical interval required to place the predicted H_0 ratio inside (1.075, 1.091) and thereby contain the empirical SH0ES/Planck value 1.083. In the framework it constrains the five Z-aging channels that accumulate the recognition-field aging correction over cosmic time.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.