applyP
plain-language theorem explainer
Parity operator on a ledger entry negates its three-dimensional position coordinate while leaving tick, charge, and cost unchanged. Researchers deriving CPT invariance from discrete recognition structures cite this definition when composing the full transformation. The implementation is a direct record update that applies spatial reflection to the position field.
Claim. Let $e$ be a ledger entry with position vector $r : Fin 3 → ℝ$. The parity-transformed entry $P(e)$ satisfies $P(e).r(i) = -e.r(i)$ for each coordinate $i$, while tick, charge, and cost fields remain identical to those of $e$.
background
A LedgerEntry records a single recognition event in the QFT ledger with fields for 3D position (Fin 3 → ℝ), phase tick, integer charge, and non-negative J-cost. The module derives CPT invariance from the ledger's double-entry structure: C from J(x) = J(1/x) symmetry, P from isotropy in D=3, and T from reversibility of the 8-tick cycle. Upstream cost definitions establish that recognition cost equals the J-cost of the event state, with non-negativity guaranteed by the recognizer comparator.
proof idea
This is a one-line definition that performs a record update on the LedgerEntry structure, replacing the position function with its pointwise negation.
why it matters
The definition supplies the parity component used by applyCPT, applyPT, cpt_involutive, cpt_mass_equality, and p_preserves_cost. It realizes the P-symmetry forced by D=3 in the unified forcing chain, enabling the CPT theorem that remains conserved even when individual C, P, or T symmetries are violated. It closes scaffolding for deriving equal masses and lifetimes between particles and antiparticles from ledger symmetry.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.