Occupancy decoded from completed buffer records

The shared source array consists of every completed request's stored point slots, with the fixed zero-scalar validity mask. Its represented occupied set is exactly the encoded union of completed punctured lines.

theorem Algebraic.MassProduction.Nonuniform.BufferModel.pointWire_vector_eval {width total completed pending dimension requestWidth : ℕ} (positive : 0 < width) (state : State total completed pending dimension width) (data : Fin total → Fin requestWidth → Bool) (targets : Fin total → Fin dimension → BinaryExtension width) (request : Fin completed) (slot : Fin (2 ^ width)) : (fun (bit : Fin (dimension * width)) => DeMorgan.Wiring.eval (input positive state data targets) (BufferInput.pointWire pending requestWidth (finProdFinEquiv (request, slot)) bit)) = binaryExtensionVectorBits positive (PaddedLinePoints.point positive (targets (state.order (Sum.inl request))) (state.directions request) slot)

Whole point-address vectors have the expected field encoding.

theorem Algebraic.MassProduction.Nonuniform.BufferModel.occupied_input {width total completed pending dimension requestWidth : ℕ} (positive : 0 < width) (state : State total completed pending dimension width) (data : Fin total → Fin requestWidth → Bool) (targets : Fin total → Fin dimension → BinaryExtension width) : MenuPointLayout.occupied (BufferInput.pointWire pending requestWidth) (BufferInput.flagWire (BufferInput.inputWidth completed pending requestWidth (2 ^ width) (dimension * width)) (PaddedLinePoints.valid positive)) (input positive state data targets) = Finset.image (binaryExtensionVectorBits positive) (occupied state targets)

The source array is precisely the completed geometric occupancy.