One complete constructive greedy-scheduler stage

This module builds the fixed-wire preprocessing omitted by the rank-list-level selector. A stage input contains a power-of-two array of previously occupied points followed by the current target. An explicit coordinatewise GF(2^width) addition circuit forms point - target (the same as point + target in characteristic two), and the verified guarded-rank, sort, least-missing, and unrank pipeline selects a disjoint recovery-line direction.

Coordinatewise packed vector addition

def Algebraic.MassProduction.SchedulerStage.vectorCoordinatePairIndex (dimension width : ℕ) (coordinate : Fin dimension) (input : Fin (2 * width)) : Fin (2 * (dimension * width))

Reorder one coordinate pair into the pair-of-whole-vectors layout.

Equations

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

def Algebraic.MassProduction.SchedulerStage.binaryExtensionVectorAddBits (dimension width : ℕ) (input : Fin (2 * (dimension * width)) → Bool) : Fin (dimension * width) → Bool

Pure semantics of coordinatewise packed field addition.

Equations

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

@[reducible]

def Algebraic.MassProduction.SchedulerStage.vectorAdditionCoordinateGateCount (width : ℕ) : ℕ

Exact gate count of one vector-addition coordinate circuit.

Equations

• Algebraic.MassProduction.SchedulerStage.vectorAdditionCoordinateGateCount width = ∑ output : Fin width, Algebraic.MassProduction.additionCoordinateGateCount output

def Algebraic.MassProduction.SchedulerStage.binaryExtensionVectorAddCircuit (dimension width : ℕ) : Circuit DeMorgan.signature (2 * (dimension * width)) (dimension * width)

Add two packed extension-field vectors coordinatewise.

Equations

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

@[simp]

theorem Algebraic.MassProduction.SchedulerStage.binaryExtensionVectorAddCircuit_size (dimension width : ℕ) : (binaryExtensionVectorAddCircuit dimension width).size = ∑ _coordinate : Fin dimension, vectorAdditionCoordinateGateCount width

@[simp]

theorem Algebraic.MassProduction.SchedulerStage.binaryExtensionVectorAddCircuit_eval {dimension width : ℕ} (input : Fin (2 * (dimension * width)) → Bool) : (binaryExtensionVectorAddCircuit dimension width).eval DeMorgan.interpretation input = binaryExtensionVectorAddBits dimension width input

@[simp]

theorem Algebraic.MassProduction.SchedulerStage.binaryExtensionVectorAddCircuit_cost {dimension width : ℕ} : (binaryExtensionVectorAddCircuit dimension width).cost DeMorgan.standardCost = dimension * (4 * width)

def Algebraic.MassProduction.SchedulerStage.binaryExtensionVectorPairBits {dimension width : ℕ} (left right : Fin (dimension * width) → Bool) : Fin (2 * (dimension * width)) → Bool

A pair of whole packed vectors, with the left vector first.

Equations

• Algebraic.MassProduction.SchedulerStage.binaryExtensionVectorPairBits left right = Algebraic.MassProduction.binaryExtensionPairBits left right

theorem Algebraic.MassProduction.SchedulerStage.vectorCoordinatePair_of_vectorPairBits {dimension width : ℕ} (left right : Fin (dimension * width) → Bool) (coordinate : Fin dimension) : binaryExtensionVectorPairBits left right ∘ vectorCoordinatePairIndex dimension width coordinate = binaryExtensionPairBits (fun (bit : Fin width) => left (finProdFinEquiv (coordinate, bit))) fun (bit : Fin width) => right (finProdFinEquiv (coordinate, bit))

theorem Algebraic.MassProduction.SchedulerStage.binaryExtensionVectorAddCircuit_eval_vectorBits {width dimension : ℕ} (widthPositive : 0 < width) (left right : Fin dimension → BinaryExtension width) : (binaryExtensionVectorAddCircuit dimension width).eval DeMorgan.interpretation (binaryExtensionVectorPairBits (binaryExtensionVectorBits widthPositive left) (binaryExtensionVectorBits widthPositive right)) = binaryExtensionVectorBits widthPositive (left + right)

