ScheduleGraphInvariants.lean`

5 declarations, 0 contain sorry, 0 declared as axioms

Regular rows and pivot columns on the surviving template slots

def OAI.Ostmann.ScheduledRegularRow line 12
Source documentation
The row assertion is restricted to surviving slots, as required by the actual H/Y partition; unused ambient labels are irrelevant.
```
def ScheduledRegularRow {I : Type*} (role : I → CopyScheduleRole)
    (g : I → I → ℤ) (pivot : ℕ → I) (n : ℕ)
    (i : CopyScheduleVertex I n) (ε : ℤ) : Prop :=
…
```
Mentions: OAI.Ostmann.CopyScheduleRole, OAI.Ostmann.CopyScheduleVertex
theorem OAI.Ostmann.scheduledRegularRow_copy line 17

theorem OAI.Ostmann.scheduledRegularRow_word line 46

Source documentation

Every copied word row has its accumulated sign, on the full current list.

theorem scheduledRegularRow_word {I : Type*} (role : I → CopyScheduleRole)
    (pivot : ℕ → I) (hpivot : ∀ k, role (pivot k) = .pivot k)
    (i : I) (hi : role i = .word) (n : ℕ) (t : Fin n → Bool) :
    ScheduledRegularRow role initialCompleteGraph pivot n (copySchedulePath n t i)
      (finalCopyParity t) := by
…

Mentions: OAI.Ostmann.CopyScheduleRole, OAI.Ostmann.ScheduledRegularRow, OAI.Ostmann.initialCompleteGraph, OAI.Ostmann.copySchedulePath, OAI.Ostmann.finalCopyParity

theorem OAI.Ostmann.scheduledRegularRow_pivot line 71

Source documentation

The unique active copy of a future pivot has regular row sign +1.

theorem scheduledRegularRow_pivot {I : Type*} (role : I → CopyScheduleRole)
    (pivot : ℕ → I) (hpivot : ∀ k, role (pivot k) = .pivot k)
    (i : I) (k : ℕ) (hi : role i = .pivot k) (n : ℕ) (hn : n ≤ k) :
    ScheduledRegularRow role initialCompleteGraph pivot n (copySchedulePositive n i) 1 := by
…

Mentions: OAI.Ostmann.CopyScheduleRole, OAI.Ostmann.ScheduledRegularRow, OAI.Ostmann.initialCompleteGraph, OAI.Ostmann.copySchedulePositive

theorem OAI.Ostmann.copyScheduleGraph_pivot_common_column line 97

Source documentation

Every incoming row is constant on the constituents of a future pivot. The targets are its actual positive copies, not a collapsed prime placeholder.

theorem copyScheduleGraph_pivot_common_column {I : Type*}
    (role : I → CopyScheduleRole) (pivot : ℕ → I)
    (k : ℕ) (a b : I) (ha : role a = .pivot k) (hb : role b = .pivot k)
    (n : ℕ) (hn : n ≤ k) (i : CopyScheduleVertex I n)
    (hi : CopyScheduleSurvives role n i) (hne : copyScheduleRole role n i ≠ .pivot k) :
    copyScheduleGraph initialCompleteGraph pivot n i (copySchedulePositive n a) =
      copyScheduleGraph initialCompleteGraph pivot n i (copySchedulePositive n b) := by
…

Mentions: OAI.Ostmann.CopyScheduleRole, OAI.Ostmann.CopyScheduleVertex, OAI.Ostmann.CopyScheduleSurvives, OAI.Ostmann.copyScheduleRole, OAI.Ostmann.copyScheduleGraph, OAI.Ostmann.initialCompleteGraph, OAI.Ostmann.copySchedulePositive