Explicit enumeration of a punctured affine line

Given packed field vectors for a target and a direction, this module emits q - 1 packed points target + scalar * direction, one for every nonzero scalar of GF(q), where q = 2^width. The scalar enumeration is a fixed noncomputable equivalence used only to hardwire constants; the resulting Boolean circuit is completely explicit and has the manuscript's q * poly(width) cost shape.

@[reducible, inline]

abbrev Algebraic.MassProduction.LineEnumeration.NonzeroScalar (width : ℕ) : Type

Nonzero scalars of the selected binary extension field.

Equations

• Algebraic.MassProduction.LineEnumeration.NonzeroScalar width = { scalar : Algebraic.MassProduction.BinaryExtension width // scalar ≠ 0 }

noncomputable def Algebraic.MassProduction.LineEnumeration.nonzeroScalarCount (width : ℕ) : ℕ

Exact number of nonzero scalars, kept instance-free in public types.

Equations

• Algebraic.MassProduction.LineEnumeration.nonzeroScalarCount width = Nat.card (Algebraic.MassProduction.LineEnumeration.NonzeroScalar width)

theorem Algebraic.MassProduction.LineEnumeration.nonzeroScalarCount_eq_two_pow_sub_one {width : ℕ} (widthPositive : 0 < width) : nonzeroScalarCount width = 2 ^ width - 1

noncomputable def Algebraic.MassProduction.LineEnumeration.enumeratedNonzeroScalar {width : ℕ} (index : Fin (nonzeroScalarCount width)) : BinaryExtension width

A fixed enumeration of every nonzero scalar.

Equations

• Algebraic.MassProduction.LineEnumeration.enumeratedNonzeroScalar index = ↑((Finite.equivFin (Algebraic.MassProduction.LineEnumeration.NonzeroScalar width)).symm index)

theorem Algebraic.MassProduction.LineEnumeration.enumeratedNonzeroScalar_ne_zero {width : ℕ} (index : Fin (nonzeroScalarCount width)) : enumeratedNonzeroScalar index ≠ 0

theorem Algebraic.MassProduction.LineEnumeration.enumeratedNonzeroScalar_surjective {width : ℕ} (scalar : BinaryExtension width) (scalarNonzero : scalar ≠ 0) : ∃ (index : Fin (nonzeroScalarCount width)), enumeratedNonzeroScalar index = scalar

theorem Algebraic.MassProduction.LineEnumeration.enumeratedNonzeroScalar_injective {width : ℕ} : Function.Injective enumeratedNonzeroScalar

Fixed scalar and vector-coordinate circuits

def Algebraic.MassProduction.LineEnumeration.constantBitVectorCircuit {width : ℕ} (inputWidth : ℕ) (bits : Fin width → Bool) : Circuit DeMorgan.signature inputWidth width

Compile a hardwired Boolean vector. Constants contribute internal nodes but zero standard cost.

Equations

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

@[simp]

theorem Algebraic.MassProduction.LineEnumeration.constantBitVectorCircuit_size {width : ℕ} (inputWidth : ℕ) (bits : Fin width → Bool) : (constantBitVectorCircuit inputWidth bits).size = width

One constant gate per output bit, and no other gates.

@[simp]

theorem Algebraic.MassProduction.LineEnumeration.constantBitVectorCircuit_eval {inputWidth n✝ : ℕ} {bits : Fin n✝ → Bool} (input : Fin inputWidth → Bool) : (constantBitVectorCircuit inputWidth bits).eval DeMorgan.interpretation input = bits

@[simp]

theorem Algebraic.MassProduction.LineEnumeration.constantBitVectorCircuit_cost {inputWidth n✝ : ℕ} {bits : Fin n✝ → Bool} : (constantBitVectorCircuit inputWidth bits).cost DeMorgan.standardCost = 0

def Algebraic.MassProduction.LineEnumeration.lineInputCoordinateCircuit (dimension width : ℕ) (side : Fin 2) (coordinate : Fin dimension) : Circuit DeMorgan.signature (2 * (dimension * width)) width

Select one field-coordinate block from the target/direction pair.

Equations

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

@[simp]

theorem Algebraic.MassProduction.LineEnumeration.lineInputCoordinateCircuit_size (dimension width : ℕ) (side : Fin 2) (coordinate : Fin dimension) : (lineInputCoordinateCircuit dimension width side coordinate).size = 0

lineInputCoordinateCircuit is pure wiring: it has no gates.

@[simp]

theorem Algebraic.MassProduction.LineEnumeration.lineInputCoordinateCircuit_eval {dimension width : ℕ} (input : Fin (2 * (dimension * width)) → Bool) (side : Fin 2) (coordinate : Fin dimension) : (lineInputCoordinateCircuit dimension width side coordinate).eval DeMorgan.interpretation input = fun (bit : Fin width) => input (finProdFinEquiv (side, finProdFinEquiv (coordinate, bit)))

@[simp]

theorem Algebraic.MassProduction.LineEnumeration.lineInputCoordinateCircuit_cost {dimension width : ℕ} (side : Fin 2) (coordinate : Fin dimension) : (lineInputCoordinateCircuit dimension width side coordinate).cost DeMorgan.standardCost = 0

noncomputable def Algebraic.MassProduction.LineEnumeration.lineInputBits {width dimension : ℕ} (widthPositive : 0 < width) (target direction : Fin dimension → BinaryExtension width) : Fin (2 * (dimension * width)) → Bool

Packed (target, direction) vector pair.

Equations

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

theorem Algebraic.MassProduction.LineEnumeration.lineInputCoordinateCircuit_eval_lineInput {width dimension : ℕ} (widthPositive : 0 < width) (target direction : Fin dimension → BinaryExtension width) (coordinate : Fin dimension) : (lineInputCoordinateCircuit dimension width 0 coordinate).eval DeMorgan.interpretation (lineInputBits widthPositive target direction) = decodeBinaryExtension widthPositive (target coordinate)

theorem Algebraic.MassProduction.LineEnumeration.lineInputDirectionCircuit_eval_lineInput {width dimension : ℕ} (widthPositive : 0 < width) (target direction : Fin dimension → BinaryExtension width) (coordinate : Fin dimension) : (lineInputCoordinateCircuit dimension width 1 coordinate).eval DeMorgan.interpretation (lineInputBits widthPositive target direction) = decodeBinaryExtension widthPositive (direction coordinate)

noncomputable def Algebraic.MassProduction.LineEnumeration.directionScalarProductCircuit {width : ℕ} (dimension : ℕ) (widthPositive : 0 < width) (coordinate : Fin dimension) (scalar : Fin (nonzeroScalarCount width)) : Circuit DeMorgan.signature (2 * (dimension * width)) width

Multiply one direction coordinate by one hardwired nonzero scalar.

Equations

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

@[simp]

theorem Algebraic.MassProduction.LineEnumeration.directionScalarProductCircuit_size {width : ℕ} (dimension : ℕ) (widthPositive : 0 < width) (coordinate : Fin dimension) (scalar : Fin (nonzeroScalarCount width)) : (directionScalarProductCircuit dimension widthPositive coordinate scalar).size = (lineInputCoordinateCircuit dimension width 1 coordinate).size + (constantBitVectorCircuit (2 * (dimension * width)) (decodeBinaryExtension widthPositive (enumeratedNonzeroScalar scalar))).size + ∑ output : Fin width, multiplicationCoordinateGateCount widthPositive output

The exact gate count of directionScalarProductCircuit.

@[simp]

theorem Algebraic.MassProduction.LineEnumeration.directionScalarProductCircuit_eval_lineInput {width dimension : ℕ} (widthPositive : 0 < width) (target direction : Fin dimension → BinaryExtension width) (coordinate : Fin dimension) (scalar : Fin (nonzeroScalarCount width)) : (directionScalarProductCircuit dimension widthPositive coordinate scalar).eval DeMorgan.interpretation (lineInputBits widthPositive target direction) = decodeBinaryExtension widthPositive (direction coordinate * enumeratedNonzeroScalar scalar)

@[simp]

theorem Algebraic.MassProduction.LineEnumeration.directionScalarProductCircuit_cost {width dimension : ℕ} (widthPositive : 0 < width) (coordinate : Fin dimension) (scalar : Fin (nonzeroScalarCount width)) : (directionScalarProductCircuit dimension widthPositive coordinate scalar).cost DeMorgan.standardCost = width * (6 * (width * width))

noncomputable def Algebraic.MassProduction.LineEnumeration.linePointCoordinateCircuit {width : ℕ} (dimension : ℕ) (widthPositive : 0 < width) (coordinate : Fin dimension) (scalar : Fin (nonzeroScalarCount width)) : Circuit DeMorgan.signature (2 * (dimension * width)) width

Add the target coordinate to a hardwired scalar multiple of the direction coordinate.

Equations

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

@[simp]

theorem Algebraic.MassProduction.LineEnumeration.linePointCoordinateCircuit_size {width : ℕ} (dimension : ℕ) (widthPositive : 0 < width) (coordinate : Fin dimension) (scalar : Fin (nonzeroScalarCount width)) : (linePointCoordinateCircuit dimension widthPositive coordinate scalar).size = (lineInputCoordinateCircuit dimension width 0 coordinate).size + (directionScalarProductCircuit dimension widthPositive coordinate scalar).size + ∑ output : Fin width, additionCoordinateGateCount output

The exact gate count of linePointCoordinateCircuit.

@[simp]

theorem Algebraic.MassProduction.LineEnumeration.linePointCoordinateCircuit_eval_lineInput {width dimension : ℕ} (widthPositive : 0 < width) (target direction : Fin dimension → BinaryExtension width) (coordinate : Fin dimension) (scalar : Fin (nonzeroScalarCount width)) : (linePointCoordinateCircuit dimension widthPositive coordinate scalar).eval DeMorgan.interpretation (lineInputBits widthPositive target direction) = decodeBinaryExtension widthPositive (target coordinate + enumeratedNonzeroScalar scalar * direction coordinate)

@[simp]

theorem Algebraic.MassProduction.LineEnumeration.linePointCoordinateCircuit_cost {width dimension : ℕ} (widthPositive : 0 < width) (coordinate : Fin dimension) (scalar : Fin (nonzeroScalarCount width)) : (linePointCoordinateCircuit dimension widthPositive coordinate scalar).cost DeMorgan.standardCost = width * (6 * (width * width)) + 4 * width

@[reducible]

noncomputable def Algebraic.MassProduction.LineEnumeration.linePointCoordinateGateCount {width : ℕ} (dimension : ℕ) (widthPositive : 0 < width) (_coordinate : Fin dimension) (scalar : Fin (nonzeroScalarCount width)) : ℕ

Named gate count and a type-stable wrapper for one coordinate.

Equations

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

noncomputable def Algebraic.MassProduction.LineEnumeration.linePointCircuit {width : ℕ} (dimension : ℕ) (widthPositive : 0 < width) (scalar : Fin (nonzeroScalarCount width)) : Circuit DeMorgan.signature (2 * (dimension * width)) (dimension * width)

Emit one complete affine-line point.

Equations

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

@[simp]

theorem Algebraic.MassProduction.LineEnumeration.linePointCircuit_size {width : ℕ} (dimension : ℕ) (widthPositive : 0 < width) (scalar : Fin (nonzeroScalarCount width)) : (linePointCircuit dimension widthPositive scalar).size = ∑ member : Fin dimension, (linePointCoordinateCircuit dimension widthPositive member scalar).size

The exact gate count of linePointCircuit.

@[simp]

theorem Algebraic.MassProduction.LineEnumeration.linePointCircuit_eval_lineInput {width dimension : ℕ} (widthPositive : 0 < width) (target direction : Fin dimension → BinaryExtension width) (scalar : Fin (nonzeroScalarCount width)) : (linePointCircuit dimension widthPositive scalar).eval DeMorgan.interpretation (lineInputBits widthPositive target direction) = binaryExtensionVectorBits widthPositive (target + enumeratedNonzeroScalar scalar • direction)

@[simp]

theorem Algebraic.MassProduction.LineEnumeration.linePointCircuit_cost {width dimension : ℕ} (widthPositive : 0 < width) (scalar : Fin (nonzeroScalarCount width)) : (linePointCircuit dimension widthPositive scalar).cost DeMorgan.standardCost = dimension * (width * (6 * (width * width)) + 4 * width)

@[reducible]

noncomputable def Algebraic.MassProduction.LineEnumeration.linePointGateCount {width : ℕ} (dimension : ℕ) (widthPositive : 0 < width) (scalar : Fin (nonzeroScalarCount width)) : ℕ

Named gate count and type-stable wrapper for one complete point.

Equations

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

noncomputable def Algebraic.MassProduction.LineEnumeration.lineEnumerationCircuit {width : ℕ} (dimension : ℕ) (widthPositive : 0 < width) : Circuit DeMorgan.signature (2 * (dimension * width)) (nonzeroScalarCount width * (dimension * width))

Emit all q - 1 non-target points in row-major scalar/vector order.

Equations

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

@[simp]

theorem Algebraic.MassProduction.LineEnumeration.lineEnumerationCircuit_size {width : ℕ} (dimension : ℕ) (widthPositive : 0 < width) : (lineEnumerationCircuit dimension widthPositive).size = ∑ member : Fin (nonzeroScalarCount width), (linePointCircuit dimension widthPositive member).size

The exact gate count of lineEnumerationCircuit.

@[simp]

theorem Algebraic.MassProduction.LineEnumeration.lineEnumerationCircuit_eval_apply {width dimension : ℕ} (widthPositive : 0 < width) (target direction : Fin dimension → BinaryExtension width) (scalar : Fin (nonzeroScalarCount width)) (bit : Fin (dimension * width)) : (lineEnumerationCircuit dimension widthPositive).eval DeMorgan.interpretation (lineInputBits widthPositive target direction) (finProdFinEquiv (scalar, bit)) = binaryExtensionVectorBits widthPositive (target + enumeratedNonzeroScalar scalar • direction) bit

theorem Algebraic.MassProduction.LineEnumeration.decode_lineEnumerationCircuit_record {width dimension : ℕ} (widthPositive : 0 < width) (target direction : Fin dimension → BinaryExtension width) (scalar : Fin (nonzeroScalarCount width)) : binaryExtensionVectorCoordinate widthPositive (directProductInput ((lineEnumerationCircuit dimension widthPositive).eval DeMorgan.interpretation (lineInputBits widthPositive target direction)) scalar) = target + enumeratedNonzeroScalar scalar • direction

Decoding one emitted record gives the intended affine-line point.

@[simp]

theorem Algebraic.MassProduction.LineEnumeration.lineEnumerationCircuit_cost {width dimension : ℕ} (widthPositive : 0 < width) : (lineEnumerationCircuit dimension widthPositive).cost DeMorgan.standardCost = nonzeroScalarCount width * (dimension * (width * (6 * (width * width)) + 4 * width))

Exact polynomial gate ledger for enumerating all nonzero points of one affine line.

theorem Algebraic.MassProduction.LineEnumeration.lineEnumerationCircuit_cost_eq_two_pow_sub_one {width dimension : ℕ} (widthPositive : 0 < width) : (lineEnumerationCircuit dimension widthPositive).cost DeMorgan.standardCost = (2 ^ width - 1) * (dimension * (width * (6 * (width * width)) + 4 * width))

The same ledger with the exact field-size count made explicit.

Exact finite-set semantics

noncomputable def Algebraic.MassProduction.LineEnumeration.enumeratedPuncturedLine {dimension width : ℕ} (target direction : Fin dimension → BinaryExtension width) : Finset (Fin dimension → BinaryExtension width)

The finite set represented by the enumerator's output records. Classical decidable equality is confined to the definition rather than exported as an instance requirement.

Equations

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

theorem Algebraic.MassProduction.LineEnumeration.enumeratedPuncturedLine_normalized_eq {dimension width : ℕ} (target : Fin dimension → BinaryExtension width) (direction : Projectivization (BinaryExtension width) (Fin dimension → BinaryExtension width)) : enumeratedPuncturedLine target (normalizeBinaryExtensionVector direction.rep) = ForbiddenRanks.binaryExtensionPuncturedLine target direction

Enumerating the normalized representative of a projective direction produces exactly its punctured affine line, independent of the representative chosen internally by Projectivization.rep.

Scheduler-to-line composition

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

Free projection of the target vector from a scheduler-stage input.

Equations

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

@[simp]

theorem Algebraic.MassProduction.LineEnumeration.schedulerStageTargetCircuit_size (dimension width depth : ℕ) : (schedulerStageTargetCircuit dimension width depth).size = 0

schedulerStageTargetCircuit is pure wiring: it has no gates.

@[simp]

theorem Algebraic.MassProduction.LineEnumeration.schedulerStageTargetCircuit_eval {depth dimension width : ℕ} (input : Fin ((Sorting.networkRecords depth + 1) * (dimension * width)) → Bool) : (schedulerStageTargetCircuit dimension width depth).eval DeMorgan.interpretation input = input ∘ SchedulerStage.stageTargetInputIndex depth (dimension * width)

@[simp]

theorem Algebraic.MassProduction.LineEnumeration.schedulerStageTargetCircuit_cost {dimension width depth : ℕ} : (schedulerStageTargetCircuit dimension width depth).cost DeMorgan.standardCost = 0

theorem Algebraic.MassProduction.LineEnumeration.schedulerStageTargetCircuit_eval_stageInput {width depth dimension : ℕ} (widthPositive : 0 < width) (points : Fin (Sorting.networkRecords depth) → Fin dimension → BinaryExtension width) (target : Fin dimension → BinaryExtension width) : (schedulerStageTargetCircuit dimension width depth).eval DeMorgan.interpretation (SchedulerStage.schedulerStageInputBits widthPositive points target) = binaryExtensionVectorBits widthPositive target

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

One fixed circuit that selects a fresh projective direction and emits all non-target points on the resulting affine line.

Equations

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

@[simp]

theorem Algebraic.MassProduction.LineEnumeration.scheduledLineEnumerationCircuit_size {width : ℕ} (dimension : ℕ) (widthPositive : 0 < width) (depth : ℕ) : (scheduledLineEnumerationCircuit dimension widthPositive depth).size = (schedulerStageTargetCircuit dimension width depth).size + (SchedulerStage.schedulerStageCircuit dimension widthPositive depth).size + (lineEnumerationCircuit dimension widthPositive).size

The exact gate count of scheduledLineEnumerationCircuit.

noncomputable def Algebraic.MassProduction.LineEnumeration.decodedLineOutputSet {width dimension : ℕ} (widthPositive : 0 < width) (output : Fin (nonzeroScalarCount width * (dimension * width)) → Bool) : Finset (Fin dimension → BinaryExtension width)

Decode an emitted row-major array of packed field vectors as a finite set. Classical equality remains local to this boundary.

Equations

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

theorem Algebraic.MassProduction.LineEnumeration.scheduledLineEnumerationCircuit_sound_input_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) (pointBits : ∀ (record : Fin (Sorting.networkRecords depth)) (bit : Fin (dimension * width)), input (SchedulerStage.stagePointInputIndex depth (dimension * width) record bit) = binaryExtensionVectorBits widthPositive (points record) bit) (targetBits : ∀ (bit : Fin (dimension * width)), input (SchedulerStage.stageTargetInputIndex depth (dimension * width) bit) = binaryExtensionVectorBits widthPositive target bit) (capacity : (SchedulerStage.pointDifferentIndices points target).card < Nat.card (Projectivization (BinaryExtension width) (Fin dimension → BinaryExtension width))) : ∃ (direction : Projectivization (BinaryExtension width) (Fin dimension → BinaryExtension width)), (∀ (scalar : Fin (nonzeroScalarCount width)), binaryExtensionVectorCoordinate widthPositive (directProductInput ((scheduledLineEnumerationCircuit dimension widthPositive depth).eval DeMorgan.interpretation input) scalar) = target + enumeratedNonzeroScalar scalar • normalizeBinaryExtensionVector direction.rep) ∧ decodedLineOutputSet widthPositive ((scheduledLineEnumerationCircuit dimension widthPositive depth).eval DeMorgan.interpretation input) = ForbiddenRanks.binaryExtensionPuncturedLine target direction ∧ Disjoint (ForbiddenRanks.binaryExtensionPuncturedLine target direction) (SchedulerStage.pointArraySet points)

