OAI/NumberTheory/Ostmann/Construction/ExpandedScheduleCoordinates.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.Ostmann.ExpandedScheduledVariable line 11
2. def OAI.Ostmann.expandedPivotAddress line 14
3. def OAI.Ostmann.ExpandedCoordinateAfter line 17
4. theorem OAI.Ostmann.ExpandedCoordinateAfter.mono line 21
5. theorem OAI.Ostmann.expandedPivotAddress_after line 28
6. theorem OAI.Ostmann.expandedPivotAddress_fresh line 33
7. theorem OAI.Ostmann.reverseExpandedCoordinates_after line 44

   Source documentation

   Descending one level adds just its reconstructed pivot coordinate; all inherited coordinates still lie strictly above the next pivot level.

   theorem reverseExpandedCoordinates_after {I α : Type*} (role : I → CopyScheduleRole)
       (depth j : ℕ) (hj : j ≤ depth) (b : Bool) (path : List Bool)
       (current : CopyScheduleAtoms role (j + 1) → List (ExpandedScheduledVariable α depth))
       (hc : ∀ i v, v ∈ current i → ExpandedCoordinateAfter (j + 1) v) :
       ∀ i v, v ∈ reverseCopyLabelMap role j b [expandedPivotAddress α depth j path] current i →
         ExpandedCoordinateAfter j v := by
   …

   Mentions: OAI.Ostmann.CopyScheduleRole, OAI.Ostmann.CopyScheduleAtoms, OAI.Ostmann.ExpandedScheduledVariable, OAI.Ostmann.ExpandedCoordinateAfter, OAI.Ostmann.reverseCopyLabelMap, OAI.Ostmann.expandedPivotAddress

8. def OAI.Ostmann.expandedRootTemplate line 59
9. theorem OAI.Ostmann.expandedRootCoordinates_after line 65
10. theorem OAI.Ostmann.expandedRootTemplate_size line 74

    Source documentation

    The prime-expanded template has a concrete polynomial word bound.

    theorem expandedRootTemplate_size {I α : Type*} [Fintype I]
        (role : I → CopyScheduleRole) (depth : ℕ) (words : CopyScheduleAtoms role depth → List α)
        (childBound pivotBound : ℕ → ℕ) (M : ℕ) (hM : 1 ≤ M)
        (hwords : ∀ i, (words i).length ≤ M) :
        (expandedRootTemplate role depth words childBound pivotBound).WordsBounded
          (2 * 3 ^ depth * Fintype.card I * M + 4) := by
    …

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