t_preserves_cost
plain-language theorem explainer
Time reversal on a ledger entry leaves its recognition cost unchanged. Researchers building discrete QFT models from Recognition Science ledger symmetries cite this when assembling the CPT theorem. The equality holds by reflexivity because applyT updates only the tick field while copying the cost field verbatim.
Claim. Let $e$ be a ledger entry recording a recognition event. Then the cost of the time-reversed entry equals the cost of $e$: $c(T e) = c(e)$, where $T$ denotes time reversal on the tick component.
background
In this QFT module a LedgerEntry is a structure with fields for 3D position, tick (a Phase), charge indicator, and a non-negative cost. The module derives CPT invariance from the ledger's double-entry structure, where T-symmetry follows because the eight-tick cycle can run forward or backward. Upstream, cost is defined as the J-cost of the recognition state in ObserverForcing and as derivedCost of the comparator in MultiplicativeRecognizerL4.
proof idea
The proof is a one-line term using reflexivity (rfl). It follows directly from the definition of applyT, which constructs the new entry by replacing only the tick with its reverse while retaining the original cost field.
why it matters
This result supplies the T-component of CPT invariance in the Recognition Science ledger model. It fills the module's target of deriving CPT from discrete symmetries, as stated in the paper proposition for PRL on CPT from discrete ledger structure. It aligns with the eight-tick octave (T7) that permits time reversal while preserving cost, supporting the full CPT combination in the framework.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.