phi_pow6_gt
plain-language theorem explainer
The theorem proves the strict lower bound 17.944 < φ^6 for the golden ratio φ. Numerics pipelines that bound mass ladders or resonance scales cite it to control growth under integer powers. The proof is a one-line wrapper that substitutes the algebraic identity φ^6 = 8φ + 5 and applies linear arithmetic to the base inequality 1.618 < φ.
Claim. $17.944 < φ^6$ where $φ = (1 + √5)/2$ is the golden ratio.
background
The module supplies rigorous numerical bounds on the golden ratio φ = (1 + √5)/2. It begins from the elementary comparison 2.236 < √5 < 2.237, which yields the base interval 1.618 < φ < 1.6185, then tightens these intervals for higher powers. Two upstream results are required: phi_gt_1618 asserts 1.618 < φ, while phi_pow6_eq asserts the algebraic reduction φ^6 = 8φ + 5 obtained by iterating the minimal relation φ^2 = φ + 1. These bounds sit inside the Recognition Science numerics layer that supplies concrete constants for the phi-ladder mass formula.
proof idea
One-line wrapper that rewrites the power via phi_pow6_eq and then applies linarith to the resulting linear inequality supplied by phi_gt_1618.
why it matters
The result feeds directly into phi_pow76_gt, which lifts the bound to φ^76 for finer numerical control in the same module. It supplies the φ^6 step required for mass verification in the Recognition framework. Within the forcing chain, φ is the self-similar fixed point (T6) whose integer powers appear in the eight-tick octave and the D = 3 spatial structure.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.