theorem proved term proof

`phi_inverse_formula`

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

formal statement (Lean)

 169theorem phi_inverse_formula : 1 / phi = phi - 1 := by

proof body

Term-mode proof.

 170  have h1 : phi > 0 := phi_pos
 171  have h2 : phi^2 = phi + 1 := phi_sq_eq
 172  field_simp
 173  nlinarith
 174
 175/-- **CALCULATED**: φ + 1/φ = √5. -/

used by (2)

From the project-wide theorem graph. These declarations reference this one in their body.

constants_predictions_cert_exists in IndisputableMonolith.Unification.ConstantsPredictionsProved decl_use
phi_plus_inverse_eq_sqrt5 in IndisputableMonolith.Unification.ConstantsPredictionsProved decl_use

depends on (2)

Lean names referenced from this declaration's body.

phi_sq_eq in IndisputableMonolith.Constants decl_use
phi_sq_eq in IndisputableMonolith.NumberTheory.PhiLadderLattice decl_use