applyC
plain-language theorem explainer
Charge conjugation maps each ledger entry to its antiparticle counterpart by negating the integer charge field while leaving position, tick, and cost unchanged. Researchers deriving CPT invariance from discrete ledger symmetries cite this operator when establishing the C component of the full transformation. The definition is realized as a direct record update that encodes the J(x) = J(1/x) duality at the ledger level.
Claim. Let $e$ be a ledger entry with charge $q$. The charge-conjugated entry $C(e)$ is defined by $C(e).charge = -q$ while $C(e)$ agrees with $e$ on position, tick, and cost.
background
A LedgerEntry records a single recognition event with a position in three-dimensional space (Fin 3 → ℝ), a phase tick, an integer charge, and a non-negative cost. The cost is the J-cost of the recognition state, obtained from the multiplicative recognizer comparator via the derivedCost function and obeying the Recognition Composition Law. The module QFT.CPTInvariance derives CPT invariance from the ledger's double-entry structure, where C-symmetry follows because the cost function satisfies J(x) = J(1/x). Upstream results establish that cost is non-negative for every recognition event and that the underlying recognizer acts on positive ratios.
proof idea
The definition is a one-line record update that replaces the charge field of the input LedgerEntry with its negation, leaving the remaining fields untouched.
why it matters
This definition supplies the C operator used to construct the full CPT transformation in applyCPT and to prove cost preservation in c_preserves_cost. It fills the C-symmetry step in the CPT theorem derived from ledger structure, linking directly to the J-uniqueness property (T5) and the eight-tick octave. It supports the claim that particles and antiparticles have equal mass under CPT invariance.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.