What a comparison loop decides

The two remaining atom kinds of a step matrix – equality and order of two points – are the ones the machine settles by comparing two argument blocks. It cannot look at a block value as a whole: it walks the cells its marks name, one canonically padded tuple at a time, reading one bit from each of the two blocks (a paired read, which is why these are element loops and not file tests). This file says that this is enough.

• DescriptiveComplexity.Draw.Data.encMap_eq_iff_padBits – two encodings are equal exactly when they agree at every padded tuple, because an encoding is supported on padded tuples (DescriptiveComplexity.Draw.Data.isPad_of_encMap) and the encoding is injective. So the equality atom is the loop found no difference.
• DescriptiveComplexity.Draw.Data.wmSetLe_encMap_iff_padBits – the binary order of two encodings is decided at the lexicographically least padded tuple where they differ, the second block containing it. So the order atom is the loop's first difference, which is why the loop keeps the first verdict rather than the last.
• DescriptiveComplexity.Draw.Data.encOrder_le_iff_padBits reads the same through the order the reduction puts on the points (DescriptiveComplexity.Draw.encOrder), which is where an order atom of the matrix actually lives.

The bridge underneath is padLt_iff: padding is an order embedding of the dd₀-tuples the control enumerates into the dd-tuples the cells are, since two padded tuples agree beyond dd₀ and so are compared inside it.

Padding is an order embedding

theorem DescriptiveComplexity.Draw.Data.padLt_iff {L : FirstOrder.Language} {dt : Data L} {A : Type} [LinearOrder A] (zero : A) (w w' : Fin dt.dd0 → A) : (∃ (p : Fin dt.dd), (∀ j < p, pad zero w j = pad zero w' j) ∧ pad zero w p < pad zero w' p) ↔ ∃ (p : Fin dt.dd0), (∀ j < p, w j = w' j) ∧ w p < w' p

Two padded tuples compare inside the coordinates they carry: they agree beyond dd₀, so the lexicographic comparison is settled before it.

theorem DescriptiveComplexity.Draw.Data.wmLt_tupLeLex_iff' {L : FirstOrder.Language} {dt : Data L} {A : Type} [LinearOrder A] (x y : Fin dt.dd → A) : WMLt tupLeLex x y ↔ ∃ (p : Fin dt.dd), (∀ j < p, x j = y j) ∧ x p < y p

The strict order the address layer reads on tuples, spelled out.

What the loop sees of a block value

noncomputable def DescriptiveComplexity.Draw.Data.padBits {L : FirstOrder.Language} (dt : Data L) {A : Type} (zero : A) (S : (Fin dt.dd → A) → Prop) (w : Fin dt.dd0 → A) : Prop

The bits of a block value the loops can read: its membership question at the canonically padded tuple of each dd₀-tuple – the cells the marks name.

Equations

• dt.padBits zero S w = S (DescriptiveComplexity.Draw.pad zero w)

theorem DescriptiveComplexity.Draw.Data.encMap_eq_padBits {L : FirstOrder.Language} {dt : Data L} {A : Type} [L.Structure A] [LinearOrder A] {zero one : A} {p q : dt.X.Map A} (h : ∀ (w : Fin dt.dd0 → A), dt.padBits zero (encMap dt.ly zero one p) w ↔ dt.padBits zero (encMap dt.ly zero one q) w) : encMap dt.ly zero one p = encMap dt.ly zero one q

An encoding is what its padded bits say: two encodings agreeing at every padded tuple agree everywhere, since neither holds off the padded tuples.

theorem DescriptiveComplexity.Draw.Data.encMap_eq_iff_padBits {L : FirstOrder.Language} {dt : Data L} {A : Type} [L.Structure A] [LinearOrder A] {zero one : A} (hzo : zero ≠ one) {p q : dt.X.Map A} : p = q ↔ ∀ (w : Fin dt.dd0 → A), dt.padBits zero (encMap dt.ly zero one p) w ↔ dt.padBits zero (encMap dt.ly zero one q) w

The equality atom is «the loop found no difference»: two points are equal exactly when their encodings agree at every cell the loop visits.

theorem DescriptiveComplexity.Draw.Data.wmSetLe_encMap_iff_padBits {L : FirstOrder.Language} {dt : Data L} {A : Type} [L.Structure A] [LinearOrder A] {zero one : A} {p q : dt.X.Map A} : WMSetLe tupLeLex (encMap dt.ly zero one p) (encMap dt.ly zero one q) ↔ (∀ (w : Fin dt.dd0 → A), dt.padBits zero (encMap dt.ly zero one p) w ↔ dt.padBits zero (encMap dt.ly zero one q) w) ∨ ∃ (w : Fin dt.dd0 → A), (∀ (w' : Fin dt.dd0 → A), (∃ (r : Fin dt.dd0), (∀ j < r, w' j = w j) ∧ w' r < w r) → (dt.padBits zero (encMap dt.ly zero one p) w' ↔ dt.padBits zero (encMap dt.ly zero one q) w')) ∧ ¬dt.padBits zero (encMap dt.ly zero one p) w ∧ dt.padBits zero (encMap dt.ly zero one q) w

The order atom is the loop's first difference: the binary order of two encodings is decided at the lexicographically least padded tuple where they differ.

theorem DescriptiveComplexity.Draw.Data.encOrder_le_iff_padBits {L : FirstOrder.Language} {dt : Data L} {A : Type} [L.Structure A] [LinearOrder A] [Finite A] {zero one : A} (hzo : zero ≠ one) (p q : dt.X.Map A) : p ≤ q ↔ (∀ (w : Fin dt.dd0 → A), dt.padBits zero (encMap dt.ly zero one p) w ↔ dt.padBits zero (encMap dt.ly zero one q) w) ∨ ∃ (w : Fin dt.dd0 → A), (∀ (w' : Fin dt.dd0 → A), (∃ (r : Fin dt.dd0), (∀ j < r, w' j = w j) ∧ w' r < w r) → (dt.padBits zero (encMap dt.ly zero one p) w' ↔ dt.padBits zero (encMap dt.ly zero one q) w')) ∧ ¬dt.padBits zero (encMap dt.ly zero one p) w ∧ dt.padBits zero (encMap dt.ly zero one q) w

The order atom, in the order the reduction chose: the comparison the loop runs is exactly the order the points carry (DescriptiveComplexity.Draw.encOrder).