OAI/NumberTheory/Ostmann/Construction/ScheduledWordLeafCoordinates.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Ostmann.treeLeafCopyPath line 13

   Source documentation

   Left arithmetic children use the positive copy of H.

   def treeLeafCopyPath : (n : ℕ) → TreeLeafIndex n → Fin n → Bool
     | 0, _ => fun j => Fin.elim0 j
     | n + 1, .inl t => Fin.snoc (treeLeafCopyPath n t) true
     | n + 1, .inr t => Fin.snoc (treeLeafCopyPath n t) false

   Mentions: OAI.Ostmann.TreeLeafIndex

2. theorem OAI.Ostmann.treeLeafCopyPath_injective line 18
3. def OAI.Ostmann.wordLeafSlot line 49
4. theorem OAI.Ostmann.wordLeafSlot_origin line 60
5. theorem OAI.Ostmann.wordLeafSlot_role line 65
6. theorem OAI.Ostmann.wordLeafSlot_left line 70
7. theorem OAI.Ostmann.wordLeafSlot_right line 76
8. theorem OAI.Ostmann.reverseCopyLabelMap_wordLeaf line 84

   Source documentation

   Reversal reads exactly the corresponding leaf prime; the inserted pivot does not replace any of the chosen word coordinates.

   theorem reverseCopyLabelMap_wordLeaf {I A : Type*} (role : I → CopyScheduleRole)
       (i : I) (hi : role i = .word) (n : ℕ) (b : Bool) (p : A)
       (x : CopyScheduleAtoms role (n + 1) → A) (t : TreeLeafIndex n) :
       reverseCopyLabelMap role n b p x (wordLeafSlot role i hi n t) =
         x (wordLeafSlot role i hi (n + 1) (if b then .inl t else .inr t)) := by
   …

   Mentions: OAI.Ostmann.CopyScheduleRole, OAI.Ostmann.CopyScheduleAtoms, OAI.Ostmann.TreeLeafIndex, OAI.Ostmann.reverseCopyLabelMap, OAI.Ostmann.wordLeafSlot

9. abbrev OAI.Ostmann.WordLeafOutside line 99
10. def OAI.Ostmann.wordLeafPartition line 103
11. theorem OAI.Ostmann.wordLeafPartition_leaf line 109
12. theorem OAI.Ostmann.wordLeafPartition_outside line 113
13. def OAI.Ostmann.wordLeafAssignment line 117
14. theorem OAI.Ostmann.wordLeafAssignment_leaf line 123
15. theorem OAI.Ostmann.wordLeafAssignment_outside line 132
16. def OAI.Ostmann.wordLeafAssignmentEquiv line 141
17. theorem OAI.Ostmann.scheduledPrimePrior_wordLeaf line 156