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

step_mu_tau_bounds

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)

 109lemma step_mu_tau_bounds : (5.86 : ℝ) < step_mu_tau ∧ step_mu_tau < (5.87 : ℝ) := by

proof body

Term-mode proof.

 110  simp only [step_mu_tau]
 111  rw [cube_faces_exact, W_exact]
 112  have h_alpha := alpha_bounds
 113  -- (2*17+3)/2 = 37/2 = 18.5
 114  -- 18.5 * 0.00729735 ≈ 0.135
 115  -- 6 - 0.135 ≈ 5.865
 116  constructor <;> nlinarith
 117
 118/-! ## Part 2: Bounds on Predicted Residues -/
 119
 120/-- Bounds on predicted_residue_mu = (gap 1332 - refined_shift) + step_e_mu.
 121    ≈ -20.706 + 11.0795 ≈ -9.6265 -/

used by (3)

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

depends on (18)

Lean names referenced from this declaration's body.