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

EQ_next_stable_band

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)

 145theorem EQ_next_stable_band :
 146    (18.5 : ℝ) < EQ_next_stable ∧ EQ_next_stable < 20.5 := by

proof body

Term-mode proof.

 147  rw [EQ_next_stable_eq]
 148  unfold EQ_human
 149  have hsq := phi_squared_bounds
 150  refine ⟨?_, ?_⟩
 151  · nlinarith [hsq.1]
 152  · nlinarith [hsq.2]
 153
 154/-! ## §5. Master certificate -/
 155

used by (3)

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

depends on (5)

Lean names referenced from this declaration's body.