pith. sign in
theorem

forward_accumulates

proved
show as:
module
IndisputableMonolith.Foundation.ArrowOfTime
domain
Foundation
line
50 · github
papers citing
71 papers (below)

plain-language theorem explainer

Forward steps with nonzero Berry phase strictly increase total Z, the summed absolute phases, for any preceding list. Researchers deriving an intrinsic arrow of time in Recognition Science cite this to obtain monotonic complexity without thermodynamics. The proof expands the post-append sum via list identities then closes the strict inequality by linear arithmetic on the positive absolute value.

Claim. Let $Z(φ_1,…,φ_n)=∑|φ_i|$. For any finite list of real phases $(φ_i)$ and any new phase $φ≠0$, $Z(φ_1,…,φ_n)<Z(φ_1,…,φ_n,φ)$.

background

Berry phases are drawn from the eight-tick cycle, each step contributing a multiple of π/4. Z-complexity is the sum of absolute values of these phases and serves as a sign-insensitive ledger of accumulated structure. The module shows that R-hat evolution on the lattice can run forward or backward, yet only the forward orientation adds positive phase while reversal negates it; absolute values therefore produce monotonic growth in one direction only.

proof idea

The tactic proof first simplifies the let-bindings for the before and after sums. It rewrites the appended list using map_append and foldl_append, then reduces the resulting cons and nil cases. linarith finishes the argument by invoking positivity of the absolute value of the nonzero new phase.

why it matters

This supplies the forward half of the Berry-phase monotonicity that defines the arrow of time in the module. It rests on the eight-tick phase definition and feeds the later constructions of temporal order (arrow_from_z) and coarse-grained entropy (entropy_from_berry) listed in the module documentation. The result closes the topological asymmetry step that lets directed time emerge from the Recognition framework without imported thermodynamics.

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

papers checked against this theorem (showing 30 of 71)

The full set is indexed internally; the public theorem page shows a capped sample so high-use declarations do not become many-thousand-row pages.