Semantic model of Batcher sorting networks

This is the record-level semantic layer used to prove that the explicit Boolean circuit sorts complete records by a projected key.

def Algebraic.MassProduction.Sorting.Semantics.SequenceBitonic {α : Type u_1} {n : ℕ} [LinearOrder α] (sequence : Fin n → α) : Prop

Four-point lattice characterization of a bitonic sequence.

Equations

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

def Algebraic.MassProduction.Sorting.Semantics.SequenceIncreasing {α : Type u_1} [LE α] {n : ℕ} (sequence : Fin n → α) : Prop

A sequence is increasing in its index order.

Equations

• Algebraic.MassProduction.Sorting.Semantics.SequenceIncreasing sequence = ∀ (i j : Fin n), i < j → sequence i ≤ sequence j

def Algebraic.MassProduction.Sorting.Semantics.SequenceDecreasing {α : Type u_1} [LE α] {n : ℕ} (sequence : Fin n → α) : Prop

A sequence is decreasing in its index order.

Equations

• Algebraic.MassProduction.Sorting.Semantics.SequenceDecreasing sequence = ∀ (i j : Fin n), i < j → sequence j ≤ sequence i

def Algebraic.MassProduction.Sorting.Semantics.SequenceSorted {α : Type u_1} [LE α] {n : ℕ} (ascending : Bool) (sequence : Fin n → α) : Prop

Sortedness in the selected direction.

Equations

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

def Algebraic.MassProduction.Sorting.Semantics.SequenceAllLE {α : Type u_1} [LE α] {n m : ℕ} (first : Fin n → α) (second : Fin m → α) : Prop

Every value of the first sequence is at most every value of the second.

Equations

• Algebraic.MassProduction.Sorting.Semantics.SequenceAllLE first second = ∀ (i : Fin n) (j : Fin m), first i ≤ second j

def Algebraic.MassProduction.Sorting.Semantics.SequenceRangeContained {α : Sort u_1} {n m : ℕ} (output : Fin n → α) (input : Fin m → α) : Prop

Every output value occurs somewhere in the input sequence.

Equations

• Algebraic.MassProduction.Sorting.Semantics.SequenceRangeContained output input = ∀ (i : Fin n), ∃ (j : Fin m), output i = input j

def Algebraic.MassProduction.Sorting.Semantics.SequencePermutes {α : Type u_1} {n : ℕ} (output input : Fin n → α) : Prop

The output sequence is a permutation of the input sequence.

Equations

• Algebraic.MassProduction.Sorting.Semantics.SequencePermutes output input = (List.ofFn output).Perm (List.ofFn input)

def Algebraic.MassProduction.Sorting.Semantics.UniqueIndexWhere {n : ℕ} {α : Sort u_1} (sequence : Fin n → α) (predicate : α → Prop) : Prop

Exactly one position of a finite sequence satisfies a predicate.

Equations

• Algebraic.MassProduction.Sorting.Semantics.UniqueIndexWhere sequence predicate = ∃ (index : Fin n), predicate (sequence index) ∧ ∀ (other : Fin n), predicate (sequence other) → other = index

noncomputable def Algebraic.MassProduction.Sorting.Semantics.matchingIndices {n : ℕ} {α : Sort u_1} (sequence : Fin n → α) (predicate : α → Prop) : Finset (Fin n)

The positions of a finite sequence satisfying a predicate. Classical decidability is confined to the value of this definition.

Equations

• Algebraic.MassProduction.Sorting.Semantics.matchingIndices sequence predicate = {index : Fin n | predicate (sequence index)}

noncomputable def Algebraic.MassProduction.Sorting.Semantics.predicateBit {α : Sort u_1} (predicate : α → Prop) (value : α) : Bool

Boolean reflection of a predicate, with the chosen decision procedure kept out of theorem signatures.

Equations

• Algebraic.MassProduction.Sorting.Semantics.predicateBit predicate value = decide (predicate value)

