OAI/NumberTheory/Ostmann/Construction/ScheduledWordTemplate.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Ostmann.scheduledHWord line 12
2. def OAI.Ostmann.scheduledWordTemplate line 19

   Source documentation

   Each internal address names the product of the pivot atom erased at that node. Both child templates read the same Y and their own H copies.

   noncomputable def scheduledWordTemplate {I σ : Type*} [Fintype I] (role : I → CopyScheduleRole)
       (address : ℕ → List Bool → σ) (childBound pivotBound : ℕ → ℕ) :
       (n : ℕ) → List Bool → (CopyScheduleAtoms role n → σ) → WordTransferTemplate σ n
     | 0, _, current => .leaf ((Finset.univ.toList : List (CopyScheduleAtoms role 0)).map current)
     | n + 1, path, current =>
         .node ⟨address n path, scheduledHWord role n true current,
           scheduledHWord role n false current, childBound n, pivotBound n⟩
           (scheduledWordTemplate role address childBound pivotBound n (true :: path)
             (reverseCopyLabelMap role n true (address n path) current))
           (scheduledWordTemplate role address childBound pivotBound n (false :: path)
             (reverseCopyLabelMap role n false (address n path) current))

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

3. theorem OAI.Ostmann.scheduledHWord_length line 31
4. theorem OAI.Ostmann.scheduledWordTemplate_words_bounded line 38

   Source documentation

   The word-size bound is inherited from the literal H partition sizes; no independent polynomial-size hypothesis is imposed on the resulting template.

   theorem scheduledWordTemplate_words_bounded {I σ : Type*} [Fintype I]
       (role : I → CopyScheduleRole) (address : ℕ → List Bool → σ)
       (childBound pivotBound : ℕ → ℕ) (n : ℕ) (B : ℕ)
       (hbase : Fintype.card (CopyScheduleAtoms role 0) + 1 ≤ B)
       (hH : ∀ j < n, 2 * Fintype.card (CopyScheduleH role j) + 4 ≤ B)
       (path : List Bool) (current : CopyScheduleAtoms role n → σ) :
       (scheduledWordTemplate role address childBound pivotBound n path current).WordsBounded B := by
   …

   Mentions: OAI.Ostmann.CopyScheduleRole, OAI.Ostmann.CopyScheduleAtoms, OAI.Ostmann.CopyScheduleH, OAI.Ostmann.scheduledWordTemplate

5. theorem OAI.Ostmann.scheduledHWord_product line 56
6. theorem OAI.Ostmann.scheduledWordTemplate_products line 65

   Source documentation

   The numerator products at the top node are precisely its independent positive and negative H copies.

   theorem scheduledWordTemplate_products {I σ : Type*} [Fintype I]
       (role : I → CopyScheduleRole) (address : ℕ → List Bool → σ)
       (childBound pivotBound : ℕ → ℕ) (n : ℕ) (path : List Bool)
       (current : CopyScheduleAtoms role (n + 1) → σ) (x : σ → ℕ) :
       wordTransferLeft ((scheduledWordTemplate role address childBound pivotBound (n + 1) path current).state x) =
         (∏ i : CopyScheduleH role n, x (current ⟨.inl (true, i.val), i.property⟩)) ∧
       wordTransferRight ((scheduledWordTemplate role address childBound pivotBound (n + 1) path current).state x) =
         (∏ i : CopyScheduleH role n, x (current ⟨.inl (false, i.val), i.property⟩)) :=
   …

   Mentions: OAI.Ostmann.CopyScheduleRole, OAI.Ostmann.CopyScheduleAtoms, OAI.Ostmann.wordTransferLeft, OAI.Ostmann.scheduledWordTemplate, OAI.Ostmann.CopyScheduleH, OAI.Ostmann.wordTransferRight