Least-missing packed ranks

The projective scheduler sorts a padded power-of-two list of forbidden ranks. This module implements the next fixed-wire step. For each sorted position it creates either rank zero or the current rank's binary successor when that value lies in a genuine gap below a hardwired upper bound. Candidate records are then sorted by a one-bit validity flag (valid first), and the first candidate value is designated as the output.

All ranks use big-endian bit order, matching the verified lexicographic sorter. The construction has linear dependence on the record count up to the sorter's logarithmic-depth factors and a polynomial dependence on rank width.

def Algebraic.MassProduction.LeastMissing.expressionBitEqual {n : ℕ} (left right : DeMorgan.Expression n) : DeMorgan.Expression n

XNOR for arbitrary Boolean expressions.

Equations

• Algebraic.MassProduction.LeastMissing.expressionBitEqual left right = (left.and right).or (left.not.and right.not)

@[simp]

theorem Algebraic.MassProduction.LeastMissing.expressionBitEqual_eval_eq_true_iff {n : ℕ} (left right : DeMorgan.Expression n) (input : Fin n → Bool) : DeMorgan.Expression.eval input (expressionBitEqual left right) = true ↔ DeMorgan.Expression.eval input left = DeMorgan.Expression.eval input right

def Algebraic.MassProduction.LeastMissing.priorExpressionBitsEqual {n : ℕ} (width : ℕ) (left right : Fin width → DeMorgan.Expression n) (pivot : Fin width) : DeMorgan.Expression n

Equality of all expression bits before a selected pivot.

Equations

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

theorem Algebraic.MassProduction.LeastMissing.priorExpressionBitsEqual_eval_eq_true_iff {width n : ℕ} (left right : Fin width → DeMorgan.Expression n) (pivot : Fin width) (input : Fin n → Bool) : DeMorgan.Expression.eval input (priorExpressionBitsEqual width left right pivot) = true ↔ ∀ previous < pivot, DeMorgan.Expression.eval input (left previous) = DeMorgan.Expression.eval input (right previous)

def Algebraic.MassProduction.LeastMissing.expressionBitsLessAt {n : ℕ} (width : ℕ) (left right : Fin width → DeMorgan.Expression n) (pivot : Fin width) : DeMorgan.Expression n

A possible first differing coordinate witnessing lexicographic order.

Equations

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

theorem Algebraic.MassProduction.LeastMissing.expressionBitsLessAt_eval_eq_true_iff {width n : ℕ} (left right : Fin width → DeMorgan.Expression n) (pivot : Fin width) (input : Fin n → Bool) : DeMorgan.Expression.eval input (expressionBitsLessAt width left right pivot) = true ↔ (∀ previous < pivot, DeMorgan.Expression.eval input (left previous) = DeMorgan.Expression.eval input (right previous)) ∧ DeMorgan.Expression.eval input (left pivot) < DeMorgan.Expression.eval input (right pivot)

def Algebraic.MassProduction.LeastMissing.expressionBitsLess {n : ℕ} (width : ℕ) (left right : Fin width → DeMorgan.Expression n) : DeMorgan.Expression n

Lexicographic strict comparison of two expression-valued bit strings.

Equations

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

theorem Algebraic.MassProduction.LeastMissing.expressionBitsLess_eval_eq_true_iff {width n : ℕ} (left right : Fin width → DeMorgan.Expression n) (input : Fin n → Bool) : DeMorgan.Expression.eval input (expressionBitsLess width left right) = true ↔ (toLex fun (bit : Fin width) => DeMorgan.Expression.eval input (left bit)) < toLex fun (bit : Fin width) => DeMorgan.Expression.eval input (right bit)

def Algebraic.MassProduction.LeastMissing.expressionXor {n : ℕ} (left right : DeMorgan.Expression n) : DeMorgan.Expression n

XOR in the De Morgan basis.

Equations

• Algebraic.MassProduction.LeastMissing.expressionXor left right = (left.or right).and (left.and right).not

@[simp]

theorem Algebraic.MassProduction.LeastMissing.expressionXor_eval {n : ℕ} (left right : DeMorgan.Expression n) (input : Fin n → Bool) : DeMorgan.Expression.eval input (expressionXor left right) = (DeMorgan.Expression.eval input left != DeMorgan.Expression.eval input right)

def Algebraic.MassProduction.LeastMissing.rankInputExpression (depth rankWidth : ℕ) (record : Fin (Sorting.networkRecords depth)) (bit : Fin rankWidth) : DeMorgan.Expression (Sorting.networkBits depth rankWidth)

Input expression for one bit of one packed rank record.

Equations

• Algebraic.MassProduction.LeastMissing.rankInputExpression depth rankWidth record bit = Algebraic.DeMorgan.Expression.input (finProdFinEquiv (record, bit))

