phi_inverse_formula
plain-language theorem explainer
The identity 1/φ = φ - 1 holds for the golden ratio φ satisfying φ² = φ + 1 with φ > 0. Researchers deriving constant predictions in Recognition Science cite this when simplifying expressions that mix φ and its reciprocal. The proof is a short algebraic reduction that invokes the quadratic relation, applies field simplification, and closes via linear arithmetic.
Claim. $1/φ = φ - 1$, where φ > 0 satisfies φ² = φ + 1.
background
This theorem sits in the module of calculated proofs for constants predicted by the Recognition Science framework. The golden ratio φ enters via the defining identity φ² = φ + 1, which is the quadratic relation x² - x - 1 = 0 solved for the positive root. Upstream lemma phi_sq_eq states: 'Key identity: φ² = φ + 1 (from the defining equation x² - x - 1 = 0).' The module also records proved bounds for α, c = 1 in RS-native units, and the Boltzmann analog k_R, all obtained with norm_num, nlinarith, and positivity.
proof idea
The proof first obtains φ > 0 from phi_pos. It then substitutes the identity φ² = φ + 1 supplied by phi_sq_eq. Field simplification rewrites the target 1/φ = φ - 1 into an equivalent polynomial equation, after which nlinarith discharges the goal by linear arithmetic.
why it matters
The result is packaged inside constants_predictions_cert_exists, the theorem that assembles the full certificate of proved constant predictions. It is also invoked directly by the sibling theorem phi_plus_inverse_eq_sqrt5 to obtain φ + 1/φ = √5. In the broader framework it supplies the algebraic relation needed for the phi-ladder mass formula and the self-similar fixed point that appears in the forcing chain after T6.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.