Constructive selection of a fresh projective direction

This module joins the verified packed sorter, least-missing selector, and projective unranker. Its input is a power-of-two array of forbidden projective ranks, with duplicates or unused positions optionally padded by the projective sentinel. Under the exact projective-capacity inequality it returns the canonical packed vector of a direction whose rank occurs nowhere in the input array.

The construction is the rank-selection core of the manuscript's greedy scheduler. Generation of the forbidden-rank array from prior recovery points, and iteration of this core over all requested targets, are kept as separate layers.

def Algebraic.MassProduction.FreshDirection.sortedRankBits (depth rankWidth : ℕ) (input : Fin (Sorting.networkBits depth rankWidth) → Bool) : Fin (Sorting.networkBits depth rankWidth) → Bool

Sort a power-of-two array of packed ranks in ascending order.

Equations

• Algebraic.MassProduction.FreshDirection.sortedRankBits depth rankWidth input = Algebraic.MassProduction.Sorting.bitonicSortBits ⋯ depth true input

def Algebraic.MassProduction.FreshDirection.freshProjectiveRankBits (dimension width depth : ℕ) (input : Fin (Sorting.networkBits depth (dimension * width)) → Bool) : Fin (dimension * width) → Bool

Pure semantics of selecting the least missing rank after sorting.

Equations

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

@[reducible]

def Algebraic.MassProduction.FreshDirection.freshProjectiveRankGateCount (dimension width depth : ℕ) : ℕ

Exact gate count of the input sorter followed by least-missing selection.

Equations

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

def Algebraic.MassProduction.FreshDirection.freshProjectiveRankCircuit (dimension width depth : ℕ) : Circuit DeMorgan.signature (Sorting.networkBits depth (dimension * width)) (dimension * width)

Explicit circuit selecting a fresh valid packed projective rank.

Equations

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

@[simp]

theorem Algebraic.MassProduction.FreshDirection.freshProjectiveRankCircuit_size (dimension width depth : ℕ) : (freshProjectiveRankCircuit dimension width depth).size = freshProjectiveRankGateCount dimension width depth

@[simp]

theorem Algebraic.MassProduction.FreshDirection.freshProjectiveRankCircuit_eval {depth dimension width : ℕ} (input : Fin (Sorting.networkBits depth (dimension * width)) → Bool) : (freshProjectiveRankCircuit dimension width depth).eval DeMorgan.interpretation input = freshProjectiveRankBits dimension width depth input

theorem Algebraic.MassProduction.FreshDirection.freshProjectiveRankCircuit_sound_of_inRange_capacity {width depth dimension : ℕ} (widthPositive : 0 < width) (input : Fin (Sorting.networkBits depth (dimension * width)) → Bool) (capacity : (LeastMissing.inRangeRankIndices (projectiveRankSentinel dimension width) input).card < Nat.card (Projectivization (BinaryExtension width) (Fin dimension → BinaryExtension width))) : toLex ((freshProjectiveRankCircuit dimension width depth).eval DeMorgan.interpretation input) < toLex (projectiveRankSentinel dimension width) ∧ ∀ (index : Fin (Sorting.networkRecords depth)), (freshProjectiveRankCircuit dimension width depth).eval DeMorgan.interpretation input ≠ LeastMissing.rankAt input index

Sentinel-aware rank selection: only input records strictly below the projective sentinel consume direction capacity.

theorem Algebraic.MassProduction.FreshDirection.freshProjectiveRankCircuit_sound {width depth dimension : ℕ} (widthPositive : 0 < width) (input : Fin (Sorting.networkBits depth (dimension * width)) → Bool) (capacity : Sorting.networkRecords depth < Nat.card (Projectivization (BinaryExtension width) (Fin dimension → BinaryExtension width))) : toLex ((freshProjectiveRankCircuit dimension width depth).eval DeMorgan.interpretation input) < toLex (projectiveRankSentinel dimension width) ∧ ∀ (index : Fin (Sorting.networkRecords depth)), (freshProjectiveRankCircuit dimension width depth).eval DeMorgan.interpretation input ≠ LeastMissing.rankAt input index

Under the total-array direction-capacity inequality, rank selection returns a valid projective rank absent from the original input array.

@[reducible]

noncomputable def Algebraic.MassProduction.FreshDirection.freshProjectiveDirectionGateCount {width : ℕ} (dimension : ℕ) (widthPositive : 0 < width) (depth : ℕ) : ℕ

Exact gate count after appending projective unranking.

Equations

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

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

Explicit circuit returning a canonical packed representative of a fresh projective direction.

Equations

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

@[simp]

theorem Algebraic.MassProduction.FreshDirection.freshProjectiveDirectionCircuit_size {width : ℕ} (dimension : ℕ) (widthPositive : 0 < width) (depth : ℕ) : (freshProjectiveDirectionCircuit dimension widthPositive depth).size = freshProjectiveDirectionGateCount dimension widthPositive depth

theorem Algebraic.MassProduction.FreshDirection.freshProjectiveDirectionCircuit_sound_of_inRange_capacity {width depth dimension : ℕ} (widthPositive : 0 < width) (input : Fin (Sorting.networkBits depth (dimension * width)) → Bool) (capacity : (LeastMissing.inRangeRankIndices (projectiveRankSentinel dimension width) input).card < Nat.card (Projectivization (BinaryExtension width) (Fin dimension → BinaryExtension width))) : ∃ (direction : Projectivization (BinaryExtension width) (Fin dimension → BinaryExtension width)), (freshProjectiveDirectionCircuit dimension widthPositive depth).eval DeMorgan.interpretation input = projectiveDirectionKey widthPositive direction ∧ ∀ (index : Fin (Sorting.networkRecords depth)), projectiveDirectionRankBits widthPositive direction ≠ LeastMissing.rankAt input index

Sentinel-aware direction selection.

theorem Algebraic.MassProduction.FreshDirection.freshProjectiveDirectionCircuit_sound {width depth dimension : ℕ} (widthPositive : 0 < 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)), (freshProjectiveDirectionCircuit dimension widthPositive depth).eval DeMorgan.interpretation input = projectiveDirectionKey widthPositive direction ∧ ∀ (index : Fin (Sorting.networkRecords depth)), projectiveDirectionRankBits widthPositive direction ≠ LeastMissing.rankAt input index

The direction circuit returns the canonical key of a projective direction whose rank was not present in the input array.

def Algebraic.MassProduction.FreshDirection.freshProjectiveRankCostBound (dimension width depth : ℕ) : ℕ

A uniform polynomial bound for sorting and least-missing selection.

Equations

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

def Algebraic.MassProduction.FreshDirection.freshProjectiveDirectionCostBound (dimension width depth : ℕ) : ℕ

A uniform polynomial bound after appending projective unranking.

Equations

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

theorem Algebraic.MassProduction.FreshDirection.freshProjectiveRankCircuit_cost_le {dimension width depth : ℕ} : (freshProjectiveRankCircuit dimension width depth).cost DeMorgan.standardCost ≤ freshProjectiveRankCostBound dimension width depth

A uniform polynomial cost bound for the fresh-rank circuit.

theorem Algebraic.MassProduction.FreshDirection.freshProjectiveDirectionCircuit_cost_le {width dimension depth : ℕ} (widthPositive : 0 < width) : (freshProjectiveDirectionCircuit dimension widthPositive depth).cost DeMorgan.standardCost ≤ freshProjectiveDirectionCostBound dimension width depth

Appending unranking preserves a polynomial gate ledger.