theorem Algebraic.MassProduction.Sorting.Semantics.UniqueIndexWhere.iff_matchingIndices_card_eq_one {n : ℕ} {α : Sort u_1} (sequence : Fin n → α) (predicate : α → Prop) : UniqueIndexWhere sequence predicate ↔ (matchingIndices sequence predicate).card = 1

Unique satisfaction is equivalent to the matching-position set having cardinality one.

theorem Algebraic.MassProduction.Sorting.Semantics.countP_predicateBit_eq_matchingIndices_card {n : ℕ} {α : Type u_1} (sequence : Fin n → α) (predicate : α → Prop) : List.countP (predicateBit predicate) (List.ofFn sequence) = (matchingIndices sequence predicate).card

Counting true predicate bits agrees with counting matching positions.

theorem Algebraic.MassProduction.Sorting.Semantics.SequenceRangeContained.trans {α : Sort u_1} {n m k : ℕ} {first : Fin n → α} {second : Fin m → α} {third : Fin k → α} (hfirst : SequenceRangeContained first second) (hsecond : SequenceRangeContained second third) : SequenceRangeContained first third

Range containment is transitive.

theorem Algebraic.MassProduction.Sorting.Semantics.SequencePermutes.refl {α : Type u_1} {n : ℕ} (input : Fin n → α) : SequencePermutes input input

Every finite sequence is a permutation of itself.

theorem Algebraic.MassProduction.Sorting.Semantics.SequencePermutes.trans {α : Type u_1} {n : ℕ} {first second third : Fin n → α} (hfirst : SequencePermutes first second) (hsecond : SequencePermutes second third) : SequencePermutes first third

Sequence permutation is transitive.

theorem Algebraic.MassProduction.Sorting.Semantics.SequencePermutes.map {α : Type u_1} {β : Type u_2} {n : ℕ} {output input : Fin n → α} (observe : α → β) (permuted : SequencePermutes output input) : SequencePermutes (fun (index : Fin n) => observe (output index)) fun (index : Fin n) => observe (input index)

Applying the same observation to two permuted finite sequences preserves their permutation relation.

theorem Algebraic.MassProduction.Sorting.Semantics.SequencePermutes.rangeContained {α : Type u_1} {n : ℕ} {output input : Fin n → α} (permuted : SequencePermutes output input) : SequenceRangeContained output input

Every output of a finite-sequence permutation is an input value.

theorem Algebraic.MassProduction.Sorting.Semantics.SequencePermutes.matchingIndices_card_eq {α : Type u_1} {n : ℕ} {output input : Fin n → α} (permuted : SequencePermutes output input) (predicate : α → Prop) : (matchingIndices output predicate).card = (matchingIndices input predicate).card

A permutation preserves the number of positions satisfying a predicate.

theorem Algebraic.MassProduction.Sorting.Semantics.UniqueIndexWhere.of_sequencePermutes {n : ℕ} {α : Type u_1} {output input : Fin n → α} {predicate : α → Prop} (permuted : SequencePermutes output input) (uniqueInput : UniqueIndexWhere input predicate) : UniqueIndexWhere output predicate

A sequence permutation preserves unique satisfaction of a predicate.

theorem Algebraic.MassProduction.Sorting.Semantics.UniqueIndexWhere.cast {leftCount : ℕ} {α : Sort u_1} {rightCount : ℕ} {sequence : Fin leftCount → α} {predicate : α → Prop} (unique : UniqueIndexWhere sequence predicate) (countEquality : leftCount = rightCount) : UniqueIndexWhere (fun (index : Fin rightCount) => sequence (Fin.cast ⋯ index)) predicate

Reindexing a finite sequence along an equality of lengths preserves its unique matching position.

theorem Algebraic.MassProduction.Sorting.Semantics.matchingIndices_cast_card {leftCount : ℕ} {α : Sort u_1} {rightCount : ℕ} (sequence : Fin leftCount → α) (predicate : α → Prop) (countEquality : leftCount = rightCount) : (matchingIndices (fun (index : Fin rightCount) => sequence (Fin.cast ⋯ index)) predicate).card = (matchingIndices sequence predicate).card

Reindexing a finite sequence along an equality of lengths preserves the number of matching positions.

