z_nonneg
plain-language theorem explainer
Z-complexity is the cumulative sum of absolute Berry phases along any finite sequence of R-hat steps. It remains non-negative at every step index. Researchers deriving an intrinsic arrow of time from discrete Berry phase accumulation cite this baseline before monotonicity arguments. The proof is a one-line term wrapper that unfolds the sum and applies non-negativity of the absolute value to each term.
Claim. Let $seq$ be a temporal sequence with $n$ steps and real Berry phases $b_i$ at each index $i$. For any step index $k < n$, the Z-complexity $Z(seq,k) := sum_{i=0}^k |b_i|$ satisfies $Z(seq,k) >= 0$.
background
The module derives the arrow of time from Berry phase monotonicity on a discrete R-hat lattice that preserves the ledger unitarily. A TemporalSequence is a structure holding the total number of steps together with a map from each step index to its real Berry phase value. Z-complexity at step k is defined as the partial sum of absolute Berry phases from the start up to k. This non-negativity result is the first concrete property extracted from that definition and precedes the module's monotonicity lemmas. Upstream results include the cellular automata step operation and the eight-tick phase map used to generate the Berry phases.
proof idea
The proof is a term-mode wrapper. It unfolds zAtStep to expose a Finset sum of absolute values, applies the library lemma Finset.sum_nonneg, and supplies the fact that the absolute value of any real number is non-negative.
why it matters
This result supplies the non-negativity of Z-complexity that underpins the module's later claims on forward accumulation and absolute monotonicity, which in turn define temporal order without importing thermodynamics. It occupies the initial position among the module's key results for extracting an arrow of time from Berry phase. In the Recognition framework it anchors the directed-time construction that follows from the eight-tick octave and the underlying forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.