def definition def or abbrev

`rhoBandLower`

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

formal statement (Lean)

  13def rhoBandLower : ℝ := phi⁻¹ ^ 2

Definition body.

  14
  15/-- The upper cognitive band boundary: `ρ_upper = 1/φ`. -/

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

rhoCriticalMin in IndisputableMonolith.Unification.CriticalRecognitionLoading decl_use
bandBoundaries_product in IndisputableMonolith.Unification.RecognitionBandGeometry decl_use
bandBoundaries_sum_to_one in IndisputableMonolith.Unification.RecognitionBandGeometry decl_use
bandLower_ratio in IndisputableMonolith.Unification.RecognitionBandGeometry decl_use
bandUpper_ratio in IndisputableMonolith.Unification.RecognitionBandGeometry decl_use
one_sub_rhoBandLower_eq_rhoBandUpper in IndisputableMonolith.Unification.RecognitionBandGeometry decl_use
one_sub_rhoBandUpper_eq_rhoBandLower in IndisputableMonolith.Unification.RecognitionBandGeometry decl_use
rhoBandLower_eq in IndisputableMonolith.Unification.RecognitionBandGeometry decl_use
rhoBandLower_lt_one in IndisputableMonolith.Unification.RecognitionBandGeometry decl_use
rhoBandLower_lt_rhoBandUpper in IndisputableMonolith.Unification.RecognitionBandGeometry decl_use
rhoBandLower_pos in IndisputableMonolith.Unification.RecognitionBandGeometry decl_use

Lean names referenced from this declaration's body.