def Algebraic.MassProduction.LeastMissing.constantRankExpressions {rankWidth n : ℕ} (rank : Fin rankWidth → Bool) : Fin rankWidth → DeMorgan.Expression n

Hardwired rank bit family.

Equations

• Algebraic.MassProduction.LeastMissing.constantRankExpressions rank bit = Algebraic.DeMorgan.Expression.constant (rank bit)

def Algebraic.MassProduction.LeastMissing.incrementCarryExpression (depth rankWidth : ℕ) (record : Fin (Sorting.networkRecords depth)) (bit : Fin rankWidth) : DeMorgan.Expression (Sorting.networkBits depth rankWidth)

Carry into a big-endian bit is the conjunction of all less-significant input bits.

Equations

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

def Algebraic.MassProduction.LeastMissing.incrementRankBitExpression (depth rankWidth : ℕ) (record : Fin (Sorting.networkRecords depth)) (bit : Fin rankWidth) : DeMorgan.Expression (Sorting.networkBits depth rankWidth)

One output bit of the big-endian increment of a packed rank.

Equations

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

def Algebraic.MassProduction.LeastMissing.rankAt {depth rankWidth : ℕ} (input : Fin (Sorting.networkBits depth rankWidth) → Bool) (record : Fin (Sorting.networkRecords depth)) : Fin rankWidth → Bool

Packed rank at one input position.

Equations

• Algebraic.MassProduction.LeastMissing.rankAt input record = Algebraic.MassProduction.Sorting.networkRecord input record

def Algebraic.MassProduction.LeastMissing.incrementRank {depth rankWidth : ℕ} (input : Fin (Sorting.networkBits depth rankWidth) → Bool) (record : Fin (Sorting.networkRecords depth)) : Fin rankWidth → Bool

Big-endian increment semantics emitted by the increment expressions.

Equations

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

Discrete semantics of binary increment

def Algebraic.MassProduction.LeastMissing.binaryCarry {width : ℕ} (bits : Fin width → Bool) (bit : Fin width) : Bool

Carry into one bit of a pure big-endian bit string.

Equations

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

def Algebraic.MassProduction.LeastMissing.binaryIncrement {width : ℕ} (bits : Fin width → Bool) : Fin width → Bool

Big-endian binary increment, modulo 2 ^ width.

Equations

• Algebraic.MassProduction.LeastMissing.binaryIncrement bits bit = (bits bit != Algebraic.MassProduction.LeastMissing.binaryCarry bits bit)

theorem Algebraic.MassProduction.LeastMissing.binaryCarry_eq_true_iff {width : ℕ} (bits : Fin width → Bool) (bit : Fin width) : binaryCarry bits bit = true ↔ ∀ (lessSignificant : Fin width), bit < lessSignificant → bits lessSignificant = true

theorem Algebraic.MassProduction.LeastMissing.binaryCarry_succ_cons {width : ℕ} (head : Bool) (tail : Fin width → Bool) (bit : Fin width) : binaryCarry (Fin.cons head tail) bit.succ = binaryCarry tail bit

theorem Algebraic.MassProduction.LeastMissing.binaryIncrement_tail_cons {width : ℕ} (head : Bool) (tail : Fin width → Bool) : Fin.tail (binaryIncrement (Fin.cons head tail)) = binaryIncrement tail

theorem Algebraic.MassProduction.LeastMissing.binaryIncrement_eq_cons_of_all_tail_true {width : ℕ} (head : Bool) (tail : Fin width → Bool) (allTailTrue : ∀ (bit : Fin width), tail bit = true) : binaryIncrement (Fin.cons head tail) = Fin.cons (!head) fun (x : Fin width) => false

theorem Algebraic.MassProduction.LeastMissing.binaryIncrement_eq_cons_of_not_all_tail_true {width : ℕ} (head : Bool) (tail : Fin width → Bool) (notAllTailTrue : ¬∀ (bit : Fin width), tail bit = true) : binaryIncrement (Fin.cons head tail) = Fin.cons head (binaryIncrement tail)

theorem Algebraic.MassProduction.LeastMissing.allFalse_isMin {width : ℕ} (bits : Fin width → Bool) (allFalse : bits = fun (x : Fin width) => false) : IsMin (toLex bits)

theorem Algebraic.MassProduction.LeastMissing.allTrue_isMax {width : ℕ} (bits : Fin width → Bool) (allTrue : bits = fun (x : Fin width) => true) : IsMax (toLex bits)

theorem Algebraic.MassProduction.LeastMissing.cons_covBy_of_tail_covBy {width : ℕ} (head : Bool) {tailLeft tailRight : Fin width → Bool} (tailCover : toLex tailLeft ⋖ toLex tailRight) : toLex (Fin.cons head tailLeft) ⋖ toLex (Fin.cons head tailRight)