def Algebraic.MassProduction.Sorting.Semantics.appendSequence {α : Sort u_1} {n m : ℕ} (first : Fin n → α) (second : Fin m → α) : Fin (n + m) → α

Concatenation of two finite sequences.

Equations

• Algebraic.MassProduction.Sorting.Semantics.appendSequence first second = Fin.append first second

theorem Algebraic.MassProduction.Sorting.Semantics.UniqueIndexWhere.append_left {leftCount : ℕ} {α : Sort u_1} {rightCount : ℕ} {left : Fin leftCount → α} {right : Fin rightCount → α} {predicate : α → Prop} (uniqueLeft : UniqueIndexWhere left predicate) (noneRight : ∀ (index : Fin rightCount), ¬predicate (right index)) : UniqueIndexWhere (Fin.append left right) predicate

A unique match in the left sequence remains unique after appending a right sequence with no matches.

theorem Algebraic.MassProduction.Sorting.Semantics.UniqueIndexWhere.append_right {leftCount : ℕ} {α : Sort u_1} {rightCount : ℕ} {left : Fin leftCount → α} {right : Fin rightCount → α} {predicate : α → Prop} (noneLeft : ∀ (index : Fin leftCount), ¬predicate (left index)) (uniqueRight : UniqueIndexWhere right predicate) : UniqueIndexWhere (Fin.append left right) predicate

A unique match in the right sequence remains unique after prepending a left sequence with no matches.

theorem Algebraic.MassProduction.Sorting.Semantics.matchingIndices_append_card {leftCount rightCount : ℕ} {α : Type u_1} (left : Fin leftCount → α) (right : Fin rightCount → α) (predicate : α → Prop) : (matchingIndices (Fin.append left right) predicate).card = (matchingIndices left predicate).card + (matchingIndices right predicate).card

Matching positions in an appended sequence split additively.

theorem Algebraic.MassProduction.Sorting.Semantics.matchingIndices_lt_card_eq_index {κ : Type u_1} {n : ℕ} [LinearOrder κ] (sequence : Fin n → κ) (increasing : SequenceIncreasing sequence) (index : Fin n) (unique : ∀ (other : Fin n), sequence other = sequence index → other = index) : (matchingIndices sequence fun (value : κ) => value < sequence index).card = ↑index

In an increasing sequence, the index of a unique value equals the number of sequence entries strictly below it.

theorem Algebraic.MassProduction.Sorting.Semantics.SequencePermutes.append {α : Type u_1} {n m : ℕ} {first firstInput : Fin n → α} {second secondInput : Fin m → α} (hfirst : SequencePermutes first firstInput) (hsecond : SequencePermutes second secondInput) : SequencePermutes (appendSequence first second) (appendSequence firstInput secondInput)

Concatenating two pairs of permuted sequences preserves permutation.

def Algebraic.MassProduction.Sorting.Semantics.pointwiseMin {α : Type u_1} [LinearOrder α] {n : ℕ} (first second : Fin n → α) : Fin n → α

Pointwise minimum of equal-length sequences.

Equations

• Algebraic.MassProduction.Sorting.Semantics.pointwiseMin first second i = min (first i) (second i)

def Algebraic.MassProduction.Sorting.Semantics.pointwiseMax {α : Type u_1} [LinearOrder α] {n : ℕ} (first second : Fin n → α) : Fin n → α

Pointwise maximum of equal-length sequences.

Equations

• Algebraic.MassProduction.Sorting.Semantics.pointwiseMax first second i = max (first i) (second i)

def Algebraic.MassProduction.Sorting.Semantics.recordFirstHalf {α : Sort u_1} {depth : ℕ} (input : Fin (networkRecords (depth + 1)) → α) : Fin (networkRecords depth) → α

First half of a record-level network sequence.

Equations

• Algebraic.MassProduction.Sorting.Semantics.recordFirstHalf input index = input (Fin.castAdd (Algebraic.MassProduction.Sorting.networkRecords depth) index)

def Algebraic.MassProduction.Sorting.Semantics.recordSecondHalf {α : Sort u_1} {depth : ℕ} (input : Fin (networkRecords (depth + 1)) → α) : Fin (networkRecords depth) → α

