Embedding a buffer model into a universal phase state

Completed request directions occupy a prefix of the fixed-capacity optional line array. The pending tuple supplies the active targets. The occupied set is exactly the buffer's completed-line union.

theorem Algebraic.MassProduction.Nonuniform.BufferModel.State.completed_add_pending {total completed pending dimension width : ℕ} (state : State total completed pending dimension width) : completed + pending = total

Completed and pending positions partition the original request count.

theorem Algebraic.MassProduction.Nonuniform.BufferModel.State.completed_le {total completed pending dimension width : ℕ} (state : State total completed pending dimension width) : completed ≤ total

Completed positions fit in the original fixed capacity.

theorem Algebraic.MassProduction.Nonuniform.BufferModel.State.pending_le {total completed pending dimension width : ℕ} (state : State total completed pending dimension width) : pending ≤ total

Pending positions fit in the original fixed capacity.

noncomputable def Algebraic.MassProduction.Nonuniform.BufferModel.State.toPhaseState {total completed pending dimension width : ℕ} (state : State total completed pending dimension width) (targets : Fin total → Fin dimension → BinaryExtension width) : PhaseState (Fin dimension → BinaryExtension width) (Projectivization (BinaryExtension width) (Fin dimension → BinaryExtension width)) total pending

Embed completed lines into optional fixed-capacity slots.

Equations

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

theorem Algebraic.MassProduction.Nonuniform.BufferModel.State.toPhaseState_occupied {total completed pending dimension width : ℕ} (state : State total completed pending dimension width) (targets : Fin total → Fin dimension → BinaryExtension width) : phaseOccupied (state.toPhaseState targets) = occupied state targets

The universal phase state has precisely the buffer's occupied points.