`Jcost_pos_of_ne_one`

proved

show as: view math explainer →

module: IndisputableMonolith.Information.LocalCache
domain: Information
line: 231 · github
papers citing: none yet

open explainer

Generate a durable explainer page for this declaration.

open lean source

IndisputableMonolith.Information.LocalCache on GitHub at line 231.

browse module

All declarations in this module, on Recognition.

explainer page

Tracked in the explainer inventory; generation is lazy so crawlers do not trigger LLM jobs.

open explainer

depends on

used by

formal source

 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
 259    nlinarith [sq_nonneg (1.62 - phi), sq_nonneg phi,
 260               show (1.62:ℝ)^3 < 5 by norm_num]
 261

papers checked against this theorem

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