Resource keys and suffix wires from a completed scheduler buffer

Copy and basis-bit metadata remain in each request's original data; the point address comes from its stored recovery list. These are all fixed wire selections. Disjoint completed lines imply distinct active resource keys.

def Algebraic.MassProduction.Nonuniform.BufferResourceWires.dataWire {total requestWidth : ℕ} (slots addressWidth : ℕ) (request : Fin total) (bit : Fin requestWidth) : DeMorgan.Wiring (BufferInput.inputWidth total 0 requestWidth slots addressWidth)

Select one original request-data bit from a completed record.

Equations

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

theorem Algebraic.MassProduction.Nonuniform.BufferResourceWires.dataWire_eval {width total dimension requestWidth : ℕ} (positive : 0 < width) (state : BufferModel.State total total 0 dimension width) (data : Fin total → Fin requestWidth → Bool) (targets : Fin total → Fin dimension → BinaryExtension width) (request : Fin total) (bit : Fin requestWidth) : DeMorgan.Wiring.eval (BufferModel.input positive state data targets) (dataWire (2 ^ width) (dimension * width) request bit) = data (state.order (Sum.inl request)) bit

The selected bit still belongs to the same original request identity.

def Algebraic.MassProduction.Nonuniform.BufferResourceWires.payload {payloadWidth requestWidth total : ℕ} (width dimension : ℕ) (projection : Fin payloadWidth → Fin requestWidth) (incidence : Fin (total * 2 ^ width)) (bit : Fin payloadWidth) : DeMorgan.Wiring (BufferInput.inputWidth total 0 requestWidth (2 ^ width) (dimension * width))

Repeat the stored request's selected payload bits at each scalar slot.

Equations

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

theorem Algebraic.MassProduction.Nonuniform.BufferResourceWires.payload_eval {width total dimension requestWidth payloadWidth : ℕ} (positive : 0 < width) (state : BufferModel.State total total 0 dimension width) (data : Fin total → Fin requestWidth → Bool) (targets : Fin total → Fin dimension → BinaryExtension width) (projection : Fin payloadWidth → Fin requestWidth) (request : Fin total) (slot : Fin (2 ^ width)) (bit : Fin payloadWidth) : DeMorgan.Wiring.eval (BufferModel.input positive state data targets) (payload width dimension projection (finProdFinEquiv (request, slot)) bit) = data (state.order (Sum.inl request)) (projection bit)

Repeated payload wires read the original data at the completed request's identity.

def Algebraic.MassProduction.Nonuniform.BufferResourceWires.keys {copyBits requestWidth selectorBits total : ℕ} (width dimension : ℕ) (copyProjection : Fin copyBits → Fin requestWidth) (selectorProjection : Fin selectorBits → Fin requestWidth) (incidence : Fin (total * 2 ^ width)) : Fin (HighRate.ResourceLayout.keyWidth copyBits dimension width selectorBits) → DeMorgan.Wiring (BufferInput.inputWidth total 0 requestWidth (2 ^ width) (dimension * width))

Resource key: preserved copy metadata, stored point, preserved basis-bit metadata.

Equations

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

theorem Algebraic.MassProduction.Nonuniform.BufferResourceWires.keys_point_eval {width total dimension requestWidth copyBits selectorBits : ℕ} (positive : 0 < width) (state : BufferModel.State total total 0 dimension width) (data : Fin total → Fin requestWidth → Bool) (targets : Fin total → Fin dimension → BinaryExtension width) (copyProjection : Fin copyBits → Fin requestWidth) (selectorProjection : Fin selectorBits → Fin requestWidth) (incidence : Fin (total * 2 ^ width)) (bit : Fin (dimension * width)) : DeMorgan.Wiring.eval (BufferModel.input positive state data targets) (keys width dimension copyProjection selectorProjection incidence (Fin.natAdd copyBits (Fin.castAdd selectorBits bit))) = binaryExtensionVectorBits positive (BufferModel.incidencePoint positive state targets incidence) bit

Reading a resource key's point field gives exactly its stored point.

theorem Algebraic.MassProduction.Nonuniform.BufferResourceWires.keys_eval {width total dimension requestWidth copyBits selectorBits copies : ℕ} (positive : 0 < width) (state : BufferModel.State total total 0 dimension width) (data : Fin total → Fin requestWidth → Bool) (targets : Fin total → Fin dimension → BinaryExtension width) (copyProjection : Fin copyBits → Fin requestWidth) (selectorProjection : Fin selectorBits → Fin requestWidth) (copiesAt : Fin total → Fin copies) (selectorsAt : Fin total → Fin width) (copyCorrect : ∀ (request : Fin total) (bit : Fin copyBits), data request (copyProjection bit) = finiteIndexBits copyBits (copiesAt request) bit) (selectorCorrect : ∀ (request : Fin total) (bit : Fin selectorBits), data request (selectorProjection bit) = finiteIndexBits selectorBits (selectorsAt request) bit) (request : Fin total) (slot : Fin (2 ^ width)) : (fun (bit : Fin (HighRate.ResourceLayout.keyWidth copyBits dimension width selectorBits)) => DeMorgan.Wiring.eval (BufferModel.input positive state data targets) (keys width dimension copyProjection selectorProjection (finProdFinEquiv (request, slot)) bit)) = HighRate.ResourceLayout.key copyBits selectorBits (HighRate.ResourceLayout.position positive (copiesAt (state.order (Sum.inl request))) (PaddedLinePoints.point positive (targets (state.order (Sum.inl request))) (state.directions request) slot) (selectorsAt (state.order (Sum.inl request))))

Every completed incidence key matches the exact resource-bank position described by the preserved request metadata and stored geometric point.

theorem Algebraic.MassProduction.Nonuniform.BufferResourceWires.activeKeys_injective {width total dimension requestWidth copyBits selectorBits : ℕ} (positive : 0 < width) (state : BufferModel.State total total 0 dimension width) (data : Fin total → Fin requestWidth → Bool) (targets : Fin total → Fin dimension → BinaryExtension width) (scheduled : BufferModel.WellScheduled state targets) (copyProjection : Fin copyBits → Fin requestWidth) (selectorProjection : Fin selectorBits → Fin requestWidth) (left right : Fin (total * 2 ^ width)) (leftActive : BufferModel.incidenceValid positive left = true) (rightActive : BufferModel.incidenceValid positive right = true) (sameKey : (fun (bit : Fin (HighRate.ResourceLayout.keyWidth copyBits dimension width selectorBits)) => DeMorgan.Wiring.eval (BufferModel.input positive state data targets) (keys width dimension copyProjection selectorProjection left bit)) = fun (bit : Fin (HighRate.ResourceLayout.keyWidth copyBits dimension width selectorBits)) => DeMorgan.Wiring.eval (BufferModel.input positive state data targets) (keys width dimension copyProjection selectorProjection right bit)) : left = right

Completed-buffer disjointness discharges the scatter uniqueness premise.