z_absolute_immune_to_reversal
plain-language theorem explainer
The theorem establishes that the absolute value of a nonzero real phase equals the absolute value of its negation. Researchers modeling the arrow of time via Berry phase accumulation in Recognition Science would cite this to confirm that Z-complexity cannot decrease under R-hat reversal. The proof is a one-line rewrite applying the evenness property of the absolute value function.
Claim. Let $phi$ be a nonzero real Berry phase. Then $|phi| = |-phi|$.
background
The module derives the arrow of time from Berry phase monotonicity on the ledger. Z-complexity is defined to take absolute values of accumulated phase, so that forward R-hat steps increase Z while reverse steps traverse the same loop with opposite orientation. Upstream results include the 8-tick phase definition (periodic with period 2 pi) and ledger factorization structures that calibrate J-cost on the discrete lattice.
proof idea
The proof is a one-line tactic wrapper that applies the absolute-value negation identity.
why it matters
This fills the local step showing reversal cannot subtract from Z, supporting the module claim that temporal order arises from Z-complexity ordering without imported thermodynamics. It aligns with the eight-tick octave periodicity and the topological asymmetry of Berry phase accumulation in the Recognition framework.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.