module module moderate

`IndisputableMonolith.QFT.CPTInvariance`

The CPTInvariance module defines parity, time-reversal, and charge-conjugation operators together with their CPT composition inside the Recognition Science framework. Researchers extending the eight-tick discretization to QFT symmetries would cite these definitions when assembling Tier 2 derivations. The module consists of type declarations for the operators and cost-preservation statements built on the imported constants and hypothesis.

claimParity operator implements spatial reflection $x o -x$; time-reversal and charge-conjugation operators are defined analogously; their composition satisfies CPT invariance on the 8-tick cycle with recognition cost preserved.

background

The module sits inside the QFT derivations tier of Recognition Science and imports the fundamental time quantum $ au_0 = 1$ tick together with the eight-tick discretization hypothesis. The upstream EightTick doc states: "The 8-tick hypothesis: time/process is discretized into 8-beat cycles. This is an EXPLICIT HYPOTHESIS about observed traces, not a definitional axiom." Supporting structures LedgerEntry and Ledger track recognition costs while the operators applyC, applyP, applyT, and applyCPT act on them.

proof idea

this is a definition module, no proofs

why it matters in Recognition Science

The module supplies the CPT operators to the parent QFT module, which assembles Tier 2 derivations of quantum field theory fundamentals from the Recognition Science framework. It supplies the discrete symmetry layer required before further QFT constructions that rest on the eight-tick octave.

scope and limits

Does not derive CPT from the T0-T8 forcing chain.
Does not link operators to the phi-ladder or mass formula.
Does not treat continuous-time limits or the alpha band.
Does not contain numerical checks against measured constants.

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