reverse_subtracts
plain-language theorem explainer
Reversing the phase of a loop negates its Berry phase contribution. Researchers deriving the arrow of time from Z-complexity monotonicity cite this to separate forward accumulation from reversal. The proof reduces to a direct algebraic identity via ring simplification after defining the negated phase.
Claim. For any real number $phi$ representing Berry phase of a loop, the forward phase $phi$ and reverse phase $-phi$ satisfy $phi + (-phi) = 0$.
background
The Arrow of Time module shows temporal direction emerging from Berry phase accumulation on the lattice: R-hat steps are unitary forward or backward, yet Z-complexity (absolute Berry phase) increases only forward. The 8-tick phase from EightTick.phase is $k pi / 4$ for $k$ in Fin 8. Anchor.Z maps sectors and rational charges to integers via quadratic and quartic terms on scaled numerators. Wedge.phase supplies the unimodular complex exponential $e^{i w}$.
proof idea
The proof introduces forward_phase as the input phase and reverse_phase as its negation, then applies simp followed by ring to obtain the zero sum. It is a one-line algebraic wrapper.
why it matters
This result supplies the sign-reversal step required for the arrow of time construction in the module. It supports forward_accumulates and the subsequent z_monotone_absolute claim that absolute phase never decreases under reversal. The theorem closes the topological asymmetry between forward and reverse R-hat traversals within the eight-tick octave and Berry phase framework.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.