Second half of a record-level network sequence.

Equations

• Algebraic.MassProduction.Sorting.Semantics.recordSecondHalf input index = input (Fin.natAdd (Algebraic.MassProduction.Sorting.networkRecords depth) index)

def Algebraic.MassProduction.Sorting.Semantics.joinRecordHalves {α : Sort u_1} {depth : ℕ} (first second : Fin (networkRecords depth) → α) : Fin (networkRecords (depth + 1)) → α

Join two record-level half sequences.

Equations

• Algebraic.MassProduction.Sorting.Semantics.joinRecordHalves first second = Fin.append first second

theorem Algebraic.MassProduction.Sorting.Semantics.appendSequence_eq_joinRecordHalves {α : Sort u_1} {depth : ℕ} (first second : Fin (networkRecords depth) → α) : appendSequence first second = joinRecordHalves first second

The record-specific and general sequence append operations agree.

def Algebraic.MassProduction.Sorting.Semantics.orderedCompareLayer {α : Type u_1} [LinearOrder α] (depth : ℕ) (ascending : Bool) (input : Fin (networkRecords (depth + 1)) → α) : Fin (networkRecords (depth + 1)) → α

One record-level butterfly layer over a linear order.

Equations

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

def Algebraic.MassProduction.Sorting.Semantics.orderedBitonicMerge {α : Type u_1} [LinearOrder α] (depth : ℕ) : Bool → (Fin (networkRecords depth) → α) → Fin (networkRecords depth) → α

Record-level bitonic merge over a linear order.

Equations

• One or more equations did not get rendered due to their size.
• Algebraic.MassProduction.Sorting.Semantics.orderedBitonicMerge 0 x✝ input = input

def Algebraic.MassProduction.Sorting.Semantics.orderedBitonicSort {α : Type u_1} [LinearOrder α] (depth : ℕ) : Bool → (Fin (networkRecords depth) → α) → Fin (networkRecords depth) → α

Record-level Batcher sorter over a linear order.

Equations

• One or more equations did not get rendered due to their size.
• Algebraic.MassProduction.Sorting.Semantics.orderedBitonicSort 0 x✝ input = input

noncomputable def Algebraic.MassProduction.Sorting.Semantics.keyedCompareSource {κ : Type u_1} {α : Sort u_2} [LinearOrder κ] (key : α → κ) (depth : ℕ) (ascending : Bool) (input : Fin (networkRecords (depth + 1)) → α) (output : Fin (networkRecords (depth + 1))) : Fin (networkRecords (depth + 1))

Source record selected for one output of a keyed compare layer.

Equations

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

noncomputable def Algebraic.MassProduction.Sorting.Semantics.keyedCompareLayer {κ : Type u_1} {α : Sort u_2} [LinearOrder κ] (key : α → κ) (depth : ℕ) (ascending : Bool) (input : Fin (networkRecords (depth + 1)) → α) : Fin (networkRecords (depth + 1)) → α

One compare layer on records ordered only through a separate key.

Equations

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

noncomputable def Algebraic.MassProduction.Sorting.Semantics.keyedBitonicMerge {κ : Type u_1} {α : Sort u_2} [LinearOrder κ] (key : α → κ) (depth : ℕ) : Bool → (Fin (networkRecords depth) → α) → Fin (networkRecords depth) → α

Keyed record-level bitonic merge.

Equations

• One or more equations did not get rendered due to their size.
• Algebraic.MassProduction.Sorting.Semantics.keyedBitonicMerge key 0 x✝ input = input

noncomputable def Algebraic.MassProduction.Sorting.Semantics.keyedBitonicSort {κ : Type u_1} {α : Sort u_2} [LinearOrder κ] (key : α → κ) (depth : ℕ) : Bool → (Fin (networkRecords depth) → α) → Fin (networkRecords depth) → α

Keyed record-level Batcher sorter.

Equations

• One or more equations did not get rendered due to their size.
• Algebraic.MassProduction.Sorting.Semantics.keyedBitonicSort key 0 x✝ input = input