diff --git a/Complexity.lean b/Complexity.lean
index e9ed8c9a26..1037577cb8 100644
--- a/Complexity.lean
+++ b/Complexity.lean
@@ -594,6 +594,8 @@ public import Complexity.Computability.Circuit.Boolean.Equality
 public import Complexity.Computability.Circuit.Boolean.EvaluationTime
 public import Complexity.Computability.Circuit.Boolean.FanInTwo
 public import Complexity.Computability.Circuit.Boolean.FirstOrder
+public import Complexity.Computability.Circuit.Boolean.FirstOrder.Ordered
+public import Complexity.Computability.Circuit.Boolean.FirstOrder.Ordered.Parity
 public import Complexity.Computability.Circuit.Boolean.FirstOrder.Parity
 public import Complexity.Computability.Circuit.Boolean.Formula
 public import Complexity.Computability.Circuit.Boolean.Formula.Andreev
diff --git a/Complexity/Computability/Circuit/Boolean/FirstOrder.lean b/Complexity/Computability/Circuit/Boolean/FirstOrder.lean
index 0e6bb8e97f..bbec0d5af9 100644
--- a/Complexity/Computability/Circuit/Boolean/FirstOrder.lean
+++ b/Complexity/Computability/Circuit/Boolean/FirstOrder.lean
@@ -35,6 +35,8 @@ facts to grow with `n`.
 
 Sentences are those of Mathlib's model theory (`FirstOrder.Language.Sentence`), and the statements
 are about structures rather than an encoding of structures as bit strings.
+The canonical ordered extension, including genuine `0`, `1`, and `max` constants and hardwired
+`≤` and `BIT`, is in `Complexity.Computability.Circuit.Boolean.FirstOrder.Ordered`.
 
 ## Main definitions
 
