ReverseCopyMap.lean`

6 declarations, 0 contain sorry, 0 declared as axioms

Reversing the literal copied-atom schedule

This construction is at the atom level: a current pivot group is one atom carrying its total product.

abbrev OAI.Ostmann.CopyScheduleAtoms line 15
def OAI.Ostmann.reverseCopyLabelMap line 20
Source documentation
The chosen child reads its H copy and the common Y. The erased pivot is represented by the coordinate that the arithmetic node reconstructs.
```
noncomputable def reverseCopyLabelMap {I σ : Type*} (role : I → CopyScheduleRole)
    (n : ℕ) (b : Bool) (pivot : σ) (current : CopyScheduleAtoms role (n + 1) → σ)
    (i : CopyScheduleAtoms role n) : σ :=
…
```
Mentions: OAI.Ostmann.CopyScheduleRole, OAI.Ostmann.CopyScheduleAtoms
theorem OAI.Ostmann.reverseCopyLabelMap_copied line 28
theorem OAI.Ostmann.reverseCopyLabelMap_retained line 35
theorem OAI.Ostmann.reverseCopyLabelMap_erased line 42

theorem OAI.Ostmann.reverseCopyLabelMap_unique_pivot line 50

Source documentation

There is exactly one replaced coordinate when the pivot group is represented by one original atom. This is the manuscript's grouping convention.

theorem reverseCopyLabelMap_unique_pivot {I σ : Type*} (role : I → CopyScheduleRole)
    (n : ℕ) (b : Bool) (pivot : σ) (current : CopyScheduleAtoms role (n + 1) → σ)
    (p : I) (hp : role p = .pivot n) (hunique : ∀ i, role i = .pivot n → i = p) :
    ∃! i : CopyScheduleAtoms role n,
      copyScheduleRole role n i.val = .pivot n ∧ reverseCopyLabelMap role n b pivot current i = pivot := by
…

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