CopyScheduleSupport.lean`

17 declarations, 0 contain sorry, 0 declared as axioms

The actual H/Y/pivot partition of the copied-slot schedule

inductive OAI.Ostmann.CopyScheduleRole line 9
def OAI.Ostmann.CopyScheduleRole.copiedAt line 18
def OAI.Ostmann.CopyScheduleRole.erasedAt line 24
def OAI.Ostmann.CopyScheduleRole.afterCopy line 28

def OAI.Ostmann.copyScheduleRole line 36

Source documentation

The role of an actual copy, including the inactive negative pivot copies.

def copyScheduleRole {I : Type*} (role : I → CopyScheduleRole) :
    (n : ℕ) → CopyScheduleVertex I n → CopyScheduleRole
  | 0, i => role i
  | n + 1, .inl (b, i) => (copyScheduleRole role n i).afterCopy b
  | n + 1, .inr i => copyScheduleRole role n i

/-- Exactly the surviving labels. Copied labels come from H, retained labels
come from Y, and every constituent of the current pivot is removed. -/

Mentions: OAI.Ostmann.CopyScheduleRole, OAI.Ostmann.CopyScheduleVertex

def OAI.Ostmann.CopyScheduleSurvives line 44

Source documentation

Exactly the surviving labels. Copied labels come from H, retained labels come from Y, and every constituent of the current pivot is removed.

def CopyScheduleSurvives {I : Type*} (role : I → CopyScheduleRole) :
    (n : ℕ) → CopyScheduleVertex I n → Prop
  | 0, _ => True
  | n + 1, .inl (_, i) => CopyScheduleSurvives role n i ∧
      (copyScheduleRole role n i).copiedAt n = true
  | n + 1, .inr i => CopyScheduleSurvives role n i ∧
      (copyScheduleRole role n i).copiedAt n = false ∧
      (copyScheduleRole role n i).erasedAt n = false

Mentions: OAI.Ostmann.CopyScheduleRole, OAI.Ostmann.CopyScheduleVertex, OAI.Ostmann.copyScheduleRole

abbrev OAI.Ostmann.CopyScheduleH line 53
abbrev OAI.Ostmann.CopyScheduleY line 57
def OAI.Ostmann.copyScheduleSurvivorEquiv line 63
Source documentation
This is a literal equivalence, not a count of an oversized ambient space.
```
def copyScheduleSurvivorEquiv {I : Type*} (role : I → CopyScheduleRole) (n : ℕ) :
    {i : CopyScheduleVertex I (n + 1) // CopyScheduleSurvives role (n + 1) i} ≃
      (Bool × CopyScheduleH role n) ⊕ CopyScheduleY role n where
…
```
Mentions: OAI.Ostmann.CopyScheduleRole, OAI.Ostmann.CopyScheduleVertex, OAI.Ostmann.CopyScheduleSurvives, OAI.Ostmann.CopyScheduleH, OAI.Ostmann.CopyScheduleY
theorem OAI.Ostmann.copyScheduleRole_path line 82
theorem OAI.Ostmann.copyScheduleSurvives_path line 92
theorem OAI.Ostmann.copyScheduleRole_positive line 101
theorem OAI.Ostmann.copyScheduleSurvives_positive line 111
theorem OAI.Ostmann.copyScheduleRole_outside line 122
theorem OAI.Ostmann.copyScheduleSurvives_reserved line 129
Source documentation
A reserved anchor really remains in Y until its designated step.
```
theorem copyScheduleSurvives_reserved {I : Type*} (role : I → CopyScheduleRole)
    (i : I) (k : ℕ) (hi : role i = .anchor k) (n : ℕ) (hn : n ≤ k) :
    CopyScheduleSurvives role n (copyScheduleOutside n i) := by
…
```
Mentions: OAI.Ostmann.CopyScheduleRole, OAI.Ostmann.CopyScheduleSurvives, OAI.Ostmann.copyScheduleOutside
theorem OAI.Ostmann.copyScheduleRole_anchor line 140
theorem OAI.Ostmann.copyScheduleSurvives_anchor line 158
Source documentation
Both fresh-anchor clones survive and thereafter remain outside.
```
theorem copyScheduleSurvives_anchor {I : Type*} (role : I → CopyScheduleRole)
    (i : I) (k : ℕ) (hi : role i = .anchor k) (n : ℕ) (hn : k < n) (b : Bool) :
    CopyScheduleSurvives role n (copyScheduleAnchor n k b i) := by
…
```
Mentions: OAI.Ostmann.CopyScheduleRole, OAI.Ostmann.CopyScheduleSurvives, OAI.Ostmann.copyScheduleAnchor