diff --git a/Complexity/Computability/Circuit/Boolean/FirstOrder/Ordered.lean b/Complexity/Computability/Circuit/Boolean/FirstOrder/Ordered.lean
new file mode 100644
index 0000000000..517248895c
--- /dev/null
+++ b/Complexity/Computability/Circuit/Boolean/FirstOrder/Ordered.lean
@@ -0,0 +1,264 @@
+/-
+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.Circuit.Boolean.FirstOrder
+public import Complexity.Logics.FirstOrder.Ordered.Basic
+import Mathlib.Algebra.BigOperators.Fin
+import Mathlib.Algebra.Order.BigOperators.Group.Finset
+import Mathlib.Tactic.FinCases
+import Mathlib.Tactic.Linarith
+
+/-!
+# Canonical ordered first-order model checking in constant depth
+
+A sentence of `FO.Ordered.language L` is compiled into an unbounded fan-in Boolean formula
+reading only the atomic facts of the relational input vocabulary `L`. The constants `0`, `1`,
+and `max`, weak order, and zero-indexed `BIT` have their canonical meanings on `Fin n`, with
+`n ≥ 2`. Numeric atoms are evaluated during construction: their truth tables are not additional
+input bits. Constants may occur in input-relation arguments and under quantifiers.
+
+The same formula decides the sentence for every input structure on this canonical universe.
+Its depth is bounded independently of `n`, and its size and number of leaves are polynomial in
+`n`, using the measures of the order-free compiler. This is the nonuniform upper-bound direction
+of the FO(≤, BIT) characterization of AC⁰. No circuit-generation or DLOGTIME-uniformity bound is
+asserted. Inputs are relation-table atoms, not serialized structure encodings; the bounds are in
+the universe size, including when the input vocabulary has no positive-arity relation symbol.
+
+## Main definitions
+
+* `Cslib.Circuits.Boolean.ModelChecking.Ordered.termValue`: canonical values of ordered terms.
+* `Cslib.Circuits.Boolean.ModelChecking.Ordered.toUnbounded`: compilation reading only the input
+  relation tables.
+
+## Main results
+
+* `Cslib.Circuits.Boolean.ModelChecking.Ordered.eval_toUnbounded_atomsOf`: correctness for
+  arbitrary assignments and input structures on the canonical universe.
+* `Cslib.Circuits.Boolean.ModelChecking.Ordered.exists_formula_realize`: every fixed ordered
+  sentence has constant-depth, polynomial-size formulas on its input relation tables.
+* `Cslib.Circuits.Boolean.ModelChecking.Ordered.leafSize_toUnbounded_le`: a polynomial leaf bound
+  for subsequent substitutions.
+
+## References
+
+* [N. Immerman, *Descriptive Complexity*][Immerman1999], Chapter 5. The formula-expansion argument
+  is in Section 5.4, proof of Theorem 5.22, in the
+  [author-hosted chapter draft](https://people.cs.umass.edu/~immerman/book/ch5.pdf); this locator
+  refers to that draft. Here it is specialized to a fixed sentence and proves only the
+  logical-to-circuit upper bound. The canonical numeric vocabulary follows Section 1.2,
+  Provisos 1.14–1.15.
+* [D. A. M. Barrington, N. Immerman, H. Straubing, *On uniformity within NC¹*]
+  [BarringtonImmermanStraubing1990]. Uniformity is not proved here.
+-/
+
+public section
+
+namespace Cslib.Circuits.Boolean.ModelChecking.Ordered
+
+open FirstOrder FirstOrder.Language
+open Cslib.Logic.FO.Ordered (language)
+
+variable {L : Language} [L.IsRelational] {n N : ℕ} [Fact (2 ≤ n)]
+
+/-- Evaluate an ordered term without using any input relation: terms are variables or one of
+the three canonical numeric constants. -/
+@[expose]
+def termValue {α : Type*} (v : α → Fin n) : (language L).Term α → Fin n
+  | .var x => v x
+  | .func (.inl f) _ => isEmptyElim f
+  | .func (.inr c) _ => ⟨c.index n, c.index_lt Fact.out⟩
+
+/-- The relation-independent term evaluator agrees with canonical ordered term semantics. -/
+@[simp]
+theorem termValue_eq_realize [L.Structure (Fin n)] {α : Type*} (v : α → Fin n)
+    (t : (language L).Term α) : termValue v t = t.realize v := by
+  cases t with
+  | var x => rfl
+  | func f ts =>
+    cases f with
+    | inl f => exact isEmptyElim f
+    | inr c => cases c <;> rfl
+
+/-- Compile an ordered formula on `Fin n`: input relations read their original atomic facts,
+numeric atoms become constants, and universal quantifiers become conjunctions over the universe.
+The input enumeration contains no numeric relation tables. -/
+@[expose]
+def toUnbounded (e : Atom L n ≃ Fin N) :
+    ∀ {k}, (language L).BoundedFormula Empty k → (Fin k → Fin n) →
+      Formula Unbounded.signature N
+  | _, .falsum, _ => constUnbounded false
+  | _, .equal t₁ t₂, xs =>
+    constUnbounded (decide (termValue (Sum.elim Empty.elim xs) t₁ =
+      termValue (Sum.elim Empty.elim xs) t₂))
+  | _, .rel (.inl R) ts, xs =>
+    .input (e ⟨⟨_, R⟩, fun i => termValue (Sum.elim Empty.elim xs) (ts i)⟩)
+  | _, .rel (.inr .le) ts, xs =>
+    constUnbounded (decide (termValue (Sum.elim Empty.elim xs) (ts 0) ≤
+      termValue (Sum.elim Empty.elim xs) (ts 1)))
+  | _, .rel (.inr .bit) ts, xs =>
+    constUnbounded ((termValue (Sum.elim Empty.elim xs) (ts 0)).val.testBit
+      (termValue (Sum.elim Empty.elim xs) (ts 1)).val)
+  | _, .imp φ ψ, xs =>
+    .gate (.or 2) ![.gate .not ![toUnbounded e φ xs], toUnbounded e ψ xs]
+  | _, .all φ, xs => .gate (.and n) fun a => toUnbounded e φ (Fin.snoc xs a)
+
+/-- Compilation decides the formula on any input structure on `Fin n`, expanded by the actual
+canonical numeric constants, weak order and zero-indexed BIT. -/
+theorem eval_toUnbounded_atomsOf [L.Structure (Fin n)] (e : Atom L n ≃ Fin N) {k : ℕ}
+    (φ : (language L).BoundedFormula Empty k) (xs : Fin k → Fin n) :
+    (toUnbounded e φ xs).eval Unbounded.interpretation
+      (atomsOf (L := L) (Equiv.refl _) ∘ e.symm) = true ↔ φ.Realize Empty.elim xs := by
+  classical
+  induction φ with
+  | falsum => simp [toUnbounded, BoundedFormula.Realize]
+  | equal t₁ t₂ =>
+    simp only [toUnbounded, eval_constUnbounded, decide_eq_true_iff, BoundedFormula.Realize,
+      termValue_eq_realize]
+  | rel R ts =>
+    cases R with
+    | inl R =>
+      simp only [toUnbounded, Formula.eval_input, Function.comp_apply]
+      refine (iff_of_eq (congrArg
+        (fun a : Atom L n => atomsOf (L := L) (Equiv.refl _) a = true)
+        (e.symm_apply_apply _))).trans ?_
+      simp only [atomsOf, decide_eq_true_iff, BoundedFormula.Realize, termValue_eq_realize]
+      rfl
+    | inr R =>
+      cases R <;>
+        simp only [toUnbounded, eval_constUnbounded, decide_eq_true_iff, BoundedFormula.Realize,
+          termValue_eq_realize] <;> rfl
+  | imp φ ψ ihφ ihψ =>
+    simp only [toUnbounded, Formula.eval_gate, Unbounded.interpretation_or,
+      BoundedFormula.Realize, ← ihφ, ← ihψ]
+    simp [Fin.exists_fin_two, imp_iff_not_or]
+  | all φ ih =>
+    simp only [toUnbounded, Formula.eval_gate, Unbounded.interpretation_and, decide_eq_true_iff,
+      BoundedFormula.Realize]
+    exact forall_congr' fun a => ih _
+
+/-- The compiled formula's depth is bounded independently of the universe size. -/
+theorem depth_toUnbounded_le (e : Atom L n ≃ Fin N) {k : ℕ}
+    (φ : (language L).BoundedFormula Empty k) (xs : Fin k → Fin n) :
+    (toUnbounded e φ xs).depth ≤ foDepth φ := by
+  induction φ with
+  | falsum => simp [toUnbounded, constUnbounded, foDepth]
+  | equal t₁ t₂ =>
+    simp only [toUnbounded, constUnbounded, foDepth]
+    split_ifs <;> simp
+  | rel R ts =>
+    cases R with
+    | inl R => simp [toUnbounded, foDepth]
+    | inr R =>
+      cases R <;> simp only [toUnbounded, constUnbounded, foDepth] <;> split_ifs <;> simp
+  | imp φ ψ ihφ ihψ =>
+    rw [toUnbounded, foDepth, Formula.depth_gate]
+    refine (Nat.add_le_add_right (Finset.sup_le (a := max (foDepth φ) (foDepth ψ) + 1)
+      fun j _ => ?_) 1).trans (by omega)
+    fin_cases j
+    · change (Formula.gate _ _).depth ≤ _
+      rw [Formula.depth_gate]
+      refine (Nat.add_le_add_right (Finset.sup_le (a := foDepth φ) fun j _ => ?_) 1).trans
+        (by omega)
+      fin_cases j
+      exact ihφ xs
+    · exact (ihψ xs).trans (by omega)
+  | all φ ih =>
+    simp only [toUnbounded, Formula.depth_gate, foDepth]
+    exact Nat.add_le_add_right (Finset.sup_le fun a _ => ih _) 1
+
+/-- The compiled formula's size is polynomial in the universe size for each fixed formula. -/
+theorem size_toUnbounded_le (e : Atom L n ≃ Fin N) {k : ℕ}
+    (φ : (language L).BoundedFormula Empty k) (xs : Fin k → Fin n) :
+    (toUnbounded e φ xs).size ≤ foSize φ * (n + 2) ^ foSize φ := by
+  induction φ with
+  | falsum => simp [toUnbounded, constUnbounded, foSize]
+  | equal t₁ t₂ =>
+    simp only [toUnbounded, constUnbounded, foSize]
+    split_ifs <;> simp
+  | rel R ts =>
+    cases R with
+    | inl R => simp [toUnbounded, foSize]
+    | inr R =>
+      cases R <;> simp only [toUnbounded, constUnbounded, foSize] <;> split_ifs <;> simp
+  | imp φ ψ ihφ ihψ =>
+    have h₁ := ihφ xs
+    have h₂ := ihψ xs
+    simp only [toUnbounded, Formula.size_gate, Fin.sum_univ_two, Matrix.cons_val_zero,
+      Matrix.cons_val_one, Fin.sum_univ_one, foSize]
+    have hφ : (n + 2) ^ foSize φ ≤ (n + 2) ^ (foSize φ + foSize ψ + 1) :=
+      Nat.pow_le_pow_right (by omega) (by omega)
+    have hψ : (n + 2) ^ foSize ψ ≤ (n + 2) ^ (foSize φ + foSize ψ + 1) :=
+      Nat.pow_le_pow_right (by omega) (by omega)
+    have hpos : 2 ≤ (n + 2) ^ (foSize φ + foSize ψ + 1) :=
+      (show 2 ≤ n + 2 by omega).trans (Nat.le_self_pow (by omega) _)
+    nlinarith [Nat.mul_le_mul_left (foSize φ) hφ, Nat.mul_le_mul_left (foSize ψ) hψ]
+  | all φ ih =>
+    simp only [toUnbounded, Formula.size_gate, foSize]
+    have hsum : ∑ a : Fin n, (toUnbounded e φ (Fin.snoc xs a)).size ≤
+        n * (foSize φ * (n + 2) ^ foSize φ) :=
+      (Finset.sum_le_card_nsmul _ _ _ fun a _ => ih _).trans_eq (by simp)
+    have hpos : 1 ≤ (n + 2) ^ foSize φ := Nat.one_le_pow _ _ (by omega)
+    have := foSize_pos φ
+    calc _ ≤ n * (foSize φ * (n + 2) ^ foSize φ) + 1 := Nat.add_le_add_right hsum 1
+      _ ≤ (foSize φ + 1) * (n + 2) ^ (foSize φ + 1) := by
+        rw [pow_succ]
+        nlinarith
+
+/-- The number of input leaves is polynomial in the universe size. -/
+theorem leafSize_toUnbounded_le (e : Atom L n ≃ Fin N) {k : ℕ}
+    (φ : (language L).BoundedFormula Empty k) (xs : Fin k → Fin n) :
+    (toUnbounded e φ xs).leafSize ≤ (n + 2) ^ foSize φ := by
+  induction φ with
+  | falsum => simp [toUnbounded, constUnbounded]
+  | equal t₁ t₂ =>
+    simp only [toUnbounded, constUnbounded]
+    split_ifs <;> simp
+  | rel R ts =>
+    cases R with
+    | inl R => simp [toUnbounded, foSize]
+    | inr R =>
+      cases R <;> simp only [toUnbounded, constUnbounded] <;> split_ifs <;> simp
+  | imp φ ψ ihφ ihψ =>
+    have h₁ := ihφ xs
+    have h₂ := ihψ xs
+    simp only [toUnbounded, Formula.leafSize_gate, Fin.sum_univ_two, Matrix.cons_val_zero,
+      Matrix.cons_val_one, Fin.sum_univ_one, foSize]
+    have hφ : (n + 2) ^ foSize φ ≤ (n + 2) ^ (foSize φ + foSize ψ) :=
+      Nat.pow_le_pow_right (by omega) (by omega)
+    have hψ : (n + 2) ^ foSize ψ ≤ (n + 2) ^ (foSize φ + foSize ψ) :=
+      Nat.pow_le_pow_right (by omega) (by omega)
+    rw [pow_succ]
+    nlinarith
+  | all φ ih =>
+    simp only [toUnbounded, Formula.leafSize_gate, foSize]
+    have hsum : ∑ a : Fin n, (toUnbounded e φ (Fin.snoc xs a)).leafSize ≤
+        n * (n + 2) ^ foSize φ :=
+      (Finset.sum_le_card_nsmul _ _ _ fun a _ => ih _).trans_eq (by simp)
+    refine hsum.trans ?_
+    rw [pow_succ, mul_comm]
+    exact Nat.mul_le_mul_left _ (by omega)
+
+/-- For each universe size at least two, one constant-depth, polynomial-size formula decides
+the ordered sentence on every interpretation of the input relations. Only the original input
+relation tables are inputs; the canonical numeric symbols are fixed by the universe size. -/
+theorem exists_formula_realize (φ : (language L).Sentence) (e : Atom L n ≃ Fin N) :
+    ∃ F : Formula Unbounded.signature N,
+      (∀ s : L.Structure (Fin n), letI := s;
+        F.eval Unbounded.interpretation (atomsOf (L := L) (Equiv.refl _) ∘ e.symm) = true ↔
+          Fin n ⊨ φ) ∧
+      F.depth ≤ foDepth φ ∧ F.size ≤ foSize φ * (n + 2) ^ foSize φ := by
+  refine ⟨toUnbounded e φ Fin.elim0, fun s => ?_,
+    depth_toUnbounded_le e φ _, size_toUnbounded_le e φ _⟩
+  let := s
+  exact (eval_toUnbounded_atomsOf e φ Fin.elim0).trans (by
+    rw [Sentence.Realize, Formula.Realize,
+      Subsingleton.elim (Empty.elim : Empty → Fin n) default,
+      Subsingleton.elim (Fin.elim0 : Fin 0 → Fin n) default])
+
+end Cslib.Circuits.Boolean.ModelChecking.Ordered
diff --git a/Complexity/Computability/Circuit/Boolean/FirstOrder/Ordered/Parity.lean b/Complexity/Computability/Circuit/Boolean/FirstOrder/Ordered/Parity.lean
new file mode 100644
index 0000000000..bbfacd83b2
--- /dev/null
+++ b/Complexity/Computability/Circuit/Boolean/FirstOrder/Ordered/Parity.lean
@@ -0,0 +1,177 @@
+/-
+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.Ordered.Query
+public import Mathlib.SetTheory.Cardinal.Finite
+import Complexity.Computability.Circuit.Boolean.FirstOrder.Ordered
+import Complexity.Computability.Circuit.Boolean.FirstOrder.Parity
+import Complexity.Computability.Circuit.Boolean.AC0
+import Complexity.Computability.Languages.Slice
+import Mathlib.Algebra.BigOperators.Fin
+import Mathlib.Tactic.Linarith
+
+/-!
+# Parity is not definable in the canonical ordered vocabulary
+
+No sentence with the canonical numeric constants `0`, `1`, and `max`, weak order, and `BIT`
+defines even cardinality of a unary input relation on all ordered structures of size at least
+two. This states the parity separation directly in `FO.Ordered.Definable`.
+
+The proof compiles a hypothetical defining sentence with `ModelChecking.Ordered.toUnbounded`,
+fixes the other input relations, and obtains polynomial-size constant-depth formulas for parity.
+Their circuits contradict the existing `parity_notMem_AC0` theorem. The two input lengths excluded
+by the ordered-structure convention are supplied by a constant circuit and an input wire.
+Numeric constants are genuine function symbols with interpretations determined by the universe
+size; only original relation tables supply input bits. No uniformity theorem is used.
+
+## Main results
+
+* `Cslib.Circuits.Boolean.ModelChecking.Ordered.not_definable_even_card`: even cardinality of a
+  unary input relation is not definable by a canonical ordered first-order sentence.
+
+## References
+
+* [M. Furst, J. B. Saxe, M. Sipser, *Parity, circuits, and the polynomial-time
+  hierarchy*][FurstSaxeSipser1984]
+* [M. Ajtai, *Σ¹₁-formulae on finite structures*][Ajtai1983]
+* [N. Immerman, *Descriptive Complexity*][Immerman1999]
+
+The result here is the canonical-structure corollary of the library's parity circuit lower bound;
+it includes the genuine numeric constants excluded by the relational-only separation.
+-/
+
+public section
+
+namespace Cslib.Circuits.Boolean.ModelChecking.Ordered
+
+open FirstOrder FirstOrder.Language Finset
+open Cslib.Logic.FO.Ordered (language)
+
+variable {L : Language} [L.IsRelational] [Finite (Σ l, L.Relations l)] {n : ℕ}
+
+/-- Compiling and restricting an ordered sentence defining even cardinality gives small,
+bounded-depth formulas for parity. -/
+private theorem exists_formula_computes_parity [Fact (2 ≤ n)] (P : L.Relations 1)
+    (N : L.Structure (Fin n)) (φ : (language L).Sentence)
+    (h : ∀ S : Finset (Fin n),
+      letI : L.Structure (Fin n) := inferInstanceAs (L.Structure (Expansion P N S));
+      Fin n ⊨ φ ↔ Even #S) :
+    ∃ F : Circuits.Formula Unbounded.signature n,
+      F.Computes Unbounded.interpretation (parity n) ∧ F.depth ≤ foDepth φ + 2 ∧
+        F.size ≤ (foSize φ + 2) * (n + 2) ^ foSize φ := by
+  classical
+  have := Fintype.ofFinite (Σ l, L.Relations l)
+  let e : Atom L n ≃ Fin (Fintype.card (Atom L n)) := Fintype.equivFin _
+  let G := toUnbounded e φ Fin.elim0
+  let sub : Fin (Fintype.card (Atom L n)) → Circuits.Formula Unbounded.signature n := fun j =>
+    if (e.symm j).1 = ⟨1, P⟩ then .gate (.and _) fun i => .input ((e.symm j).2 i)
+    else constUnbounded (decide (N.RelMap (e.symm j).1.2 (e.symm j).2))
+  have hsubd : ∀ j, (sub j).depth ≤ 1 := fun j => by
+    simp only [sub, constUnbounded]
+    split_ifs <;> simp
+  have hsubs : ∀ j, (sub j).size ≤ 1 := fun j => by
+    simp only [sub, constUnbounded]
+    split_ifs <;> simp
+  refine ⟨.gate .not ![G.bind sub], fun y => ?_, ?_, ?_⟩
+  · set S : Finset (Fin n) := {i | y i = true}
+    let : L.Structure (Fin n) := inferInstanceAs (L.Structure (Expansion P N S))
+    have hatoms : (fun j => (sub j).eval Unbounded.interpretation y) =
+        atomsOf (L := L) (M := Expansion P N S) (Equiv.refl _) ∘ e.symm := by
+      funext j
+      simp only [sub, Function.comp_apply, atomsOf]
+      obtain ⟨⟨l, R⟩, t⟩ := e.symm j
+      by_cases hR : (⟨l, R⟩ : Σ l, L.Relations l) = ⟨1, P⟩
+      · rw [ite_eq_left hR]
+        refine Bool.eq_iff_iff.2 ?_
+        simp only [Circuits.Formula.eval_gate, Circuits.Formula.eval_input,
+          Unbounded.interpretation_and, decide_eq_true_iff]
+        change _ ↔ (if _ then _ else _)
+        rw [ite_eq_left hR]
+        refine forall_congr' fun i => ?_
+        change _ ↔ t i ∈ S
+        simp [S]
+      · rw [ite_eq_right hR]
+        refine Bool.eq_iff_iff.2 ?_
+        simp only [eval_constUnbounded, decide_eq_true_iff]
+        exact (Expansion.relMap_of_ne hR _).symm
+    have hreal : (G.bind sub).eval Unbounded.interpretation y = true ↔ Even #S := by
+      rw [Circuits.Formula.eval_bind, hatoms]
+      refine (eval_toUnbounded_atomsOf e φ Fin.elim0).trans ?_
+      rw [Subsingleton.elim (Empty.elim : Empty → Fin n) default,
+        Subsingleton.elim (Fin.elim0 : Fin 0 → Fin n) default]
+      exact h S
+    simp only [Circuits.Formula.eval_gate, Unbounded.interpretation_not, Matrix.cons_val_zero]
+    change _ = decide (#S % 2 = 1)
+    rw [Nat.even_iff] at hreal
+    cases hv : (G.bind sub).eval Unbounded.interpretation y
+    · rw [hv] at hreal
+      have : #S % 2 = 1 := by
+        rcases Nat.mod_two_eq_zero_or_one #S with h0 | h1
+        · exact absurd (hreal.2 h0) (by simp)
+        · exact h1
+      simp [this]
+    · have := hreal.1 hv
+      simp [this]
+  · have h := Circuits.Formula.depth_bind_le hsubd G
+    have hG : G.depth ≤ foDepth φ := depth_toUnbounded_le e φ Fin.elim0
+    simp only [Circuits.Formula.depth_gate, Finset.univ_unique, Finset.sup_singleton,
+      Fin.default_eq_zero, Matrix.cons_val_zero]
+    omega
+  · have h := Circuits.Formula.size_bind_le hsubs G
+    have hs : G.size ≤ foSize φ * (n + 2) ^ foSize φ := size_toUnbounded_le e φ Fin.elim0
+    have hl : G.leafSize ≤ (n + 2) ^ foSize φ := leafSize_toUnbounded_le e φ Fin.elim0
+    have hpos : 1 ≤ (n + 2) ^ foSize φ := Nat.one_le_pow _ _ (by omega)
+    simp only [Circuits.Formula.size_gate, Fin.sum_univ_one, Matrix.cons_val_zero]
+    nlinarith
+
+/-- **Parity is not definable in canonical ordered first-order logic.** In any finite relational
+input vocabulary with a unary relation `P`, no sentence using canonical `≤`, `BIT`, `0`, `1`, and
+`max` defines even cardinality of `P` on all ordered structures of size at least two. -/
+theorem not_definable_even_card (P : L.Relations 1) :
+    ¬ Cslib.Logic.FO.Ordered.Definable {M : Cslib.Logic.FO.Ordered.Structure L |
+      Even (Nat.card {x : M // Structure.RelMap P ![x]})} := by
+  classical
+  rintro ⟨φ, hφ⟩
+  apply parity_notMem_AC0
+  refine ConstDepth.mem_iff.2
+    ⟨foDepth φ + 2, fun n => (foSize φ + 2) * (n + 2) ^ foSize φ, by fun_prop, fun n => ?_⟩
+  rw [_root_.Language.slice_ofSlices]
+  suffices ∃ F : Circuits.Formula Unbounded.signature n,
+      F.Computes Unbounded.interpretation (parity n) ∧ F.depth ≤ foDepth φ + 2 ∧
+        F.size ≤ (foSize φ + 2) * (n + 2) ^ foSize φ by
+    obtain ⟨F, hF, hd, hs⟩ := this
+    exact ⟨F.toCircuit, hF.toCircuit, F.depth_toCircuit_le.trans hd, by simpa using hs⟩
+  by_cases hn : 2 ≤ n
+  · let : Fact (2 ≤ n) := ⟨hn⟩
+    let N : L.Structure (Fin n) := ⟨fun f => isEmptyElim f, fun _ _ => False⟩
+    refine exists_formula_computes_parity P N φ fun S => ?_
+    let : L.Structure (Fin n) := inferInstanceAs (L.Structure (Expansion P N S))
+    let M : Cslib.Logic.FO.Ordered.Structure L :=
+      ⟨n, hn, inferInstanceAs (L.Structure (Expansion P N S))⟩
+    have hcard : Nat.card {x : M // Structure.RelMap P ![x]} = #S := by
+      rw [← Nat.card_eq_finsetCard S]
+      refine Nat.card_congr (Equiv.subtypeEquivRight fun x => ?_)
+      exact Expansion.relMap_self (P := P) (N := N) (S := S) ![x]
+    have hM := (hφ M).symm
+    change (Fin n ⊨ φ) ↔ Even (Nat.card {x : M // Structure.RelMap P ![x]}) at hM
+    rwa [hcard] at hM
+  · have hn' : n = 0 ∨ n = 1 := by omega
+    rcases hn' with rfl | rfl
+    · refine ⟨constUnbounded false, ?_, ?_, ?_⟩
+      · intro x
+        simp [parity]
+      · simp [constUnbounded]
+      · have hpow : 1 ≤ (0 + 2) ^ foSize φ := Nat.one_le_pow _ _ (by omega)
+        simp only [constUnbounded, Bool.false_eq_true, ↓reduceIte, Circuits.Formula.size_gate]
+        simpa using (show 1 ≤ (foSize φ + 2) * (0 + 2) ^ foSize φ by nlinarith)
+    · refine ⟨.input 0, ?_, by simp, by simp⟩
+      intro x
+      simp [parity, Finset.univ_unique, Fin.default_eq_zero]
+
+end Cslib.Circuits.Boolean.ModelChecking.Ordered
diff --git a/Complexity/Computability/Circuit/Boolean/FirstOrder/Parity.lean b/Complexity/Computability/Circuit/Boolean/FirstOrder/Parity.lean
index aa59154d99..ff2420c4cc 100644
--- a/Complexity/Computability/Circuit/Boolean/FirstOrder/Parity.lean
+++ b/Complexity/Computability/Circuit/Boolean/FirstOrder/Parity.lean
@@ -44,6 +44,8 @@ The language is relational, as in `ModelChecking.toUnbounded`, and has finitely
 symbols, so that a structure on `Fin n` has finitely many atomic facts. Constant symbols, such as
 `min` and `max` in [Immerman1999], are not covered; a numerical constant can be expressed by a
 unary numerical relation holding of one element.
+The separation with genuine canonical `0`, `1`, and `max` constants, stated directly through
+`FO.Ordered.Definable`, is in `Complexity.Computability.Circuit.Boolean.FirstOrder.Ordered.Parity`.
 
 ## Main definitions
 
diff --git a/ComplexityTests/OrderedFirstOrderCircuits.lean b/ComplexityTests/OrderedFirstOrderCircuits.lean
new file mode 100644
index 0000000000..52d5ec3925
--- /dev/null
+++ b/ComplexityTests/OrderedFirstOrderCircuits.lean
@@ -0,0 +1,237 @@
+/-
+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.Circuit.Boolean.FirstOrder.Ordered
+import Complexity.Computability.Circuit.Boolean.FirstOrder.Ordered.Parity
+
+/-!
+# Canonical ordered first-order circuit clients
+
+These examples evaluate the generated formulas on actual input bits. They cover genuine numeric
+constants in input atoms, least-significant-bit indexing, quantifier binding, exact gate and leaf
+counts, the minimum permitted universe, and a numeric-only sentence with no input bits.
+-/
+
+namespace ComplexityTests.OrderedFirstOrderCircuits
+
+open FirstOrder Language
+open Cslib.Circuits.Boolean
+
+private inductive Relation : ℕ → Type
+  | mark : Relation 1
+
+private abbrev inputLanguage : Language where
+  Functions _ := Empty
+  Relations := Relation
+
+private instance : inputLanguage.IsRelational := fun _ => inferInstance
+
+private def atomEquiv (n : ℕ) : ModelChecking.Atom inputLanguage n ≃ Fin n where
+  toFun a := match a with | ⟨⟨_, .mark⟩, xs⟩ => xs 0
+  invFun i := ⟨⟨1, .mark⟩, fun _ => i⟩
+  left_inv := by
+    rintro ⟨⟨_, r⟩, xs⟩
+    cases r
+    exact congrArg
+      (fun t : Fin 1 → Fin n => (⟨⟨1, Relation.mark⟩, t⟩ : ModelChecking.Atom inputLanguage n))
+      (funext fun i => congrArg xs (Subsingleton.elim 0 i))
+  right_inv _ := rfl
+
+open Cslib.Logic.FO.Ordered
+
+private instance : Fact (2 ≤ 2) := ⟨by decide⟩
+private instance : Fact (2 ≤ 3) := ⟨by decide⟩
+private instance : Fact (2 ≤ 9) := ⟨by decide⟩
+
+private def compile {n : ℕ} [Fact (2 ≤ n)] (φ : (language inputLanguage).Sentence) :=
+  ModelChecking.Ordered.toUnbounded (atomEquiv n) φ Fin.elim0
+
+private def marked (t : (language inputLanguage).Term Empty) :
+    (language inputLanguage).Sentence :=
+  Relations.formula₁ (L := language inputLanguage) (Sum.inl Relation.mark) t
+
+-- All three numeric constants can occur directly in an input-relation argument.
+example :
+    (compile (n := 3) (marked (zero inputLanguage))).eval Unbounded.interpretation
+      ![true, false, true] = true ∧
+    (compile (n := 3) (marked (one inputLanguage))).eval Unbounded.interpretation
+      ![true, false, true] = false ∧
+    (compile (n := 3) (marked (max inputLanguage))).eval Unbounded.interpretation
+      ![true, false, true] = true := by decide
+
+-- Compiling an input atom produces exactly one input leaf and no operation gate.
+example :
+    (compile (n := 3) (marked (max inputLanguage))).size = 0 ∧
+    (compile (n := 3) (marked (max inputLanguage))).depth = 0 ∧
+    (compile (n := 3) (marked (max inputLanguage))).leafSize = 1 := by decide
+
+private def lowBit : (language inputLanguage).Sentence :=
+  bit inputLanguage (max inputLanguage) (zero inputLanguage)
+
+private def nextBit : (language inputLanguage).Sentence :=
+  bit inputLanguage (max inputLanguage) (one inputLanguage)
+
+-- In the non-power-of-two universe of size three, max is binary 10.
+example :
+    (compile (n := 3) lowBit).eval Unbounded.interpretation ![true, true, true] = false ∧
+    (compile (n := 3) nextBit).eval Unbounded.interpretation ![false, false, false] = true ∧
+    (compile (n := 2) lowBit).eval Unbounded.interpretation ![false, false] = true := by decide
+
+-- Numeric predicates read no input leaves, even when all source bits change.
+example (x y : Fin 3 → Bool) :
+    (compile (n := 3) nextBit).eval Unbounded.interpretation x =
+      (compile (n := 3) nextBit).eval Unbounded.interpretation y ∧
+    (compile (n := 3) nextBit).size = 1 ∧
+    (compile (n := 3) nextBit).depth = 1 ∧
+    (compile (n := 3) nextBit).leafSize = 0 := by
+  refine ⟨?_, by decide⟩
+  change (ModelChecking.constUnbounded true).eval Unbounded.interpretation x =
+    (ModelChecking.constUnbounded true).eval Unbounded.interpretation y
+  simp
+
+private def mixed : (language inputLanguage).Sentence :=
+  ((Relations.boundedFormula₁ (L := language inputLanguage) (Sum.inl Relation.mark)
+      (.var (.inr 0))).iff
+    (Relations.boundedFormula₂ (L := language inputLanguage) (Sum.inr NumericRelation.bit)
+      (.var (.inr 0)) (one inputLanguage)) ⊓
+    (Relations.boundedFormula₂ (L := language inputLanguage) (Sum.inr NumericRelation.le)
+      (zero inputLanguage) (.var (.inr 0))) ⊓
+    (Relations.boundedFormula₂ (L := language inputLanguage) (Sum.inr NumericRelation.le)
+      (.var (.inr 0)) (max inputLanguage))).all
+
+-- A quantified formula accepts exactly the intended input predicate, with fixed numeric data.
+example :
+    (compile (n := 3) mixed).eval Unbounded.interpretation ![false, false, true] = true ∧
+    (compile (n := 3) mixed).eval Unbounded.interpretation ![false, true, true] = false ∧
+    (compile (n := 2) mixed).eval Unbounded.interpretation ![false, false] = true := by decide
+
+private def nested : (language inputLanguage).Sentence :=
+  ((Term.var (Sum.inr (0 : Fin 2)) : (language inputLanguage).Term (Empty ⊕ Fin 2)).bdEqual
+    (.var (.inr 1)) ⊓
+    Relations.boundedFormula₂ (L := language inputLanguage) (Sum.inr NumericRelation.le)
+      (.var (.inr 1)) (max inputLanguage)).ex.all
+
+-- The existentially bound variable can equal the surrounding universally bound variable.
+example :
+    (compile (n := 3) nested).eval Unbounded.interpretation ![false, true, false] = true ∧
+    (compile (n := 2) nested).eval Unbounded.interpretation ![true, false] = true := by decide
+
+private def markedAbove : (language inputLanguage).Sentence :=
+  (Relations.boundedFormula₂ (L := language inputLanguage) (Sum.inr NumericRelation.le)
+    (.var (.inr (0 : Fin 2))) (.var (.inr 1)) ⊓
+    Relations.boundedFormula₁ (L := language inputLanguage) (Sum.inl Relation.mark)
+      (.var (.inr 1))).ex.all
+
+-- Every x has a marked y above it exactly when max is marked. Reversing the two bound
+-- variables, or capturing the outer variable, changes one of these two verdicts.
+example :
+    (compile (n := 3) markedAbove).eval Unbounded.interpretation ![false, false, true] = true ∧
+    (compile (n := 3) markedAbove).eval Unbounded.interpretation ![true, false, false] = false :=
+  by decide
+
+private def allMarked : (language inputLanguage).Sentence :=
+  (Relations.boundedFormula₁ (L := language inputLanguage) (Sum.inl Relation.mark)
+    (.var (.inr 0))).all
+
+-- Quantifier expansion adds one gate, while its three relation-table leaves remain inputs.
+example :
+    (compile (n := 3) allMarked).size = 1 ∧
+    (compile (n := 3) allMarked).depth = 1 ∧
+    (compile (n := 3) allMarked).leafSize = 3 := by decide
+
+-- The correctness theorem applies to the same explicit enumeration used by computation.
+example (s : inputLanguage.Structure (Fin 3)) :
+    letI := s;
+    (compile (n := 3) mixed).eval Unbounded.interpretation
+      (ModelChecking.atomsOf (L := inputLanguage) (Equiv.refl _) ∘ (atomEquiv 3).symm) = true ↔
+        Fin 3 ⊨ mixed := by
+  let _ := s
+  exact (ModelChecking.Ordered.eval_toUnbounded_atomsOf (atomEquiv 3) mixed Fin.elim0).trans (by
+    rw [Sentence.Realize, Formula.Realize]
+    exact iff_of_eq (congrArg₂
+      (fun (v : Empty → Fin 3) (xs : Fin 0 → Fin 3) => BoundedFormula.Realize mixed v xs)
+      (Subsingleton.elim _ _) (Subsingleton.elim _ _)))
+
+private def emptyAtoms (n : ℕ) : ModelChecking.Atom Language.empty n ≃ Fin 0 where
+  toFun a := a.1.2.elim
+  invFun := Fin.elim0
+  left_inv a := a.1.2.elim
+  right_inv i := i.elim0
+
+-- No positive-arity input symbol is required: this is a formula on zero input bits.
+example :
+    (ModelChecking.Ordered.toUnbounded (n := 3) (emptyAtoms 3)
+      (bit Language.empty (max Language.empty) (one Language.empty)) Fin.elim0).eval
+        Unbounded.interpretation Fin.elim0 = true ∧
+    (ModelChecking.Ordered.toUnbounded (n := 2) (emptyAtoms 2)
+      ((zero Language.empty).equal (one Language.empty)) Fin.elim0).eval
+        Unbounded.interpretation Fin.elim0 = false := by decide
+
+private inductive NullaryRelation : ℕ → Type
+  | flag : NullaryRelation 0
+
+private abbrev nullaryLanguage : Language where
+  Functions _ := Empty
+  Relations := NullaryRelation
+
+private instance : nullaryLanguage.IsRelational := fun _ => inferInstance
+
+private def nullaryAtoms (n : ℕ) : ModelChecking.Atom nullaryLanguage n ≃ Fin 1 where
+  toFun _ := 0
+  invFun _ := ⟨⟨0, .flag⟩, Fin.elim0⟩
+  left_inv := by
+    rintro ⟨⟨_, r⟩, xs⟩
+    cases r
+    exact congrArg
+      (fun t : Fin 0 → Fin n => (⟨⟨0, NullaryRelation.flag⟩, t⟩ :
+        ModelChecking.Atom nullaryLanguage n)) (Subsingleton.elim _ _)
+  right_inv i := Subsingleton.elim _ _
+
+private def flag : (language nullaryLanguage).Sentence :=
+  .rel (Sum.inl NullaryRelation.flag) Fin.elim0
+
+-- A nullary input relation still contributes one input bit at every universe size.
+example :
+    (ModelChecking.Ordered.toUnbounded (n := 2) (nullaryAtoms 2) flag Fin.elim0).eval
+      Unbounded.interpretation ![true] = true ∧
+    (ModelChecking.Ordered.toUnbounded (n := 3) (nullaryAtoms 3) flag Fin.elim0).eval
+      Unbounded.interpretation ![false] = false ∧
+    (ModelChecking.Ordered.toUnbounded (n := 3) (nullaryAtoms 3) flag Fin.elim0).leafSize = 1 :=
+  by decide
+
+private instance : Fintype (Σ l, inputLanguage.Relations l) where
+  elems := {⟨1, Relation.mark⟩}
+  complete := by rintro ⟨_, r⟩; cases r; simp
+
+private def markedStructure {n : ℕ} [Fact (2 ≤ n)] (x : Fin n → Bool) :
+    Cslib.Logic.FO.Ordered.Structure inputLanguage :=
+  ⟨n, Fact.out, { RelMap := fun r t => match r with | .mark => x (t 0) = true }⟩
+
+private def evenMarked : Query inputLanguage :=
+  {M | Even (Nat.card {x : M //
+    FirstOrder.Language.Structure.RelMap (L := inputLanguage) Relation.mark ![x]})}
+
+-- The separated query has both accepting and rejecting canonical structures, including
+-- the empty predicate, an even nonempty predicate, and a singleton predicate.
+example : markedStructure ![false, false] ∈ evenMarked := by
+  change Even (Nat.card {x : Fin 2 // ![false, false] x = true})
+  rw [Nat.card_eq_fintype_card]
+  decide
+
+example : markedStructure ![true, true] ∈ evenMarked := by
+  change Even (Nat.card {x : Fin 2 // ![true, true] x = true})
+  rw [Nat.card_eq_fintype_card]
+  decide
+
+example : markedStructure ![true, false] ∉ evenMarked := by
+  change ¬ Even (Nat.card {x : Fin 2 // ![true, false] x = true})
+  rw [Nat.card_eq_fintype_card]
+  decide
+
+example : ¬ Definable evenMarked :=
+  ModelChecking.Ordered.not_definable_even_card (L := inputLanguage) Relation.mark
+
+end ComplexityTests.OrderedFirstOrderCircuits