OAI/NumberTheory/Ostmann/Construction/SelectedNodeSources.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Ostmann.reverseCopyLabelMap_wordOutside_property line 12

   Source documentation

   A property of the outside coordinates survives one literal reversal.

   theorem reverseCopyLabelMap_wordOutside_property {I A : Type*}
       (role : I → CopyScheduleRole) (i : I) (hi : role i = .word)
       (n : ℕ) (b : Bool) (P : A) (current : CopyScheduleAtoms role (n + 1) → A)
       (F : A → Prop) (hP : F P)
       (hcurrent : ∀ v : WordLeafOutside role i hi (n + 1), F (current v.val))
       (v : WordLeafOutside role i hi n) :
       F (reverseCopyLabelMap role n b P current v.val) := by
   …

   Mentions: OAI.Ostmann.CopyScheduleRole, OAI.Ostmann.CopyScheduleAtoms, OAI.Ostmann.WordLeafOutside, OAI.Ostmann.reverseCopyLabelMap

2. theorem OAI.Ostmann.descendAtomSources_wordOutside line 41

   Source documentation

   The whole path uses only initial outside coordinates and earlier pivots.

   theorem descendAtomSources_wordOutside {I B : Type*}
       (role : I → CopyScheduleRole) (i : I) (hi : role i = .word)
       (h n d : ℕ) (path : Fin h → Bool)
       (source : CopyScheduleAtoms role (n + h) → B ⊕ ℕ) (F : B ⊕ ℕ → Prop)
       (hsource : ∀ v : WordLeafOutside role i hi (n + h), F (source v.val))
       (hpivot : ∀ k, d ≤ k → k < d + h → F (.inr k)) :
       ∀ v : WordLeafOutside role i hi n,
         F (descendAtomSources role h n d path source v.val) := by
   …

   Mentions: OAI.Ostmann.CopyScheduleRole, OAI.Ostmann.CopyScheduleAtoms, OAI.Ostmann.WordLeafOutside, OAI.Ostmann.descendAtomSources

3. def OAI.Ostmann.WordSourceOutside line 59
4. theorem OAI.Ostmann.scheduledRawNodeSources_wordOutside line 64
5. def OAI.Ostmann.selectedNodeSources line 82

   Source documentation

   Restricting the source type does not change the value or identify sources.

   noncomputable def selectedNodeSources {I : Type*}
       (role : I → CopyScheduleRole) (i : I) (hi : role i = .word)
       (n : ℕ) (j : Fin (2 ^ n - 1))
       (v : WordLeafOutside role i hi (scheduledNodeLevel n j + 1)) :
       WordLeafOutside role i hi n ⊕ Fin (preorderNodePath n j).length :=
   …

   Mentions: OAI.Ostmann.CopyScheduleRole, OAI.Ostmann.WordLeafOutside, OAI.Ostmann.scheduledNodeLevel, OAI.Ostmann.preorderNodePath

6. theorem OAI.Ostmann.selectedNodeSources_unbound line 97
7. theorem OAI.Ostmann.selectedNodeSources_injective line 106
8. theorem OAI.Ostmann.selectedNodeSources_eval line 116