module module

`IndisputableMonolith.QFT.CPTInvariance`

show as: view Lean formalization →

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

generate prose now

used by (1)

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

IndisputableMonolith.QFT module_import

depends on (2)

Lean names referenced from this declaration's body.

IndisputableMonolith.Constants module_import
IndisputableMonolith.RRF.Hypotheses.EightTick module_import

declarations in this module (26)

structure ParityOp L48
structure TimeReversalOp L53
structure LedgerEntry L60
structure Ledger L73
def applyC L82
theorem c_preserves_cost L87
def applyP L93
theorem p_preserves_cost L97
def reverseTick L103
def applyT L106
theorem t_preserves_cost L110
def applyCPT L116
theorem cpt_preserves_cost L120
theorem cpt_preserves_balance L124
theorem reverseTick_involutive L143
theorem cpt_involutive L156
def knownViolations L174
def applyPT L184
theorem pt_involutive L188
theorem cpt_mass_equality L198
theorem cpt_lifetime_equality L224
structure CPTFalsifier L249
def cptBounds L260
def cpt_mass_bound L266
theorem cpt_bound_tight L269
theorem no_observed_cpt_violation L273