SchedulePairwiseReplay.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

The reduced support implies every original pairwise-coprimality gate

theorem OAI.Ostmann.scheduleAtomUnitsValid_root line 13
def OAI.Ostmann.scheduleAtomPairwiseValid line 22

theorem OAI.Ostmann.schedule_pairwise_of_reduced_support line 37

Source documentation

All H-coprimalities are forced by the signed reconstruction and inherited frequency-units. Only the Y checks and top pairwise support need be retained.

theorem schedule_pairwise_of_reduced_support {I : Type*} [Fintype I]
    (role : I → CopyScheduleRole) (childBound pivotBound : ℕ → ℕ)
    (n : ℕ) (x : CopyScheduleAtoms role n → ℕ) (t : FrequencyTree ℤ n)
    (hu : ∀ j < n, ∀ a b, role a = .pivot j → role b = .pivot j → a = b)
    (hv : ValidTransferHistory (scheduleAtomSystem role childBound pivotBound) n ⟨n, x⟩ t)
    (hunits : scheduleAtomUnitsValid role childBound pivotBound (totalAtomUnitRanges role) n x t)
    (hY : scheduleAtomCoprimalitiesValid role childBound pivotBound n x t)
    (hpair : Pairwise (fun i j => (x i).Coprime (x j))) :
    scheduleAtomPairwiseValid role childBound pivotBound n x t := by
…

Mentions: OAI.Ostmann.CopyScheduleRole, OAI.Ostmann.CopyScheduleAtoms, OAI.Ostmann.FrequencyTree, OAI.Ostmann.ValidTransferHistory, OAI.Ostmann.scheduleAtomSystem, OAI.Ostmann.scheduleAtomUnitsValid, OAI.Ostmann.totalAtomUnitRanges, OAI.Ostmann.scheduleAtomCoprimalitiesValid, OAI.Ostmann.scheduleAtomPairwiseValid