Arbitrary-base lexicographic tuple numbering

The first coordinate is most significant, as required by Immerman's ordered first-order queries. Coordinate reversal converts the existing colexicographic tuple numbering to this convention. For every base n and dimension k, the resulting map is a bijection with Fin (n ^ k); its order agrees with Mathlib's Pi.Lex. No power-of-two restriction or binary concatenation is used. The standard canonical constants use n ≥ 2, and the tuple for one needs positive dimension. The zero-dimensional universe still has one element.

This numbers the full tuple universe; native tuple BIT is constructed in Ordered.TupleBit. Numeric-preserving full-tuple composition is supplied in Ordered.FullTuple.Composition. Numeric predicates on restricted domains require separate constructions.

Main definitions

• Cslib.Logic.FO.Ordered.lexEquiv: first-coordinate-most-significant tuple numbering.
• Cslib.Logic.FO.Ordered.lexRank: the natural-number rank of a tuple.
• Cslib.Logic.FO.Ordered.tupleZero, Cslib.Logic.FO.Ordered.tupleOne, Cslib.Logic.FO.Ordered.tupleMax: the canonical full-domain tuples.

Main results

• Cslib.Logic.FO.Ordered.lexRank_lt_iff: order is determined by the first differing coordinate.
• Cslib.Logic.FO.Ordered.lexRank_lt_iff_lex: agreement with Mathlib's lexicographic relation.
• Cslib.Logic.FO.Ordered.lexRank_comp_lt_lexRank_comp_iff: increasing maps of coordinates preserve lexicographic order.
• Cslib.Logic.FO.Ordered.lexRank_tupleZero, Cslib.Logic.FO.Ordered.lexRank_tupleOne, Cslib.Logic.FO.Ordered.lexRank_tupleMax: exact canonical ranks.

References

• N. Immerman, Descriptive Complexity, Remark 1.32 and Exercise 1.33(1), with the full-domain hypothesis. Ordered.TupleBit supplies Exercise 1.33(3).

def Cslib.Logic.FO.Ordered.lexEquiv {n k : ℕ} : (Fin k → Fin n) ≃ Fin (n ^ k)

Number full tuples in arbitrary base, with the first coordinate most significant.

def Cslib.Logic.FO.Ordered.lexRank {n k : ℕ} (x : Fin k → Fin n) : ℕ

The natural-number rank of a tuple in lexicographic order.

theorem Cslib.Logic.FO.Ordered.lexRank_eq_tupleIndex {n k : ℕ} (x : Fin k → Fin n) : lexRank x = tupleIndex (x ∘ Fin.rev)

Lexicographic rank is the existing colexicographic index after coordinate reversal.

theorem Cslib.Logic.FO.Ordered.lexRank_apply {n k : ℕ} (x : Fin k → Fin n) : lexRank x = ∑ i : Fin k, ↑(x i) * n ^ ↑i.rev

Digit i has weight n ^ (k - 1 - i); i.rev is that reversed position.

theorem Cslib.Logic.FO.Ordered.lexEquiv_symm_apply_val {n k : ℕ} (r : Fin (n ^ k)) (i : Fin k) : ↑(lexEquiv.symm r i) = ↑r / n ^ ↑i.rev % n

Decode a lexicographic rank by division and remainder in the original base.

theorem Cslib.Logic.FO.Ordered.lexRank_lt {n k : ℕ} (x : Fin k → Fin n) : lexRank x < n ^ k

theorem Cslib.Logic.FO.Ordered.lexRank_injective {n k : ℕ} : Function.Injective lexRank

theorem Cslib.Logic.FO.Ordered.lexRank_lt_iff {n k : ℕ} (x y : Fin k → Fin n) : lexRank x < lexRank y ↔ ∃ (i : Fin k), x i < y i ∧ ∀ j < i, x j = y j

Numerical order agrees with the first coordinate at which the tuples differ.

theorem Cslib.Logic.FO.Ordered.lexRank_lt_iff_lex {n k : ℕ} (x y : Fin k → Fin n) : lexRank x < lexRank y ↔ Pi.Lex (fun (x1 x2 : Fin k) => x1 < x2) (fun {i : Fin k} (x1 x2 : Fin n) => x1 < x2) x y

The canonical numbering agrees with Mathlib's lexicographic relation.

theorem Cslib.Logic.FO.Ordered.lexRank_comp_lt_lexRank_comp_iff {n n' k : ℕ} {f : Fin n → Fin n'} (hf : StrictMono f) (x y : Fin k → Fin n) : lexRank (f ∘ x) < lexRank (f ∘ y) ↔ lexRank x < lexRank y

Applying an increasing map to every coordinate preserves lexicographic order.

def Cslib.Logic.FO.Ordered.tupleZero {n k : ℕ} [Fact (2 ≤ n)] : Fin k → Fin n

The all-zero tuple.

def Cslib.Logic.FO.Ordered.tupleOne {n k : ℕ} [Fact (2 ≤ n)] : Fin (k + 1) → Fin n

The tuple whose last coordinate is one and whose other coordinates are zero.

def Cslib.Logic.FO.Ordered.tupleMax {n k : ℕ} [Fact (2 ≤ n)] : Fin k → Fin n

The tuple with every coordinate at its maximum.

theorem Cslib.Logic.FO.Ordered.lexRank_tupleZero {n k : ℕ} [Fact (2 ≤ n)] : lexRank tupleZero = 0

The all-zero tuple has rank 0.

theorem Cslib.Logic.FO.Ordered.lexRank_tupleOne {n k : ℕ} [Fact (2 ≤ n)] : lexRank tupleOne = 1

The tuple with last coordinate one and the others zero has rank 1.

theorem Cslib.Logic.FO.Ordered.lexRank_tupleMax {n k : ℕ} [Fact (2 ≤ n)] : lexRank tupleMax = n ^ k - 1

The tuple of maximal coordinates has the largest rank, n ^ k - 1.