Initial and completed scheduler states

The initial buffer has no occupied lines and keeps requests in their original order. A completed buffer determines a permutation of all request identities and, after undoing that permutation, a disjoint recovery line for every original target.

def Algebraic.MassProduction.Nonuniform.BufferModel.State.initial (total dimension width : ℕ) : State total 0 total dimension width

Empty occupied state, with every request pending in its original order.

Equations

• Algebraic.MassProduction.Nonuniform.BufferModel.State.initial total dimension width = { order := Equiv.emptySum (Fin 0) (Fin total), directions := Fin.elim0 }

theorem Algebraic.MassProduction.Nonuniform.BufferModel.State.initial_order {total dimension width : ℕ} (request : Fin total) : (initial total dimension width).order (Sum.inr request) = request

Initial pending positions are original request identities.

theorem Algebraic.MassProduction.Nonuniform.BufferModel.State.initial_wellScheduled {total dimension width : ℕ} (targets : Fin total → Fin dimension → BinaryExtension width) : WellScheduled (initial total dimension width) targets

The empty occupied state satisfies the disjointness invariant.

theorem Algebraic.MassProduction.Nonuniform.BufferModel.initial_input {width total requestWidth dimension : ℕ} (positive : 0 < width) (data : Fin total → Fin requestWidth → Bool) (targets : Fin total → Fin dimension → BinaryExtension width) : input positive (State.initial total dimension width) data targets = BufferInput.encode (fun (request : Fin 0) => request.elim0) data

The initial encoded input is just the original pending records, with an empty completed prefix. It contains no chosen directions.

def Algebraic.MassProduction.Nonuniform.BufferModel.State.finishedOrder {total dimension width : ℕ} (state : State total total 0 dimension width) : Equiv.Perm (Fin total)

Once all requests are completed, the stored order is a permutation.

Equations

• state.finishedOrder = (Equiv.sumEmpty (Fin total) (Fin 0)).symm.trans state.order

theorem Algebraic.MassProduction.Nonuniform.BufferModel.State.finishedOrder_apply {total dimension width : ℕ} (state : State total total 0 dimension width) (request : Fin total) : state.finishedOrder request = state.order (Sum.inl request)

Completed positions map to their original request identities.

def Algebraic.MassProduction.Nonuniform.BufferModel.State.scheduledDirections {total dimension width : ℕ} (state : State total total 0 dimension width) (request : Fin total) : Projectivization (BinaryExtension width) (Fin dimension → BinaryExtension width)

Read the selected direction by original request identity.

Equations

• state.scheduledDirections request = state.directions ((Equiv.symm state.finishedOrder) request)

theorem Algebraic.MassProduction.Nonuniform.BufferModel.State.scheduledDirections_disjoint {total dimension width : ℕ} (state : State total total 0 dimension width) (targets : Fin total → Fin dimension → BinaryExtension width) (valid : WellScheduled state targets) : Pairwise fun (left right : Fin total) => Disjoint (puncturedLine (targets left) (state.scheduledDirections left)) (puncturedLine (targets right) (state.scheduledDirections right))

Completed-buffer disjointness gives disjoint recovery lines in the original request order, including when several targets are equal.