pith. machine review for the scientific record. sign in
theorem

forward_accumulates

proved
show as:
view math explainer →
module
IndisputableMonolith.Foundation.ArrowOfTime
domain
Foundation
line
50 · github
papers citing
28 papers (below)

open explainer

Read the cached plain-language explainer.

open lean source

IndisputableMonolith.Foundation.ArrowOfTime on GitHub at line 50.

browse module

All declarations in this module, on Recognition.

explainer page

A cached Ask Recognition explainer exists for this declaration.

open explainer

depends on

formal source

  47  intro i _; exact abs_nonneg _
  48
  49/-- Forward direction: adding a step with nonzero Berry phase increases Z. -/
  50theorem forward_accumulates (phases : List ℝ) (new_phase : ℝ) (hn : new_phase ≠ 0) :
  51    let z_before := (phases.map fun p => |p|).foldl (· + ·) 0
  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). -/
  60theorem reverse_subtracts (phase : ℝ) :
  61    let forward_phase := phase
  62    let reverse_phase := -phase
  63    forward_phase + reverse_phase = 0 := by
  64  simp only
  65  ring
  66
  67/-- Z-complexity uses absolute values, so reversal adds to Z, not subtracts. -/
  68theorem z_absolute_immune_to_reversal (phase : ℝ) (hp : phase ≠ 0) :
  69    |phase| = |-phase| := by
  70  rw [abs_neg]
  71
  72/-- The arrow of time: if Z(t₁) < Z(t₂), then t₁ is before t₂. -/
  73def isBefore (z1 z2 : ℝ) : Prop := z1 < z2
  74
  75/-- The before relation is transitive (time is ordered). -/
  76theorem before_transitive (z1 z2 z3 : ℝ) (h12 : isBefore z1 z2) (h23 : isBefore z2 z3) :
  77    isBefore z1 z3 := by
  78  unfold isBefore at *; linarith
  79
  80/-- The before relation is irreflexive (a moment is not before itself). -/