Guarded ranks for forbidden projective directions

The greedy scheduler forms difference vectors between the current target and previously occupied recovery points. A nonzero difference forbids its projective direction; a zero difference forbids nothing. This module gives an explicit Boolean circuit for the fixed-width operation

• zero vector -> the invalid projective-rank sentinel;
• nonzero vector -> its canonical projective block rank.

It then replicates that circuit over a power-of-two packed array. Padding by zero vectors therefore becomes padding by the sentinel automatically.

def Algebraic.MassProduction.ForbiddenRanks.rawVectorBit (vectorWidth : ℕ) (input : Fin (2 * vectorWidth) → Bool) (bit : Fin vectorWidth) : Bool

The raw vector is the first half of the postprocessor input.

Equations

• Algebraic.MassProduction.ForbiddenRanks.rawVectorBit vectorWidth input bit = input (finProdFinEquiv (0, bit))

def Algebraic.MassProduction.ForbiddenRanks.computedRankBit (vectorWidth : ℕ) (input : Fin (2 * vectorWidth) → Bool) (bit : Fin vectorWidth) : Bool

The already-computed rank is the second half of the postprocessor input.

Equations

• Algebraic.MassProduction.ForbiddenRanks.computedRankBit vectorWidth input bit = input (finProdFinEquiv (1, bit))

def Algebraic.MassProduction.ForbiddenRanks.rawVectorZeroExpression (vectorWidth : ℕ) : DeMorgan.Expression (2 * vectorWidth)

Test whether every bit in the raw-vector half is zero.

Equations

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

@[simp]

theorem Algebraic.MassProduction.ForbiddenRanks.rawVectorZeroExpression_eval_eq_true_iff {vectorWidth : ℕ} (input : Fin (2 * vectorWidth) → Bool) : DeMorgan.Expression.eval input (rawVectorZeroExpression vectorWidth) = true ↔ ∀ (bit : Fin vectorWidth), rawVectorBit vectorWidth input bit = false

def Algebraic.MassProduction.ForbiddenRanks.guardedRankOutputExpression (dimension width : ℕ) (output : Fin (dimension * width)) : DeMorgan.Expression (2 * (dimension * width))

Select the sentinel on a zero raw vector and the computed rank otherwise.

Equations

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

@[simp]

theorem Algebraic.MassProduction.ForbiddenRanks.guardedRankOutputExpression_eval {dimension width : ℕ} (input : Fin (2 * (dimension * width)) → Bool) (output : Fin (dimension * width)) : DeMorgan.Expression.eval input (guardedRankOutputExpression dimension width output) = if DeMorgan.Expression.eval input (rawVectorZeroExpression (dimension * width)) = true then projectiveRankSentinel dimension width output else computedRankBit (dimension * width) input output

theorem Algebraic.MassProduction.ForbiddenRanks.rawVectorZeroExpression_standardCost {vectorWidth : ℕ} : (rawVectorZeroExpression vectorWidth).standardCost = 2 * vectorWidth

theorem Algebraic.MassProduction.ForbiddenRanks.guardedRankOutputExpression_standardCost_le {dimension width : ℕ} (output : Fin (dimension * width)) : (guardedRankOutputExpression dimension width output).standardCost ≤ 4 * (dimension * width) + 4

@[reducible]

def Algebraic.MassProduction.ForbiddenRanks.guardedRankOutputGateCount (dimension width : ℕ) (output : Fin (dimension * width)) : ℕ

Gate count of one independently compiled guarded output bit.

Equations

• Algebraic.MassProduction.ForbiddenRanks.guardedRankOutputGateCount dimension width output = (Algebraic.MassProduction.ForbiddenRanks.guardedRankOutputExpression dimension width output).gateCount

def Algebraic.MassProduction.ForbiddenRanks.guardedRankPostprocessCircuit (dimension width : ℕ) : Circuit DeMorgan.signature (2 * (dimension * width)) (dimension * width)

Postprocess a (raw vector, computed rank) pair.

Equations

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

@[simp]

theorem Algebraic.MassProduction.ForbiddenRanks.guardedRankPostprocessCircuit_size (dimension width : ℕ) : (guardedRankPostprocessCircuit dimension width).size = ∑ output : Fin (dimension * width), guardedRankOutputGateCount dimension width output

@[simp]

theorem Algebraic.MassProduction.ForbiddenRanks.guardedRankPostprocessCircuit_eval {dimension width : ℕ} (input : Fin (2 * (dimension * width)) → Bool) (output : Fin (dimension * width)) : (guardedRankPostprocessCircuit dimension width).eval DeMorgan.interpretation input output = if DeMorgan.Expression.eval input (rawVectorZeroExpression (dimension * width)) = true then projectiveRankSentinel dimension width output else computedRankBit (dimension * width) input output

