theorem proved term proof

`cp_violation_small`

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

formal statement (Lean)

 176theorem cp_violation_small :
 177    jarlskogInvariant > 0 ∧ jarlskogInvariant < 1e-4 := by

proof body

Term-mode proof.

 178  unfold jarlskogInvariant
 179  constructor <;> norm_num
 180
 181/-! ## Unitarity Triangle -/
 182
 183/-- The unitarity of the CKM matrix gives constraints:
 184
 185    V_ud V_ub* + V_cd V_cb* + V_td V_tb* = 0
 186
 187    This forms a triangle in the complex plane.
 188    The angles α, β, γ are related to CP violation.
 189
 190    RS predicts these angles are φ-related. -/

depends on (18)

Lean names referenced from this declaration's body.

of in IndisputableMonolith.Astrophysics.NucleosynthesisTiers decl_use
predicts in IndisputableMonolith.Decision.AbileneParadox decl_use
of in IndisputableMonolith.Foundation.DAlembert.LedgerFactorization decl_use
of in IndisputableMonolith.Foundation.PhiForcingDerived decl_use
of in IndisputableMonolith.Foundation.SpectralEmergence decl_use
Triangle in IndisputableMonolith.Gravity.ReggeCalculus decl_use
of in IndisputableMonolith.Information.PhysicsComplexityStructure decl_use
V_cb in IndisputableMonolith.Physics.CKM decl_use
V_cd in IndisputableMonolith.Physics.CKM decl_use
V_ub in IndisputableMonolith.Physics.CKM decl_use
V_ud in IndisputableMonolith.Physics.CKM decl_use
jarlskogInvariant in IndisputableMonolith.StandardModel.CKMMatrix decl_use
V_cb in IndisputableMonolith.StandardModel.CKMMatrix decl_use
V_cd in IndisputableMonolith.StandardModel.CKMMatrix decl_use
V_tb in IndisputableMonolith.StandardModel.CKMMatrix decl_use
V_td in IndisputableMonolith.StandardModel.CKMMatrix decl_use
V_ub in IndisputableMonolith.StandardModel.CKMMatrix decl_use
V_ud in IndisputableMonolith.StandardModel.CKMMatrix decl_use