pith. machine review for the scientific record. sign in
def

PhiSelection

definition
show as:
view math explainer →
module
IndisputableMonolith.RecogSpec.PhiSelectionCore
domain
RecogSpec
line
7 · github
papers citing
none yet

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

A cached Ask Recognition explainer exists for this declaration.

open explainer

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