Complete finite mass-production circuit

This module hardwires packed target points into the grouped scheduler, keeps request suffixes as the only runtime inputs, and composes that front end with the complete scatter-evaluate-gather-decode pipeline. It proves end-to-end recovery and the exact top-level gate-cost ledger.

Hardwired grouped scheduling

noncomputable def Algebraic.MassProduction.RoutingAssembly.fixedGroupedTargetAssemblyCircuit {width groups requestsPerGroup dimension : ℕ} (totalRequests suffixWidth : ℕ) (widthPositive : 0 < width) (targets : Fin groups → Fin requestsPerGroup → Fin dimension → BinaryExtension width) : Circuit DeMorgan.signature (totalRequests * suffixWidth) (groups * (requestsPerGroup * SchedulerIteration.pointBitWidth dimension width))

Assemble a fixed rectangular target family for the grouped scheduler. The suffix inputs are deliberately ignored by this zero-cost layer.

Equations

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

@[simp]

theorem Algebraic.MassProduction.RoutingAssembly.fixedGroupedTargetAssemblyCircuit_size {width groups requestsPerGroup dimension : ℕ} (totalRequests suffixWidth : ℕ) (widthPositive : 0 < width) (targets : Fin groups → Fin requestsPerGroup → Fin dimension → BinaryExtension width) : (fixedGroupedTargetAssemblyCircuit totalRequests suffixWidth widthPositive targets).size = groups * (requestsPerGroup * SchedulerIteration.pointBitWidth dimension width)

Every output bit is a hardwired constant: exactly one constant gate per output bit and no other gates.

@[simp]

theorem Algebraic.MassProduction.RoutingAssembly.fixedGroupedTargetAssemblyCircuit_cost {width groups requestsPerGroup dimension totalRequests : ℕ} (suffixWidth : ℕ) (widthPositive : 0 < width) (targets : Fin groups → Fin requestsPerGroup → Fin dimension → BinaryExtension width) : (fixedGroupedTargetAssemblyCircuit totalRequests suffixWidth widthPositive targets).cost DeMorgan.standardCost = 0

theorem Algebraic.MassProduction.RoutingAssembly.fixedGroupedTargetAssemblyCircuit_eval {width groups requestsPerGroup dimension totalRequests : ℕ} (suffixWidth : ℕ) (widthPositive : 0 < width) (targets : Fin groups → Fin requestsPerGroup → Fin dimension → BinaryExtension width) (input : Fin (totalRequests * suffixWidth) → Bool) : (fixedGroupedTargetAssemblyCircuit totalRequests suffixWidth widthPositive targets).eval DeMorgan.interpretation input = GroupedScheduler.groupedTargetArrayBits widthPositive targets

noncomputable def Algebraic.MassProduction.RoutingAssembly.fixedScheduleAndSuffixCircuit {Prefix : Type u} {width groups totalRequests dimension : ℕ} (widthPositive : 0 < width) (groupsPositive : 0 < groups) (schedulerDepth suffixWidth : ℕ) (allFit : GroupedScheduler.requestGroupSize totalRequests groups * LineEnumeration.nonzeroScalarCount width ≤ Sorting.networkRecords schedulerDepth) (placement : Prefix ↪ PackedBitPosition dimension width) (requestSource : Fin totalRequests → Prefix) (dummyTarget : Fin dimension → BinaryExtension width) : Circuit DeMorgan.signature (totalRequests * suffixWidth) (groups * (GroupedScheduler.requestGroupSize totalRequests groups * SchedulerIteration.lineBitWidth dimension width) + totalRequests * suffixWidth)

Run the grouped greedy scheduler on hardwired packed target points while passing every runtime suffix bit through unchanged.

Equations

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

@[simp]

theorem Algebraic.MassProduction.RoutingAssembly.fixedScheduleAndSuffixCircuit_size {Prefix : Type u} {width groups totalRequests dimension : ℕ} (widthPositive : 0 < width) (groupsPositive : 0 < groups) (schedulerDepth suffixWidth : ℕ) (allFit : GroupedScheduler.requestGroupSize totalRequests groups * LineEnumeration.nonzeroScalarCount width ≤ Sorting.networkRecords schedulerDepth) (placement : Prefix ↪ PackedBitPosition dimension width) (requestSource : Fin totalRequests → Prefix) (dummyTarget : Fin dimension → BinaryExtension width) : (fixedScheduleAndSuffixCircuit widthPositive groupsPositive schedulerDepth suffixWidth allFit placement requestSource dummyTarget).size = (fixedGroupedTargetAssemblyCircuit totalRequests suffixWidth widthPositive (GroupedScheduler.paddedGroupedTargets ⋯ (fun (request : Fin totalRequests) => packedTargetPoint widthPositive placement (requestSource request)) dummyTarget)).size + groups * SchedulerIteration.greedyScheduleGateCount dimension widthPositive schedulerDepth (GroupedScheduler.requestGroupSize totalRequests groups)

