TemporalSequence

formal source

  30noncomputable section
  31
  32/-- A sequence of R-hat steps with accumulated Berry phase at each step. -/
  33structure TemporalSequence where
  34  n_steps : ℕ
  35  berry_at_step : Fin n_steps → ℝ
  36
  37/-- Z-complexity at step k: sum of absolute Berry phases up to k. -/
  38def zAtStep (seq : TemporalSequence) (k : Fin seq.n_steps) : ℝ :=
  39  (Finset.univ.filter (fun i : Fin seq.n_steps => i.val ≤ k.val)).sum
  40    (fun i => |seq.berry_at_step i|)
  41
  42/-- Z is non-negative at every step. -/
  43theorem z_nonneg (seq : TemporalSequence) (k : Fin seq.n_steps) :
  44    0 ≤ zAtStep seq k := by
  45  unfold zAtStep
  46  apply Finset.sum_nonneg
  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