phi_quarter_lt
plain-language theorem explainer
The theorem establishes that the fourth root of the golden ratio lies strictly below the certified upper bound 1.12783849. Numerics work in Recognition Science would cite this when assembling interval enclosures for powers of φ on the phi-ladder. The proof raises both sides to the fourth power, chains two decimal inequalities on φ to obtain the powered comparison, and recovers the root inequality via monotonicity of real exponentiation.
Claim. $ (1 + √5)/2 ^{1/4} < 1.12783849 $
background
The module supplies rigorous decimal bounds on the golden ratio φ = (1 + √5)/2 and selected roots by starting from algebraic comparisons on √5. The strategy records that 2.236² < 5 < 2.237², hence 2.236 < √5 < 2.237 and therefore 1.618 < φ < 1.6185, with tighter decimal versions obtained by carrying more places. Upstream lemmas include the definition phi_quarter_hi := 1.12783849 together with the theorem φ < 1.6180340 (proved via sqrt5_lt_22360680) and the auxiliary inequality 1.6180340 < phi_quarter_hi ^ 4.
proof idea
Non-negativity of both sides is recorded first. The identity (goldenRatio ^ (1/4)) ^ 4 = goldenRatio is verified by exponent arithmetic. The comparison goldenRatio < phi_quarter_hi ^ 4 is obtained by transitivity of the two supplied decimal bounds. The powered inequality is then fed to Real.rpow_lt_rpow_iff to conclude the root inequality, after which a simpa normalizes the displayed exponent back to 1/4.
why it matters
The result supplies the upper half of the consolidated quarter-root bounds theorem that appears immediately downstream. It supports numerical verification of self-similar quantities derived from φ, consistent with the fixed-point property of the golden ratio in the Recognition framework and the eight-tick octave structure. The bound is used when placing mass-ladder rungs or computing Berry thresholds that require certified intervals around φ to a fractional power.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.