c_preserves_cost
plain-language theorem explainer
Charge conjugation on a ledger entry leaves its cost unchanged. This encodes the J-cost symmetry J(x) = J(1/x) at the discrete recognition level. Researchers deriving CPT invariance from ledger structures would cite the result. The equality holds by direct reflexivity on the definitions of applyC and the cost function.
Claim. For any ledger entry $e$, the cost after charge conjugation satisfies $cost(C(e)) = cost(e)$.
background
The module derives CPT invariance from the ledger's double-entry structure in Recognition Science. Charge conjugation C swaps particle and antiparticle entries while preserving the underlying recognition cost. LedgerEntry is the structure holding a 3D position, tick phase, integer charge, and nonnegative real cost. The cost function itself is the J-cost induced by a multiplicative recognizer on positive ratios, as defined in the upstream MultiplicativeRecognizerL4 and ObserverForcing modules.
proof idea
The proof is a one-line reflexivity that applies the definition of applyC to the cost field of the LedgerEntry structure.
why it matters
This supplies the C-symmetry leg of the CPT invariance theorem targeted by the module. It realizes the J(x) = J(1/x) symmetry at the ledger level, consistent with the Recognition Composition Law and the eight-tick octave structure. The result feeds the broader derivation of CPT from discrete ledger symmetries outlined in the module documentation.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.