Jcost_min_at_one

formal source

 225  · exact Jcost_pos_away_from_one r hr
 226
 227/-- J-cost is minimized at r = 1 (balanced firing rates). -/
 228theorem Jcost_min_at_one : Jcost 1 = 0 := Jcost_unit0
 229
 230/-- J-cost is strictly positive when r ≠ 1. -/
 231theorem Jcost_pos_of_ne_one (r : ℝ) (hr : 0 < r) (hr_ne : r ≠ 1) :
 232    0 < Jcost r := by
 233  have h := Jcost_eq_sq (ne_of_gt hr)
 234  rw [h]
 235  apply div_pos
 236  · have : r - 1 ≠ 0 := sub_ne_zero.mpr hr_ne
 237    positivity
 238  · positivity
 239
 240/-! ## §5  Working Memory Capacity -/
 241
 242/-- Working memory capacity prediction: φ³ ≈ 4.236.
 243    The cache hierarchy at ratio φ gives Level 1 (working memory)
 244    capacity = φ³ relative to Level 0 (focal attention, capacity 1). -/
 245noncomputable def working_memory_capacity : ℝ := phi ^ 3
 246
 247theorem working_memory_approx :
 248    4 < working_memory_capacity ∧ working_memory_capacity < 5 := by
 249  unfold working_memory_capacity
 250  constructor
 251  · -- φ³ > 4: use φ > 1.61 and 1.61³ > 4
 252    have hphi : phi > 1.61 := Constants.phi_gt_onePointSixOne
 253    have hphi_pos : (0:ℝ) ≤ 1.61 := by norm_num
 254    nlinarith [sq_nonneg phi, sq_nonneg (phi - 1.61), Constants.phi_pos,
 255               show (1.61:ℝ)^3 > 4 by norm_num]
 256  · -- φ³ < 5: use φ < 1.62
 257    have hphi : phi < 1.62 := Constants.phi_lt_onePointSixTwo
 258    have hphi_pos : (0:ℝ) < phi := Constants.phi_pos