def
definition
def or abbrev
theta_experimental_bound
show as:
view Lean formalization →
formal statement (Lean)
55noncomputable def theta_experimental_bound : ℝ := 1e-10
proof body
Definition body.
56
57/-- The neutron EDM scales with θ:
58 d_n ≈ θ × (10⁻¹⁶ e·cm)
59
60 Experimental limit: d_n < 3 × 10⁻²⁶ e·cm
61 Therefore: |θ| < 3 × 10⁻¹⁰ -/