theorem proved term proof

`log_phi_interval_contains`

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

formal statement (Lean)

  51theorem log_phi_interval_contains :
  52    logPhiInterval.contains (Real.log ((1 + Real.sqrt 5) / 2)) := log_phi_in_interval

Term-mode proof.

  53
  54/-- Example: Prove log(φ) > 0.48 (using interval lo = 481/1000 = 0.481) -/

Lean names referenced from this declaration's body.