def
definition
PhiSelection
show as:
view math explainer →
open explainer
Read the cached plain-language explainer.
open lean source
IndisputableMonolith.RecogSpec.PhiSelectionCore on GitHub at line 7.
browse module
All declarations in this module, on Recognition.
explainer page
used by
formal source
4namespace RecogSpec
5
6/-- φ selection criterion: φ² = φ + 1 and φ > 0. -/
7def PhiSelection (φ : ℝ) : Prop :=
8 φ ^ 2 = φ + 1 ∧ φ > 0
9
10end RecogSpec
11end IndisputableMonolith