phi_pow76_gt
plain-language theorem explainer
This theorem proves the strict inequality 7638724000000000 < φ^76 for the golden ratio φ. It is cited inside mass-verification lemmas that anchor the phi-ladder numerics. The proof factors the exponent as 70 + 6, pulls the two prior lower bounds, and chains them with a short calc block of numerical comparisons.
Claim. $7638724000000000 < φ^{76}$, where $φ = (1 + √5)/2$ denotes the golden ratio.
background
The Numerics.Interval.PhiBounds module supplies rigorous lower and upper bounds on integer powers of φ by starting from tight algebraic inequalities on √5 (2.236 < √5 < 2.237) and propagating them via the functional equation satisfied by φ. Two immediate upstream results are used: phi_pow6_gt asserts 17.944 < φ^6 and phi_pow70_gt asserts 425698000000000 < φ^70. These stepping-stone bounds are themselves obtained from the same √5 sandwich and the recurrence φ^{n} = φ^{n-1} + φ^{n-2}.
proof idea
The tactic proof rewrites φ^76 = φ^70 · φ^6 by ring_nf, retrieves the two lower bounds via have, asserts positivity of φ^70, and then executes a three-line calc that compares the target constant first to the product of the two numerical bounds (norm_num), then replaces each factor by the corresponding power (nlinarith twice).
why it matters
The declaration is invoked by the private lemma phi76_gt inside Masses.Verification, which rewrites Constants.phi to goldenRatio and applies this bound directly. It therefore supplies a concrete numerical anchor for the 76th rung of the phi-ladder used in mass verification, consistent with the self-similar fixed-point property (T6) and the eight-tick octave structure (T7) of the Recognition Science forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.