module module high

`IndisputableMonolith.QFT.CPTInvariance`

The CPTInvariance module defines charge conjugation, parity, and time reversal operators on ledger entries using the eight-tick discretization and RS time quantum. It proves each operator preserves J-cost and that their composition leaves the ledger invariant. QFT derivations in Recognition Science cite this module when verifying discrete symmetries from the forcing chain. The structure consists of operator definitions followed by preservation lemmas and a combined CPT application.

claimParity operator $P$ implements spatial reflection on states. Time reversal $T$ inverts tick direction within the 8-beat cycle. Charge conjugation $C$ flips defect sign. The composition satisfies $J(CPT(x)) = J(x)$ for ledger entry $x$, with each operator preserving cost.

background

This module belongs to the QFT tier of Recognition Science derivations. It imports the fundamental RS time quantum τ₀ = 1 tick from Constants and the 8-tick discretization hypothesis from EightTick, which states that time and process are discretized into 8-beat cycles as an explicit hypothesis about observed traces rather than a definitional axiom.

proof idea

This is a definition module. It introduces ParityOp as spatial reflection, TimeReversalOp, LedgerEntry, and the application functions applyC, applyP, applyT. Separate lemmas establish cost preservation for each operator before applyCPT combines them into the invariance statement.

why it matters in Recognition Science

The module supplies the discrete symmetry operators required by the parent QFT module for deriving quantum field theory fundamentals from Recognition Science. It completes the Tier 2 derivation slot for CPT invariance, linking the eight-tick hypothesis directly to ledger invariance under the composition of C, P, and T.

scope and limits

Does not derive CPT from the forcing chain without the eight-tick hypothesis.
Does not treat continuous gauge or Lorentz symmetries.
Does not produce numerical mass or coupling predictions.
Does not interface with experimental CP-violation data.

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