The exact gate count of fixedScheduleAndSuffixCircuit.

theorem Algebraic.MassProduction.RoutingAssembly.fixedScheduleAndSuffixCircuit_eval {Prefix : Type u} {width groups totalRequests dimension : ℕ} (widthPositive : 0 < width) (groupsPositive : 0 < groups) (schedulerDepth suffixWidth : ℕ) (allFit : GroupedScheduler.requestGroupSize totalRequests groups * LineEnumeration.nonzeroScalarCount width ≤ Sorting.networkRecords schedulerDepth) (placement : Prefix ↪ PackedBitPosition dimension width) (requestSource : Fin totalRequests → Prefix) (dummyTarget : Fin dimension → BinaryExtension width) (input : Fin (totalRequests * suffixWidth) → Bool) : (fixedScheduleAndSuffixCircuit widthPositive groupsPositive schedulerDepth suffixWidth allFit placement requestSource dummyTarget).eval DeMorgan.interpretation input = let groupSize := GroupedScheduler.requestGroupSize totalRequests groups; have capacity := ⋯; have targets := fun (request : Fin totalRequests) => packedTargetPoint widthPositive placement (requestSource request); have paddedTargets := GroupedScheduler.paddedGroupedTargets capacity targets dummyTarget; Fin.append (GroupedScheduler.groupedScheduleOutput dimension widthPositive schedulerDepth groups groupSize allFit paddedTargets) input

@[simp]

theorem Algebraic.MassProduction.RoutingAssembly.fixedScheduleAndSuffixCircuit_cost {Prefix : Type u} {width groups totalRequests dimension : ℕ} (widthPositive : 0 < width) (groupsPositive : 0 < groups) (schedulerDepth suffixWidth : ℕ) (allFit : GroupedScheduler.requestGroupSize totalRequests groups * LineEnumeration.nonzeroScalarCount width ≤ Sorting.networkRecords schedulerDepth) (placement : Prefix ↪ PackedBitPosition dimension width) (requestSource : Fin totalRequests → Prefix) (dummyTarget : Fin dimension → BinaryExtension width) : (fixedScheduleAndSuffixCircuit widthPositive groupsPositive schedulerDepth suffixWidth allFit placement requestSource dummyTarget).cost DeMorgan.standardCost = (GroupedScheduler.groupedScheduleCircuit dimension widthPositive schedulerDepth groups (GroupedScheduler.requestGroupSize totalRequests groups) allFit).cost DeMorgan.standardCost

noncomputable def Algebraic.MassProduction.RoutingAssembly.finiteMassProductionCircuit {Prefix : Type u} {width groups totalRequests dimension scatterPaddingCount scatterDepth gatherPaddingCount gatherDepth : ℕ} (widthPositive : 0 < width) (groupsPositive : 0 < groups) (schedulerDepth suffixWidth groupBitWidth orderWidth : ℕ) (allFit : GroupedScheduler.requestGroupSize totalRequests groups * LineEnumeration.nonzeroScalarCount width ≤ Sorting.networkRecords schedulerDepth) (incidenceFits : totalRequests * LineEnumeration.nonzeroScalarCount width ≤ 2 ^ orderWidth) (placement : Prefix ↪ PackedBitPosition dimension width) (requestSource : Fin totalRequests → Prefix) (dummyTarget : Fin dimension → BinaryExtension width) (scatterRecordCount : totalRequests * LineEnumeration.nonzeroScalarCount width + 2 ^ (groupBitWidth + dimension * width) + scatterPaddingCount = Sorting.networkRecords scatterDepth) (resourceCircuits : Fin (ResourceEvaluation.resourceBitCount dimension width) → Circuit DeMorgan.signature (groups * suffixWidth) groups) (gatherRecordCount : 2 ^ (groupBitWidth + dimension * width) + totalRequests * LineEnumeration.nonzeroScalarCount width + gatherPaddingCount = Sorting.networkRecords gatherDepth) : Circuit DeMorgan.signature (totalRequests * suffixWidth) totalRequests

The complete finite mass-production circuit. Its only runtime inputs are the row-major suffixes; selected function prefixes, packed target points, and the dummy padding target are nonuniform construction data.

Equations

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

@[simp]

