def definition def or abbrev

`phi_to_e`

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

formal statement (Lean)

  79noncomputable def phi_to_e : ℝ := phi ^ (exp 1)

proof body

Definition body.

  80
  81/-! ## Possible φ-Formulas for e -/
  82
  83/-- Attempt 1: e ≈ φ + φ⁻¹ + 1/2
  84
  85    φ + 1/φ = φ + φ - 1 = 2φ - 1 ≈ 2.236
  86    Plus 1/2 = 2.736 (not quite e ≈ 2.718) -/

depends on (2)

Lean names referenced from this declaration's body.

for in IndisputableMonolith.Foundation.UniversalForcingSelfReference decl_use
Possible in IndisputableMonolith.Modal.Possibility decl_use