pith. sign in
def

zAtStep

definition
show as:
module
IndisputableMonolith.Foundation.ArrowOfTime
domain
Foundation
line
38 · github
papers citing
4 papers (below)

plain-language theorem explainer

Z-complexity at step k sums the absolute Berry phases accumulated in a TemporalSequence up to that index. Researchers establishing the arrow of time via Berry phase monotonicity in Recognition Science cite this definition when proving non-decreasing complexity measures. The definition is a direct Finset sum that filters steps by index and applies absolute value to each berry phase entry.

Claim. Let $seq$ be a temporal sequence with $n$ steps and real Berry phase $b_i$ at each step $i$. Define the Z-complexity at step $k$ by $z(k) := sum_{i=0 to k} |b_i|$.

background

The ArrowOfTime module derives an intrinsic time direction from Berry phase accumulation under R-hat steps on a preserved ledger. A TemporalSequence is the structure holding the total number of steps together with a function that assigns a real-valued Berry phase to each Fin-indexed step. Z-complexity is then obtained by taking absolute values of those phases and forming the partial sum up to the current step.

proof idea

Direct definition. It constructs a Finset by filtering the universal set of steps to those whose index is at most k, then sums the absolute values of the corresponding berry_at_step entries.

why it matters

This definition supplies the Z-complexity measure that feeds the non-negativity theorem z_nonneg and the monotonicity results that follow. It realizes the key step in the Q3 arrow-of-time construction, where forward R-hat steps increase Z while reversals cannot decrease it because absolute values are taken. The construction sits inside the Recognition Science framework as the complexity accumulator that distinguishes before from after without importing thermodynamic assumptions.

Switch to Lean above to see the machine-checked source, dependencies, and usage graph.

papers checked against this theorem (showing 4 of 4)