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

eta_bar_interval

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)

 245theorem eta_bar_interval : (0.28 : ℝ) < wolfenstein_eta ∧ wolfenstein_eta < 0.40 := by

proof body

Term-mode proof.

 246  unfold wolfenstein_eta; constructor <;> norm_num
 247
 248/-- ρ̄ is in the RS-predicted interval (0.10, 0.20).
 249    From unitarity triangle with δ = π/2: the real part ρ̄ ≈ 0.13. -/

depends on (6)

Lean names referenced from this declaration's body.