theorem Algebraic.MassProduction.LeastMissing.cons_rollover_covBy (width : ℕ) : toLex (Fin.cons false fun (x : Fin width) => true) ⋖ toLex (Fin.cons true fun (x : Fin width) => false)

theorem Algebraic.MassProduction.LeastMissing.binaryIncrement_covBy_of_lt (width : ℕ) (bits : Fin width → Bool) : toLex bits < toLex (binaryIncrement bits) → toLex bits ⋖ toLex (binaryIncrement bits)

Whenever binary increment increases, it is the immediate lexicographic successor.

theorem Algebraic.MassProduction.LeastMissing.lt_binaryIncrement_of_not_all_true (width : ℕ) (bits : Fin width → Bool) : (¬∀ (bit : Fin width), bits bit = true) → toLex bits < toLex (binaryIncrement bits)

theorem Algebraic.MassProduction.LeastMissing.incrementRank_eq_binaryIncrement {depth rankWidth : ℕ} (input : Fin (Sorting.networkBits depth rankWidth) → Bool) (record : Fin (Sorting.networkRecords depth)) : incrementRank input record = binaryIncrement (rankAt input record)

theorem Algebraic.MassProduction.LeastMissing.incrementRank_covBy_of_lt {depth rankWidth : ℕ} (input : Fin (Sorting.networkBits depth rankWidth) → Bool) (record : Fin (Sorting.networkRecords depth)) (increases : toLex (rankAt input record) < toLex (incrementRank input record)) : toLex (rankAt input record) ⋖ toLex (incrementRank input record)

theorem Algebraic.MassProduction.LeastMissing.rankAt_lt_incrementRank_of_lt {depth rankWidth : ℕ} (input : Fin (Sorting.networkBits depth rankWidth) → Bool) (record : Fin (Sorting.networkRecords depth)) (greater : Fin rankWidth → Bool) (currentLt : toLex (rankAt input record) < toLex greater) : toLex (rankAt input record) < toLex (incrementRank input record)

def Algebraic.MassProduction.LeastMissing.firstRecord (depth : ℕ) : Fin (Sorting.networkRecords depth)

The first record of every nonempty power-of-two sorting array.

Equations

• Algebraic.MassProduction.LeastMissing.firstRecord depth = ⟨0, ⋯⟩

def Algebraic.MassProduction.LeastMissing.zeroCandidateExpression {rankWidth : ℕ} (upperBound : Fin rankWidth → Bool) (depth : ℕ) (record : Fin (Sorting.networkRecords depth)) : DeMorgan.Expression (Sorting.networkBits depth rankWidth)

The rank-zero candidate is enabled only at position zero and only when zero is below both the first forbidden rank and the upper bound.

Equations

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

def Algebraic.MassProduction.LeastMissing.successorCandidateExpression {rankWidth : ℕ} (upperBound : Fin rankWidth → Bool) (depth : ℕ) (record : Fin (Sorting.networkRecords depth)) : DeMorgan.Expression (Sorting.networkBits depth rankWidth)

Successor candidate at one sorted rank position.

Equations

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

def Algebraic.MassProduction.LeastMissing.candidateFlagExpression {rankWidth : ℕ} (upperBound : Fin rankWidth → Bool) (depth : ℕ) (record : Fin (Sorting.networkRecords depth)) : DeMorgan.Expression (Sorting.networkBits depth rankWidth)

A position is a candidate if it supplies zero or a valid successor gap.

Equations

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

def Algebraic.MassProduction.LeastMissing.candidateValueBitExpression {rankWidth : ℕ} (upperBound : Fin rankWidth → Bool) (depth : ℕ) (record : Fin (Sorting.networkRecords depth)) (bit : Fin rankWidth) : DeMorgan.Expression (Sorting.networkBits depth rankWidth)

Candidate value; zero has priority when both local conditions hold.

Equations

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

@[reducible, inline]

abbrev Algebraic.MassProduction.LeastMissing.candidateRecordWidth (rankWidth : ℕ) : ℕ

Candidate records consist of a validity flag followed by rank bits.

Equations

• Algebraic.MassProduction.LeastMissing.candidateRecordWidth rankWidth = rankWidth + 1

def Algebraic.MassProduction.LeastMissing.candidateRecordBitExpression {rankWidth : ℕ} (upperBound : Fin rankWidth → Bool) (depth : ℕ) (output : Fin (Sorting.networkBits depth (candidateRecordWidth rankWidth))) : DeMorgan.Expression (Sorting.networkBits depth rankWidth)

One output formula of the candidate generator.

Equations

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

def Algebraic.MassProduction.LeastMissing.candidateRecordsBits {rankWidth depth : ℕ} (upperBound : Fin rankWidth → Bool) (input : Fin (Sorting.networkBits depth rankWidth) → Bool) : Fin (Sorting.networkBits depth (candidateRecordWidth rankWidth)) → Bool

