diff --git a/Complexity.lean b/Complexity.lean
index 9735d61c91..0663417417 100644
--- a/Complexity.lean
+++ b/Complexity.lean
@@ -1203,6 +1203,7 @@ public import Complexity.Computability.Complexity.CookLevin.Tableau
 public import Complexity.Computability.Complexity.Fagin.Converse
 public import Complexity.Computability.Complexity.Fagin.Layout
 public import Complexity.Computability.Complexity.Fagin.Ordered
+public import Complexity.Computability.Complexity.Fagin.Ordered.Verifier
 public import Complexity.Computability.Complexity.Fagin.Power
 public import Complexity.Computability.Complexity.Fagin.SAT
 public import Complexity.Computability.Complexity.Fagin.Small
@@ -1211,6 +1212,7 @@ public import Complexity.Computability.Complexity.Fagin.Tableau
 public import Complexity.Computability.Complexity.Fagin.Tableau.Defs
 public import Complexity.Computability.Complexity.Fagin.Tableau.Semantics
 public import Complexity.Computability.Complexity.Fagin.Verifier
+public import Complexity.Computability.Complexity.Fagin.Witness
 public import Complexity.Computability.Complexity.FineGrained
 public import Complexity.Computability.Complexity.FineGrained.Assignment
 public import Complexity.Computability.Complexity.FineGrained.BruteForce
@@ -2788,6 +2790,7 @@ public import Complexity.Languages.Probabilistic.Vector
 public import Complexity.Logics.FirstOrder.Basic
 public import Complexity.Logics.FirstOrder.Encoding
 public import Complexity.Logics.FirstOrder.Encoding.Layout
+public import Complexity.Logics.FirstOrder.Encoding.Sum
 public import Complexity.Logics.FirstOrder.Interpretation
 public import Complexity.Logics.FirstOrder.Interpretation.Constants
 public import Complexity.Logics.FirstOrder.Interpretation.Encoding
@@ -2931,6 +2934,7 @@ public import Complexity.Logics.Propositional.Resolution.TseitinExpander
 public import Complexity.Logics.Propositional.SigmaThree
 public import Complexity.Logics.Propositional.Tseitin
 public import Complexity.Logics.SecondOrder.Coloring
+public import Complexity.Logics.SecondOrder.Encoding
 public import Complexity.Logics.SecondOrder.Existential
 public import Complexity.Logics.SecondOrder.Grounding
 public import Complexity.Logics.SecondOrder.IndependentSet
