ScheduledFinalInteraction.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

Every distinct final pair has a genuine one-sided scheduled interaction

def OAI.Ostmann.scheduledPairMatching line 11

theorem OAI.Ostmann.scheduled_final_pair_interaction line 18

Source documentation

The two final reassignments induce this literal matching of retained prime slots. The short modulus is one of the constructed outside anchors.

theorem scheduled_final_pair_interaction {I : Type*} (role : I → CopyScheduleRole)
    (pivot : ℕ → I) (n m : ℕ) (word : Fin m ≃ {i : I // role i = .word})
    (anchor : Fin (n + 1) → I) (ha : ∀ j, role (anchor j) = .anchor j)
    (hp : ∀ k < n + 1, role (pivot k) = .pivot k)
    (e f : FinalParityReassignments n m) (hef : e ≠ f) :
    ∃ (h : CopyScheduleH role (n + 1)) (j : Fin (n + 1)) (b : Bool),
      let a := scheduledPastAnchor role n (anchor j) j (ha j) b
…

Mentions: OAI.Ostmann.CopyScheduleRole, OAI.Ostmann.FinalParityReassignments, OAI.Ostmann.CopyScheduleH, OAI.Ostmann.scheduledPastAnchor

theorem OAI.Ostmann.scheduledPairMatching_origin line 58
Source documentation
The matching also preserves the original role, so it preserves both its character and its unconditioned harmonic marginal.
```
theorem scheduledPairMatching_origin {I : Type*} (role : I → CopyScheduleRole)
    (n m : ℕ) (word : Fin m ≃ {i : I // role i = .word})
    (e f : FinalParityReassignments n m) (h : CopyScheduleH role (n + 1)) :
    copyScheduleOrigin (n + 1) (scheduledPairMatching role n m word e f h).val =
      copyScheduleOrigin (n + 1) h.val := by
…
```
Mentions: OAI.Ostmann.CopyScheduleRole, OAI.Ostmann.FinalParityReassignments, OAI.Ostmann.CopyScheduleH, OAI.Ostmann.copyScheduleOrigin, OAI.Ostmann.scheduledPairMatching
theorem OAI.Ostmann.scheduled_final_pair_nonprincipal line 71