phi_pow76_lt
plain-language theorem explainer
The theorem supplies the concrete upper bound φ^76 < 7.646046 × 10^15 for the golden ratio. Mass-verification code in the Recognition framework cites it when placing particles on the phi-ladder mass formula. The proof splits the exponent algebraically into 70 + 6, invokes the two prior power bounds, and finishes with nlinarith plus norm_num comparison.
Claim. $φ^{76} < 7646046000000000$ where $φ = (1 + √5)/2$ is the golden ratio.
background
The module Numerics.Interval.PhiBounds supplies rigorous interval bounds on φ by starting from 2.236² < 5 < 2.237² and propagating to tighter decimal estimates on φ itself. These bounds are then lifted to high powers via repeated multiplication and algebraic identities. The immediate predecessors are the theorems phi_pow70_lt (φ^70 < 4.26011 × 10^14) and phi_pow6_lt (φ^6 < 17.948), both obtained by the same reduction-to-lower-powers pattern.
proof idea
Ring_nf rewrites the exponent as 76 = 70 + 6. The two prior bounds phi_pow70_lt and phi_pow6_lt are pulled in, positivity of φ^6 is asserted, and a calc block applies nlinarith to the product inequality followed by norm_num to reach the target constant.
why it matters
The bound is consumed by the lemma phi76_lt in Masses.Verification, which rewrites Constants.phi to goldenRatio and applies this result directly. It therefore supplies one concrete numerical anchor for the phi-ladder mass formula yardstick · φ^(rung − 8 + gap(Z)) used in particle-mass checks. The step sits inside the T6 self-similar fixed-point construction and the eight-tick octave scaling.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.