phi_pow16_lt
plain-language theorem explainer
The theorem establishes an upper bound of 2207.5 on the golden ratio raised to the sixteenth power. Interval arithmetic practitioners verifying powers of φ for Recognition Science numerics would cite it. The proof substitutes the closed-form expression φ^16 = 987φ + 610 and reduces the resulting linear inequality via the bound φ < 1.6185.
Claim. Let φ = (1 + √5)/2. Then φ^{16} < 2207.5.
background
The module supplies rigorous bounds on the golden ratio φ using its algebraic properties and interval estimates derived from √5. It starts from the inequalities 2.236² < 5 < 2.237² to sandwich φ between 1.618 and 1.6185, then tightens these for applications in higher powers.
proof idea
The proof rewrites the target inequality using the equality φ^16 = 987 φ + 610. It then applies the known upper bound φ < 1.6185 and invokes linear arithmetic to verify the resulting numerical inequality.
why it matters
This result feeds directly into the proofs of φ^32 < 4873100 and φ^70 < 426011000000000, as well as the interval membership check for φ^16 in the Pow module. It contributes to the numerical scaffolding required for the phi-ladder in mass formulas, where φ-powers determine discrete rungs, and supports verification of constants such as the fine-structure inverse in the interval (137.030, 137.039).
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.