Packed vector addition agrees exactly with field-vector addition.

Fixed input layout for the occupied points and target

def Algebraic.MassProduction.SchedulerStage.stagePointInputIndex (depth vectorWidth : ℕ) (record : Fin (Sorting.networkRecords depth)) (bit : Fin vectorWidth) : Fin ((Sorting.networkRecords depth + 1) * vectorWidth)

One bit of the point block in a (points..., target) stage input.

Equations

• Algebraic.MassProduction.SchedulerStage.stagePointInputIndex depth vectorWidth record bit = Algebraic.MassProduction.blockPrefixIndex (finProdFinEquiv (record, bit))

def Algebraic.MassProduction.SchedulerStage.stageTargetInputIndex (depth vectorWidth : ℕ) (bit : Fin vectorWidth) : Fin ((Sorting.networkRecords depth + 1) * vectorWidth)

One bit of the final target block in a (points..., target) stage input.

Equations

• Algebraic.MassProduction.SchedulerStage.stageTargetInputIndex depth vectorWidth bit = Algebraic.MassProduction.blockSuffixIndex bit

def Algebraic.MassProduction.SchedulerStage.stageDifferenceInputIndex (depth vectorWidth : ℕ) (record : Fin (Sorting.networkRecords depth)) (input : Fin (2 * vectorWidth)) : Fin ((Sorting.networkRecords depth + 1) * vectorWidth)

Inputs for one vector subtraction/addition inside the global stage layout.

Equations

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

def Algebraic.MassProduction.SchedulerStage.pointTargetDifferenceArrayRawCircuit (dimension width depth : ℕ) : Circuit DeMorgan.signature ((Sorting.networkRecords depth + 1) * (dimension * width)) (Sorting.networkRecords depth * (dimension * width))

Raw parallel circuit before spelling its output count as networkBits.

Equations

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

@[simp]

theorem Algebraic.MassProduction.SchedulerStage.pointTargetDifferenceArrayRawCircuit_size (dimension width depth : ℕ) : (pointTargetDifferenceArrayRawCircuit dimension width depth).size = ∑ _record : Fin (Sorting.networkRecords depth), ∑ _coordinate : Fin dimension, vectorAdditionCoordinateGateCount width

def Algebraic.MassProduction.SchedulerStage.pointTargetDifferenceArrayCircuit (dimension width depth : ℕ) : Circuit DeMorgan.signature ((Sorting.networkRecords depth + 1) * (dimension * width)) (Sorting.networkRecords depth * (dimension * width))

Compute all point-minus-target vectors in parallel.

Equations

• Algebraic.MassProduction.SchedulerStage.pointTargetDifferenceArrayCircuit dimension width depth = Algebraic.MassProduction.SchedulerStage.pointTargetDifferenceArrayRawCircuit dimension width depth

@[simp]

theorem Algebraic.MassProduction.SchedulerStage.pointTargetDifferenceArrayCircuit_size (dimension width depth : ℕ) : (pointTargetDifferenceArrayCircuit dimension width depth).size = ∑ _record : Fin (Sorting.networkRecords depth), ∑ _coordinate : Fin dimension, vectorAdditionCoordinateGateCount width

@[simp]

theorem Algebraic.MassProduction.SchedulerStage.pointTargetDifferenceArrayRawCircuit_eval_apply {depth dimension width : ℕ} (input : Fin ((Sorting.networkRecords depth + 1) * (dimension * width)) → Bool) (record : Fin (Sorting.networkRecords depth)) (bit : Fin (dimension * width)) : (pointTargetDifferenceArrayRawCircuit dimension width depth).eval DeMorgan.interpretation input (finProdFinEquiv (record, bit)) = (binaryExtensionVectorAddCircuit dimension width).eval DeMorgan.interpretation (input ∘ stageDifferenceInputIndex depth (dimension * width) record) bit

