Preserving the scheduler invariant through one halving step

Request identities are updated by an equivalence. Newly accepted recovery lines avoid all previously occupied points and every other accepted line, so the enlarged completed buffer remains a disjoint schedule.

def Algebraic.MassProduction.Nonuniform.BufferModel.State.advance {total completed pending dimension width accepted remaining : ℕ} (state : State total completed pending dimension width) (permutation : Equiv.Perm (Fin pending)) (split : accepted + remaining = pending) (directions : Fin pending → Projectivization (BinaryExtension width) (Fin dimension → BinaryExtension width)) : State total (completed + accepted) remaining dimension width

Move a permuted pending prefix into the completed request partition.

Equations

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

theorem Algebraic.MassProduction.Nonuniform.BufferModel.line_subset_occupied {total completed pending dimension width : ℕ} (state : State total completed pending dimension width) (targets : Fin total → Fin dimension → BinaryExtension width) (index : Fin completed) : line state targets index ⊆ occupied state targets

Each completed line is included in the occupied set.

theorem Algebraic.MassProduction.Nonuniform.BufferModel.advance_line_completed {total completed pending dimension width accepted remaining : ℕ} (state : State total completed pending dimension width) (permutation : Equiv.Perm (Fin pending)) (split : accepted + remaining = pending) (directions : Fin pending → Projectivization (BinaryExtension width) (Fin dimension → BinaryExtension width)) (targets : Fin total → Fin dimension → BinaryExtension width) (index : Fin completed) : line (state.advance permutation split directions) targets (Fin.castAdd accepted index) = line state targets index

Previously completed lines retain their targets and directions.

theorem Algebraic.MassProduction.Nonuniform.BufferModel.advance_line_accepted {total completed pending dimension width accepted remaining : ℕ} (state : State total completed pending dimension width) (permutation : Equiv.Perm (Fin pending)) (split : accepted + remaining = pending) (directions : Fin pending → Projectivization (BinaryExtension width) (Fin dimension → BinaryExtension width)) (targets : Fin total → Fin dimension → BinaryExtension width) (index : Fin accepted) : line (state.advance permutation split directions) targets (Fin.natAdd completed index) = puncturedLine (pendingTargets state targets (permutation (BufferAdvance.acceptedIndex split index))) (directions (permutation (BufferAdvance.acceptedIndex split index)))

Newly completed lines use the selected pending target and candidate direction.

theorem Algebraic.MassProduction.Nonuniform.BufferModel.advance_pendingTargets {total completed pending dimension width accepted remaining : ℕ} (state : State total completed pending dimension width) (permutation : Equiv.Perm (Fin pending)) (split : accepted + remaining = pending) (directions : Fin pending → Projectivization (BinaryExtension width) (Fin dimension → BinaryExtension width)) (targets : Fin total → Fin dimension → BinaryExtension width) (index : Fin remaining) : pendingTargets (state.advance permutation split directions) targets index = pendingTargets state targets (permutation (BufferAdvance.pendingIndex split index))

The pending target tuple is the permuted suffix of the previous tuple.

theorem Algebraic.MassProduction.Nonuniform.BufferModel.advance_completedRecord_old {width total completed pending dimension accepted remaining requestWidth : ℕ} (positive : 0 < width) (state : State total completed pending dimension width) (permutation : Equiv.Perm (Fin pending)) (split : accepted + remaining = pending) (directions : Fin pending → Projectivization (BinaryExtension width) (Fin dimension → BinaryExtension width)) (data : Fin total → Fin requestWidth → Bool) (targets : Fin total → Fin dimension → BinaryExtension width) (index : Fin completed) : completedRecord positive (state.advance permutation split directions) data targets (Fin.castAdd accepted index) = completedRecord positive state data targets index

Old completed records survive advancement bit for bit.

theorem Algebraic.MassProduction.Nonuniform.BufferModel.advance_completedRecord_new {width total completed pending dimension accepted remaining requestWidth : ℕ} (positive : 0 < width) (state : State total completed pending dimension width) (permutation : Equiv.Perm (Fin pending)) (split : accepted + remaining = pending) (directions : Fin pending → Projectivization (BinaryExtension width) (Fin dimension → BinaryExtension width)) (data : Fin total → Fin requestWidth → Bool) (targets : Fin total → Fin dimension → BinaryExtension width) (index : Fin accepted) : completedRecord positive (state.advance permutation split directions) data targets (Fin.natAdd completed index) = Fin.append (pendingRecord state data (permutation (BufferAdvance.acceptedIndex split index))) fun (pointBit : Fin (2 ^ width * (dimension * width))) => have pair := finProdFinEquiv.symm pointBit; binaryExtensionVectorBits positive (PaddedLinePoints.point positive (pendingTargets state targets (permutation (BufferAdvance.acceptedIndex split index))) (directions (permutation (BufferAdvance.acceptedIndex split index))) pair.1) pair.2

New completed records use the accepted original data and generated line.

theorem Algebraic.MassProduction.Nonuniform.BufferModel.advance_pendingRecord {total completed pending dimension width accepted remaining requestWidth : ℕ} (state : State total completed pending dimension width) (permutation : Equiv.Perm (Fin pending)) (split : accepted + remaining = pending) (directions : Fin pending → Projectivization (BinaryExtension width) (Fin dimension → BinaryExtension width)) (data : Fin total → Fin requestWidth → Bool) (index : Fin remaining) : pendingRecord (state.advance permutation split directions) data index = pendingRecord state data (permutation (BufferAdvance.pendingIndex split index))

New pending records are precisely the permuted original-data suffix.

theorem Algebraic.MassProduction.Nonuniform.BufferModel.advance_wellScheduled {total completed pending dimension width accepted remaining : ℕ} (state : State total completed pending dimension width) (permutation : Equiv.Perm (Fin pending)) (split : accepted + remaining = pending) (directions : Fin pending → Projectivization (BinaryExtension width) (Fin dimension → BinaryExtension width)) (targets : Fin total → Fin dimension → BinaryExtension width) (previous : WellScheduled state targets) (clean : ∀ (index : Fin accepted), Clean (fun (request : Fin pending) (direction : Projectivization (BinaryExtension width) (Fin dimension → BinaryExtension width)) => puncturedLine (pendingTargets state targets request) direction) (occupied state targets) directions (permutation (BufferAdvance.acceptedIndex split index))) : WellScheduled (state.advance permutation split directions) targets

Accepting a clean prefix preserves pairwise disjointness of all completed lines.