def
definition
cptBounds
show as:
view math explainer →
open explainer
Read the cached plain-language explainer.
open lean source
IndisputableMonolith.QFT.CPTInvariance on GitHub at line 260.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
formal source
257 violation : massDiff ≠ 0 ∨ lifetimeDiff ≠ 0
258
259/-- Current experimental bounds (from PDG). -/
260def cptBounds : String :=
261 "Proton/antiproton mass: |Δm/m| < 10⁻⁹\n" ++
262 "Electron/positron mass: |Δm/m| < 8×10⁻⁹\n" ++
263 "K⁰/K̄⁰ mass: |Δm| < 10⁻¹⁸ GeV"
264
265/-- CPT violation bound (proton/antiproton relative mass difference). -/
266def cpt_mass_bound : ℚ := 1 / 10^9 -- < 10⁻⁹
267
268/-- **THEOREM**: The experimental CPT bound is extremely tight. -/
269theorem cpt_bound_tight : cpt_mass_bound < 1 / 10^8 := by norm_num [cpt_mass_bound]
270
271/-- **THEOREM**: No CPT violation has ever been observed at current precision.
272 This is encoded as the bound being less than any reasonable detection threshold. -/
273theorem no_observed_cpt_violation : cpt_mass_bound < 1 / 1000000 := by
274 norm_num [cpt_mass_bound]
275
276end CPTInvariance
277end QFT
278end IndisputableMonolith