theorem Algebraic.MassProduction.RoutingAssembly.finiteMassProductionCircuit_size {Prefix : Type u} {width groups totalRequests dimension scatterPaddingCount scatterDepth gatherPaddingCount gatherDepth : ℕ} (widthPositive : 0 < width) (groupsPositive : 0 < groups) (schedulerDepth suffixWidth groupBitWidth orderWidth : ℕ) (allFit : GroupedScheduler.requestGroupSize totalRequests groups * LineEnumeration.nonzeroScalarCount width ≤ Sorting.networkRecords schedulerDepth) (incidenceFits : totalRequests * LineEnumeration.nonzeroScalarCount width ≤ 2 ^ orderWidth) (placement : Prefix ↪ PackedBitPosition dimension width) (requestSource : Fin totalRequests → Prefix) (dummyTarget : Fin dimension → BinaryExtension width) (scatterRecordCount : totalRequests * LineEnumeration.nonzeroScalarCount width + 2 ^ (groupBitWidth + dimension * width) + scatterPaddingCount = Sorting.networkRecords scatterDepth) (resourceCircuits : Fin (ResourceEvaluation.resourceBitCount dimension width) → Circuit DeMorgan.signature (groups * suffixWidth) groups) (gatherRecordCount : 2 ^ (groupBitWidth + dimension * width) + totalRequests * LineEnumeration.nonzeroScalarCount width + gatherPaddingCount = Sorting.networkRecords gatherDepth) : (finiteMassProductionCircuit widthPositive groupsPositive schedulerDepth suffixWidth groupBitWidth orderWidth allFit incidenceFits placement requestSource dummyTarget scatterRecordCount resourceCircuits gatherRecordCount).size = (fixedScheduleAndSuffixCircuit widthPositive groupsPositive schedulerDepth suffixWidth allFit placement requestSource dummyTarget).size + (assembledPipelineCircuit groupsPositive suffixWidth groupBitWidth orderWidth incidenceFits ⋯ placement requestSource scatterRecordCount resourceCircuits gatherRecordCount).size

The exact gate count of finiteMassProductionCircuit.

theorem Algebraic.MassProduction.RoutingAssembly.finiteMassProductionCircuit_eval {Prefix : Type u} {width groups totalRequests dimension scatterPaddingCount scatterDepth gatherPaddingCount gatherDepth : ℕ} (widthPositive : 0 < width) (groupsPositive : 0 < groups) (schedulerDepth suffixWidth groupBitWidth orderWidth : ℕ) (allFit : GroupedScheduler.requestGroupSize totalRequests groups * LineEnumeration.nonzeroScalarCount width ≤ Sorting.networkRecords schedulerDepth) (incidenceFits : totalRequests * LineEnumeration.nonzeroScalarCount width ≤ 2 ^ orderWidth) (placement : Prefix ↪ PackedBitPosition dimension width) (requestSource : Fin totalRequests → Prefix) (dummyTarget : Fin dimension → BinaryExtension width) (scatterRecordCount : totalRequests * LineEnumeration.nonzeroScalarCount width + 2 ^ (groupBitWidth + dimension * width) + scatterPaddingCount = Sorting.networkRecords scatterDepth) (resourceCircuits : Fin (ResourceEvaluation.resourceBitCount dimension width) → Circuit DeMorgan.signature (groups * suffixWidth) groups) (gatherRecordCount : 2 ^ (groupBitWidth + dimension * width) + totalRequests * LineEnumeration.nonzeroScalarCount width + gatherPaddingCount = Sorting.networkRecords gatherDepth) (input : Fin (totalRequests * suffixWidth) → Bool) : (finiteMassProductionCircuit widthPositive groupsPositive schedulerDepth suffixWidth groupBitWidth orderWidth allFit incidenceFits placement requestSource dummyTarget scatterRecordCount resourceCircuits gatherRecordCount).eval DeMorgan.interpretation input = let groupSize := GroupedScheduler.requestGroupSize totalRequests groups; have capacity := ⋯; have targets := fun (request : Fin totalRequests) => packedTargetPoint widthPositive placement (requestSource request); have paddedTargets := GroupedScheduler.paddedGroupedTargets capacity targets dummyTarget; have schedule := GroupedScheduler.groupedScheduleOutput dimension widthPositive schedulerDepth groups groupSize allFit paddedTargets; (assembledPipelineCircuit groupsPositive suffixWidth groupBitWidth orderWidth incidenceFits capacity placement requestSource scatterRecordCount resourceCircuits gatherRecordCount).eval DeMorgan.interpretation (Fin.append schedule input)