theorem Algebraic.MassProduction.ForbiddenRanks.guardedRankPostprocessCircuit_cost_le {dimension width : ℕ} : (guardedRankPostprocessCircuit dimension width).cost DeMorgan.standardCost ≤ dimension * width * (4 * (dimension * width) + 4)

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

Preserve the raw vector alongside the projective rank computed from it.

Equations

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

@[simp]

theorem Algebraic.MassProduction.ForbiddenRanks.rawAndProjectiveRankCircuit_size {width : ℕ} (dimension : ℕ) (widthPositive : 0 < width) : (rawAndProjectiveRankCircuit dimension widthPositive).size = (projectiveDirectionRankCircuit dimension widthPositive).size

rawAndProjectiveRankCircuit has exactly the gates of projectiveDirectionRankCircuit; the surrounding wiring adds none.

@[simp]

theorem Algebraic.MassProduction.ForbiddenRanks.rawAndProjectiveRankCircuit_raw {width dimension : ℕ} (widthPositive : 0 < width) (input : Fin (dimension * width) → Bool) (bit : Fin (dimension * width)) : (rawAndProjectiveRankCircuit dimension widthPositive).eval DeMorgan.interpretation input (finProdFinEquiv (0, bit)) = input bit

@[simp]

theorem Algebraic.MassProduction.ForbiddenRanks.rawAndProjectiveRankCircuit_rank {width dimension : ℕ} (widthPositive : 0 < width) (input : Fin (dimension * width) → Bool) (bit : Fin (dimension * width)) : (rawAndProjectiveRankCircuit dimension widthPositive).eval DeMorgan.interpretation input (finProdFinEquiv (1, bit)) = (projectiveDirectionRankCircuit dimension widthPositive).eval DeMorgan.interpretation input bit

@[simp]

theorem Algebraic.MassProduction.ForbiddenRanks.rawAndProjectiveRankCircuit_cost {width dimension : ℕ} (widthPositive : 0 < width) : (rawAndProjectiveRankCircuit dimension widthPositive).cost DeMorgan.standardCost = (projectiveDirectionRankCircuit dimension widthPositive).cost DeMorgan.standardCost

theorem Algebraic.MassProduction.ForbiddenRanks.rawVectorZero_after_rawAndRank_iff {width dimension : ℕ} (widthPositive : 0 < width) (input : Fin (dimension * width) → Bool) : DeMorgan.Expression.eval ((rawAndProjectiveRankCircuit dimension widthPositive).eval DeMorgan.interpretation input) (rawVectorZeroExpression (dimension * width)) = true ↔ input = fun (x : Fin (dimension * width)) => false

noncomputable def Algebraic.MassProduction.ForbiddenRanks.guardedProjectiveRankCircuit {width : ℕ} (dimension : ℕ) (widthPositive : 0 < width) : Circuit DeMorgan.signature (dimension * width) (dimension * width)

Rank one vector, mapping the zero vector to the sentinel.

Equations

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

@[simp]

theorem Algebraic.MassProduction.ForbiddenRanks.guardedProjectiveRankCircuit_size {width : ℕ} (dimension : ℕ) (widthPositive : 0 < width) : (guardedProjectiveRankCircuit dimension widthPositive).size = (rawAndProjectiveRankCircuit dimension widthPositive).size + ∑ output : Fin (dimension * width), guardedRankOutputGateCount dimension width output

The exact gate count of guardedProjectiveRankCircuit.

@[simp]

theorem Algebraic.MassProduction.ForbiddenRanks.guardedProjectiveRankCircuit_eval_zero {width dimension : ℕ} (widthPositive : 0 < width) : ((guardedProjectiveRankCircuit dimension widthPositive).eval DeMorgan.interpretation fun (x : Fin (dimension * width)) => false) = projectiveRankSentinel dimension width

theorem Algebraic.MassProduction.ForbiddenRanks.guardedProjectiveRankCircuit_eval_of_ne_zero {width dimension : ℕ} (widthPositive : 0 < width) (input : Fin (dimension * width) → Bool) (inputNonzero : input ≠ fun (x : Fin (dimension * width)) => false) : (guardedProjectiveRankCircuit dimension widthPositive).eval DeMorgan.interpretation input = (projectiveDirectionRankCircuit dimension widthPositive).eval DeMorgan.interpretation input

On a nonzero packed vector, guarded ranking agrees with the complete normalizer-plus-ranker circuit.