diff --git a/Complexity/Computability/Complexity/Fagin/Ordered/Verifier.lean b/Complexity/Computability/Complexity/Fagin/Ordered/Verifier.lean
new file mode 100644
index 0000000000..ac63cf935a
--- /dev/null
+++ b/Complexity/Computability/Complexity/Fagin/Ordered/Verifier.lean
@@ -0,0 +1,200 @@
+/-
+Copyright (c) 2026 Samuel Schlesinger. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Samuel Schlesinger
+-/
+
+module
+-- upstream: candidate
+
+public import Complexity.Computability.Complexity.Fagin.Ordered
+public import Complexity.Computability.Complexity.Fagin.Witness
+
+/-!
+# Ordered existential second-order queries are in NP
+
+Witness relations are materialized as additional input tables, and the existing native ordered
+first-order model checker evaluates the matrix. The numeric constants, order and BIT keep their
+canonical interpretations; they are neither guessed nor supplied in the input. Together with the
+ordered tableau construction, this gives Fagin's characterization for arbitrary ordered queries
+at the source-only structure encoding, with universes of size at least two.
+
+The vocabulary and sentence are fixed. Polynomial bounds may depend on their relation arities
+and the formula; this is data complexity. Malformed relation tables and universes of size zero
+or one are rejected. The characterization concerns typed inputs under `encStructure`.
+
+## Main definitions
+
+* `Cslib.Logic.ESO.Sentence.orderedMatrix`: move the witness vocabulary before the numeric
+  vocabulary so the existing ordered first-order model checker applies.
+
+## Main results
+
+* `Cslib.Logic.ESO.Sentence.realize_orderedMatrix`: the vocabulary reordering preserves the
+  matrix's semantics, including numeric constants and predicates.
+* `Cslib.Logic.ESO.Sentence.Layout.exists_orderedVerifier`: a native polynomial-time verifier
+  with the layout's certificate-length polynomial and an explicit length guard.
+* `Cslib.Logic.FO.Ordered.ESODefinable.encodedLanguage_mem_NP`: the ordered ESO-to-NP direction.
+* `Cslib.Logic.FO.Ordered.esoDefinable_iff_encodedLanguage_mem_NP`: the ordered characterization.
+
+## References
+
+* [R. Fagin, *Generalized first-order spectra and polynomial-time recognizable sets*][Fagin1974]
+* [N. Immerman, *Descriptive Complexity*, Proposition 7.6 and Theorem 7.8][Immerman1999].
+  The construction guesses relation tables and applies fixed first-order model checking; the
+  universal-matrix strengthening of Theorem 7.8 is not asserted.
+-/
+
+public section
+
+namespace Cslib.Logic
+
+open FirstOrder Language Structure
+open Cslib.Complexity Turing.MultiTapeTM
+open FO.Ordered (language numericLanguage)
+
+namespace ESO.Sentence
+
+/-- Reorder the witness and numeric vocabularies without changing either interpretation. -/
+private def orderedMatrixMap (L R : Language) :
+    (language L).sum R →ᴸ language (L.sum R) where
+  onFunction _
+    | .inl (.inl f) => .inl (.inl f)
+    | .inl (.inr f) => .inr f
+    | .inr f => .inl (.inr f)
+  onRelation _
+    | .inl (.inl r) => .inl (.inl r)
+    | .inl (.inr r) => .inr r
+    | .inr r => .inl (.inr r)
+
+private instance orderedMatrixMap_isExpansionOn (L R : Language) (M : Type*)
+    [L.Structure M] [R.Structure M] [numericLanguage.Structure M] :
+    (orderedMatrixMap L R).IsExpansionOn M where
+  map_onFunction f _ := by rcases f with (f | f) | f <;> rfl
+  map_onRelation r _ := by rcases r with (r | r) | r <;> rfl
+
+variable {L : Language} (Φ : Sentence (language L))
+
+/-- The first-order matrix with witness relations among the input symbols and the canonical
+numeric vocabulary last, as required by the ordered first-order model checker. -/
+def orderedMatrix : (language (L.sum (varLanguage Φ.arity))).Sentence :=
+  (orderedMatrixMap L (varLanguage Φ.arity)).onSentence Φ.matrix
+
+/-- Reordering the vocabulary preserves the first-order matrix on any choice of witness
+relations, with the same canonical numeric structure on both sides. -/
+theorem realize_orderedMatrix {n : ℕ} [Fact (2 ≤ n)] [L.Structure (Fin n)]
+    (R : ∀ i, Set (Fin (Φ.arity i) → Fin n)) :
+    (letI := varLanguage.structure R; Fin n ⊨ Φ.orderedMatrix) ↔
+      (letI := varLanguage.structure R; Fin n ⊨ Φ.matrix) := by
+  let _ := varLanguage.structure R
+  exact LHom.realize_onSentence (Fin n) (orderedMatrixMap L (varLanguage Φ.arity)) Φ.matrix
+
+namespace Layout
+
+variable {Φ} (ℓ : Layout Φ) {m : ℕ} (e : Fin m ≃ Φ.Var)
+    [L.IsRelational] (v : Vocabulary L)
+
+/-- Ordered model checking of the materialized input is exactly checking the original matrix
+in the certificate expansion. The shape check also rejects malformed original inputs. -/
+theorem mem_queryLanguage_witnessInput (a : EncodedStructure) (w : List Bool) :
+    ℓ.witnessInput e (a, w) ∈
+        FO.Ordered.queryLanguage (v.sum (varLanguage.vocabulary Φ.arity e)) Φ.orderedMatrix ↔
+      v.WellFormed a ∧ ∃ hn : 2 ≤ a.1,
+        letI : Fact (2 ≤ a.1) := ⟨hn⟩
+        letI := v.decode a
+        letI := varLanguage.structure (ℓ.certRel a.1 (encStructure a).length w)
+        Fin a.1 ⊨ Φ.matrix := by
+  simp only [FO.Ordered.queryLanguage, Set.mem_ofPred_eq,
+    wellFormed_witnessInput_iff, witnessInput_card]
+  apply and_congr_right
+  intro ha
+  apply exists_congr
+  intro hn
+  let _ : Fact (2 ≤ a.1) := ⟨hn⟩
+  rw [decode_witnessInput ℓ e v a w ha]
+  let _ := v.decode a
+  exact Φ.realize_orderedMatrix _
+
+/-- Existentially choosing a certificate of the prescribed length is equivalent to ordered ESO
+truth, with exactly the original source-only encoding and shape rejection. -/
+theorem exists_witnessInput_mem_queryLanguage_iff (a : EncodedStructure) :
+    (∃ w : List Bool, w.length = ℓ.polynomial.eval (encStructure a).length ∧
+      ℓ.witnessInput e (a, w) ∈
+        FO.Ordered.queryLanguage (v.sum (varLanguage.vocabulary Φ.arity e)) Φ.orderedMatrix) ↔
+      a ∈ FO.Ordered.Query.encodedLanguage
+        {M : FO.Ordered.Structure L | Φ.Realize M} v := by
+  constructor
+  · rintro ⟨w, _, hw⟩
+    obtain ⟨ha, hn, hmatrix⟩ := (ℓ.mem_queryLanguage_witnessInput e v a w).1 hw
+    exact ⟨ha, hn, ℓ.certRel a.1 (encStructure a).length w, hmatrix⟩
+  · rintro ⟨ha, hn, R, hR⟩
+    have hN : 0 < (encStructure a).length := by
+      simp only [encStructure, length_encPair]
+      omega
+    obtain ⟨w, hw, hrel⟩ := ℓ.exists_certificate (card_le_length_encStructure a) hN R
+    refine ⟨w, hw, (ℓ.mem_queryLanguage_witnessInput e v a w).2 ⟨ha, hn, ?_⟩⟩
+    rw [hrel]
+    exact hR
+
+/-- Every fixed ordered ESO sentence has an actual polynomial-time verifier with the layout's
+certificate polynomial. The verifier explicitly rejects certificates of the wrong length. Its
+construction composes polynomial-time witness materialization with native ordered FO model
+checking; no verifier or efficiency premise is assumed. -/
+theorem exists_orderedVerifier :
+    ∃ V : EncodedStructure × List Bool → Bool,
+      ComputableInPolyTime V (encPair encStructure encBits) encBool ∧
+      IsVerifier encStructure ℓ.polynomial V
+        (FO.Ordered.Query.encodedLanguage {M : FO.Ordered.Structure L | Φ.Realize M} v) ∧
+      ∀ a w, V (a, w) = true → w.length = ℓ.polynomial.eval (encStructure a).length := by
+  let e := (Finite.equivFin Φ.Var).symm
+  obtain ⟨f, hf, hdec⟩ := L_subset_P
+    (FO.Ordered.queryLanguage_mem_L (v.sum (varLanguage.vocabulary Φ.arity e)) Φ.orderedMatrix)
+  let V := f ∘ ℓ.witnessInput e
+  have hV : ComputableInPolyTime V (encPair encStructure encBits) encBool :=
+    hf.comp (ℓ.computableInPolyTime_witnessInput e)
+  have hverifies : IsVerifier encStructure ℓ.polynomial V
+      (FO.Ordered.Query.encodedLanguage {M : FO.Ordered.Structure L | Φ.Realize M} v) := by
+    intro a
+    rw [← ℓ.exists_witnessInput_mem_queryLanguage_iff e v a]
+    exact exists_congr fun w => and_congr_right fun _ => hdec _
+  exact ⟨strictVerifier encStructure ℓ.polynomial V,
+    computableInPolyTime_strictVerifier _ _ hV, hverifies.strictVerifier,
+    fun _ _ => length_eq_of_strictVerifier_eq_true⟩
+
+end Layout
+
+variable [L.IsRelational] (v : Vocabulary L)
+
+/-- The source-only encoded language of a fixed ordered ESO sentence is in native `NP`.
+Universe sizes below two and malformed source tables are excluded by the existing query API. -/
+theorem ordered_queryLanguage_mem_NP :
+    FO.Ordered.Query.encodedLanguage {M : FO.Ordered.Structure L | Φ.Realize M} v ∈
+      NP encStructure := by
+  classical
+  let ℓ : Layout Φ := Classical.choice inferInstance
+  obtain ⟨V, hV, hverifies, _⟩ := ℓ.exists_orderedVerifier v
+  exact ⟨ℓ.polynomial, V, hV, hverifies⟩
+
+end ESO.Sentence
+
+namespace FO.Ordered
+
+/-- Every existential second-order definable ordered query has its source-only encoded language
+in native nondeterministic polynomial time. No invariance under permutations is required. -/
+theorem ESODefinable.encodedLanguage_mem_NP {L : Language} [L.IsRelational] (v : Vocabulary L)
+    {K : Query L} (hK : ESODefinable K) : K.encodedLanguage v ∈ NP encStructure := by
+  obtain ⟨Φ, hΦ⟩ := hK
+  have hK' : K = {M : Ordered.Structure L | Φ.Realize M} := Set.ext hΦ
+  rw [hK']
+  exact Φ.ordered_queryLanguage_mem_NP v
+
+/-- **Ordered Fagin characterization:** arbitrary queries of canonically ordered finite
+structures are ESO-definable exactly when their source-only encoded languages are in native
+`NP`. The universe has at least two elements and malformed relation tables are rejected. -/
+theorem esoDefinable_iff_encodedLanguage_mem_NP {L : Language} [L.IsRelational]
+    (v : Vocabulary L) (K : Query L) : ESODefinable K ↔ K.encodedLanguage v ∈ NP encStructure :=
+  ⟨ESODefinable.encodedLanguage_mem_NP v, ESODefinable.of_queryLanguage_mem_NP v⟩
+
+end FO.Ordered
+
+end Cslib.Logic
diff --git a/Complexity/Computability/Complexity/Fagin/Verifier.lean b/Complexity/Computability/Complexity/Fagin/Verifier.lean
index ce054e1d1b..bcc2685e4d 100644
--- a/Complexity/Computability/Complexity/Fagin/Verifier.lean
+++ b/Complexity/Computability/Complexity/Fagin/Verifier.lean
@@ -52,6 +52,8 @@ is not proved here.
 
 * `Cslib.Logic.ESO.Sentence.Layout.eval_eq_true_iff`: the evaluator decides truth in the expansion
   of the decoded structure by the certificate relations.
+* `Cslib.Logic.ESO.Sentence.Layout.exists_certificate`: every family of witness relations is
+  represented by a certificate of the prescribed polynomial length.
 * `Cslib.Logic.ESO.Sentence.Layout.realize_iff_exists_certificate`: a decoded structure satisfies
   the sentence exactly when some certificate is accepted.
 * `Cslib.Logic.ESO.Sentence.Layout.computableInPolyTime_verifier`: the verifier is
@@ -179,6 +181,15 @@ private theorem certRel_certificate {n N : ℕ} (hn : n ≤ N) (hN : 0 < N)
     rwa [tupleIndex_injective hxy]
   · exact fun hx => ⟨i, x, rfl, hx⟩
 
+/-- Every family of witness relations has a certificate of the prescribed polynomial length,
+provided the input-length parameter bounds the universe size. This is independent of the base
+language, so it also applies when the base has canonical numeric constants. -/
+theorem exists_certificate {n N : ℕ} (hn : n ≤ N) (hN : 0 < N)
+    (R : ∀ i, Set (Fin (Φ.arity i) → Fin n)) :
+    ∃ w : List Bool, w.length = ℓ.polynomial.eval N ∧ ℓ.certRel n N w = R :=
+  ⟨ℓ.certificate n N R, (ℓ.length_certificate n N R).trans (ℓ.eval_polynomial N).symm,
+    ℓ.certRel_certificate hn hN R⟩
+
 /-! ### The evaluator -/
 
 variable [L.IsRelational] (v : Vocabulary L)
diff --git a/Complexity/Computability/Complexity/Fagin/Witness.lean b/Complexity/Computability/Complexity/Fagin/Witness.lean
new file mode 100644
index 0000000000..dfedc288f2
--- /dev/null
+++ b/Complexity/Computability/Complexity/Fagin/Witness.lean
@@ -0,0 +1,209 @@
+/-
+Copyright (c) 2026 Samuel Schlesinger. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Samuel Schlesinger
+-/
+
+module
+-- upstream: candidate
+
+public import Complexity.Computability.Complexity.Fagin.Verifier
+public import Complexity.Logics.FirstOrder.Encoding.Sum
+public import Complexity.Logics.SecondOrder.Encoding
+import Complexity.Computability.Machines.Turing.MultiTape.Complexity.PolyTime.BitString
+import Complexity.Computability.Machines.Turing.MultiTape.Complexity.PolyTime.Nat
+import Complexity.Computability.Machines.Turing.MultiTape.Encodings.Length
+
+/-!
+# Materializing existential relation witnesses
+
+The certificate layout of an existential second-order sentence already reads a polynomial-length
+word as a family of relation tables. This module materializes those tables and appends them to
+the original encoded structure. The transformation has a native polynomial-time certificate and
+its decoded structure is exactly the expansion by the guessed relations. Missing witness bits
+read as false; nullary relations have one table entry, and an empty family adds no tables.
+
+## Main definitions
+
+* `Cslib.Logic.ESO.Sentence.Layout.witnessInput`: append the certificate's relation tables.
+
+## Main results
+
+* `Cslib.Logic.ESO.Sentence.Layout.wellFormed_witnessInput_iff`: materialization preserves and
+  reflects the validity of the original input tables.
+* `Cslib.Logic.ESO.Sentence.Layout.decode_witnessInput`: the decoded output is the expansion by
+  the certificate relations.
+* `Cslib.Logic.ESO.Sentence.Layout.computableInPolyTime_witnessInput`: materialization is
+  polynomial-time in the original input and certificate lengths.
+
+## References
+
+* [R. Fagin, *Generalized first-order spectra and polynomial-time recognizable sets*][Fagin1974]
+* [N. Immerman, *Descriptive Complexity*][Immerman1999]
+-/
+
+public section
+
+universe u v u' v'
+
+open FirstOrder Language Structure Turing.MultiTapeTM
+
+namespace Cslib.Logic.ESO
+
+
+namespace Sentence.Layout
+
+variable {L : Language.{u, v}} {Φ : Sentence L} (ℓ : Layout Φ) {m : ℕ}
+    (e : Fin m ≃ Φ.Var)
+
+/-- A relation table materialized from the certificate, in tuple-index order. -/
+@[expose]
+def witnessTable (a : EncodedStructure) (w : List Bool) (i : Φ.Var) : List Bool :=
+  (List.range (a.1 ^ Φ.arity i)).map fun idx =>
+    w.getD (ℓ.position (encStructure a).length i idx) false
+
+/-- Append the materialized witness relations to the original relation tables. The sentence and
+its enumeration are fixed parameters, not parts of the machine input. -/
+@[expose]
+def witnessInput (p : EncodedStructure × List Bool) : EncodedStructure :=
+  (p.1.1, p.1.2 ++ List.ofFn fun j : Fin m => ℓ.witnessTable p.1 p.2 (e j))
+
+/-- Materialization does not change the universe. -/
+@[simp]
+theorem witnessInput_card (p : EncodedStructure × List Bool) :
+    (ℓ.witnessInput e p).1 = p.1.1 :=
+  rfl
+
+/-- A materialized relation table has one entry for each tuple, including one for arity zero. -/
+@[simp]
+theorem length_witnessTable (a : EncodedStructure) (w : List Bool) (i : Φ.Var) :
+    (ℓ.witnessTable a w i).length = a.1 ^ Φ.arity i := by
+  simp [witnessTable]
+
+/-- Reading a materialized table returns the corresponding certificate bit. -/
+theorem getD_witnessTable (a : EncodedStructure) (w : List Bool) (i : Φ.Var)
+    (x : Fin (Φ.arity i) → Fin a.1) :
+    (ℓ.witnessTable a w i).getD (tupleIndex x) false =
+      w.getD (ℓ.position (encStructure a).length i (tupleIndex x)) false := by
+  rw [List.getD_eq_getElem _ _ (by rw [length_witnessTable]; exact tupleIndex_lt x)]
+  simp [witnessTable]
+
+/-- The materialized witness tables always have the declared shapes, even for short certificates.
+Short certificates supply false bits to the missing positions. -/
+theorem wellFormed_witnessTables (a : EncodedStructure) (w : List Bool) :
+    (varLanguage.vocabulary Φ.arity e).WellFormed
+      (a.1, List.ofFn fun j : Fin m => ℓ.witnessTable a w (e j)) := by
+  constructor
+  · exact List.length_ofFn
+  · intro j
+    change Fin m at j
+    change ((List.ofFn fun j : Fin m => ℓ.witnessTable a w (e j)).getD j []).length =
+      a.1 ^ Φ.arity (e j)
+    rw [List.getD_eq_getElem _ _ (by simp)]
+    simp only [List.getElem_ofFn, length_witnessTable]
+
+variable {K : Language.{u', v'}} (v : Vocabulary K)
+
+/-- Appending witness tables preserves and reflects source shape validity; it cannot repair a
+missing, extra, or incorrectly sized source relation table. -/
+theorem wellFormed_witnessInput_iff (a : EncodedStructure) (w : List Bool) :
+    (v.sum (varLanguage.vocabulary Φ.arity e)).WellFormed (ℓ.witnessInput e (a, w)) ↔
+      v.WellFormed a := by
+  change (v.sum (varLanguage.vocabulary Φ.arity e)).WellFormed
+    (a.1, a.2 ++ List.ofFn fun j : Fin m => ℓ.witnessTable a w (e j)) ↔ v.WellFormed a
+  exact (Vocabulary.wellFormed_sum_iff v (varLanguage.vocabulary Φ.arity e)
+    a.1 a.2 _ List.length_ofFn).trans (and_iff_left (ℓ.wellFormed_witnessTables e a w))
+
+/-- The output decodes to exactly the input structure expanded by the certificate relations. -/
+theorem decode_witnessInput [K.IsRelational] (a : EncodedStructure) (w : List Bool)
+    (ha : v.WellFormed a) :
+    (v.sum (varLanguage.vocabulary Φ.arity e)).decode (ℓ.witnessInput e (a, w)) =
+      @sumStructure K (varLanguage Φ.arity) (Fin a.1) (v.decode a)
+        (varLanguage.structure (ℓ.certRel a.1 (encStructure a).length w)) := by
+  apply FirstOrder.Language.Structure.ext
+  · funext k f
+    exact isEmptyElim f
+  · funext k r x
+    change Fin k → Fin a.1 at x
+    apply propext
+    cases r with
+    | inl r =>
+      change ((v.sum (varLanguage.vocabulary Φ.arity e)).table
+        (a.1, a.2 ++ List.ofFn fun j : Fin m => ℓ.witnessTable a w (e j))
+        ⟨k, Sum.inl r⟩).getD (tupleIndex x) false = true ↔ _
+      erw [Vocabulary.table_sum_inl v (varLanguage.vocabulary Φ.arity e)
+        a.1 a.2 _ ha.1 ⟨k, r⟩]
+      rfl
+    | inr r =>
+      obtain ⟨i, rfl⟩ := r
+      change ((v.sum (varLanguage.vocabulary Φ.arity e)).table
+        (a.1, a.2 ++ List.ofFn fun j : Fin m => ℓ.witnessTable a w (e j))
+        ⟨Φ.arity i, Sum.inr ⟨i, rfl⟩⟩).getD (tupleIndex x) false = true ↔ _
+      erw [Vocabulary.table_sum_inr v (varLanguage.vocabulary Φ.arity e)
+        a.1 a.2 _ ha.1 ⟨Φ.arity i, ⟨i, rfl⟩⟩]
+      change ((List.ofFn fun j : Fin m => ℓ.witnessTable a w (e j)).getD
+        (e.symm i : ℕ) []).getD (tupleIndex x) false = true ↔ _
+      rw [List.getD_eq_getElem
+        (List.ofFn fun j : Fin m => ℓ.witnessTable a w (e j)) []
+        (by simp)]
+      simp only [List.getElem_ofFn]
+      change (ℓ.witnessTable a w (e (e.symm i))).getD (tupleIndex x) false = true ↔
+        x ∈ ℓ.certRel a.1 (encStructure a).length w i
+      rw [Equiv.apply_symm_apply]
+      erw [getD_witnessTable ℓ a w i x]
+      rfl
+
+/-- The exact additional encoding cost is the sum of the framed witness-table lengths. -/
+theorem length_encStructure_witnessInput (a : EncodedStructure) (w : List Bool) :
+    (encStructure (ℓ.witnessInput e (a, w))).length = (encStructure a).length +
+      ∑ j : Fin m, (2 * a.1 ^ Φ.arity (e j) + 1) := by
+  simp [witnessInput, encStructure, length_encList, List.sum_ofFn, Nat.add_assoc]
+
+/-- A uniform polynomial bound in the original encoded input length, independent of witness
+contents and length. The sentence and layout determine the constants and degree. -/
+theorem length_encStructure_witnessInput_le (a : EncodedStructure) (w : List Bool) :
+    (encStructure (ℓ.witnessInput e (a, w))).length ≤ (encStructure a).length +
+      m * (2 * (encStructure a).length ^ ℓ.degree + 1) := by
+  have hN : 0 < (encStructure a).length := by
+    simp only [encStructure, length_encPair]
+    omega
+  have hp (j : Fin m) : a.1 ^ Φ.arity (e j) ≤ (encStructure a).length ^ ℓ.degree :=
+    (Nat.pow_le_pow_left (card_le_length_encStructure a) _).trans
+      (Nat.pow_le_pow_right hN (ℓ.arity_le (e j)))
+  rw [length_encStructure_witnessInput]
+  exact Nat.add_le_add_left
+    ((Finset.sum_le_sum fun j _ => Nat.add_le_add_right (Nat.mul_le_mul_left 2 (hp j)) 1).trans_eq
+      (by simp)) _
+
+open ComputableInPolyTime
+
+/-- Materializing one fixed relation uses polynomially many certificate lookups. -/
+@[fun_prop]
+theorem computableInPolyTime_witnessTable (i : Φ.Var) :
+    ComputableInPolyTime (fun p : EncodedStructure × List Bool => ℓ.witnessTable p.1 p.2 i)
+      (encPair encStructure encBits) encBits := by
+  unfold witnessTable
+  refine mapToBitsWithInput (range.comp ((unary_pow _).comp
+    ((fst encUnary (encList encBits)).comp (fst encStructure encBits)))) ?_
+  refine bitsGetDWithInput
+    ((snd encStructure encBits).comp (fst (encPair encStructure encBits) encUnary)) ?_ false
+  unfold position
+  exact unary_add' (unary_mul' (const (ℓ.block i : ℕ))
+    ((unary_pow ℓ.degree).comp ((encoding_length encStructure).comp
+      ((fst encStructure encBits).comp (fst (encPair encStructure encBits) encUnary)))))
+    (snd (encPair encStructure encBits) encUnary)
+
+/-- The entire witness expansion is computed by an actual polynomial-time machine on the input
+and certificate. No well-formedness or certificate-length premise is needed for its running time. -/
+@[fun_prop]
+theorem computableInPolyTime_witnessInput :
+    ComputableInPolyTime (ℓ.witnessInput e) (encPair encStructure encBits) encStructure := by
+  unfold witnessInput
+  refine ((fst encUnary (encList encBits)).comp (fst encStructure encBits)).prod
+    (listAppend' ((snd encUnary (encList encBits)).comp (fst encStructure encBits)) ?_)
+  simpa only [List.ofFn_eq_map] using
+    mapConst (List.finRange m) (fun j _ => ℓ.computableInPolyTime_witnessTable (e j))
+
+end Sentence.Layout
+
+end Cslib.Logic.ESO
diff --git a/Complexity/Logics/FirstOrder/Encoding/Sum.lean b/Complexity/Logics/FirstOrder/Encoding/Sum.lean
new file mode 100644
index 0000000000..66d1271a73
--- /dev/null
+++ b/Complexity/Logics/FirstOrder/Encoding/Sum.lean
@@ -0,0 +1,140 @@
+/-
+Copyright (c) 2026 Samuel Schlesinger. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Samuel Schlesinger
+-/
+
+module
+-- upstream: candidate
+
+public import Complexity.Logics.FirstOrder.Encoding
+import Mathlib.Logic.Equiv.Fin.Basic
+import Mathlib.Logic.Equiv.Sum
+import Mathlib.Data.List.GetD
+
+/-!
+# Encodings for sums of relational vocabularies
+
+`Vocabulary.sum` enumerates the left language's relation symbols before the right language's.
+Consequently concatenating the two lists of relation tables gives the encoding for the sum
+language. Table lookup preserves both parts, and well-formedness splits into the corresponding
+conditions on the two lists. No tables for function symbols are introduced.
+
+## Main definitions
+
+* `Cslib.Logic.Vocabulary.sum`: the concatenated enumeration of two relational vocabularies.
+
+## Main results
+
+* `Cslib.Logic.Vocabulary.table_sum_inl`, `Cslib.Logic.Vocabulary.table_sum_inr`: lookup in
+  concatenated relation tables.
+* `Cslib.Logic.Vocabulary.wellFormed_sum_iff`: well-formedness of the combined input, including
+  malformed source inputs when the right-hand table count is fixed.
+-/
+
+public section
+
+universe u v u' v'
+
+namespace Cslib.Logic.Vocabulary
+
+open FirstOrder Language
+
+variable {L : Language.{u, v}} {L' : Language.{u', v'}}
+
+/-- Enumerate the symbols of the left vocabulary followed by the symbols of the right one. -/
+@[expose] def sum (v : Vocabulary L) (w : Vocabulary L') : Vocabulary (L.sum L') where
+  count := v.count + w.count
+  symbol := finSumFinEquiv.symm.trans
+    ((v.symbol.sumCongr w.symbol).trans (Equiv.sigmaSumDistrib L.Relations L'.Relations).symm)
+
+/-- The sum vocabulary has one entry for each entry of its two summands. -/
+@[simp] theorem sum_count (v : Vocabulary L) (w : Vocabulary L') :
+    (v.sum w).count = v.count + w.count := rfl
+
+/-- A left relation retains its original table index. -/
+@[simp] theorem index_sum_inl (v : Vocabulary L) (w : Vocabulary L')
+    (r : Σ n, L.Relations n) :
+    (v.sum w).index ⟨r.1, Sum.inl r.2⟩ = v.index r := rfl
+
+/-- A right relation's table index is shifted by the number of left relations. -/
+@[simp] theorem index_sum_inr (v : Vocabulary L) (w : Vocabulary L')
+    (r : Σ n, L'.Relations n) :
+    (v.sum w).index ⟨r.1, Sum.inr r.2⟩ = v.count + w.index r := rfl
+
+/-- The arity of a left entry in the combined enumeration is unchanged. -/
+@[simp] theorem arity_sum_castAdd (v : Vocabulary L) (w : Vocabulary L') (i : Fin v.count) :
+    (v.sum w).arity (Fin.castAdd w.count i) = v.arity i := by
+  change ((Equiv.sigmaSumDistrib L.Relations L'.Relations).symm
+    ((v.symbol.sumCongr w.symbol) (finSumFinEquiv.symm (Fin.castAdd w.count i)))).1 = _
+  rw [finSumFinEquiv_symm_apply_castAdd]
+  rfl
+
+/-- The arity of a right entry in the combined enumeration is unchanged. -/
+@[simp] theorem arity_sum_natAdd (v : Vocabulary L) (w : Vocabulary L') (i : Fin w.count) :
+    (v.sum w).arity (Fin.natAdd v.count i) = w.arity i := by
+  change ((Equiv.sigmaSumDistrib L.Relations L'.Relations).symm
+    ((v.symbol.sumCongr w.symbol) (finSumFinEquiv.symm (Fin.natAdd v.count i)))).1 = _
+  rw [finSumFinEquiv_symm_apply_natAdd]
+  rfl
+
+/-- Left relation tables are preserved by concatenation when the left list has its expected
+number of tables. -/
+theorem table_sum_inl (v : Vocabulary L) (w : Vocabulary L') (n : ℕ)
+    (xs ys : List (List Bool)) (hlen : xs.length = v.count) (r : Σ k, L.Relations k) :
+    (v.sum w).table (n, xs ++ ys) ⟨r.1, Sum.inl r.2⟩ = v.table (n, xs) r := by
+  simp only [table, index_sum_inl]
+  exact List.getD_append xs ys [] _ (hlen ▸ v.index_lt r)
+
+/-- Right relation tables are preserved by concatenation when the left list has its expected
+number of tables. -/
+theorem table_sum_inr (v : Vocabulary L) (w : Vocabulary L') (n : ℕ)
+    (xs ys : List (List Bool)) (hlen : xs.length = v.count) (r : Σ k, L'.Relations k) :
+    (v.sum w).table (n, xs ++ ys) ⟨r.1, Sum.inr r.2⟩ = w.table (n, ys) r := by
+  simp only [table, index_sum_inr]
+  rw [List.getD_append_right _ _ _ _ (by omega), hlen, Nat.add_sub_cancel_left]
+
+private theorem wellFormed_sum_iff_of_left_length (v : Vocabulary L) (w : Vocabulary L')
+    (n : ℕ) (xs ys : List (List Bool)) (hx : xs.length = v.count) :
+    (v.sum w).WellFormed (n, xs ++ ys) ↔ v.WellFormed (n, xs) ∧ w.WellFormed (n, ys) := by
+  constructor
+  · rintro ⟨hlen, htables⟩
+    have hy : ys.length = w.count := by simpa [hx] using hlen
+    refine ⟨⟨hx, fun i => ?_⟩, ⟨hy, fun i => ?_⟩⟩
+    · have h := htables (Fin.castAdd w.count i)
+      simpa only [Fin.val_castAdd, arity_sum_castAdd,
+        List.getD_append xs ys [] i (by omega)] using h
+    · have h := htables (Fin.natAdd v.count i)
+      simpa only [Fin.val_natAdd, arity_sum_natAdd,
+        List.getD_append_right xs ys [] (v.count + i) (by omega), hx,
+        Nat.add_sub_cancel_left] using h
+  · rintro ⟨⟨_, hxs⟩, ⟨hy, hys⟩⟩
+    refine ⟨by simp [sum_count, hx, hy], ?_⟩
+    intro i
+    refine Fin.addCases (fun i => ?_) (fun i => ?_) i
+    · simpa only [Fin.val_castAdd, arity_sum_castAdd,
+        List.getD_append xs ys [] i (by omega)] using hxs i
+    · simpa only [Fin.val_natAdd, arity_sum_natAdd,
+        List.getD_append_right xs ys [] (v.count + i) (by omega), hx,
+        Nat.add_sub_cancel_left] using hys i
+
+/-- If the number of right tables is fixed, combined well-formedness is exactly well-formedness
+of both inputs. In particular a malformed left input cannot be repaired by appending right
+tables. -/
+theorem wellFormed_sum_iff (v : Vocabulary L) (w : Vocabulary L') (n : ℕ)
+    (xs ys : List (List Bool)) (hy : ys.length = w.count) :
+    (v.sum w).WellFormed (n, xs ++ ys) ↔ v.WellFormed (n, xs) ∧ w.WellFormed (n, ys) := by
+  constructor
+  · intro h
+    have hx : xs.length = v.count := by simpa [hy] using h.1
+    exact (wellFormed_sum_iff_of_left_length v w n xs ys hx).1 h
+  · intro h
+    exact (wellFormed_sum_iff_of_left_length v w n xs ys h.1.1).2 h
+
+/-- Concatenating well-formed relation tables gives a well-formed sum-language input. -/
+theorem WellFormed.sum {v : Vocabulary L} {w : Vocabulary L'} {n : ℕ}
+    {xs ys : List (List Bool)} (hx : v.WellFormed (n, xs)) (hy : w.WellFormed (n, ys)) :
+    (v.sum w).WellFormed (n, xs ++ ys) :=
+  (wellFormed_sum_iff v w n xs ys hy.1).2 ⟨hx, hy⟩
+
+end Cslib.Logic.Vocabulary
diff --git a/Complexity/Logics/SecondOrder/Encoding.lean b/Complexity/Logics/SecondOrder/Encoding.lean
new file mode 100644
index 0000000000..190adc4aa5
--- /dev/null
+++ b/Complexity/Logics/SecondOrder/Encoding.lean
@@ -0,0 +1,59 @@
+/-
+Copyright (c) 2026 Samuel Schlesinger. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Samuel Schlesinger
+-/
+
+module
+-- upstream: candidate
+
+public import Complexity.Logics.FirstOrder.Encoding
+public import Complexity.Logics.SecondOrder.Existential
+
+/-!
+# Encodings of finite families of relation variables
+
+`Cslib.Logic.ESO.varLanguage.vocabulary` converts an enumeration of finitely many relation
+variables into the vocabulary that serializes their truth tables. It retains the declared
+arity of each variable, including nullary relations, and admits an empty family.
+
+## Main definitions
+
+* `Cslib.Logic.ESO.varLanguage.vocabulary`: the vocabulary induced by a variable enumeration.
+
+## Main results
+
+* `Cslib.Logic.ESO.varLanguage.arity_vocabulary`: table arities are the declared arities.
+* `Cslib.Logic.ESO.varLanguage.index_vocabulary`: table indices are enumeration positions.
+-/
+
+public section
+
+open FirstOrder Language
+
+namespace Cslib.Logic.ESO
+
+namespace varLanguage
+
+variable {ι : Type} {m : ℕ} (arity : ι → ℕ) (e : Fin m ≃ ι)
+
+/-- Enumerate relation variables in the supplied order, retaining their arities. -/
+@[expose]
+def vocabulary : Vocabulary (varLanguage arity) where
+  count := m
+  symbol := e.trans (Equiv.sigmaFiberEquiv arity).symm
+
+/-- The arity of a variable in the enumeration is its declared arity. -/
+@[simp]
+theorem arity_vocabulary (j : Fin m) : (vocabulary arity e).arity j = arity (e j) :=
+  rfl
+
+/-- A relation variable's table is at its position in the supplied enumeration. -/
+@[simp]
+theorem index_vocabulary (r : Σ k, (varLanguage arity).Relations k) :
+    (vocabulary arity e).index r = (e.symm r.2.1 : ℕ) :=
+  rfl
+
+end varLanguage
+
+end Cslib.Logic.ESO
diff --git a/ComplexityTests/FaginWitness.lean b/ComplexityTests/FaginWitness.lean
new file mode 100644
index 0000000000..3f4dc3236c
--- /dev/null
+++ b/ComplexityTests/FaginWitness.lean
@@ -0,0 +1,171 @@
+/-
+Copyright (c) 2026 Samuel Schlesinger. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Samuel Schlesinger
+-/
+
+import Complexity.Computability.Complexity.Fagin.Witness
+import ComplexityTests.FaginEncoding
+
+/-!
+# Tests for materialized existential relation witnesses
+
+A mixed unary/binary/nullary family checks block selection, tuple orientation, source table
+preservation and exact encoded lengths. Its layout deliberately leaves a block unused. The
+tests also cover empty families, short and excessive certificates, and malformed source inputs.
+-/
+
+namespace ComplexityTests.FaginWitness
+
+open FirstOrder Language Cslib.Logic Cslib.Logic.ESO
+open ComplexityTests.FaginEncoding
+
+/-- No input relation tables are present, so the universe size alone determines input length. -/
+private def emptyVocabulary : Vocabulary Language.empty where
+  count := 0
+  symbol := Equiv.equivOfIsEmpty _ _
+
+/-- Three witness variables, respectively unary, binary, and nullary. -/
+private abbrev mixed : ESO.Sentence Language.empty :=
+  ⟨Fin 3, ![1, 2, 0], ⊤⟩
+
+/-- Block zero is unused; the three variables occupy blocks one, two, and three. -/
+private def mixedLayout : mixed.Layout where
+  blocks := 4
+  block := ⟨Fin.succ, Fin.succ_injective 3⟩
+  degree := 2
+  arity_le i := by fin_cases i <;> decide
+
+private abbrev mixedVocabulary :=
+  varLanguage.vocabulary mixed.arity (Equiv.refl (Fin 3))
+
+private abbrev expandedVocabulary := emptyVocabulary.sum mixedVocabulary
+
+/-- At universe size two and input length five, the block width is twenty-five. The unary
+relation contains zero, the binary relation contains only `(1, 0)`, and the nullary relation
+is true. -/
+private def certificate : List Bool :=
+  (List.range 100).map fun j => decide (j = 25 ∨ j = 51 ∨ j = 75)
+
+/-- The certificate has exactly the layout's prescribed length. -/
+example : (encStructure (2, [])).length = 5 ∧
+    certificate.length = mixedLayout.polynomial.eval (encStructure (2, [])).length := by
+  rw [Sentence.Layout.eval_polynomial]
+  decide +kernel
+
+/-- Concrete materialization retains relation order and each declared arity. -/
+example : mixedLayout.witnessInput (Equiv.refl _) ((2, []), certificate) =
+    (2, [ [true, false], [false, true, false, false], [true] ]) := by
+  decide +kernel
+
+example : expandedVocabulary.WellFormed
+    (mixedLayout.witnessInput (Equiv.refl _) ((2, []), certificate)) := by
+  rw [Sentence.Layout.wellFormed_witnessInput_iff]
+  decide +kernel
+
+/-- The first tuple coordinate is the least significant radix digit: `(1, 0)` is true,
+whereas `(0, 1)` is false. -/
+example :
+    (expandedVocabulary.decode
+      (mixedLayout.witnessInput (Equiv.refl _) ((2, []), certificate))).RelMap
+      (Sum.inr ⟨1, rfl⟩) ![(1 : Fin 2), (0 : Fin 2)] ∧
+    ¬ (expandedVocabulary.decode
+      (mixedLayout.witnessInput (Equiv.refl _) ((2, []), certificate))).RelMap
+      (Sum.inr ⟨1, rfl⟩) ![(0 : Fin 2), (1 : Fin 2)] := by
+  change _ = true ∧ ¬ _ = true
+  decide +kernel
+
+/-- The nullary relation is a single truth value, independent of any argument. -/
+example : (expandedVocabulary.decode
+    (mixedLayout.witnessInput (Equiv.refl _) ((2, []), certificate))).RelMap
+      (Sum.inr ⟨2, rfl⟩) ![] := by
+  change _ = true
+  decide +kernel
+
+/-- Reordering the variable enumeration reorders tables while retaining their relation meanings. -/
+example : mixedLayout.witnessInput (Equiv.swap (0 : Fin 3) 2) ((2, []), certificate) =
+    (2, [ [true], [false, true, false, false], [true, false] ]) := by
+  decide +kernel
+
+/-- Changing every bit of the unused block has no effect on the materialized relations. -/
+example : mixedLayout.witnessInput (Equiv.refl _)
+    ((2, []), List.replicate 25 true ++ certificate.drop 25) =
+    mixedLayout.witnessInput (Equiv.refl _) ((2, []), certificate) := by
+  decide +kernel
+
+/-- A short word supplies false for absent positions, even though the tables retain full size. -/
+example : mixedLayout.witnessInput (Equiv.refl _)
+    ((2, []), List.replicate 25 false ++ [true]) =
+    (2, [ [true, false], [false, false, false, false], [false] ]) := by
+  decide +kernel
+
+/-- Additional bits outside all queried positions are ignored by the total materializer. -/
+example : mixedLayout.witnessInput (Equiv.refl _) ((2, []), certificate ++ [true, true]) =
+    mixedLayout.witnessInput (Equiv.refl _) ((2, []), certificate) := by
+  decide +kernel
+
+/-- In an empty universe, positive-arity tables are empty but a nullary table still has one bit.
+The materializer itself is independent of the ordered query's separate `n ≥ 2` restriction. -/
+example : mixedLayout.witnessInput (Equiv.refl _) ((0, []), [false, false, false, true]) =
+    (0, [ [], [], [true] ]) := by
+  decide +kernel
+
+/-- Existing source relations stay in front of the guessed tables. A missing certificate has
+all-false witness relations. -/
+example : mixedLayout.witnessInput (Equiv.refl _) (edge, []) =
+    (2, [ [false, true, true, false], [false, false], [false, false, false, false], [false] ]) := by
+  decide +kernel
+
+private abbrev graphExpandedVocabulary := graphVocabulary.sum mixedVocabulary
+
+/-- Source adjacency survives decoding the enlarged structure. -/
+example :
+    (graphExpandedVocabulary.decode (mixedLayout.witnessInput (Equiv.refl _) (edge, []))).RelMap
+      (Sum.inl adj) ![(0 : Fin 2), (1 : Fin 2)] ∧
+    ¬ (graphExpandedVocabulary.decode (mixedLayout.witnessInput (Equiv.refl _) (edge, []))).RelMap
+      (Sum.inl adj) ![(0 : Fin 2), (0 : Fin 2)] := by
+  change _ = true ∧ ¬ _ = true
+  decide +kernel
+
+/-- Appending witnesses cannot repair missing source tables, for any certificate. -/
+example (w : List Bool) : ¬ graphExpandedVocabulary.WellFormed
+    (mixedLayout.witnessInput (Equiv.refl _) ((2, []), w)) := by
+  rw [Sentence.Layout.wellFormed_witnessInput_iff]
+  decide +kernel
+
+/-- Extra source tables remain invalid. -/
+example (w : List Bool) : ¬ graphExpandedVocabulary.WellFormed
+    (mixedLayout.witnessInput (Equiv.refl _) ((2, [ [false, true, true, false], [] ]), w)) := by
+  rw [Sentence.Layout.wellFormed_witnessInput_iff]
+  decide +kernel
+
+/-- A source relation with the wrong number of entries remains invalid. -/
+example (w : List Bool) : ¬ graphExpandedVocabulary.WellFormed
+    (mixedLayout.witnessInput (Equiv.refl _) ((2, [ [false, true, true] ]), w)) := by
+  rw [Sentence.Layout.wellFormed_witnessInput_iff]
+  decide +kernel
+
+/-- Exact lengths include the frame around each materialized table. -/
+example :
+    (encStructure (mixedLayout.witnessInput (Equiv.refl _) ((2, []), certificate))).length = 22 ∧
+    (encStructure (mixedLayout.witnessInput (Equiv.refl _) (edge, []))).length = 31 := by
+  decide +kernel
+
+/-- A family with no relation variables needs no blocks. -/
+private abbrev noWitness : ESO.Sentence Language.graph :=
+  ⟨Fin 0, fun _ => 0, ⊤⟩
+
+private def noWitnessLayout : noWitness.Layout where
+  blocks := 0
+  block := (Equiv.refl _).toEmbedding
+  degree := 0
+  arity_le _ := le_rfl
+
+/-- The empty family neither reads the certificate nor adds relation tables. -/
+example : noWitnessLayout.witnessInput (Equiv.refl _) (edge, [true, false]) = edge ∧
+    noWitnessLayout.witnessInput (Equiv.refl _) ((2, []), [true]) = (2, []) ∧
+    noWitnessLayout.polynomial.eval 14 = 0 := by
+  rw [Sentence.Layout.eval_polynomial]
+  decide +kernel
+
+end ComplexityTests.FaginWitness
diff --git a/ComplexityTests/OrderedFaginVerifier.lean b/ComplexityTests/OrderedFaginVerifier.lean
new file mode 100644
index 0000000000..a8413f4713
--- /dev/null
+++ b/ComplexityTests/OrderedFaginVerifier.lean
@@ -0,0 +1,258 @@
+/-
+Copyright (c) 2026 Samuel Schlesinger. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Samuel Schlesinger
+-/
+
+import Complexity.Computability.Complexity.Fagin.Ordered.Verifier
+import ComplexityTests.OrderedFagin
+
+/-!
+# Ordered ESO verifier regression tests
+
+Existential colorings exercise source relations and canonical constants together. A second
+sentence forces its unary witness to agree with canonical BIT under a quantifier. Concrete
+positive and negative instances test the ordered semantics, while the new characterization
+supplies native NP membership without any verifier or complexity assumption.
+-/
+
+namespace ComplexityTests.OrderedFaginVerifier
+
+open FirstOrder Language Structure Cslib.Logic Cslib.Logic.FO Cslib.Logic.FO.Ordered
+open Cslib.Complexity Turing.MultiTapeTM
+open ComplexityTests.OrderedFagin (graphVocabulary oneEdge)
+
+/-- The new forward direction accepts the existing query whose truth changes under a swap of
+the two input vertices, so it requires no invariance under unordered input isomorphisms. -/
+example : ComplexityTests.OrderedFagin.edgeZeroMaxQuery.encodedLanguage graphVocabulary ∈
+    NP encStructure :=
+  ESODefinable.encodedLanguage_mem_NP graphVocabulary
+    (show Ordered.Definable ComplexityTests.OrderedFagin.edgeZeroMaxQuery from
+      ⟨ComplexityTests.OrderedFagin.edgeZeroMax, fun _ => Iff.rfl⟩).esoDefinable
+
+private abbrev witnessLanguage (L : Language) :=
+  (language L).sum (ESO.varLanguage fun _ : Fin 1 => 1)
+
+private def marked {L : Language} {k : ℕ}
+    (t : (witnessLanguage L).Term (Empty ⊕ Fin k)) :
+    (witnessLanguage L).BoundedFormula Empty k :=
+  Relations.boundedFormula₁ (Sum.inr ⟨0, rfl⟩) t
+
+private def numeric {L : Language} {k : ℕ} (c : NumericFunction 0) :
+    (witnessLanguage L).Term (Empty ⊕ Fin k) :=
+  .func (Sum.inl (Sum.inr c)) Fin.elim0
+
+/-- The two sides of a coloring are distinguished by canonical zero and maximum. -/
+private abbrev coloring : ESO.Sentence (language Language.graph) where
+  Var := Fin 1
+  arity _ := 1
+  matrix := marked (numeric .zero) ⊓
+    ((marked (numeric .max)).not ⊓
+      ((Relations.boundedFormula₂ (Sum.inl (Sum.inl adj)) (.var (.inr 0)) (.var (.inr 1))).imp
+        ((marked (.var (.inr 0))).iff ((marked (.var (.inr 1))).not))).all.all)
+
+private def coloringQuery : Query Language.graph := {M | coloring.Realize M}
+
+/-- One self-loop forces the same vertex to have opposite colors. -/
+private def loop : Ordered.Structure Language.graph where
+  size := 2
+  size_ge_two := le_refl _
+  input.RelMap
+    | .adj, xs => xs 0 = 0 ∧ xs 1 = 0
+
+private theorem coloring_forward : coloring.Realize (oneEdge true) := by
+  let _ : Fact (2 ≤ 2) := ⟨by decide⟩
+  let _ : Language.graph.Structure (Fin 2) := (oneEdge true).input
+  let R : Fin 1 → Set (Fin 1 → Fin 2) := fun _ => {xs | xs 0 = 0}
+  refine ⟨R, ?_⟩
+  let _ := ESO.varLanguage.structure (arity := fun _ : Fin 1 => 1) R
+  change Fin 2 ⊨ coloring.matrix
+  simp only [coloring, FirstOrder.Language.Sentence.Realize, Formula.Realize,
+    BoundedFormula.realize_inf, BoundedFormula.realize_not, BoundedFormula.realize_all,
+    BoundedFormula.realize_imp, BoundedFormula.realize_iff]
+  change (0 : Fin 2) = 0 ∧ (¬ (1 : Fin 2) = 0) ∧
+    ∀ x y : Fin 2, (x = 0 ∧ y = 1) → (x = 0 ↔ ¬ y = 0)
+  refine ⟨rfl, by decide, ?_⟩
+  rintro x y ⟨rfl, rfl⟩
+  decide
+
+private theorem coloring_loop : ¬ coloring.Realize loop := by
+  rintro ⟨R, hR⟩
+  change Fin 1 → Set (Fin 1 → Fin 2) at R
+  let _ : Fact (2 ≤ 2) := ⟨by decide⟩
+  let _ : Language.graph.Structure (Fin 2) := loop.input
+  let _ := ESO.varLanguage.structure (arity := fun _ : Fin 1 => 1) R
+  change Fin 2 ⊨ coloring.matrix at hR
+  simp only [coloring, FirstOrder.Language.Sentence.Realize, Formula.Realize,
+    BoundedFormula.realize_inf, BoundedFormula.realize_not, BoundedFormula.realize_all,
+    BoundedFormula.realize_imp, BoundedFormula.realize_iff] at hR
+  have hz := hR.1
+  have he := hR.2.2 (0 : Fin 2) (0 : Fin 2)
+  simp only [marked] at hz he
+  erw [BoundedFormula.realize_rel₁] at hz
+  erw [BoundedFormula.realize_rel₂, BoundedFormula.realize_rel₁,
+    BoundedFormula.realize_rel₁] at he
+  change ![(0 : Fin 2)] ∈ R 0 at hz
+  change ((0 : Fin 2) = 0 ∧ (0 : Fin 2) = 0) →
+    (![(0 : Fin 2)] ∈ R 0 ↔ ¬ ![(0 : Fin 2)] ∈ R 0) at he
+  exact ((he ⟨rfl, rfl⟩).mp hz) hz
+
+/-- These are actual source-only encodings of accepted and rejected ordered structures. -/
+example : encode graphVocabulary (oneEdge true) ∈ coloringQuery.encodedLanguage graphVocabulary ∧
+    encode graphVocabulary loop ∉ coloringQuery.encodedLanguage graphVocabulary := by
+  simp only [mem_encodedLanguage_encode]
+  exact ⟨coloring_forward, coloring_loop⟩
+
+/-- The new direction certifies the query with genuine existential witnesses. -/
+example : coloringQuery.encodedLanguage graphVocabulary ∈ NP encStructure :=
+  ESODefinable.encodedLanguage_mem_NP graphVocabulary ⟨coloring, fun _ => Iff.rfl⟩
+
+/-- Both directions of the characterization apply to the same concrete existential query. -/
+example : ESODefinable coloringQuery :=
+  (esoDefinable_iff_encodedLanguage_mem_NP graphVocabulary coloringQuery).mpr
+    (coloring.ordered_queryLanguage_mem_NP graphVocabulary)
+
+private def colorLayout : coloring.Layout where
+  blocks := 1
+  block := (Equiv.refl _).toEmbedding
+  degree := 1
+  arity_le _ := le_rfl
+
+private def colorInput : EncodedStructure := (2, [ [false, false, true, false] ])
+private def colorCertificate : List Bool := true :: List.replicate 13 false
+
+/-- The witness layout checks the actual directed-edge encoding, with its original framing. -/
+example : ∃ w : List Bool,
+    w.length = colorLayout.polynomial.eval (encStructure colorInput).length ∧
+    colorLayout.witnessInput (Equiv.refl _) (colorInput, w) ∈
+      queryLanguage (graphVocabulary.sum
+        (ESO.varLanguage.vocabulary coloring.arity (Equiv.refl _))) coloring.orderedMatrix := by
+  refine ⟨colorCertificate, ?_, ?_⟩
+  · rw [ESO.Sentence.Layout.eval_polynomial]
+    decide +kernel
+  · apply (colorLayout.mem_queryLanguage_witnessInput (Equiv.refl _) graphVocabulary _ _).mpr
+    refine ⟨by decide, by decide, ?_⟩
+    let _ : Fact (2 ≤ 2) := ⟨by decide⟩
+    let _ : Language.graph.Structure (Fin 2) := graphVocabulary.decode colorInput
+    let _ := ESO.varLanguage.structure (arity := fun _ : Fin 1 => 1)
+      (colorLayout.certRel 2 (encStructure colorInput).length colorCertificate)
+    change Fin 2 ⊨ coloring.matrix
+    simp only [coloring, FirstOrder.Language.Sentence.Realize, Formula.Realize,
+      BoundedFormula.realize_inf, BoundedFormula.realize_not, BoundedFormula.realize_all,
+      BoundedFormula.realize_imp, BoundedFormula.realize_iff]
+    refine ⟨rfl, ?_, ?_⟩
+    · change ¬ false = true
+      decide
+    · intro x y
+      fin_cases x <;> fin_cases y <;>
+        change (_ = true → (_ = true ↔ ¬ _ = true)) <;> decide +kernel
+
+/-- The strict guard accepts the prescribed length even for an always-accepting inner checker. -/
+example : strictVerifier encStructure colorLayout.polynomial (fun _ => true)
+    (colorInput, colorCertificate) = true := by
+  rw [strictVerifier_eq_true_iff, ESO.Sentence.Layout.eval_polynomial]
+  decide +kernel
+
+/-- Neither truncation nor padding can bypass the explicit length guard. -/
+example : strictVerifier encStructure colorLayout.polynomial (fun _ => true)
+      (colorInput, colorCertificate.drop 1) ≠ true ∧
+    strictVerifier encStructure colorLayout.polynomial (fun _ => true)
+      (colorInput, colorCertificate ++ [false]) ≠ true := by
+  constructor
+  · intro h
+    have hlen := length_eq_of_strictVerifier_eq_true h
+    rw [ESO.Sentence.Layout.eval_polynomial] at hlen
+    change 13 = 14 at hlen
+    omega
+  · intro h
+    have hlen := length_eq_of_strictVerifier_eq_true h
+    rw [ESO.Sentence.Layout.eval_polynomial] at hlen
+    change 15 = 14 at hlen
+    omega
+
+private def emptyVocabulary : Vocabulary Language.empty where
+  count := 0
+  symbol := Equiv.equivOfIsEmpty _ _
+
+private def emptyInput (n : ℕ) (hn : 2 ≤ n) : Ordered.Structure Language.empty where
+  size := n
+  size_ge_two := hn
+  input.funMap f := isEmptyElim f
+  input.RelMap r := isEmptyElim r
+
+/-- The witness must equal bit one everywhere, and contain the maximum element. -/
+private abbrev bitWitness : ESO.Sentence (language Language.empty) where
+  Var := Fin 1
+  arity _ := 1
+  matrix := ((marked (.var (.inr 0))).iff
+    (Relations.boundedFormula₂ (Sum.inl (Sum.inr NumericRelation.bit))
+      (.var (.inr 0)) (numeric .one))).all ⊓ marked (numeric .max)
+
+private def bitQuery : Query Language.empty := {M | bitWitness.Realize M}
+
+private theorem bitWitness_three : bitWitness.Realize (emptyInput 3 (by decide)) := by
+  let _ : Fact (2 ≤ 3) := ⟨by decide⟩
+  let _ : Language.empty.Structure (Fin 3) := (emptyInput 3 (by decide)).input
+  let R : Fin 1 → Set (Fin 1 → Fin 3) := fun _ => {xs | (xs 0).val.testBit 1 = true}
+  refine ⟨R, ?_⟩
+  let _ := ESO.varLanguage.structure (arity := fun _ : Fin 1 => 1) R
+  change Fin 3 ⊨ bitWitness.matrix
+  simp only [bitWitness, FirstOrder.Language.Sentence.Realize, Formula.Realize,
+    BoundedFormula.realize_inf, BoundedFormula.realize_all, BoundedFormula.realize_iff]
+  change (∀ x : Fin 3, (x.val.testBit 1 = true ↔ x.val.testBit 1 = true)) ∧
+    (2 : ℕ).testBit 1 = true
+  exact ⟨fun _ => Iff.rfl, by decide⟩
+
+private theorem bitWitness_two : ¬ bitWitness.Realize (emptyInput 2 (by decide)) := by
+  rintro ⟨R, hR⟩
+  change Fin 1 → Set (Fin 1 → Fin 2) at R
+  let _ : Fact (2 ≤ 2) := ⟨by decide⟩
+  let _ : Language.empty.Structure (Fin 2) := (emptyInput 2 (by decide)).input
+  let _ := ESO.varLanguage.structure (arity := fun _ : Fin 1 => 1) R
+  change Fin 2 ⊨ bitWitness.matrix at hR
+  simp only [bitWitness, FirstOrder.Language.Sentence.Realize, Formula.Realize,
+    BoundedFormula.realize_inf, BoundedFormula.realize_all, BoundedFormula.realize_iff] at hR
+  have hmax := hR.2
+  have hbit := hR.1 (1 : Fin 2)
+  simp only [marked] at hmax hbit
+  erw [BoundedFormula.realize_rel₁] at hmax
+  erw [BoundedFormula.realize_rel₁, BoundedFormula.realize_rel₂] at hbit
+  change ![(1 : Fin 2)] ∈ R 0 at hmax
+  change ![(1 : Fin 2)] ∈ R 0 ↔ (1 : ℕ).testBit 1 = true at hbit
+  exact (by decide : ¬ (1 : ℕ).testBit 1 = true) (hbit.mp hmax)
+
+/-- Canonical BIT is computed from the size and indices; it is absent from the source tables. -/
+example : encode emptyVocabulary (emptyInput 3 (by decide)) ∈
+      bitQuery.encodedLanguage emptyVocabulary ∧
+    encode emptyVocabulary (emptyInput 2 (by decide)) ∉
+      bitQuery.encodedLanguage emptyVocabulary := by
+  simp only [mem_encodedLanguage_encode]
+  exact ⟨bitWitness_three, bitWitness_two⟩
+
+example : bitQuery.encodedLanguage emptyVocabulary ∈ NP encStructure :=
+  (esoDefinable_iff_encodedLanguage_mem_NP emptyVocabulary bitQuery).mp
+    ⟨bitWitness, fun _ => Iff.rfl⟩
+
+/-- An empty witness family and a true matrix do not waive source validity. -/
+private def always : Query Language.graph :=
+  {M | (ESO.Sentence.ofSentence (⊤ : (language Language.graph).Sentence)).Realize M}
+
+example : always.encodedLanguage graphVocabulary ∈ NP encStructure :=
+  (ESO.Sentence.ofSentence (⊤ : (language Language.graph).Sentence)).ordered_queryLanguage_mem_NP
+    graphVocabulary
+
+/-- Missing, extra, and incorrectly sized source tables are rejected even with a true matrix. -/
+example : (2, []) ∉ always.encodedLanguage graphVocabulary ∧
+    (2, [ [false, false, false, false], [] ]) ∉ always.encodedLanguage graphVocabulary ∧
+    (2, [ [false] ]) ∉ always.encodedLanguage graphVocabulary :=
+  ⟨Query.not_mem_encodedLanguage_of_not_wellFormed _ _ (by decide),
+    Query.not_mem_encodedLanguage_of_not_wellFormed _ _ (by decide),
+    Query.not_mem_encodedLanguage_of_not_wellFormed _ _ (by decide)⟩
+
+/-- Correctly shaped universes below two remain outside the ordered convention. -/
+example : (0, [ [] ]) ∉ always.encodedLanguage graphVocabulary ∧
+    (1, [ [false] ]) ∉ always.encodedLanguage graphVocabulary :=
+  ⟨Query.not_mem_encodedLanguage_of_lt_two _ _ (by decide),
+    Query.not_mem_encodedLanguage_of_lt_two _ _ (by decide)⟩
+
+end ComplexityTests.OrderedFaginVerifier
diff --git a/ROADMAP.md b/ROADMAP.md
index db07115f67..4f2597a49a 100644
--- a/ROADMAP.md
+++ b/ROADMAP.md
@@ -259,7 +259,6 @@ universe size, not supplied as unverified input tables. In dependency order:
   machines and the translation to `encCircuitValue`.
 - Numeric certificates for further restricted-domain families; canonical BIT on a restricted
   domain need not be first-order definable.
-- The ordered ESO-to-NP direction of Fagin's theorem.
 - Order-free: SAT-to-3SAT, graph-property hardness, and bridges to the separately encoded
   problems.
 - **The Immerman–Vardi theorem:** on ordered finite structures, first-order logic with least