pt_involutive
plain-language theorem explainer
The PT operator on ledger entries is involutive, so two successive applications restore the original entry. Researchers deriving discrete symmetries in Recognition Science QFT models cite it to confirm parity-time reversal from the ledger structure. The proof reduces via definition unfolding, case split on the entry constructor, and direct invocation of negation and reverse-tick involution lemmas.
Claim. For any ledger entry $e$ with position vector, phase, charge, and cost, the combined parity-time operator satisfies $PT(PT(e)) = e$.
background
LedgerEntry records a recognition event via a 3D position (Fin 3 → ℝ), Phase tick, integer charge, and non-negative real cost. The module extracts CPT invariance from the ledger's double-entry bookkeeping, with C from J-cost reciprocity, P from 3D lattice isotropy, and T from the reversible eight-tick cycle. Upstream constants supply the fundamental tick τ₀ = 1 and the J-cost definition for recognition events.
proof idea
Definition unfolding of applyPT, applyP, and applyT is followed by case analysis on the LedgerEntry mk constructor. Congruence matches the four fields; functional extensionality plus double negation handles the position vector; the reverseTick_involutive lemma dispatches the tick component.
why it matters
The result supplies the involution property required for PT symmetry in the ledger model, a direct step toward the CPT theorem that the combined operator is conserved. It anchors the T-symmetry claim arising from the eight-tick octave and supports the subsequent mass-equality statement that CPT plus PT invariance yields C invariance.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.