structure definition def or abbrev

`CPTFalsifier`

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

formal statement (Lean)

 249structure CPTFalsifier where
 250  /-- The particle type. -/
 251  particle : String
 252  /-- Mass difference (should be 0). -/
 253  massDiff : ℝ
 254  /-- Lifetime difference (should be 0). -/
 255  lifetimeDiff : ℝ
 256  /-- Evidence of violation. -/
 257  violation : massDiff ≠ 0 ∨ lifetimeDiff ≠ 0
 258
 259/-- Current experimental bounds (from PDG). -/

depends on (7)

Lean names referenced from this declaration's body.

of in IndisputableMonolith.Astrophysics.NucleosynthesisTiers decl_use
Mass in IndisputableMonolith.Constants.RSNativeUnits decl_use
of in IndisputableMonolith.Foundation.DAlembert.LedgerFactorization decl_use
of in IndisputableMonolith.Foundation.PhiForcingDerived decl_use
from in IndisputableMonolith.Foundation.PrimitiveDistinction decl_use
of in IndisputableMonolith.Foundation.SpectralEmergence decl_use
of in IndisputableMonolith.Information.PhysicsComplexityStructure decl_use