Pure semantics of all generated candidate records.

Equations

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

@[reducible]

def Algebraic.MassProduction.LeastMissing.candidateRecordBitGateCount {rankWidth : ℕ} (upperBound : Fin rankWidth → Bool) (depth : ℕ) (output : Fin (Sorting.networkBits depth (candidateRecordWidth rankWidth))) : ℕ

Gate count of one independently compiled candidate output.

Equations

• Algebraic.MassProduction.LeastMissing.candidateRecordBitGateCount upperBound depth output = (Algebraic.MassProduction.LeastMissing.candidateRecordBitExpression upperBound depth output).gateCount

def Algebraic.MassProduction.LeastMissing.candidateRecordsCircuit {rankWidth : ℕ} (upperBound : Fin rankWidth → Bool) (depth : ℕ) : Circuit DeMorgan.signature (Sorting.networkBits depth rankWidth) (Sorting.networkBits depth (candidateRecordWidth rankWidth))

Explicit circuit generating one candidate record per sorted input rank.

Equations

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

@[simp]

theorem Algebraic.MassProduction.LeastMissing.candidateRecordsCircuit_size {rankWidth : ℕ} (upperBound : Fin rankWidth → Bool) (depth : ℕ) : (candidateRecordsCircuit upperBound depth).size = ∑ output : Fin (Sorting.networkBits depth (candidateRecordWidth rankWidth)), candidateRecordBitGateCount upperBound depth output

@[simp]

theorem Algebraic.MassProduction.LeastMissing.candidateRecordsCircuit_eval {rankWidth : ℕ} (upperBound : Fin rankWidth → Bool) (depth : ℕ) (input : Fin (Sorting.networkBits depth rankWidth) → Bool) : (candidateRecordsCircuit upperBound depth).eval DeMorgan.interpretation input = candidateRecordsBits upperBound input

def Algebraic.MassProduction.LeastMissing.candidateFlagBit (rankWidth : ℕ) : Fin (candidateRecordWidth rankWidth)

The candidate validity flag is the first bit of its generated record.

Equations

• Algebraic.MassProduction.LeastMissing.candidateFlagBit rankWidth = ⟨0, ⋯⟩

def Algebraic.MassProduction.LeastMissing.candidateValueBit {rankWidth : ℕ} (bit : Fin rankWidth) : Fin (candidateRecordWidth rankWidth)

The candidate value occupies the remaining bits of its generated record.

Equations

• Algebraic.MassProduction.LeastMissing.candidateValueBit bit = ⟨↑bit + 1, ⋯⟩

@[simp]

theorem Algebraic.MassProduction.LeastMissing.candidateRecordsBits_flag {rankWidth depth : ℕ} (upperBound : Fin rankWidth → Bool) (input : Fin (Sorting.networkBits depth rankWidth) → Bool) (record : Fin (Sorting.networkRecords depth)) : Sorting.networkRecord (candidateRecordsBits upperBound input) record (candidateFlagBit rankWidth) = DeMorgan.Expression.eval input (candidateFlagExpression upperBound depth record)

@[simp]

theorem Algebraic.MassProduction.LeastMissing.candidateRecordsBits_value {rankWidth depth : ℕ} (upperBound : Fin rankWidth → Bool) (input : Fin (Sorting.networkBits depth rankWidth) → Bool) (record : Fin (Sorting.networkRecords depth)) (bit : Fin rankWidth) : Sorting.networkRecord (candidateRecordsBits upperBound input) record (candidateValueBit bit) = DeMorgan.Expression.eval input (candidateValueBitExpression upperBound depth record bit)

theorem Algebraic.MassProduction.LeastMissing.candidateFlagFits (rankWidth : ℕ) : 1 ≤ candidateRecordWidth rankWidth

The one-bit validity key fits every candidate record.

def Algebraic.MassProduction.LeastMissing.firstCandidateValueIndex {rankWidth : ℕ} (depth : ℕ) (bit : Fin rankWidth) : Fin (Sorting.networkBits depth (candidateRecordWidth rankWidth))

Flat output index selecting a value bit of the first candidate record.

Equations

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

def Algebraic.MassProduction.LeastMissing.leastMissingBits {rankWidth : ℕ} (upperBound : Fin rankWidth → Bool) (depth : ℕ) (input : Fin (Sorting.networkBits depth rankWidth) → Bool) : Fin rankWidth → Bool

Semantics of candidate generation, descending validity sort, and first candidate selection.

Equations

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

def Algebraic.MassProduction.LeastMissing.candidateFlag {rankWidth depth : ℕ} (upperBound : Fin rankWidth → Bool) (input : Fin (Sorting.networkBits depth rankWidth) → Bool) (record : Fin (Sorting.networkRecords depth)) : Bool

Boolean validity flag generated at one rank position.

