applyT
plain-language theorem explainer
The definition applyT implements time reversal on a ledger entry by replacing its tick field with the output of reverseTick. Researchers deriving discrete CPT invariance in Recognition Science QFT models would cite this operator when composing symmetries. It is realized as a direct record update that copies position, charge, and cost unchanged.
Claim. For a ledger entry $e$ with position $x : Fin 3 → ℝ$, tick $τ$, charge $q ∈ ℤ$, and cost $c ≥ 0$, the time-reversal map $T(e)$ yields the entry with identical $x$, $q$, $c$ but tick replaced by reverseTick($τ$).
background
The module derives CPT invariance from the ledger's double-entry structure in Recognition Science. A LedgerEntry records a recognition event via 3D position, Phase tick (in units of the fundamental time quantum $τ₀ = 1$), integer charge, and non-negative cost. Time reversal corresponds to the eight-tick cycle running backward, consistent with the T-symmetry forced by the octave period. Upstream results supply the tick constant as the RS-native time quantum and cost as the J-cost of a multiplicative recognizer.
proof idea
The definition is a one-line wrapper that applies reverseTick to the tick field of the input LedgerEntry while copying the remaining fields.
why it matters
This operator supplies the T component for the full CPT map and its involution theorems. It fills the T-symmetry slot in the module's derivation of CPT from ledger structure, realizing the eight-tick octave (T7) of the forcing chain. Downstream results include applyCPT, cpt_involutive, cpt_mass_equality, and t_preserves_cost, which establish particle-antiparticle mass equality under the combined symmetry.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.