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
13 papers (below)

open explainer

Generate a durable explainer page for this declaration.

open lean source

IndisputableMonolith.Foundation.ArrowOfTime on GitHub at line 50.

browse module

All declarations in this module, on Recognition.

explainer page

Tracked in the explainer inventory; generation is lazy so crawlers do not trigger LLM jobs.

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). -/

papers checked against this theorem (showing 13 of 13)