theorem Algebraic.MassProduction.ForbiddenRanks.guardedProjectiveRankCircuit_eval_direction {width dimension : ℕ} (widthPositive : 0 < width) (widthAtLeastTwo : 2 ≤ width) (input : Fin (dimension * width) → Bool) (inputNonzero : input ≠ fun (x : Fin (dimension * width)) => false) : ∃ (direction : Projectivization (BinaryExtension width) (Fin dimension → BinaryExtension width)), (guardedProjectiveRankCircuit dimension widthPositive).eval DeMorgan.interpretation input = projectiveDirectionRankBits widthPositive direction

Every nonzero packed vector is guarded-ranked by its actual projective direction.

theorem Algebraic.MassProduction.ForbiddenRanks.guardedProjectiveRankCircuit_lt_sentinel_iff {width dimension : ℕ} (widthPositive : 0 < width) (widthAtLeastTwo : 2 ≤ width) (input : Fin (dimension * width) → Bool) : toLex ((guardedProjectiveRankCircuit dimension widthPositive).eval DeMorgan.interpretation input) < toLex (projectiveRankSentinel dimension width) ↔ input ≠ fun (x : Fin (dimension * width)) => false

A guarded rank lies below the projective sentinel exactly when its raw packed vector is nonzero.

theorem Algebraic.MassProduction.ForbiddenRanks.guardedProjectiveRankCircuit_eval_vectorBits {width dimension : ℕ} (widthPositive : 0 < width) (widthAtLeastTwo : 2 ≤ width) (vector : Fin dimension → BinaryExtension width) (vectorNonzero : vector ≠ 0) : (guardedProjectiveRankCircuit dimension widthPositive).eval DeMorgan.interpretation (binaryExtensionVectorBits widthPositive vector) = projectiveDirectionRankBits widthPositive (Projectivization.mk (BinaryExtension width) vector vectorNonzero)

On explicitly encoded nonzero field vectors, guarded ranking is exactly the rank of the projective class of that vector.

def Algebraic.MassProduction.ForbiddenRanks.guardedProjectiveRankCostBound (dimension width : ℕ) : ℕ

Polynomial bound for sentinel-guarded normalization and ranking.

Equations

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

theorem Algebraic.MassProduction.ForbiddenRanks.guardedProjectiveRankCircuit_cost_le {width dimension : ℕ} (widthPositive : 0 < width) : (guardedProjectiveRankCircuit dimension widthPositive).cost DeMorgan.standardCost ≤ guardedProjectiveRankCostBound dimension width

@[reducible]

noncomputable def Algebraic.MassProduction.ForbiddenRanks.guardedProjectiveRankGateCount {width : ℕ} (dimension : ℕ) (widthPositive : 0 < width) : ℕ

Replicate guarded ranking over a power-of-two array of packed vectors.

Equations

• Algebraic.MassProduction.ForbiddenRanks.guardedProjectiveRankGateCount dimension widthPositive = (Algebraic.MassProduction.ForbiddenRanks.guardedProjectiveRankCircuit dimension widthPositive).size

noncomputable def Algebraic.MassProduction.ForbiddenRanks.forbiddenRankArrayCircuit {width : ℕ} (dimension : ℕ) (widthPositive : 0 < width) (depth : ℕ) : Circuit DeMorgan.signature (Sorting.networkBits depth (dimension * width)) (Sorting.networkBits depth (dimension * width))

Apply guarded projective ranking independently to every record in the power-of-two array.

Equations

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

@[simp]

theorem Algebraic.MassProduction.ForbiddenRanks.forbiddenRankArrayCircuit_size {width : ℕ} (dimension : ℕ) (widthPositive : 0 < width) (depth : ℕ) : (forbiddenRankArrayCircuit dimension widthPositive depth).size = Sorting.networkRecords depth * guardedProjectiveRankGateCount dimension widthPositive

@[simp]

theorem Algebraic.MassProduction.ForbiddenRanks.forbiddenRankArrayCircuit_eval_apply {width dimension : ℕ} (widthPositive : 0 < width) (depth : ℕ) (input : Fin (Sorting.networkBits depth (dimension * width)) → Bool) (record : Fin (Sorting.networkRecords depth)) (bit : Fin (dimension * width)) : (forbiddenRankArrayCircuit dimension widthPositive depth).eval DeMorgan.interpretation input (finProdFinEquiv (record, bit)) = (guardedProjectiveRankCircuit dimension widthPositive).eval DeMorgan.interpretation (directProductInput input record) bit