Equations

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

def Algebraic.MassProduction.LeastMissing.candidateValue {rankWidth depth : ℕ} (upperBound : Fin rankWidth → Bool) (input : Fin (Sorting.networkBits depth rankWidth) → Bool) (record : Fin (Sorting.networkRecords depth)) : Fin rankWidth → Bool

Rank value generated at one candidate position.

Equations

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

@[simp]

theorem Algebraic.MassProduction.LeastMissing.rankInputExpression_eval {depth rankWidth : ℕ} (input : Fin (Sorting.networkBits depth rankWidth) → Bool) (record : Fin (Sorting.networkRecords depth)) (bit : Fin rankWidth) : DeMorgan.Expression.eval input (rankInputExpression depth rankWidth record bit) = rankAt input record bit

@[simp]

theorem Algebraic.MassProduction.LeastMissing.constantRankExpressions_eval {rankWidth n : ℕ} (rank : Fin rankWidth → Bool) (input : Fin n → Bool) (bit : Fin rankWidth) : DeMorgan.Expression.eval input (constantRankExpressions rank bit) = rank bit

@[simp]

theorem Algebraic.MassProduction.LeastMissing.incrementRankBitExpression_eval {depth rankWidth : ℕ} (input : Fin (Sorting.networkBits depth rankWidth) → Bool) (record : Fin (Sorting.networkRecords depth)) (bit : Fin rankWidth) : DeMorgan.Expression.eval input (incrementRankBitExpression depth rankWidth record bit) = incrementRank input record bit

theorem Algebraic.MassProduction.LeastMissing.zeroCandidateExpression_eval_eq_true_iff {rankWidth depth : ℕ} (upperBound : Fin rankWidth → Bool) (input : Fin (Sorting.networkBits depth rankWidth) → Bool) (record : Fin (Sorting.networkRecords depth)) : DeMorgan.Expression.eval input (zeroCandidateExpression upperBound depth record) = true ↔ record = firstRecord depth ∧ (toLex fun (x : Fin rankWidth) => false) < toLex (rankAt input record) ∧ (toLex fun (x : Fin rankWidth) => false) < toLex upperBound

theorem Algebraic.MassProduction.LeastMissing.successorCandidateExpression_eval_eq_true_iff {rankWidth depth : ℕ} (upperBound : Fin rankWidth → Bool) (input : Fin (Sorting.networkBits depth rankWidth) → Bool) (record : Fin (Sorting.networkRecords depth)) : DeMorgan.Expression.eval input (successorCandidateExpression upperBound depth record) = true ↔ toLex (rankAt input record) < toLex (incrementRank input record) ∧ toLex (incrementRank input record) < toLex upperBound ∧ ∀ (hasNext : ↑record + 1 < Sorting.networkRecords depth), toLex (incrementRank input record) < toLex (rankAt input ⟨↑record + 1, hasNext⟩)

theorem Algebraic.MassProduction.LeastMissing.candidateValue_of_zero {rankWidth depth : ℕ} (upperBound : Fin rankWidth → Bool) (input : Fin (Sorting.networkBits depth rankWidth) → Bool) (record : Fin (Sorting.networkRecords depth)) (zeroTrue : DeMorgan.Expression.eval input (zeroCandidateExpression upperBound depth record) = true) : candidateValue upperBound input record = fun (x : Fin rankWidth) => false

theorem Algebraic.MassProduction.LeastMissing.candidateValue_of_not_zero {rankWidth depth : ℕ} (upperBound : Fin rankWidth → Bool) (input : Fin (Sorting.networkBits depth rankWidth) → Bool) (record : Fin (Sorting.networkRecords depth)) (zeroFalse : DeMorgan.Expression.eval input (zeroCandidateExpression upperBound depth record) = false) : candidateValue upperBound input record = incrementRank input record

theorem Algebraic.MassProduction.LeastMissing.candidateFlag_sound {rankWidth depth : ℕ} (upperBound : Fin rankWidth → Bool) (input : Fin (Sorting.networkBits depth rankWidth) → Bool) (sorted : Sorting.FlatKeysSorted ⋯ true input) (record : Fin (Sorting.networkRecords depth)) (flagTrue : candidateFlag upperBound input record = true) : toLex (candidateValue upperBound input record) < toLex upperBound ∧ ∀ (index : Fin (Sorting.networkRecords depth)), candidateValue upperBound input record ≠ rankAt input index

Every asserted candidate is below the upper bound and absent from the entire sorted rank array.

Existence of a generated gap

theorem Algebraic.MassProduction.LeastMissing.candidate_exists_of_missing {rankWidth depth : ℕ} (upperBound missing : Fin rankWidth → Bool) (input : Fin (Sorting.networkBits depth rankWidth) → Bool) (missingBelowBound : toLex missing < toLex upperBound) (missingAbsent : ∀ (index : Fin (Sorting.networkRecords depth)), missing ≠ rankAt input index) : ∃ (record : Fin (Sorting.networkRecords depth)), candidateFlag upperBound input record = true

