  10noncomputable section
  11
  12/-- The lower cognitive band boundary: `ρ_min = 1/φ²`. -/
  13def rhoBandLower : ℝ := phi⁻¹ ^ 2
  14
  15/-- The upper cognitive band boundary: `ρ_upper = 1/φ`. -/
  16def rhoBandUpper : ℝ := phi⁻¹
  17
  18theorem rhoBandLower_eq : rhoBandLower = phi⁻¹ ^ 2 := by
  19  rfl
  20
  21theorem rhoBandUpper_eq : rhoBandUpper = phi⁻¹ := by
  22  rfl
  23
  24theorem rhoBandUpper_pos : 0 < rhoBandUpper := by
  25  unfold rhoBandUpper
  26  exact inv_pos.mpr phi_pos
  27
  28theorem rhoBandUpper_lt_one : rhoBandUpper < 1 := by
  29  unfold rhoBandUpper
  30  exact inv_lt_one_of_one_lt₀ one_lt_phi
  31
  32theorem rhoBandLower_pos : 0 < rhoBandLower := by
  33  unfold rhoBandLower
  34  have h : 0 < phi⁻¹ := inv_pos.mpr phi_pos
  35  positivity
  36
  37theorem rhoBandLower_lt_one : rhoBandLower < 1 := by
  38  unfold rhoBandLower
  39  have hpos : 0 < phi⁻¹ := inv_pos.mpr phi_pos
  40  have hlt : phi⁻¹ < 1 := inv_lt_one_of_one_lt₀ one_lt_phi
  41  nlinarith
  42
  43theorem rhoBandLower_lt_rhoBandUpper : rhoBandLower < rhoBandUpper := by

papers checked against this theorem

No papers in the current corpus map onto this theorem yet.