pith. machine review for the scientific record. sign in
theorem proved tactic proof

working_memory_approx

show as:
view Lean formalization →

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

generate prose now

formal statement (Lean)

 247theorem working_memory_approx :
 248    4 < working_memory_capacity ∧ working_memory_capacity < 5 := by

proof body

Tactic-mode proof.

 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
 262/-! ## Status -/
 263

used by (1)

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

depends on (6)

Lean names referenced from this declaration's body.