OAI/NumberTheory/Ostmann/Construction/ScheduledMatchedEdges.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Ostmann.scheduledMatchedGraph line 11
2. theorem OAI.Ostmann.constituentMatchedGraph_eq line 18
3. theorem OAI.Ostmann.scheduledMatchedGraph_self line 25
4. theorem OAI.Ostmann.scheduledMatchedGraph_outside line 32
5. def OAI.Ostmann.scheduledPastAnchor line 40
6. theorem OAI.Ostmann.scheduledMatchedGraph_anchor_word line 50

   Source documentation

   This is an identity for the computed graph, with the counterpart slot identified by the actual inverse matching permutation.

   theorem scheduledMatchedGraph_anchor_word {I : Type*} (role : I → CopyScheduleRole)
       (pivot : ℕ → I) (n : ℕ) (e : Equiv.Perm (CopyScheduleH role (n + 1)))
       (a i i' : I) (j : Fin (n + 1)) (ha : role a = .anchor j) (b : Bool)
       (hap : ∀ k < n + 1, a ≠ pivot k) (hai : a ≠ i) (hai' : a ≠ i')
       (t t' : Fin (n + 1) → Bool) (h : CopyScheduleH role (n + 1))
       (hh : h.val = copySchedulePath (n + 1) t i)
       (hh' : (e.symm h).val = copySchedulePath (n + 1) t' i') :
       scheduledMatchedGraph role pivot (n + 1) e
         (.inr (scheduledPastAnchor role n a j ha b)) (.inl h) =
         anchorIncoming (fun _ => 1) t j b - anchorIncoming (fun _ => 1) t' j b := by
   …

   Mentions: OAI.Ostmann.CopyScheduleRole, OAI.Ostmann.CopyScheduleH, OAI.Ostmann.copySchedulePath, OAI.Ostmann.scheduledMatchedGraph, OAI.Ostmann.scheduledPastAnchor, OAI.Ostmann.anchorIncoming

7. theorem OAI.Ostmann.scheduledMatchedGraph_word_anchor line 70
8. theorem OAI.Ostmann.scheduledMatchedGraph_changed_code line 95

   Source documentation

   A changed code with unchanged final parity supplies a genuine signed square in the actual matching graph. All other graph entries remain arbitrary.

   theorem scheduledMatchedGraph_changed_code {I : Type*} (role : I → CopyScheduleRole)
       (pivot : ℕ → I) (n : ℕ) (e : Equiv.Perm (CopyScheduleH role (n + 1)))
       (anchor : Fin (n + 1) → I) (ha : ∀ j, role (anchor j) = .anchor j)
       (hp : ∀ k < n + 1, role (pivot k) = .pivot k)
       (i i' : I) (hi : role i = .word) (hi' : role i' = .word)
       (t t' : Fin (n + 1) → Bool) (h : CopyScheduleH role (n + 1))
       (hh : h.val = copySchedulePath (n + 1) t i)
       (hh' : (e.symm h).val = copySchedulePath (n + 1) t' i')
       (hparity : finalCopyParity t = finalCopyParity t')
       (hcode : finiteAnchorCode (fun _ => 1) t ≠ finiteAnchorCode (fun _ => 1) t') :
       ∃ (j : Fin (n + 1)) (b : Bool),
         let a := scheduledPastAnchor role n (anchor j) j (ha j) b
   …

   Mentions: OAI.Ostmann.CopyScheduleRole, OAI.Ostmann.CopyScheduleH, OAI.Ostmann.copySchedulePath, OAI.Ostmann.finalCopyParity, OAI.Ostmann.finiteAnchorCode, OAI.Ostmann.scheduledPastAnchor