Distinct active incidences in a completed buffer

The completed-buffer invariant gives the exact injectivity premise needed by shared resource scatter. This includes repeated original targets and the fixed invalid zero slot of every line.

noncomputable def Algebraic.MassProduction.Nonuniform.BufferModel.incidencePoint {width total completed pending dimension : ℕ} (positive : 0 < width) (state : State total completed pending dimension width) (targets : Fin total → Fin dimension → BinaryExtension width) (incidence : Fin (completed * 2 ^ width)) : Fin dimension → BinaryExtension width

The field point at one flattened completed request/scalar position.

Equations

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

noncomputable def Algebraic.MassProduction.Nonuniform.BufferModel.incidenceValid {width completed : ℕ} (positive : 0 < width) (incidence : Fin (completed * 2 ^ width)) : Bool

Fixed validity of one flattened scalar slot.

Equations

• Algebraic.MassProduction.Nonuniform.BufferModel.incidenceValid positive incidence = Algebraic.MassProduction.Nonuniform.PaddedLinePoints.valid positive (finProdFinEquiv.symm incidence).2

theorem Algebraic.MassProduction.Nonuniform.BufferModel.incidencePoint_injective {width total completed pending dimension : ℕ} (positive : 0 < width) (state : State total completed pending dimension width) (targets : Fin total → Fin dimension → BinaryExtension width) (scheduled : WellScheduled state targets) (left right : Fin (completed * 2 ^ width)) (leftActive : incidenceValid positive left = true) (rightActive : incidenceValid positive right = true) (samePoint : incidencePoint positive state targets left = incidencePoint positive state targets right) : left = right

Disjoint completed lines make all active incidence points distinct.