Uniqueness of sorted finite sequences #
A sorted permutation of an already sorted identifier sequence is pointwise equal to that sequence. Distinct identifiers therefore restore literal output positions after a data-dependent sorting pass.
theorem
Algebraic.MassProduction.Nonuniform.increasingPermutations_eq
{count : ℕ}
{Key : Type u_1}
[LinearOrder Key]
{left right : Fin count → Key}
(permuted : Sorting.Semantics.SequencePermutes left right)
(leftSorted : Sorting.Semantics.SequenceIncreasing left)
(rightSorted : Sorting.Semantics.SequenceIncreasing right)
:
Increasing permutations agree at every position, including repetitions.
theorem
Algebraic.MassProduction.Nonuniform.existsIndexPermutation
{count : ℕ}
{Record : Type u_1}
{output input : Fin count → Record}
(permuted : Sorting.Semantics.SequencePermutes output input)
(distinct : Function.Injective input)
:
∃ (indices : Equiv.Perm (Fin count)), ∀ (index : Fin count), output index = input (indices index)
When input records are distinct, a record permutation is realized by an actual permutation of positions. Identifiers provide this distinctness.
theorem
Algebraic.MassProduction.Nonuniform.restoredIndexPermutations
{count : ℕ}
{Record : Type u_1}
{Marked : Type u_2}
{Identifier : Type u_3}
[LinearOrder Identifier]
(body : Marked → Record)
(identifier : Record → Identifier)
(input sorted : Fin count → Record)
(marked output : Fin count → Marked)
(firstPermutes : Sorting.Semantics.SequencePermutes sorted input)
(bodyPreserved : ∀ (index : Fin count), body (marked index) = sorted index)
(lastPermutes : Sorting.Semantics.SequencePermutes output marked)
(initiallyOrdered : StrictMono fun (index : Fin count) => identifier (input index))
(finallyOrdered : Sorting.Semantics.SequenceIncreasing fun (index : Fin count) => identifier (body (output index)))
:
Sorting, attaching marks, and sorting by preserved distinct identifiers restore every original position. The two index permutations are inverse.