theorem Algebraic.MassProduction.SchedulerStage.pointTargetDifferenceArrayCircuit_eval_apply {depth dimension width : ℕ} (input : Fin ((Sorting.networkRecords depth + 1) * (dimension * width)) → Bool) (record : Fin (Sorting.networkRecords depth)) (bit : Fin (dimension * width)) : (pointTargetDifferenceArrayCircuit dimension width depth).eval DeMorgan.interpretation input (finProdFinEquiv (record, bit)) = (binaryExtensionVectorAddCircuit dimension width).eval DeMorgan.interpretation (input ∘ stageDifferenceInputIndex depth (dimension * width) record) bit

Reading one generated difference block evaluates the corresponding vector-addition circuit on that point and the shared target.

@[simp]

theorem Algebraic.MassProduction.SchedulerStage.pointTargetDifferenceArrayCircuit_cost {dimension width depth : ℕ} : (pointTargetDifferenceArrayCircuit dimension width depth).cost DeMorgan.standardCost = Sorting.networkRecords depth * (dimension * (4 * width))

theorem Algebraic.MassProduction.SchedulerStage.stageDifferenceInput_eq_pair {depth vectorWidth : ℕ} (input : Fin ((Sorting.networkRecords depth + 1) * vectorWidth) → Bool) (point target : Fin vectorWidth → Bool) (record : Fin (Sorting.networkRecords depth)) (pointBits : ∀ (bit : Fin vectorWidth), input (stagePointInputIndex depth vectorWidth record bit) = point bit) (targetBits : ∀ (bit : Fin vectorWidth), input (stageTargetInputIndex depth vectorWidth bit) = target bit) : input ∘ stageDifferenceInputIndex depth vectorWidth record = binaryExtensionPairBits point target

noncomputable def Algebraic.MassProduction.SchedulerStage.packedPointArrayBits {width depth dimension : ℕ} (widthPositive : 0 < width) (points : Fin (Sorting.networkRecords depth) → Fin dimension → BinaryExtension width) : Fin (Sorting.networkRecords depth * (dimension * width)) → Bool

Row-major packed bits of the occupied-point array.

Equations

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

noncomputable def Algebraic.MassProduction.SchedulerStage.schedulerStageInputBits {width depth dimension : ℕ} (widthPositive : 0 < width) (points : Fin (Sorting.networkRecords depth) → Fin dimension → BinaryExtension width) (target : Fin dimension → BinaryExtension width) : Fin ((Sorting.networkRecords depth + 1) * (dimension * width)) → Bool

Canonical (points..., target) input expected by a scheduler stage.

Equations

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

@[simp]

theorem Algebraic.MassProduction.SchedulerStage.schedulerStageInputBits_point {width depth dimension : ℕ} (widthPositive : 0 < width) (points : Fin (Sorting.networkRecords depth) → Fin dimension → BinaryExtension width) (target : Fin dimension → BinaryExtension width) (record : Fin (Sorting.networkRecords depth)) (bit : Fin (dimension * width)) : schedulerStageInputBits widthPositive points target (stagePointInputIndex depth (dimension * width) record bit) = binaryExtensionVectorBits widthPositive (points record) bit

@[simp]

theorem Algebraic.MassProduction.SchedulerStage.schedulerStageInputBits_target {width depth dimension : ℕ} (widthPositive : 0 < width) (points : Fin (Sorting.networkRecords depth) → Fin dimension → BinaryExtension width) (target : Fin dimension → BinaryExtension width) (bit : Fin (dimension * width)) : schedulerStageInputBits widthPositive points target (stageTargetInputIndex depth (dimension * width) bit) = binaryExtensionVectorBits widthPositive target bit

