phi_plus_inverse_eq_sqrt5
plain-language theorem explainer
The golden ratio satisfies φ + 1/φ = √5. Researchers bundling RS constant predictions cite it when assembling certificates for α bounds and c = 1. The proof rewrites via the inverse formula, squares 2φ - 1 to reach 5, confirms positivity from the 1.5 lower bound, and closes with nlinarith.
Claim. Let φ be the golden ratio. Then φ + 1/φ = √5.
background
The module supplies calculated proofs for constants listed in the COMPLETE_PROBLEM_REGISTRY, including 0 < α < 0.1, c = 1 in RS-native units, and 0 < k_R < 0.5. The golden ratio φ is the positive root of x² - x - 1 = 0. Upstream lemmas establish the core relations φ² = φ + 1 and 1/φ = φ - 1, together with the tighter bound φ > 1.5.
proof idea
The tactic sequence first rewrites the left side using phi_inverse_formula. It invokes phi_sq_eq to obtain φ² = φ + 1, computes (2φ - 1)² = 5 by nlinarith, verifies positivity via phi_gt_onePointFive, equates the square root of the square to the positive root with Real.sqrt_sq, and finishes with nlinarith.
why it matters
The result appears inside constants_predictions_cert_exists, which packages the full set of proved constant predictions. It supplies one of the phi identities required for the calculated status of the registry items. In the framework it confirms algebraic closure for the self-similar fixed point φ forced at T6.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.