def definition def or abbrev

`jarlskog`

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

formal statement (Lean)

  40noncomputable def jarlskog : ℝ := jarlskog_pred

Definition body.

  41
  42/-- Phenomenological facts required by the CKM demo.
  43    Documented in `docs/Assumptions.md`. -/

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

CKMPhenomenology in IndisputableMonolith.Physics.CKM decl_use
jarlskog_summary in IndisputableMonolith.Physics.CKM decl_use
jarlskog_summary_of_facts in IndisputableMonolith.Physics.CKM decl_use
PMNSScoreCardCert in IndisputableMonolith.Physics.PMNSScoreCard decl_use
pmnsScoreCardCert_holds in IndisputableMonolith.Physics.PMNSScoreCard decl_use

Lean names referenced from this declaration's body.