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

TemporalSequence

definition
show as:
view math explainer →
module
IndisputableMonolith.Foundation.ArrowOfTime
domain
Foundation
line
33 · github
papers citing
3 papers (below)

open explainer

Generate a durable explainer page for this declaration.

open lean source

IndisputableMonolith.Foundation.ArrowOfTime on GitHub at line 33.

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

used by

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

papers checked against this theorem (showing 3 of 3)