SchedulePivotSlots.lean`

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

The active pivot group has exactly its original constituent slots

theorem OAI.Ostmann.CopyScheduleRole.afterCopy_eq_pivot line 9
theorem OAI.Ostmann.copySchedulePositive_injective line 13
theorem OAI.Ostmann.surviving_pivot_is_positive line 23
Source documentation
No old pivot can remain active: the active group is copied positively until its own step and is then erased in its entirety.
```
theorem surviving_pivot_is_positive {I : Type*} (role : I → CopyScheduleRole)
    (n k : ℕ) (v : CopyScheduleVertex I n)
    (hv : CopyScheduleSurvives role n v) (hw : copyScheduleRole role n v = .pivot k) :
    n ≤ k ∧ ∃ i : I, role i = .pivot k ∧ v = copySchedulePositive n i := by
…
```
Mentions: OAI.Ostmann.CopyScheduleRole, OAI.Ostmann.CopyScheduleVertex, OAI.Ostmann.CopyScheduleSurvives, OAI.Ostmann.copyScheduleRole, OAI.Ostmann.copySchedulePositive
abbrev OAI.Ostmann.SurvivingPivotSlot line 53
def OAI.Ostmann.survivingPivotEquiv line 56
theorem OAI.Ostmann.surviving_pivot_card line 70
theorem OAI.Ostmann.unique_active_pivot_atom line 78
Source documentation
At its own step there is one active atom whenever the original group was represented by one atom. Its internal prime constituents need no new copies.
```
theorem unique_active_pivot_atom {I : Type*} (role : I → CopyScheduleRole)
    (k : ℕ) (p : I) (hp : role p = .pivot k)
    (hunique : ∀ i, role i = .pivot k → i = p) :
    ∃! v : CopyScheduleVertex I k,
      CopyScheduleSurvives role k v ∧ copyScheduleRole role k v = .pivot k := by
…
```
Mentions: OAI.Ostmann.CopyScheduleRole, OAI.Ostmann.CopyScheduleVertex, OAI.Ostmann.CopyScheduleSurvives, OAI.Ostmann.copyScheduleRole