OAI/NumberTheory/Ostmann/Construction/ExpandedScheduleState.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Ostmann.wordTransferLeftState_node line 12

   Source documentation

   Expose the child assignment with any decidable equality instance.

   theorem wordTransferLeftState_node {σ : Type*} [DecidableEq σ] {n : ℕ}
       (d : WordTransferNode σ) (l r : WordTransferTemplate σ n) (x : σ → ℕ) (P : ℕ) :
       (wordTransferSystem σ).leftState ((WordTransferTemplate.node d l r).state x) P =
         l.state (Function.update x d.target P) := by
   …

   Mentions: OAI.Ostmann.WordTransferNode, OAI.Ostmann.WordTransferTemplate, OAI.Ostmann.wordTransferSystem

2. theorem OAI.Ostmann.wordTransferRightState_node line 21
3. theorem OAI.Ostmann.word_product_update_of_fresh line 30
4. theorem OAI.Ostmann.reverseCopyLabelMap_product_update line 40

   Source documentation

   At the reconstructed pivot we read P, at H the selected copy, and at Y the common retained value. This equality includes composite atom words.

   theorem reverseCopyLabelMap_product_update {I σ : Type*} [DecidableEq σ] (role : I → CopyScheduleRole)
       (n : ℕ) (b : Bool) (pivot : σ) (P : ℕ)
       (current : CopyScheduleAtoms role (n + 1) → List σ) (x : σ → ℕ)
       (hfresh : ∀ i j, j ∈ current i → j ≠ pivot) (i : CopyScheduleAtoms role n) :
       ((reverseCopyLabelMap role n b [pivot] current i).map (Function.update x pivot P)).prod =
         reverseCopyLabelMap role n b P (fun j => ((current j).map x).prod) i := by
   …

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

5. theorem OAI.Ostmann.expandedHWord_product_update line 55

   Source documentation

   The inserted coordinate does not alter any of the actual H-copy products that enter the reversing numerator.

   theorem expandedHWord_product_update {I σ : Type*} [Fintype I] [DecidableEq σ] (role : I → CopyScheduleRole)
       (n : ℕ) (b : Bool) (current : CopyScheduleAtoms role (n + 1) → List σ)
       (x : σ → ℕ) (pivot : σ) (P : ℕ) (hfresh : ∀ i j, j ∈ current i → j ≠ pivot) :
       ((expandedHWord role n b current).map (Function.update x pivot P)).prod =
         ((expandedHWord role n b current).map x).prod := by
   …

   Mentions: OAI.Ostmann.CopyScheduleRole, OAI.Ostmann.CopyScheduleAtoms, OAI.Ostmann.expandedHWord