Request identities through buffer advancement

Tagged completed/pending indices form one permutation of the original requests. Moving a selected prefix into the completed side is an explicit equivalence, so no request is lost or duplicated during phase compaction.

def Algebraic.MassProduction.Nonuniform.BufferOrder.advance {completed pending total accepted remaining : ℕ} (order : Fin completed ⊕ Fin pending ≃ Fin total) (permutation : Equiv.Perm (Fin pending)) (split : accepted + remaining = pending) : Fin (completed + accepted) ⊕ Fin remaining ≃ Fin total

Reassociate the accepted prefix into the completed side, then apply the phase's request permutation and the previous global request order.

Equations

• One or more equations did not get rendered due to their size.

theorem Algebraic.MassProduction.Nonuniform.BufferOrder.advance_completed {completed pending total accepted remaining : ℕ} (order : Fin completed ⊕ Fin pending ≃ Fin total) (permutation : Equiv.Perm (Fin pending)) (split : accepted + remaining = pending) (index : Fin completed) : (advance order permutation split) (Sum.inl (Fin.castAdd accepted index)) = order (Sum.inl index)

Previously completed request identities do not change.

theorem Algebraic.MassProduction.Nonuniform.BufferOrder.advance_accepted {completed pending total accepted remaining : ℕ} (order : Fin completed ⊕ Fin pending ≃ Fin total) (permutation : Equiv.Perm (Fin pending)) (split : accepted + remaining = pending) (index : Fin accepted) : (advance order permutation split) (Sum.inl (Fin.natAdd completed index)) = order (Sum.inr (permutation (BufferAdvance.acceptedIndex split index)))

The newly completed identities are exactly the selected permuted prefix.

theorem Algebraic.MassProduction.Nonuniform.BufferOrder.advance_pending {completed pending total accepted remaining : ℕ} (order : Fin completed ⊕ Fin pending ≃ Fin total) (permutation : Equiv.Perm (Fin pending)) (split : accepted + remaining = pending) (index : Fin remaining) : (advance order permutation split) (Sum.inr index) = order (Sum.inr (permutation (BufferAdvance.pendingIndex split index)))

The remaining identities are exactly the selected permuted suffix.