OAI/NumberTheory/Ostmann/Construction/ScheduledMatchedCodeSplit.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Ostmann.scheduledMatchedGraph_changed_code_split line 11

   Source documentation

   A changed code chooses either the small-anchor-to-word character or the word-to-large-anchor character. The same computed graph is used in both cases.

   theorem scheduledMatchedGraph_changed_code_split {I : Type*} (role : I → CopyScheduleRole)
       (pivot : ℕ → I) (n : ℕ) (e : Equiv.Perm (CopyScheduleH role (n + 1)))
       (small large : Fin (n + 1) → I)
       (hsmall : ∀ j, role (small j) = .anchor j) (hlarge : ∀ j, role (large 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')
       (hcode : finiteAnchorCode (fun _ => 1) t ≠ finiteAnchorCode (fun _ => 1) t') :
       ∃ (j : Fin (n + 1)) (b : Bool),
         let a := scheduledPastAnchor role n (small j) j (hsmall j) b
   …

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