noncomputable def Algebraic.MassProduction.ForbiddenRanks.nonzeroVectorIndices {depth vectorWidth : ℕ} (input : Fin (Sorting.networkBits depth vectorWidth) → Bool) : Finset (Fin (Sorting.networkRecords depth))

Positions containing genuine nonzero difference vectors.

Equations

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

theorem Algebraic.MassProduction.ForbiddenRanks.inRangeRankIndices_forbiddenRankArray {width depth dimension : ℕ} (widthPositive : 0 < width) (widthAtLeastTwo : 2 ≤ width) (input : Fin (Sorting.networkBits depth (dimension * width)) → Bool) : LeastMissing.inRangeRankIndices (projectiveRankSentinel dimension width) ((forbiddenRankArrayCircuit dimension widthPositive depth).eval DeMorgan.interpretation input) = nonzeroVectorIndices input

Guarded ranking sends exactly the zero-vector positions to the sentinel, so the number of in-range ranks is the number of nonzero input blocks.

def Algebraic.MassProduction.ForbiddenRanks.forbiddenRankArrayCostBound (dimension width depth : ℕ) : ℕ

Replicated guarded-ranking cost bound.

Equations

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

theorem Algebraic.MassProduction.ForbiddenRanks.forbiddenRankArrayCircuit_cost_le {width dimension depth : ℕ} (widthPositive : 0 < width) : (forbiddenRankArrayCircuit dimension widthPositive depth).cost DeMorgan.standardCost ≤ forbiddenRankArrayCostBound dimension width depth

noncomputable def Algebraic.MassProduction.ForbiddenRanks.freshDirectionFromDifferencesCircuit {width : ℕ} (dimension : ℕ) (widthPositive : 0 < width) (depth : ℕ) : Circuit DeMorgan.signature (Sorting.networkBits depth (dimension * width)) (dimension * width)

One constructive scheduler stage: guarded-rank all forbidden difference vectors, sort their ranks, choose a missing valid rank, and unrank it.

Equations

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

@[simp]

theorem Algebraic.MassProduction.ForbiddenRanks.freshDirectionFromDifferencesCircuit_size {width : ℕ} (dimension : ℕ) (widthPositive : 0 < width) (depth : ℕ) : (freshDirectionFromDifferencesCircuit dimension widthPositive depth).size = Sorting.networkRecords depth * guardedProjectiveRankGateCount dimension widthPositive + FreshDirection.freshProjectiveDirectionGateCount dimension widthPositive depth

One guarded rank per input record, then the fresh-direction search.

theorem Algebraic.MassProduction.ForbiddenRanks.freshDirectionFromDifferencesCircuit_sound_of_nonzero_capacity {width depth dimension : ℕ} (widthPositive : 0 < width) (widthAtLeastTwo : 2 ≤ width) (input : Fin (Sorting.networkBits depth (dimension * width)) → Bool) (capacity : (nonzeroVectorIndices input).card < Nat.card (Projectivization (BinaryExtension width) (Fin dimension → BinaryExtension width))) : ∃ (direction : Projectivization (BinaryExtension width) (Fin dimension → BinaryExtension width)), (freshDirectionFromDifferencesCircuit dimension widthPositive depth).eval DeMorgan.interpretation input = projectiveDirectionKey widthPositive direction ∧ (∀ (record : Fin (Sorting.networkRecords depth)), projectiveDirectionRankBits widthPositive direction ≠ (guardedProjectiveRankCircuit dimension widthPositive).eval DeMorgan.interpretation (directProductInput input record)) ∧ ∀ (record : Fin (Sorting.networkRecords depth)), (directProductInput input record ≠ fun (x : Fin (dimension * width)) => false) → ∃ (forbiddenDirection : Projectivization (BinaryExtension width) (Fin dimension → BinaryExtension width)), (guardedProjectiveRankCircuit dimension widthPositive).eval DeMorgan.interpretation (directProductInput input record) = projectiveDirectionRankBits widthPositive forbiddenDirection ∧ direction ≠ forbiddenDirection

A scheduler stage returns a canonical direction key whose rank differs from the guarded rank of every packed input vector. Each nonzero input block also comes with its actual forbidden projective direction and a proof that the selected direction is different from it.