theorem Algebraic.MassProduction.SchedulerStage.pointTargetDifferenceArrayCircuit_eval_vectorBits {width depth dimension : ℕ} (widthPositive : 0 < width) (input : Fin ((Sorting.networkRecords depth + 1) * (dimension * width)) → Bool) (points : Fin (Sorting.networkRecords depth) → Fin dimension → BinaryExtension width) (target : Fin dimension → BinaryExtension width) (pointBits : ∀ (record : Fin (Sorting.networkRecords depth)) (bit : Fin (dimension * width)), input (stagePointInputIndex depth (dimension * width) record bit) = binaryExtensionVectorBits widthPositive (points record) bit) (targetBits : ∀ (bit : Fin (dimension * width)), input (stageTargetInputIndex depth (dimension * width) bit) = binaryExtensionVectorBits widthPositive target bit) (record : Fin (Sorting.networkRecords depth)) : directProductInput ((pointTargetDifferenceArrayCircuit dimension width depth).eval DeMorgan.interpretation input) record = binaryExtensionVectorBits widthPositive (points record - target)

With correctly encoded point and target blocks, the preprocessing circuit emits the packed characteristic-two difference point - target.

noncomputable def Algebraic.MassProduction.SchedulerStage.pointDifferentIndices {depth dimension width : ℕ} (points : Fin (Sorting.networkRecords depth) → Fin dimension → BinaryExtension width) (target : Fin dimension → BinaryExtension width) : Finset (Fin (Sorting.networkRecords depth))

Point-array positions that differ from the current target. Positions equal to the target are valid padding and forbid no projective direction.

Equations

• Algebraic.MassProduction.SchedulerStage.pointDifferentIndices points target = {record : Fin (Algebraic.MassProduction.Sorting.networkRecords depth) | points record ≠ target}

theorem Algebraic.MassProduction.SchedulerStage.nonzeroVectorIndices_differenceArray {width depth dimension : ℕ} (widthPositive : 0 < width) (input : Fin ((Sorting.networkRecords depth + 1) * (dimension * width)) → Bool) (points : Fin (Sorting.networkRecords depth) → Fin dimension → BinaryExtension width) (target : Fin dimension → BinaryExtension width) (pointBits : ∀ (record : Fin (Sorting.networkRecords depth)) (bit : Fin (dimension * width)), input (stagePointInputIndex depth (dimension * width) record bit) = binaryExtensionVectorBits widthPositive (points record) bit) (targetBits : ∀ (bit : Fin (dimension * width)), input (stageTargetInputIndex depth (dimension * width) bit) = binaryExtensionVectorBits widthPositive target bit) : ForbiddenRanks.nonzeroVectorIndices ((pointTargetDifferenceArrayCircuit dimension width depth).eval DeMorgan.interpretation input) = pointDifferentIndices points target

For the canonical stage input, nonzero generated differences occur exactly at the non-padding point positions.

The complete stage and its geometric correctness

noncomputable def Algebraic.MassProduction.SchedulerStage.schedulerStageCircuit {width : ℕ} (dimension : ℕ) (widthPositive : 0 < width) (depth : ℕ) : Circuit DeMorgan.signature ((Sorting.networkRecords depth + 1) * (dimension * width)) (dimension * width)

Complete fixed-wire circuit for one greedy scheduling stage.

Equations

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

@[simp]

theorem Algebraic.MassProduction.SchedulerStage.schedulerStageCircuit_size {width : ℕ} (dimension : ℕ) (widthPositive : 0 < width) (depth : ℕ) : (schedulerStageCircuit dimension widthPositive depth).size = (pointTargetDifferenceArrayCircuit dimension width depth).size + (ForbiddenRanks.freshDirectionFromDifferencesCircuit dimension widthPositive depth).size

A scheduler stage has exactly the gates of its difference array followed by the fresh-direction search.

def Algebraic.MassProduction.SchedulerStage.schedulerStageCostBound (dimension width depth : ℕ) : ℕ

Uniform polynomial ledger for one fully expanded scheduler stage.

Equations

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

theorem Algebraic.MassProduction.SchedulerStage.schedulerStageCircuit_cost_le {width dimension depth : ℕ} (widthPositive : 0 < width) : (schedulerStageCircuit dimension widthPositive depth).cost DeMorgan.standardCost ≤ schedulerStageCostBound dimension width depth

