GraphCopySchedule.lean`

18 declarations, 0 contain sorry, 0 declared as axioms

The graph on the literal copied and retained slot labels

The ambient label type includes both alternatives at a transfer. The actual partition restricts the copied alternative to H and the retained alternative to Y. Thus copying and retaining never identify two surviving slots.

def OAI.Ostmann.CopyScheduleVertex line 16

Source documentation

A copied label remembers its sign; a retained label remembers its old slot.

def CopyScheduleVertex (I : Type u) : ℕ → Type u
  | 0 => I
  | n + 1 => (Bool × CopyScheduleVertex I n) ⊕ CopyScheduleVertex I n

def OAI.Ostmann.copyScheduleOutside line 20
def OAI.Ostmann.copySchedulePositive line 24
def OAI.Ostmann.copySchedulePath line 28

def OAI.Ostmann.copyScheduleAnchor line 35

Source documentation

A fresh anchor is retained until its reserved step, copied exactly once, and then retained at every later step.

noncomputable def copyScheduleAnchor {I : Type*} :
    (n : ℕ) → ℕ → Bool → I → CopyScheduleVertex I n
  | 0, _, _, i => i
  | n + 1, j, b, i =>
      if j = n then Sum.inl (b, copyScheduleOutside n i)
      else Sum.inr (copyScheduleAnchor n j b i)

Mentions: OAI.Ostmann.CopyScheduleVertex, OAI.Ostmann.copyScheduleOutside

theorem OAI.Ostmann.copyScheduleAnchor_new line 42
theorem OAI.Ostmann.copyScheduleAnchor_old line 49
def OAI.Ostmann.copySchedulePredecessor line 58
Source documentation
Collapse only the erased pivot. Both surviving alternatives have their original predecessor, as in the manuscript's H/Y partition.
```
def copySchedulePredecessor {I : Type*} {n : ℕ} (p : CopyScheduleVertex I n) :
    Option (CopyScheduleVertex I n ⊕ CopyScheduleVertex I n) → CopyScheduleVertex I n
  | none => p
  | some (.inl i) => i
  | some (.inr i) => i
```
Mentions: OAI.Ostmann.CopyScheduleVertex
def OAI.Ostmann.copyScheduleGraph line 64
theorem OAI.Ostmann.copySchedulePath_snoc line 72
theorem OAI.Ostmann.copyScheduleGraph_outside_copy line 79
theorem OAI.Ostmann.copyScheduleGraph_copy_outside line 85
theorem OAI.Ostmann.copyScheduleGraph_copy_copy line 91
theorem OAI.Ostmann.copyScheduleGraph_diagonal line 99
theorem OAI.Ostmann.copyScheduleGraph_fresh_to_path line 110
Source documentation
Incoming edges from an unused reserved anchor simply accumulate the signs of the copied word. The pivot sequence does not enter this identity.
```
theorem copyScheduleGraph_fresh_to_path {I : Type*}
    (g : I → I → ℤ) (pivot : ℕ → I) (n : ℕ) (a i : I) (t : Fin n → Bool) :
    copyScheduleGraph g pivot n (copyScheduleOutside n a) (copySchedulePath n t i) =
      finalCopyParity t * g a i := by
…
```
Mentions: OAI.Ostmann.copyScheduleGraph, OAI.Ostmann.copyScheduleOutside, OAI.Ostmann.copySchedulePath, OAI.Ostmann.finalCopyParity
theorem OAI.Ostmann.copyScheduleGraph_fresh_to_positive line 127
theorem OAI.Ostmann.copyScheduleGraph_path_to_positive line 139
Source documentation
A regular original word has the same signed edge to every future active pivot. The hypothesis refers only to the initial graph's off-diagonal edges.
```
theorem copyScheduleGraph_path_to_positive {I : Type*}
    (g : I → I → ℤ) (pivot : ℕ → I) (n : ℕ) (i a : I)
    (hp : ∀ k < n, g i (pivot k) = 1) (ha : g i a = 1) (t : Fin n → Bool) :
    copyScheduleGraph g pivot n (copySchedulePath n t i) (copySchedulePositive n a) =
      finalCopyParity t := by
…
```
Mentions: OAI.Ostmann.copyScheduleGraph, OAI.Ostmann.copySchedulePath, OAI.Ostmann.copySchedulePositive, OAI.Ostmann.finalCopyParity

theorem OAI.Ostmann.copyScheduleGraph_path_to_fresh line 161

Source documentation

The same regular row holds against every anchor not yet used.

theorem copyScheduleGraph_path_to_fresh {I : Type*}
    (g : I → I → ℤ) (pivot : ℕ → I) (n : ℕ) (i a : I)
    (ha : g i a = 1) (t : Fin n → Bool) :
    copyScheduleGraph g pivot n (copySchedulePath n t i) (copyScheduleOutside n a) =
      finalCopyParity t := by
…

Mentions: OAI.Ostmann.copyScheduleGraph, OAI.Ostmann.copySchedulePath, OAI.Ostmann.copyScheduleOutside, OAI.Ostmann.finalCopyParity