Input-layout-general form of scheduler-and-enumerator correctness.

theorem Algebraic.MassProduction.LineEnumeration.scheduledLineEnumerationCircuit_sound_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 : (SchedulerStage.pointDifferentIndices points target).card < Nat.card (Projectivization (BinaryExtension width) (Fin dimension → BinaryExtension width))) : ∃ (direction : Projectivization (BinaryExtension width) (Fin dimension → BinaryExtension width)), (∀ (scalar : Fin (nonzeroScalarCount width)), binaryExtensionVectorCoordinate widthPositive (directProductInput ((scheduledLineEnumerationCircuit dimension widthPositive depth).eval DeMorgan.interpretation (SchedulerStage.schedulerStageInputBits widthPositive points target)) scalar) = target + enumeratedNonzeroScalar scalar • normalizeBinaryExtensionVector direction.rep) ∧ decodedLineOutputSet widthPositive ((scheduledLineEnumerationCircuit dimension widthPositive depth).eval DeMorgan.interpretation (SchedulerStage.schedulerStageInputBits widthPositive points target)) = ForbiddenRanks.binaryExtensionPuncturedLine target direction ∧ Disjoint (ForbiddenRanks.binaryExtensionPuncturedLine target direction) (SchedulerStage.pointArraySet points)

The scheduler and enumerator compose end to end: every output record is the prescribed point of one projective punctured line, the decoded output set is exactly that line, and it avoids every supplied occupied point.