Any explicitly missing rank below the upper bound produces either the zero candidate or a successor-gap candidate. No sortedness assumption is needed for existence: the greatest array position whose value is below the missing rank supplies the local gap.

theorem Algebraic.MassProduction.LeastMissing.exists_missing_of_active_capacity {rankWidth depth : ℕ} (upperBound : Fin rankWidth → Bool) (input : Fin (Sorting.networkBits depth rankWidth) → Bool) (active : Finset (Fin (Sorting.networkRecords depth))) (covers : ∀ (index : Fin (Sorting.networkRecords depth)), toLex (rankAt input index) < toLex upperBound → index ∈ active) (capacity : active.card < Nat.card { rank : Lex (Fin rankWidth → Bool) // rank < toLex upperBound }) : ∃ (missing : Fin rankWidth → Bool), toLex missing < toLex upperBound ∧ ∀ (index : Fin (Sorting.networkRecords depth)), missing ≠ rankAt input index

If every in-range array position is covered by a smaller active set, then some rank below upperBound is absent. Positions holding the upper-bound sentinel need not belong to active, so padding does not consume capacity.

noncomputable def Algebraic.MassProduction.LeastMissing.inRangeRankIndices {rankWidth depth : ℕ} (upperBound : Fin rankWidth → Bool) (input : Fin (Sorting.networkBits depth rankWidth) → Bool) : Finset (Fin (Sorting.networkRecords depth))

The indices whose packed ranks lie strictly below the sentinel.

Equations

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

theorem Algebraic.MassProduction.LeastMissing.inRangeRankIndices_card_eq_of_recordsPermute {rankWidth depth : ℕ} (upperBound : Fin rankWidth → Bool) {output input : Fin (Sorting.networkBits depth rankWidth) → Bool} (recordsPermute : Sorting.FlatRecordsPermute output input) : (inRangeRankIndices upperBound output).card = (inRangeRankIndices upperBound input).card

Permuting complete packed rank records preserves the number of non-sentinel records.

theorem Algebraic.MassProduction.LeastMissing.exists_missing_of_inRange_capacity {rankWidth depth : ℕ} (upperBound : Fin rankWidth → Bool) (input : Fin (Sorting.networkBits depth rankWidth) → Bool) (capacity : (inRangeRankIndices upperBound input).card < Nat.card { rank : Lex (Fin rankWidth → Bool) // rank < toLex upperBound }) : ∃ (missing : Fin rankWidth → Bool), toLex missing < toLex upperBound ∧ ∀ (index : Fin (Sorting.networkRecords depth)), missing ≠ rankAt input index

A missing rank exists whenever the number of non-sentinel input records is smaller than the valid rank interval.

theorem Algebraic.MassProduction.LeastMissing.exists_missing_of_capacity {rankWidth depth : ℕ} (upperBound : Fin rankWidth → Bool) (input : Fin (Sorting.networkBits depth rankWidth) → Bool) (capacity : Sorting.networkRecords depth < Nat.card { rank : Lex (Fin rankWidth → Bool) // rank < toLex upperBound }) : ∃ (missing : Fin rankWidth → Bool), toLex missing < toLex upperBound ∧ ∀ (index : Fin (Sorting.networkRecords depth)), missing ≠ rankAt input index

If the strict interval below upperBound has more ranks than the packed array has records, then some rank in that interval is absent from the array.

theorem Algebraic.MassProduction.LeastMissing.flatRecordsPermute_exists_output_for_input {depth recordWidth : ℕ} {output input : Fin (Sorting.networkBits depth recordWidth) → Bool} (recordsPermute : Sorting.FlatRecordsPermute output input) (inputIndex : Fin (Sorting.networkRecords depth)) : ∃ (outputIndex : Fin (Sorting.networkRecords depth)), Sorting.flatRecords output outputIndex = Sorting.flatRecords input inputIndex

theorem Algebraic.MassProduction.LeastMissing.flatRecordsPermute_exists_input_for_output {depth recordWidth : ℕ} {output input : Fin (Sorting.networkBits depth recordWidth) → Bool} (recordsPermute : Sorting.FlatRecordsPermute output input) (outputIndex : Fin (Sorting.networkRecords depth)) : ∃ (inputIndex : Fin (Sorting.networkRecords depth)), Sorting.flatRecords output outputIndex = Sorting.flatRecords input inputIndex

theorem Algebraic.MassProduction.LeastMissing.leastMissingBits_sound_of_exists_candidate {rankWidth : ℕ} (upperBound : Fin rankWidth → Bool) (depth : ℕ) (input : Fin (Sorting.networkBits depth rankWidth) → Bool) (sorted : Sorting.FlatKeysSorted ⋯ true input) (existsCandidate : ∃ (record : Fin (Sorting.networkRecords depth)), candidateFlag upperBound input record = true) : toLex (leastMissingBits upperBound depth input) < toLex upperBound ∧ ∀ (index : Fin (Sorting.networkRecords depth)), leastMissingBits upperBound depth input ≠ rankAt input index

If candidate generation finds any valid gap, the selector returns one valid missing rank.

theorem Algebraic.MassProduction.LeastMissing.leastMissingBits_sound_of_capacity {rankWidth : ℕ} (upperBound : Fin rankWidth → Bool) (depth : ℕ) (input : Fin (Sorting.networkBits depth rankWidth) → Bool) (sorted : Sorting.FlatKeysSorted ⋯ true input) (capacity : Sorting.networkRecords depth < Nat.card { rank : Lex (Fin rankWidth → Bool) // rank < toLex upperBound }) : toLex (leastMissingBits upperBound depth input) < toLex upperBound ∧ ∀ (index : Fin (Sorting.networkRecords depth)), leastMissingBits upperBound depth input ≠ rankAt input index

Cardinality closes the selector's candidate-existence premise: whenever the strict rank interval below the upper bound is larger than the input array, the selected output is a missing in-range rank.

theorem Algebraic.MassProduction.LeastMissing.leastMissingBits_sound_of_inRange_capacity {rankWidth : ℕ} (upperBound : Fin rankWidth → Bool) (depth : ℕ) (input : Fin (Sorting.networkBits depth rankWidth) → Bool) (sorted : Sorting.FlatKeysSorted ⋯ true input) (capacity : (inRangeRankIndices upperBound input).card < Nat.card { rank : Lex (Fin rankWidth → Bool) // rank < toLex upperBound }) : toLex (leastMissingBits upperBound depth input) < toLex upperBound ∧ ∀ (index : Fin (Sorting.networkRecords depth)), leastMissingBits upperBound depth input ≠ rankAt input index

Sentinel-aware selector correctness. Only records whose ranks are below upperBound count against the available rank interval.

@[reducible]

def Algebraic.MassProduction.LeastMissing.leastMissingGateCount {rankWidth : ℕ} (upperBound : Fin rankWidth → Bool) (depth : ℕ) : ℕ

Total gate count of the candidate generator followed by its selector sort.

Equations

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

def Algebraic.MassProduction.LeastMissing.leastMissingCircuit {rankWidth : ℕ} (upperBound : Fin rankWidth → Bool) (depth : ℕ) : Circuit DeMorgan.signature (Sorting.networkBits depth rankWidth) rankWidth

Explicit least-missing-rank circuit for an already sorted rank array.

Equations

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

@[simp]

theorem Algebraic.MassProduction.LeastMissing.leastMissingCircuit_size {rankWidth : ℕ} (upperBound : Fin rankWidth → Bool) (depth : ℕ) : (leastMissingCircuit upperBound depth).size = leastMissingGateCount upperBound depth

@[simp]

theorem Algebraic.MassProduction.LeastMissing.leastMissingCircuit_eval {rankWidth : ℕ} (upperBound : Fin rankWidth → Bool) (depth : ℕ) (input : Fin (Sorting.networkBits depth rankWidth) → Bool) : (leastMissingCircuit upperBound depth).eval DeMorgan.interpretation input = leastMissingBits upperBound depth input

theorem Algebraic.MassProduction.LeastMissing.leastMissingCircuit_sound_of_exists_candidate {rankWidth : ℕ} (upperBound : Fin rankWidth → Bool) (depth : ℕ) (input : Fin (Sorting.networkBits depth rankWidth) → Bool) (sorted : Sorting.FlatKeysSorted ⋯ true input) (existsCandidate : ∃ (record : Fin (Sorting.networkRecords depth)), candidateFlag upperBound input record = true) : toLex ((leastMissingCircuit upperBound depth).eval DeMorgan.interpretation input) < toLex upperBound ∧ ∀ (index : Fin (Sorting.networkRecords depth)), (leastMissingCircuit upperBound depth).eval DeMorgan.interpretation input ≠ rankAt input index

Circuit-level form of least-missing soundness.

theorem Algebraic.MassProduction.LeastMissing.leastMissingCircuit_sound_of_capacity {rankWidth : ℕ} (upperBound : Fin rankWidth → Bool) (depth : ℕ) (input : Fin (Sorting.networkBits depth rankWidth) → Bool) (sorted : Sorting.FlatKeysSorted ⋯ true input) (capacity : Sorting.networkRecords depth < Nat.card { rank : Lex (Fin rankWidth → Bool) // rank < toLex upperBound }) : toLex ((leastMissingCircuit upperBound depth).eval DeMorgan.interpretation input) < toLex upperBound ∧ ∀ (index : Fin (Sorting.networkRecords depth)), (leastMissingCircuit upperBound depth).eval DeMorgan.interpretation input ≠ rankAt input index

Circuit-level least-missing correctness under the finite-capacity hypothesis used by the scheduler.

theorem Algebraic.MassProduction.LeastMissing.leastMissingCircuit_sound_of_inRange_capacity {rankWidth : ℕ} (upperBound : Fin rankWidth → Bool) (depth : ℕ) (input : Fin (Sorting.networkBits depth rankWidth) → Bool) (sorted : Sorting.FlatKeysSorted ⋯ true input) (capacity : (inRangeRankIndices upperBound input).card < Nat.card { rank : Lex (Fin rankWidth → Bool) // rank < toLex upperBound }) : toLex ((leastMissingCircuit upperBound depth).eval DeMorgan.interpretation input) < toLex upperBound ∧ ∀ (index : Fin (Sorting.networkRecords depth)), (leastMissingCircuit upperBound depth).eval DeMorgan.interpretation input ≠ rankAt input index

Circuit-level sentinel-aware least-missing correctness.

def Algebraic.MassProduction.LeastMissing.expressionBitsLessCostBound (width bitCost : ℕ) : ℕ

A uniform polynomial bound for comparing expression bit strings whose individual bit expressions cost at most bitCost.

Equations

• Algebraic.MassProduction.LeastMissing.expressionBitsLessCostBound width bitCost = width * (width * (4 * bitCost + 6) + 2 * bitCost + 3) + width

theorem Algebraic.MassProduction.LeastMissing.expressionBitsLess_standardCost_le {width n : ℕ} (left right : Fin width → DeMorgan.Expression n) (bitCost : ℕ) (leftCost : ∀ (bit : Fin width), (left bit).standardCost ≤ bitCost) (rightCost : ∀ (bit : Fin width), (right bit).standardCost ≤ bitCost) : (expressionBitsLess width left right).standardCost ≤ expressionBitsLessCostBound width bitCost

theorem Algebraic.MassProduction.LeastMissing.incrementRankBitExpression_standardCost_le {depth rankWidth : ℕ} (record : Fin (Sorting.networkRecords depth)) (bit : Fin rankWidth) : (incrementRankBitExpression depth rankWidth record bit).standardCost ≤ 2 * rankWidth + 4

def Algebraic.MassProduction.LeastMissing.candidateOutputCostBound (rankWidth : ℕ) : ℕ

Uniform polynomial cost per generated candidate output.

Equations

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

theorem Algebraic.MassProduction.LeastMissing.zeroCandidateExpression_standardCost_le {rankWidth : ℕ} (upperBound : Fin rankWidth → Bool) (depth : ℕ) (record : Fin (Sorting.networkRecords depth)) : (zeroCandidateExpression upperBound depth record).standardCost ≤ 2 * expressionBitsLessCostBound rankWidth 0 + 1

theorem Algebraic.MassProduction.LeastMissing.successorCandidateExpression_standardCost_le {rankWidth : ℕ} (upperBound : Fin rankWidth → Bool) (depth : ℕ) (record : Fin (Sorting.networkRecords depth)) : (successorCandidateExpression upperBound depth record).standardCost ≤ 3 * expressionBitsLessCostBound rankWidth (2 * rankWidth + 4) + 2

theorem Algebraic.MassProduction.LeastMissing.candidateRecordBitExpression_standardCost_le {rankWidth : ℕ} (upperBound : Fin rankWidth → Bool) (depth : ℕ) (output : Fin (Sorting.networkBits depth (candidateRecordWidth rankWidth))) : (candidateRecordBitExpression upperBound depth output).standardCost ≤ candidateOutputCostBound rankWidth

theorem Algebraic.MassProduction.LeastMissing.candidateRecordsCircuit_cost_le {rankWidth : ℕ} (upperBound : Fin rankWidth → Bool) (depth : ℕ) : (candidateRecordsCircuit upperBound depth).cost DeMorgan.standardCost ≤ Sorting.networkBits depth (candidateRecordWidth rankWidth) * candidateOutputCostBound rankWidth

Candidate generation is linear in the record count and polynomial in rank width.

theorem Algebraic.MassProduction.LeastMissing.leastMissingCircuit_cost_le {rankWidth : ℕ} (upperBound : Fin rankWidth → Bool) (depth : ℕ) : (leastMissingCircuit upperBound depth).cost DeMorgan.standardCost ≤ Sorting.networkBits depth (candidateRecordWidth rankWidth) * candidateOutputCostBound rankWidth + depth * depth * Sorting.networkRecords depth * (2 * candidateRecordWidth rankWidth * (2 * (1 * (6 * 1 + 4)) + 4))

Complete gate ledger for candidate generation and validity selection.