theorem Algebraic.MassProduction.RoutingAssembly.finiteMassProductionCircuit_recovers {Prefix : Type u} {width dimension groups totalRequests scatterPaddingCount scatterDepth gatherPaddingCount gatherDepth : ℕ} (widthPositive : 0 < width) (widthAtLeastTwo : 2 ≤ width) (dimensionPositive : 0 < dimension) (groupsPositive : 0 < groups) (schedulerDepth suffixWidth groupBitWidth orderWidth : ℕ) (groupFits : groups ≤ 2 ^ groupBitWidth) (allFit : GroupedScheduler.requestGroupSize totalRequests groups * LineEnumeration.nonzeroScalarCount width ≤ Sorting.networkRecords schedulerDepth) (directionCapacity : GroupedScheduler.requestGroupSize totalRequests groups * LineEnumeration.nonzeroScalarCount width < Nat.card (Projectivization (BinaryExtension width) (Fin dimension → BinaryExtension width))) (incidenceFits : totalRequests * LineEnumeration.nonzeroScalarCount width ≤ 2 ^ orderWidth) (placement : Prefix ↪ PackedBitPosition dimension width) (function : Prefix → (Fin suffixWidth → Bool) → Bool) (requestSource : Fin totalRequests → Prefix) (dummyTarget : Fin dimension → BinaryExtension width) (scatterRecordCount : totalRequests * LineEnumeration.nonzeroScalarCount width + 2 ^ (groupBitWidth + dimension * width) + scatterPaddingCount = Sorting.networkRecords scatterDepth) (resourceCircuits : Fin (ResourceEvaluation.resourceBitCount dimension width) → Circuit DeMorgan.signature (groups * suffixWidth) groups) (computes : ∀ (point : Fin (ResourceEvaluation.pointCount dimension width)) (bit : Fin width), (resourceCircuits (ResourceEvaluation.resourceMemberIndex point bit)).ComputesWith DeMorgan.interpretation (directProduct (ResourceEvaluation.packedResourceFunction widthPositive placement function point bit) groups)) (gatherRecordCount : 2 ^ (groupBitWidth + dimension * width) + totalRequests * LineEnumeration.nonzeroScalarCount width + gatherPaddingCount = Sorting.networkRecords gatherDepth) (input : Fin (totalRequests * suffixWidth) → Bool) : (finiteMassProductionCircuit widthPositive groupsPositive schedulerDepth suffixWidth groupBitWidth orderWidth allFit incidenceFits placement requestSource dummyTarget scatterRecordCount resourceCircuits gatherRecordCount).eval DeMorgan.interpretation input = fun (request : Fin totalRequests) => function (requestSource request) fun (bit : Fin suffixWidth) => input (finProdFinEquiv (request, bit))

The fully assembled circuit, including the verified deterministic grouped scheduler, computes the requested functions on all row-major suffix inputs.

@[simp]

theorem Algebraic.MassProduction.RoutingAssembly.finiteMassProductionCircuit_cost {Prefix : Type u} {width groups totalRequests dimension scatterPaddingCount scatterDepth gatherPaddingCount gatherDepth : ℕ} (widthPositive : 0 < width) (groupsPositive : 0 < groups) (schedulerDepth suffixWidth groupBitWidth orderWidth : ℕ) (allFit : GroupedScheduler.requestGroupSize totalRequests groups * LineEnumeration.nonzeroScalarCount width ≤ Sorting.networkRecords schedulerDepth) (incidenceFits : totalRequests * LineEnumeration.nonzeroScalarCount width ≤ 2 ^ orderWidth) (placement : Prefix ↪ PackedBitPosition dimension width) (requestSource : Fin totalRequests → Prefix) (dummyTarget : Fin dimension → BinaryExtension width) (scatterRecordCount : totalRequests * LineEnumeration.nonzeroScalarCount width + 2 ^ (groupBitWidth + dimension * width) + scatterPaddingCount = Sorting.networkRecords scatterDepth) (resourceCircuits : Fin (ResourceEvaluation.resourceBitCount dimension width) → Circuit DeMorgan.signature (groups * suffixWidth) groups) (gatherRecordCount : 2 ^ (groupBitWidth + dimension * width) + totalRequests * LineEnumeration.nonzeroScalarCount width + gatherPaddingCount = Sorting.networkRecords gatherDepth) : (finiteMassProductionCircuit widthPositive groupsPositive schedulerDepth suffixWidth groupBitWidth orderWidth allFit incidenceFits placement requestSource dummyTarget scatterRecordCount resourceCircuits gatherRecordCount).cost DeMorgan.standardCost = (GroupedScheduler.groupedScheduleCircuit dimension widthPositive schedulerDepth groups (GroupedScheduler.requestGroupSize totalRequests groups) allFit).cost DeMorgan.standardCost + ((CanonicalRouting.matchedCanonicalRoutingCircuit scatterDepth (IncidenceRouting.incidenceKeyWidth groupBitWidth dimension width) suffixWidth).cost DeMorgan.standardCost + ∑ member : Fin (ResourceEvaluation.resourceBitCount dimension width), (resourceCircuits member).cost DeMorgan.standardCost + (CanonicalMetadataRouting.matchedCanonicalRoutingCircuit gatherDepth (IncidenceRouting.incidenceKeyWidth groupBitWidth dimension width) (orderWidth + 1) width).cost DeMorgan.standardCost + totalRequests * (LineEnumeration.nonzeroScalarCount width * 4))

Exact top-level finite cost ledger: scheduler, scatter routing, shorter resource bank, gather routing, and decoder.