def definition def or abbrev

`J_CP_obs`

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

formal statement (Lean)

 232noncomputable def J_CP_obs : ℝ := 3.08e-5

Definition body.

 233
 234/-- From J_CP > 0 (proved in Jarlskog invariant module), η̄ > 0.
 235    Proof: J_CP = A²λ⁶η̄ > 0 with A, λ > 0 forces η̄ > 0. -/

Lean names referenced from this declaration's body.