theorem Algebraic.MassProduction.SchedulerStage.schedulerStageCircuit_disjoint_of_nonzero_capacity {width depth dimension : ℕ} (widthPositive : 0 < width) (widthAtLeastTwo : 2 ≤ width) (input : Fin ((Sorting.networkRecords depth + 1) * (dimension * width)) → Bool) (points : Fin (Sorting.networkRecords depth) → Fin dimension → BinaryExtension width) (target : Fin dimension → BinaryExtension width) (used : Finset (Fin dimension → BinaryExtension width)) (pointBits : ∀ (record : Fin (Sorting.networkRecords depth)) (bit : Fin (dimension * width)), input (stagePointInputIndex depth (dimension * width) record bit) = binaryExtensionVectorBits widthPositive (points record) bit) (targetBits : ∀ (bit : Fin (dimension * width)), input (stageTargetInputIndex depth (dimension * width) bit) = binaryExtensionVectorBits widthPositive target bit) (usedCovered : ∀ point ∈ used, ∃ (record : Fin (Sorting.networkRecords depth)), points record = point) (capacity : (pointDifferentIndices points target).card < Nat.card (Projectivization (BinaryExtension width) (Fin dimension → BinaryExtension width))) : ∃ (direction : Projectivization (BinaryExtension width) (Fin dimension → BinaryExtension width)), (schedulerStageCircuit dimension widthPositive depth).eval DeMorgan.interpretation input = projectiveDirectionKey widthPositive direction ∧ Disjoint (ForbiddenRanks.binaryExtensionPuncturedLine target direction) used

One fully explicit stage selects a canonical direction whose punctured line avoids every point represented in the input array.

theorem Algebraic.MassProduction.SchedulerStage.schedulerStageCircuit_disjoint {width depth dimension : ℕ} (widthPositive : 0 < width) (widthAtLeastTwo : 2 ≤ width) (input : Fin ((Sorting.networkRecords depth + 1) * (dimension * width)) → Bool) (points : Fin (Sorting.networkRecords depth) → Fin dimension → BinaryExtension width) (target : Fin dimension → BinaryExtension width) (used : Finset (Fin dimension → BinaryExtension width)) (pointBits : ∀ (record : Fin (Sorting.networkRecords depth)) (bit : Fin (dimension * width)), input (stagePointInputIndex depth (dimension * width) record bit) = binaryExtensionVectorBits widthPositive (points record) bit) (targetBits : ∀ (bit : Fin (dimension * width)), input (stageTargetInputIndex depth (dimension * width) bit) = binaryExtensionVectorBits widthPositive target bit) (usedCovered : ∀ point ∈ used, ∃ (record : Fin (Sorting.networkRecords depth)), points record = point) (capacity : Sorting.networkRecords depth < Nat.card (Projectivization (BinaryExtension width) (Fin dimension → BinaryExtension width))) : ∃ (direction : Projectivization (BinaryExtension width) (Fin dimension → BinaryExtension width)), (schedulerStageCircuit dimension widthPositive depth).eval DeMorgan.interpretation input = projectiveDirectionKey widthPositive direction ∧ Disjoint (ForbiddenRanks.binaryExtensionPuncturedLine target direction) used

The total-array capacity condition is a convenient sufficient form of one-stage correctness.

theorem Algebraic.MassProduction.SchedulerStage.schedulerStageCircuit_disjoint_vectorInput_of_nonzero_capacity {width depth dimension : ℕ} (widthPositive : 0 < width) (widthAtLeastTwo : 2 ≤ width) (points : Fin (Sorting.networkRecords depth) → Fin dimension → BinaryExtension width) (target : Fin dimension → BinaryExtension width) (used : Finset (Fin dimension → BinaryExtension width)) (usedCovered : ∀ point ∈ used, ∃ (record : Fin (Sorting.networkRecords depth)), points record = point) (capacity : (pointDifferentIndices points target).card < Nat.card (Projectivization (BinaryExtension width) (Fin dimension → BinaryExtension width))) : ∃ (direction : Projectivization (BinaryExtension width) (Fin dimension → BinaryExtension width)), (schedulerStageCircuit dimension widthPositive depth).eval DeMorgan.interpretation (schedulerStageInputBits widthPositive points target) = projectiveDirectionKey widthPositive direction ∧ Disjoint (ForbiddenRanks.binaryExtensionPuncturedLine target direction) used

