def definition def or abbrev

`PhiSelection`

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

formal statement (Lean)

   7def PhiSelection (φ : ℝ) : Prop :=

Definition body.

   8  φ ^ 2 = φ + 1 ∧ φ > 0
   9
  10end RecogSpec
  11end IndisputableMonolith

From the project-wide theorem graph. These declarations reference this one in their body.

common_constants_fail_selection in IndisputableMonolith.PhiSupport.Alternatives decl_use
e_fails_selection in IndisputableMonolith.PhiSupport.Alternatives decl_use
pi_fails_selection in IndisputableMonolith.PhiSupport.Alternatives decl_use
sqrt2_fails_selection in IndisputableMonolith.PhiSupport.Alternatives decl_use
sqrt3_fails_selection in IndisputableMonolith.PhiSupport.Alternatives decl_use
sqrt5_fails_selection in IndisputableMonolith.PhiSupport.Alternatives decl_use