phi_tight_bounds
plain-language theorem explainer
The golden ratio satisfies the decimal bounds 1.61803395 < φ < 1.6180340. Numerics and physics modules cite this bundled interval whenever a verified tight range for φ is needed in phi-ladder or J-cost calculations. The proof is a one-line term that directly pairs the lower and upper bound lemmas already proved in the same module.
Claim. $1.61803395 < φ < 1.6180340$ where $φ = (1 + √5)/2$ is the golden ratio.
background
The module supplies rigorous decimal bounds on φ = (1 + √5)/2 by comparing squares of rational approximations to 5. The strategy uses 2.2360679² < 5 < 2.2360680² to obtain corresponding bounds on √5 and hence on φ. Upstream lemmas phi_gt_161803395 and phi_lt_16180340 establish the separate inequalities that are combined here.
proof idea
The proof is a term-mode wrapper that constructs the conjunction by applying the pair of theorems phi_gt_161803395 and phi_lt_16180340.
why it matters
This supplies the canonical tight bound on φ that feeds into downstream results such as the IMF slope theorem in ObservabilityLimits and the V_ub match in CKMGeometry. It aligns with the Recognition Science framework where φ is the self-similar fixed point (T6) used to define the eight-tick octave and mass ladder. The bound ensures numerical stability in J-cost calculations.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.