Public sentinel-aware vector-level form of one constructive stage.

theorem Algebraic.MassProduction.SchedulerStage.schedulerStageCircuit_disjoint_vectorInput {width depth dimension : ℕ} (widthPositive : 0 < width) (widthAtLeastTwo : 2 ≤ width) (points : Fin (Sorting.networkRecords depth) → Fin dimension → BinaryExtension width) (target : Fin dimension → BinaryExtension width) (used : Finset (Fin dimension → BinaryExtension width)) (usedCovered : ∀ point ∈ used, ∃ (record : Fin (Sorting.networkRecords depth)), points record = point) (capacity : Sorting.networkRecords depth < Nat.card (Projectivization (BinaryExtension width) (Fin dimension → BinaryExtension width))) : ∃ (direction : Projectivization (BinaryExtension width) (Fin dimension → BinaryExtension width)), (schedulerStageCircuit dimension widthPositive depth).eval DeMorgan.interpretation (schedulerStageInputBits widthPositive points target) = projectiveDirectionKey widthPositive direction ∧ Disjoint (ForbiddenRanks.binaryExtensionPuncturedLine target direction) used

Public vector-level form under total-array capacity.

noncomputable def Algebraic.MassProduction.SchedulerStage.pointArraySet {depth dimension width : ℕ} (points : Fin (Sorting.networkRecords depth) → Fin dimension → BinaryExtension width) : Finset (Fin dimension → BinaryExtension width)

The finite set of points appearing in a packed stage array. Its decidable equality is kept local to this definition.

Equations

• Algebraic.MassProduction.SchedulerStage.pointArraySet points = Finset.image points Finset.univ

theorem Algebraic.MassProduction.SchedulerStage.schedulerStageCircuit_disjoint_all_points_of_nonzero_capacity {width depth dimension : ℕ} (widthPositive : 0 < width) (widthAtLeastTwo : 2 ≤ width) (points : Fin (Sorting.networkRecords depth) → Fin dimension → BinaryExtension width) (target : Fin dimension → BinaryExtension width) (capacity : (pointDifferentIndices points target).card < Nat.card (Projectivization (BinaryExtension width) (Fin dimension → BinaryExtension width))) : ∃ (direction : Projectivization (BinaryExtension width) (Fin dimension → BinaryExtension width)), (schedulerStageCircuit dimension widthPositive depth).eval DeMorgan.interpretation (schedulerStageInputBits widthPositive points target) = projectiveDirectionKey widthPositive direction ∧ Disjoint (ForbiddenRanks.binaryExtensionPuncturedLine target direction) (pointArraySet points)

In particular, a sentinel-aware stage avoids the entire supplied point array.

theorem Algebraic.MassProduction.SchedulerStage.schedulerStageCircuit_disjoint_all_points {width depth dimension : ℕ} (widthPositive : 0 < width) (widthAtLeastTwo : 2 ≤ width) (points : Fin (Sorting.networkRecords depth) → Fin dimension → BinaryExtension width) (target : Fin dimension → BinaryExtension width) (capacity : Sorting.networkRecords depth < Nat.card (Projectivization (BinaryExtension width) (Fin dimension → BinaryExtension width))) : ∃ (direction : Projectivization (BinaryExtension width) (Fin dimension → BinaryExtension width)), (schedulerStageCircuit dimension widthPositive depth).eval DeMorgan.interpretation (schedulerStageInputBits widthPositive points target) = projectiveDirectionKey widthPositive direction ∧ Disjoint (ForbiddenRanks.binaryExtensionPuncturedLine target direction) (pointArraySet points)

A stage avoids the entire supplied power-of-two point array under total array capacity.