`IndisputableMonolith.Cost.FixedPoint`

IndisputableMonolith/Cost/FixedPoint.lean · 13 lines · 1 declarations

Explainer status: pending

   1import Mathlib
   2import IndisputableMonolith.Constants
   3-- import IndisputableMonolith.PhiSupport  -- [not in public release]
   4
   5namespace IndisputableMonolith
   6namespace Cost
   7
   8/-- Canonical lemma: φ is the positive solution of x = 1 + 1/x. -/
   9lemma phi_is_cost_fixed_point : Constants.phi = 1 + 1 / Constants.phi := by
  10  simpa using IndisputableMonolith.PhiSupport.phi_fixed_point
  11
  12end Cost
  13end IndisputableMonolith

source mirrored from github.com/jonwashburn/shape-of-logic