OAI/NumberTheory/Ostmann/Construction/ExpandedOutsideCoordinates.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Ostmann.ExpandedActualCoordinates line 11
2. theorem OAI.Ostmann.copyScheduleY_not_pivot line 16
3. theorem OAI.Ostmann.reverseExpandedActualCoordinates line 28

   Source documentation

   Reversing a step inserts an integer only at the erased active pivot; all other role types retain actual-prime words.

   theorem reverseExpandedActualCoordinates {I α : Type*} (role : I → CopyScheduleRole)
       (depth n : ℕ) (b : Bool) (pivot : ExpandedScheduledVariable α depth)
       (current : CopyScheduleAtoms role (n + 1) → List (ExpandedScheduledVariable α depth))
       (hc : ExpandedActualCoordinates role depth (n + 1) current) :
       ExpandedActualCoordinates role depth n (reverseCopyLabelMap role n b [pivot] current) := by
   …

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

4. theorem OAI.Ostmann.expandedRoot_actual_coordinates line 49
5. theorem OAI.Ostmann.expandedYWord_actual line 58

   Source documentation

   Thus every constituent of Y is an actual prime variable even after ancestor pivots have already been reconstructed.

   theorem expandedYWord_actual {I α : Type*} (role : I → CopyScheduleRole)
       (depth n : ℕ)
       (current : CopyScheduleAtoms role (n + 1) → List (ExpandedScheduledVariable α depth))
       (hc : ExpandedActualCoordinates role depth (n + 1) current)
       (i : CopyScheduleY role n) :
       ∀ v ∈ current ⟨.inr i.val, i.property⟩, ∃ a : α, v = .inl a := by
   …

   Mentions: OAI.Ostmann.CopyScheduleRole, OAI.Ostmann.CopyScheduleAtoms, OAI.Ostmann.ExpandedScheduledVariable, OAI.Ostmann.ExpandedActualCoordinates, OAI.Ostmann.CopyScheduleY