cpt_preserves_cost
plain-language theorem explainer
The CPT transformation leaves the recognition cost of any ledger entry unchanged. Researchers deriving QFT symmetries from Recognition Science's discrete ledger structure would cite this result to establish combined charge-parity-time invariance. The proof is a one-line reflexivity that follows directly from the definition of applyCPT, which modifies only position, tick, and charge while copying the cost field verbatim.
Claim. For every ledger entry $e$, the cost after the combined charge-parity-time reversal transformation equals the original cost: $cost(CPT(e)) = cost(e)$.
background
The module QFT-005 derives CPT invariance from the ledger's double-entry structure. LedgerEntry records a single recognition event with 3D position (Fin 3 → ℝ), phase tick, charge indicator (ℤ), and non-negative cost (ℝ). Cost itself is the J-cost of the underlying state, as defined in ObserverForcing.cost and derived from the comparator in MultiplicativeRecognizerL4.cost. The module states that C arises from J(x) = J(1/x) symmetry, P from D=3 isotropy, and T from the reversible 8-tick cycle.
proof idea
Term-mode proof consisting of a single reflexivity. It holds because applyCPT is defined by composing applyC, applyP, and applyT, each of which constructs a new LedgerEntry that retains the input cost field unchanged.
why it matters
This result supplies the cost-invariance step required for the CPT theorem in the QFT-005 module. It supports the claim that the combined transformation is conserved while individual C, P, or T may break, consistent with the eight-tick octave (T7) and J-uniqueness (T5). The declaration closes one link in the ledger-to-QFT derivation chain and aligns with the Recognition Composition Law's multiplicative structure.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.