`IndisputableMonolith.RecogSpec.PhiSelectionCore`

IndisputableMonolith/RecogSpec/PhiSelectionCore.lean · 12 lines · 1 declarations

Explainer status: pending

   1import Mathlib
   2
   3namespace IndisputableMonolith
   4namespace RecogSpec
   5
   6/-- φ selection criterion: φ² = φ + 1 and φ > 0. -/
   7def PhiSelection (φ : ℝ) : Prop :=
   8  φ ^ 2 = φ + 1 ∧ φ > 0
   9
  10end RecogSpec
  11end IndisputableMonolith
  12

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