theorem Algebraic.MassProduction.LineEnumeration.scheduledLineEnumerationCircuit_sound {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)), (∀ (scalar : Fin (nonzeroScalarCount width)), binaryExtensionVectorCoordinate widthPositive (directProductInput ((scheduledLineEnumerationCircuit dimension widthPositive depth).eval DeMorgan.interpretation (SchedulerStage.schedulerStageInputBits widthPositive points target)) scalar) = target + enumeratedNonzeroScalar scalar • normalizeBinaryExtensionVector direction.rep) ∧ decodedLineOutputSet widthPositive ((scheduledLineEnumerationCircuit dimension widthPositive depth).eval DeMorgan.interpretation (SchedulerStage.schedulerStageInputBits widthPositive points target)) = ForbiddenRanks.binaryExtensionPuncturedLine target direction ∧ Disjoint (ForbiddenRanks.binaryExtensionPuncturedLine target direction) (SchedulerStage.pointArraySet points)

The total-array capacity condition is a convenient sufficient form of the end-to-end scheduler-and-enumerator theorem.

def Algebraic.MassProduction.LineEnumeration.scheduledLineEnumerationCostBound (dimension width depth : ℕ) : ℕ

Complete gate ledger for fresh-direction selection followed by line enumeration.

Equations

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

theorem Algebraic.MassProduction.LineEnumeration.scheduledLineEnumerationCircuit_cost_le {width dimension depth : ℕ} (widthPositive : 0 < width) : (scheduledLineEnumerationCircuit dimension widthPositive depth).cost DeMorgan.standardCost ≤ scheduledLineEnumerationCostBound dimension width depth