forward_accumulates
Adding a nonzero real phase to a finite list strictly increases the total absolute phase sum Z. Workers on the Recognition Science arrow of time cite this to derive an intrinsic before-after ordering from Berry phase accumulation alone. The proof reduces the two foldl sums via list append identities and invokes positivity of the absolute value on the added phase.
claimLet $P = (p_1, p_2, ..., p_n)$ be a finite list of real phases and let $q$ be a nonzero real number. Then the sum of absolute values over $P$ is strictly less than the corresponding sum over the extended list $P$ appended with $q$.
background
Z-complexity is the sum of absolute Berry phases accumulated along a sequence of R-hat steps. The module shows that this sum is monotonically non-decreasing in the forward direction, supplying an intrinsic temporal order without external thermodynamics. The eight-tick phase definition supplies the discrete angles $kπ/4$ that enter the Berry phases, while the wedge phase construction produces the unimodular complex numbers whose arguments are these phases.
proof idea
Tactic proof. The first two simp and rw steps expand the foldl sums over the appended list, reducing the inequality to the single term |new_phase|. The final linarith step applies abs_pos.mpr to the hypothesis new_phase ≠ 0.
why it matters in Recognition Science
This theorem supplies the forward half of the Z-monotonicity argument that defines the arrow of time. It feeds the later construction of temporal order via Z-complexity ordering and the emergence of entropy as coarse-grained Z. Within the Recognition framework it closes the step from eight-tick phase periodicity to directed time, consistent with the T7 octave and the absolute-value treatment of Berry phase.
scope and limits
- Does not prove that Z remains bounded or converges.
- Does not extend the inequality to continuous-time limits.
- Does not address phase accumulation under non-unitary maps.
- Does not derive thermodynamic entropy directly.
formal statement (Lean)
50theorem forward_accumulates (phases : List ℝ) (new_phase : ℝ) (hn : new_phase ≠ 0) :
51 let z_before := (phases.map fun p => |p|).foldl (· + ·) 0
proof body
Tactic-mode proof.
52 let z_after := ((phases ++ [new_phase]).map fun p => |p|).foldl (· + ·) 0
53 z_before < z_after := by
54 simp only
55 rw [List.map_append, List.foldl_append]
56 simp only [List.map_cons, List.map_nil, List.foldl_cons, List.foldl_nil]
57 linarith [abs_pos.mpr hn]
58
59/-- Reversing a loop subtracts phase (opposite sign). -/