ScheduledTransferGraph.lean`

6 declarations, 0 contain sorry, 0 declared as axioms

Restricting the graph update to the actual H/Y partition

def OAI.Ostmann.scheduledRetainedGraph line 12

Source documentation

The input graph retains only the total pivot and the actual H/Y slots.

noncomputable def scheduledRetainedGraph {I : Type*} (role : I → CopyScheduleRole)
    (g : I → I → ℤ) (pivot : ℕ → I) (n : ℕ) :
    Option (CopyScheduleH role n ⊕ CopyScheduleY role n) →
      Option (CopyScheduleH role n ⊕ CopyScheduleY role n) → ℤ :=
…

Mentions: OAI.Ostmann.CopyScheduleRole, OAI.Ostmann.CopyScheduleH, OAI.Ostmann.CopyScheduleY

def OAI.Ostmann.scheduledOutputVertex line 24
Source documentation
No unused copied or retained alternative occurs in this map.
```
def scheduledOutputVertex {I : Type*} (role : I → CopyScheduleRole) (n : ℕ) :
    (Bool × CopyScheduleH role n) ⊕ CopyScheduleY role n →
      {i : CopyScheduleVertex I (n + 1) // CopyScheduleSurvives role (n + 1) i} :=
…
```
Mentions: OAI.Ostmann.CopyScheduleRole, OAI.Ostmann.CopyScheduleH, OAI.Ostmann.CopyScheduleY, OAI.Ostmann.CopyScheduleVertex, OAI.Ostmann.CopyScheduleSurvives
theorem OAI.Ostmann.scheduledRetainedGraph_update line 31
Source documentation
The graph used by the exact local phase formula is the restriction of our recursively constructed graph to the genuine surviving slots.
```
theorem scheduledRetainedGraph_update {I : Type*} (role : I → CopyScheduleRole)
    (g : I → I → ℤ) (pivot : ℕ → I) (n : ℕ)
    (i j : (Bool × CopyScheduleH role n) ⊕ CopyScheduleY role n) :
    transferredGraph (scheduledRetainedGraph role g pivot n) i j =
      copyScheduleGraph g pivot (n + 1)
        (scheduledOutputVertex role n i).val (scheduledOutputVertex role n j).val := by
…
```
Mentions: OAI.Ostmann.CopyScheduleRole, OAI.Ostmann.CopyScheduleH, OAI.Ostmann.CopyScheduleY, OAI.Ostmann.transferredGraph, OAI.Ostmann.scheduledRetainedGraph, OAI.Ostmann.copyScheduleGraph, OAI.Ostmann.scheduledOutputVertex
theorem OAI.Ostmann.scheduledRetainedGraph_diagonal line 48

theorem OAI.Ostmann.scheduledRetainedGraph_pivot_column line 55

Source documentation

The pivot-column exponent in the local phase is independent of which constituent is chosen to represent that active pivot group.

theorem scheduledRetainedGraph_pivot_column {I : Type*} (role : I → CopyScheduleRole)
    (pivot : ℕ → I) (hpivot : ∀ k, role (pivot k) = .pivot k)
    (n : ℕ) (p : I) (hp : role p = .pivot n)
    (i : CopyScheduleH role n ⊕ CopyScheduleY role n) :
    scheduledRetainedGraph role initialCompleteGraph pivot n (some i) none =
      copyScheduleGraph initialCompleteGraph pivot n
        (Sum.elim Subtype.val Subtype.val i) (copySchedulePositive n p) := by
…

Mentions: OAI.Ostmann.CopyScheduleRole, OAI.Ostmann.CopyScheduleH, OAI.Ostmann.CopyScheduleY, OAI.Ostmann.scheduledRetainedGraph, OAI.Ostmann.initialCompleteGraph, OAI.Ostmann.copyScheduleGraph, OAI.Ostmann.copySchedulePositive

theorem OAI.Ostmann.scheduledRetainedGraph_word_pivot line 78

Source documentation

The regular row hypotheses required when removing the pivot factors are consequences of the constructed graph and original role distinction.

theorem scheduledRetainedGraph_word_pivot {I : Type*} (role : I → CopyScheduleRole)
    (pivot : ℕ → I) (hpivot : ∀ k, role (pivot k) = .pivot k)
    (n : ℕ) (i : I) (hi : role i = .word) (t : Fin n → Bool)
    (h : CopyScheduleH role n) (hh : h.val = copySchedulePath n t i) :
    scheduledRetainedGraph role initialCompleteGraph pivot n (some (.inl h)) none =
      finalCopyParity t := by
…

Mentions: OAI.Ostmann.CopyScheduleRole, OAI.Ostmann.CopyScheduleH, OAI.Ostmann.copySchedulePath, OAI.Ostmann.scheduledRetainedGraph, OAI.Ostmann.initialCompleteGraph, OAI.Ostmann.finalCopyParity