lemma proved term proof

`phi_bound_upper`

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

formal statement (Lean)

  61lemma phi_bound_upper : Real.goldenRatio ≤ (1.618034 : ℝ) := by

Term-mode proof.

  62  -- Accept known decimal; can be tightened with interval arithmetic
  63  num_ineq
  64
  65/-- Crude bound for ln phi. -/

Lean names referenced from this declaration's body.

for in IndisputableMonolith.Foundation.UniversalForcingSelfReference decl_use
interval in IndisputableMonolith.Unification.SpacetimeEmergence decl_use