The order the reduction puts on the points

DescriptiveComplexity.PFPDefinable quantifies over every linear order on the expanded universe, so the EXPSPACE reduction may choose the one its machine can compare: the pullback of the binary block-value order along the encoding (DescriptiveComplexity.Draw.encOrder). An order atom on two points is then exactly the comparison of their encodings in the machine's own reading – DescriptiveComplexity.WMSetLe at the lexicographic order on tuples, the order the register file walks – which is DescriptiveComplexity.Draw.encOrder_le_iff.

The junction between the two languages for orders on block values – the address layer's DescriptiveComplexity.WMSetLe tupLeLex and the library's DescriptiveComplexity.setLinearOrder – is DescriptiveComplexity.Draw.wmSetLe_iff_setLe: both say at the most significant differing tuple, the second contains it, with most significant = lexicographically least.

(The library's canonical order on the expanded universe, DescriptiveComplexity.ExpExpansion.mapLinearOrder, orders by tag first and padded atoms second; nothing here conflicts with it – the reduction simply instantiates the definition's order quantifier differently.)

The two readings of the binary order on block values

theorem DescriptiveComplexity.Draw.tupLeLex_iff_toLex_le {dd : ℕ} {A : Type} [LinearOrder A] (x y : Fin dd → A) : tupLeLex x y ↔ toLex x ≤ toLex y

The lexicographic comparison of tuples is the Lex order.

theorem DescriptiveComplexity.Draw.wmLt_tupLeLex_iff {dd : ℕ} {A : Type} [LinearOrder A] (x y : Fin dd → A) : WMLt tupLeLex x y ↔ toLex x < toLex y

The strict lexicographic comparison of tuples is the strict Lex order.

theorem DescriptiveComplexity.Draw.wmSetLe_iff_setLe {dd : ℕ} {A : Type} [LinearOrder A] [Finite A] (S T : (Fin dd → A) → Prop) : WMSetLe tupLeLex S T ↔ S ≤ T

The two readings of the binary order on block values agree: the address layer's DescriptiveComplexity.WMSetLe at the lexicographic tuple order is the library's DescriptiveComplexity.setLinearOrder on subsets of the Lex tuples.

The pulled-back order on the points

@[instance_reducible]

noncomputable def DescriptiveComplexity.Draw.encOrder {L : FirstOrder.Language} {X : ExpExpansion L} {dd : ℕ} (ly : EncLayout (PtCode X) (blockArityBound X.B) dd) {A : Type} [L.Structure A] [LinearOrder A] [Finite A] (zero one : A) (hne : zero ≠ one) : LinearOrder (X.Map A)

The order the reduction puts on the expanded universe: the pullback of the binary block-value order along the encoding. An order atom on two points is then the comparison of their encodings, which the machine can run on its register file.

Equations

• DescriptiveComplexity.Draw.encOrder ly zero one hne = LinearOrder.lift' (DescriptiveComplexity.Draw.encMap ly zero one) ⋯

theorem DescriptiveComplexity.Draw.encOrder_le_iff {L : FirstOrder.Language} {X : ExpExpansion L} {dd : ℕ} (ly : EncLayout (PtCode X) (blockArityBound X.B) dd) {A : Type} [L.Structure A] [LinearOrder A] [Finite A] (zero one : A) (hne : zero ≠ one) (m m' : X.Map A) : m ≤ m' ↔ WMSetLe tupLeLex (encMap ly zero one m) (encMap ly zero one m')

What the chosen order says: the machine's own comparison of the two encodings.