ScheduledAnchorGraph.lean`

8 declarations, 0 contain sorry, 0 declared as axioms

Anchor codes derived from the full copied-slot schedule

theorem OAI.Ostmann.copyScheduleGraph_path_to_anchor line 13

Source documentation

Every outgoing word-to-anchor edge is its final copy parity.

theorem copyScheduleGraph_path_to_anchor {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) (j : ℕ) (hj : j < n) (b : Bool) :
    copyScheduleGraph g pivot n (copySchedulePath n t i) (copyScheduleAnchor n j b a) =
      finalCopyParity t := by
…

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

theorem OAI.Ostmann.copyScheduleGraph_anchor_to_path line 51

Source documentation

The incoming anchor edge has exactly the previously constructed code. The initial graph is the only source of the two hypotheses.

theorem copyScheduleGraph_anchor_to_path {I : Type*}
    (g : I → I → ℤ) (pivot : ℕ → I) (n : ℕ) (i a : I)
    (hp : ∀ k < n, g a (pivot k) = 1) (ha : g a i = 1)
    (t : Fin n → Bool) (j : Fin n) (b : Bool) :
    copyScheduleGraph g pivot n (copyScheduleAnchor n j b a) (copySchedulePath n t i) =
      anchorIncoming (fun _ => 1) t j b := by
…

Mentions: OAI.Ostmann.copyScheduleGraph, OAI.Ostmann.copyScheduleAnchor, OAI.Ostmann.copySchedulePath, OAI.Ostmann.anchorIncoming

def OAI.Ostmann.initialCompleteGraph line 104
Source documentation
The level-zero graph has exponent one on every distinct ordered pair.
```
noncomputable def initialCompleteGraph {I : Type*} (i j : I) : ℤ :=
…
```
theorem OAI.Ostmann.initialCompleteGraph_self line 107
theorem OAI.Ostmann.initialCompleteGraph_of_ne line 110

def OAI.Ostmann.scheduledFinalGraph line 115

Source documentation

The final graph is obtained by restricting the computed graph to the surviving words, anchors, and remaining slots.

noncomputable def scheduledFinalGraph {I J : Type*} {n m : ℕ}
    (pivot : ℕ → I) (word : Fin m → I) (anchor : Fin (n + 1) → I)
    (other : J → CopyScheduleVertex I (n + 1)) :
    FinalGraphVertex n m J → FinalGraphVertex n m J → ℤ :=
…

Mentions: OAI.Ostmann.CopyScheduleVertex, OAI.Ostmann.FinalGraphVertex

theorem OAI.Ostmann.scheduledFinalGraph_diagonal line 126

theorem OAI.Ostmann.scheduledFinalGraph_reassignment line 134

Source documentation

Every distinct parity-preserving reassignment of the actual scheduled graph has the required signed-square edge and zero reverse edge.

theorem scheduledFinalGraph_reassignment {I J : Type*} {n m : ℕ}
    (pivot : ℕ → I) (word : Fin m → I) (anchor : Fin (n + 1) → I)
    (other : J → CopyScheduleVertex I (n + 1))
    (hwp : ∀ i k, k < n + 1 → word i ≠ pivot k)
    (hpa : ∀ j k, k < n + 1 → anchor j ≠ pivot k)
    (hwa : ∀ i j, word i ≠ anchor j)
    (e f : FinalParityReassignments n m) (hef : e ≠ f) :
    ∃ (x : ParityPathSum n × Fin m) (j : Fin (n + 1)) (b : Bool),
      let G := graphDifference
…

Mentions: OAI.Ostmann.CopyScheduleVertex, OAI.Ostmann.FinalParityReassignments, OAI.Ostmann.ParityPathSum, OAI.Ostmann.graphDifference