TimeReversalOp
The TimeReversalOp structure introduces the time reversal operator in the Recognition Science QFT ledger model as a placeholder asserting negation on real time. Researchers deriving CPT invariance from discrete symmetries would cite it when assembling the T component of the ledger double-entry rules. The declaration is a bare structure definition with a single trivial field and no further reduction.
claimThe time reversal operator is the structure whose single field requires that negation holds for every real number $t$, serving as the T-symmetry component in the ledger whose entries are balanced collections of recognition events.
background
The module QFT-005 derives CPT invariance from the ledger's double-entry structure. C-symmetry follows from J(x) = J(1/x) cost duality, P-symmetry from the isotropic 3D voxel lattice, and T-symmetry from the eight-tick cycle running forward or backward. The Ledger structure requires that the sum of charges over its list of entries equals zero.
proof idea
This is a structure definition with an empty proof body. It simply declares the TimeReversalOp carrier together with the placeholder field negate that holds trivially for all real t.
why it matters in Recognition Science
The definition supplies the T component needed for the CPT theorem targeted in the module's PRL outline. It sits downstream of the eight-tick octave (T7) and the actualization operator A that selects minimal-J configurations. Sibling declarations such as applyT and applyCPT are expected to use it to establish cost preservation under reversal.
scope and limits
- Does not supply a concrete map implementing time negation.
- Does not prove that the operator preserves the J-cost function.
- Does not link the reversal to the phi-ladder or mass formulas.
- Does not address individual C or P violations.
formal statement (Lean)
53structure TimeReversalOp where
54 /-- Reversal negates time. -/
55 negate : ∀ t : ℝ, True -- Placeholder
56
57/-! ## Ledger Structure and Symmetries -/
58
59/-- A ledger entry representing a recognition event. -/