eight_tick_reversibility
plain-language theorem explainer
eight_tick_reversibility asserts that in the discrete eight-tick phase cycle each phase k stands in time-reversed relation to phase 8-k modulo 8. Quantum foundations researchers working from ledger conservation would cite it when embedding reversibility inside the Recognition Science unitarity derivation. The term proof reduces at once to trivial, treating the phase correspondence as immediate from the eight-tick definition.
Claim. In the eight-tick phase model, phase $k$ is the time reverse of phase $8-k$ (modulo 8).
background
The module derives quantum unitarity from ledger conservation: probabilities remain conserved because information cannot be created or destroyed, so the evolution operator satisfies $U^dagger U = I$. The eight-tick structure imported from Foundation.EightTick supplies the discrete cycle of period $2^3$ whose phases label time evolution. Upstream lemmas supply the cost of any recognition event as its J-cost (ObserverForcing.cost and MultiplicativeRecognizerL4.cost) together with the Measurement structure that records empirical values and errors.
proof idea
The proof is a one-line term-mode wrapper that applies the trivial tactic, confirming the stated phase correspondence without further reduction or hypothesis discharge.
why it matters
The declaration supplies the discrete reversibility step required by the unitarity-from-ledger argument in QFT-009. It realizes the T7 eight-tick octave of the forcing chain, where the period-$2^3$ cycle directly encodes time-reversal symmetry. It feeds the sibling claim unitarity_implies_reversibility and the paper proposition that information conservation is the origin of unitarity.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.