theorem Algebraic.MassProduction.ForbiddenRanks.freshDirectionFromDifferencesCircuit_sound {width depth dimension : ℕ} (widthPositive : 0 < width) (widthAtLeastTwo : 2 ≤ width) (input : Fin (Sorting.networkBits depth (dimension * width)) → Bool) (capacity : Sorting.networkRecords depth < Nat.card (Projectivization (BinaryExtension width) (Fin dimension → BinaryExtension width))) : ∃ (direction : Projectivization (BinaryExtension width) (Fin dimension → BinaryExtension width)), (freshDirectionFromDifferencesCircuit dimension widthPositive depth).eval DeMorgan.interpretation input = projectiveDirectionKey widthPositive direction ∧ (∀ (record : Fin (Sorting.networkRecords depth)), projectiveDirectionRankBits widthPositive direction ≠ (guardedProjectiveRankCircuit dimension widthPositive).eval DeMorgan.interpretation (directProductInput input record)) ∧ ∀ (record : Fin (Sorting.networkRecords depth)), (directProductInput input record ≠ fun (x : Fin (dimension * width)) => false) → ∃ (forbiddenDirection : Projectivization (BinaryExtension width) (Fin dimension → BinaryExtension width)), (guardedProjectiveRankCircuit dimension widthPositive).eval DeMorgan.interpretation (directProductInput input record) = projectiveDirectionRankBits widthPositive forbiddenDirection ∧ direction ≠ forbiddenDirection

Total-array capacity is a convenient sufficient condition for the sentinel-aware scheduler theorem.

def Algebraic.MassProduction.ForbiddenRanks.freshDirectionFromDifferencesCostBound (dimension width depth : ℕ) : ℕ

Polynomial cost bound for a scheduler stage once its difference array is available.

Equations

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

theorem Algebraic.MassProduction.ForbiddenRanks.freshDirectionFromDifferencesCircuit_cost_le {width dimension depth : ℕ} (widthPositive : 0 < width) : (freshDirectionFromDifferencesCircuit dimension widthPositive depth).cost DeMorgan.standardCost ≤ freshDirectionFromDifferencesCostBound dimension width depth

noncomputable def Algebraic.MassProduction.ForbiddenRanks.binaryExtensionPuncturedLine {dimension width : ℕ} (target : Fin dimension → BinaryExtension width) (direction : Projectivization (BinaryExtension width) (Fin dimension → BinaryExtension width)) : Finset (Fin dimension → BinaryExtension width)

A punctured line over the concrete binary extension field, using a local finite enumeration rather than exporting another global typeclass instance.

Equations

• Algebraic.MassProduction.ForbiddenRanks.binaryExtensionPuncturedLine target direction = Algebraic.MassProduction.puncturedLine target direction

theorem Algebraic.MassProduction.ForbiddenRanks.freshDirectionFromDifferencesCircuit_disjoint_of_nonzero_capacity {width dimension depth : ℕ} (widthPositive : 0 < width) (widthAtLeastTwo : 2 ≤ width) (target : Fin dimension → BinaryExtension width) (used : Finset (Fin dimension → BinaryExtension width)) (input : Fin (Sorting.networkBits depth (dimension * width)) → Bool) (covers : ∀ point ∈ used, ∃ (record : Fin (Sorting.networkRecords depth)), directProductInput input record = binaryExtensionVectorBits widthPositive (point - target)) (capacity : (nonzeroVectorIndices input).card < Nat.card (Projectivization (BinaryExtension width) (Fin dimension → BinaryExtension width))) : ∃ (direction : Projectivization (BinaryExtension width) (Fin dimension → BinaryExtension width)), (freshDirectionFromDifferencesCircuit dimension widthPositive depth).eval DeMorgan.interpretation input = projectiveDirectionKey widthPositive direction ∧ Disjoint (binaryExtensionPuncturedLine target direction) used

Sentinel-aware geometric scheduler-stage correctness. Zero padding does not count against direction capacity.

theorem Algebraic.MassProduction.ForbiddenRanks.freshDirectionFromDifferencesCircuit_disjoint {width dimension depth : ℕ} (widthPositive : 0 < width) (widthAtLeastTwo : 2 ≤ width) (target : Fin dimension → BinaryExtension width) (used : Finset (Fin dimension → BinaryExtension width)) (input : Fin (Sorting.networkBits depth (dimension * width)) → Bool) (covers : ∀ point ∈ used, ∃ (record : Fin (Sorting.networkRecords depth)), directProductInput input record = binaryExtensionVectorBits widthPositive (point - target)) (capacity : Sorting.networkRecords depth < Nat.card (Projectivization (BinaryExtension width) (Fin dimension → BinaryExtension width))) : ∃ (direction : Projectivization (BinaryExtension width) (Fin dimension → BinaryExtension width)), (freshDirectionFromDifferencesCircuit dimension widthPositive depth).eval DeMorgan.interpretation input = projectiveDirectionKey widthPositive direction ∧ Disjoint (binaryExtensionPuncturedLine target direction) used

Geometric scheduler-stage correctness under the simpler total-array capacity condition.