diff --git a/Complexity.lean b/Complexity.lean
index ef5a5d1563..746cc4742c 100644
--- a/Complexity.lean
+++ b/Complexity.lean
@@ -1309,6 +1309,8 @@ public import Complexity.Computability.Complexity.Classes.Oracle.WitnessBit
 public import Complexity.Computability.Complexity.Classes.P
 public import Complexity.Computability.Complexity.Classes.P.Closure
 public import Complexity.Computability.Complexity.Classes.P.Complement
+public import Complexity.Computability.Complexity.Classes.P.FirstOrder
+public import Complexity.Computability.Complexity.Classes.P.FirstOrder.ModelChecker
 public import Complexity.Computability.Complexity.Classes.P.Slices
 public import Complexity.Computability.Complexity.Classes.P.WordRAM
 public import Complexity.Computability.Complexity.Classes.PCP
@@ -3419,6 +3421,7 @@ public import Complexity.Logics.FirstOrder.Ordered.FullTuple.Composition
 public import Complexity.Logics.FirstOrder.Ordered.FullTuple.DomainInterpretation
 public import Complexity.Logics.FirstOrder.Ordered.FullTuple.Encoding
 public import Complexity.Logics.FirstOrder.Ordered.Interpretation
+public import Complexity.Logics.FirstOrder.Ordered.LeastFixedPoint
 public import Complexity.Logics.FirstOrder.Ordered.Multiplication
 public import Complexity.Logics.FirstOrder.Ordered.Multiplication.Blocks
 public import Complexity.Logics.FirstOrder.Ordered.Multiplication.Bounds
diff --git a/Complexity/Computability/Complexity/Classes/P/FirstOrder.lean b/Complexity/Computability/Complexity/Classes/P/FirstOrder.lean
new file mode 100644
index 0000000000..0b79d68e53
--- /dev/null
+++ b/Complexity/Computability/Complexity/Classes/P/FirstOrder.lean
@@ -0,0 +1,260 @@
+/-
+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.Classes.P.FirstOrder.ModelChecker
+public import Complexity.Computability.Complexity.Classes.P
+public import Complexity.Logics.FirstOrder.Ordered.LeastFixedPoint
+import Complexity.Computability.Complexity.Fagin.Verifier
+import Complexity.Computability.Machines.Turing.MultiTape.Complexity.PolyTime.Iteration
+import Complexity.Computability.Machines.Turing.MultiTape.Complexity.PolyTime.BitString
+import Complexity.Computability.Machines.Turing.MultiTape.Complexity.PolyTime.Nat.Binary
+import Complexity.Computability.Machines.Turing.MultiTape.Complexity.PolyTime.Nat.Div
+
+/-!
+# Polynomial-time evaluation of ordered FO(LFP)
+
+For each fixed formula, the finite evaluator is computed by a native multi-tape Turing machine
+in polynomial time. The proof uses the library's certified closure rules for Boolean operations,
+bounded quantification, table construction and iteration. A fixed point's working table has
+exactly `n ^ k` bits after each step, so the loop calculus accounts for the size of intermediate
+states as well as the number of iterations.
+
+The input vocabulary and formula are fixed. Polynomial degrees may depend on the formula's
+quantifier nesting and relation arities; no polynomial combined-complexity claim is made when
+the formula itself is part of the input.
+
+## Main results
+
+* `Cslib.Logic.FO.LFP.ModelChecker.computableInPolyTime_eval`: the raw bounded evaluator has a
+  native polynomial-time certificate, uniformly in polynomial-time input assignments.
+* `Cslib.Logic.FO.LFP.ModelChecker.computableInPolyTime_modelChecker`: the sentence decider,
+  including shape and universe-size checks, is polynomial time.
+* `Cslib.Logic.FO.Ordered.LFPDefinable.encodedLanguage_mem_P`: every ordered FO(LFP)-definable
+  query belongs to the existing native machine class `P` under `encStructure`.
+
+## References
+
+* [N. Immerman, *Relational queries computable in polynomial time*][Immerman1986], Section 2.
+-/
+
+public section
+
+universe u v w
+
+open FirstOrder Language Turing.MultiTapeTM
+
+namespace Cslib.Logic.FO.LFP.ModelChecker
+
+variable {L : Language.{u, v}} [L.IsRelational] (v : Vocabulary L)
+
+open ComputableInPolyTime
+
+private theorem termValue_poly {α : Type w} (t : (Ordered.language L).Term α)
+    {γ : Type} {enc : γ ↪ List Bool} {n : γ → ℕ} {σ : γ → α → ℕ}
+    (hn : ComputableInPolyTime n enc encUnary)
+    (hσ : ∀ x, ComputableInPolyTime (fun a => σ a x) enc encUnary) :
+    ComputableInPolyTime (fun a => termValue (n a) (σ a) t) enc encUnary := by
+  cases t with
+  | var x => exact hσ x
+  | func f ts =>
+    cases f with
+    | inl f => exact isEmptyElim f
+    | inr c =>
+      cases c with
+      | zero => exact const 0
+      | one => exact const 1
+      | max => exact unary_sub.comp (hn.prod (const 1))
+
+private theorem valuesIndex_poly {k : ℕ} {γ : Type} {enc : γ ↪ List Bool}
+    {n : γ → ℕ} {xs : γ → Fin k → ℕ}
+    (hn : ComputableInPolyTime n enc encUnary)
+    (hxs : ∀ j, ComputableInPolyTime (fun a => xs a j) enc encUnary) :
+    ComputableInPolyTime (fun a => valuesIndex (n a) (xs a)) enc encUnary := by
+  induction k with
+  | zero => exact const 0
+  | succ k ih =>
+    exact unary_add.comp ((hxs 0).prod
+      (unary_mul.comp (hn.prod (ih fun j => hxs j.succ))))
+
+omit [L.IsRelational] in
+private theorem relBit_poly {k : ℕ} (r : (Ordered.language L).Relations k)
+    {γ : Type} {enc : γ ↪ List Bool} {a : γ → EncodedStructure} {xs : γ → Fin k → ℕ}
+    (ha : ComputableInPolyTime a enc encStructure)
+    (hxs : ∀ j, ComputableInPolyTime (fun x => xs x j) enc encUnary) :
+    ComputableInPolyTime (fun x => relBit v (a x) r (xs x)) enc encBool := by
+  cases r with
+  | inl r =>
+    exact bitsGetDWithInput
+      (v.computableInPolyTime_table ⟨_, r⟩ ha)
+      (valuesIndex_poly ha.fst' hxs) false
+  | inr r =>
+    cases r with
+    | le => exact unary_le' (hxs 0) (hxs 1)
+    | bit => exact binary_testBit (unary_to_binary.comp (hxs 0)) (hxs 1)
+
+private theorem foEval_poly {α : Type w} {k : ℕ}
+    (φ : (Ordered.language L).BoundedFormula α k) :
+    ∀ {γ : Type} {enc : γ ↪ List Bool} {a : γ → EncodedStructure} {σ : γ → α → ℕ}
+      {xs : γ → Fin k → ℕ},
+      ComputableInPolyTime a enc encStructure →
+      (∀ x, ComputableInPolyTime (fun y => σ y x) enc encUnary) →
+      (∀ j, ComputableInPolyTime (fun y => xs y j) enc encUnary) →
+      ComputableInPolyTime (fun y => foEval v (a y) (σ y) φ (xs y)) enc encBool := by
+  induction φ with
+  | falsum => intros; exact const false
+  | equal s t =>
+    intro γ enc a σ xs ha hσ hxs
+    have hv (z) : ComputableInPolyTime
+        (fun y => Sum.elim (σ y) (xs y) z) enc encUnary := by
+      cases z with
+      | inl x => exact hσ x
+      | inr j => exact hxs j
+    exact beq (termValue_poly s ha.fst' hv) (termValue_poly t ha.fst' hv)
+  | rel r ts =>
+    intro γ enc a σ xs ha hσ hxs
+    apply relBit_poly v r ha
+    intro j
+    apply termValue_poly (ts j) ha.fst'
+    intro z
+    cases z with
+    | inl x => exact hσ x
+    | inr j => exact hxs j
+  | imp φ ψ ihφ ihψ =>
+    intro γ enc a σ xs ha hσ hxs
+    exact bool_or.comp ((bool_not.comp (ihφ ha hσ hxs)).prod (ihψ ha hσ hxs))
+  | @all k φ ih =>
+    intro γ enc a σ xs ha hσ hxs
+    apply allWithInput (range.comp ha.fst')
+    apply ih (ha.comp (fst enc encUnary)) (fun x => (hσ x).comp (fst enc encUnary))
+    intro j
+    refine Fin.lastCases ?_ (fun i => ?_) j
+    · simpa only [Fin.snoc_last] using snd enc encUnary
+    · simpa only [Fin.snoc_castSucc, Function.comp_def] using
+        (hxs i).comp (fst enc encUnary)
+
+private theorem eval_poly {Γ : List ℕ} {α : Type w}
+    (φ : RawFormula (Ordered.language L) Γ α) :
+    ∀ {γ : Type} {enc : γ ↪ List Bool} {a : γ → EncodedStructure}
+      {tables : γ → List (List Bool)} {σ : γ → α → ℕ},
+      ComputableInPolyTime a enc encStructure →
+      ComputableInPolyTime tables enc (encList encBits) →
+      (∀ x, ComputableInPolyTime (fun y => σ y x) enc encUnary) →
+      ComputableInPolyTime (fun y => eval v φ (a y) (tables y) (σ y)) enc encBool := by
+  induction φ with
+  | ofFO φ =>
+    intro γ enc a tables σ ha ht hσ
+    exact foEval_poly v φ ha hσ (fun j => j.elim0)
+  | rel r ts =>
+    intro γ enc a tables σ ha ht hσ
+    exact bitsGetDWithInput ((listGetD []).comp (ht.prod (const (relIndex r))))
+      (valuesIndex_poly ha.fst' (fun j => termValue_poly (ts j) ha.fst' hσ)) false
+  | neg φ ih =>
+    intro γ enc a tables σ ha ht hσ
+    exact bool_not.comp (ih ha ht hσ)
+  | conj φ ψ ihφ ihψ =>
+    intro γ enc a tables σ ha ht hσ
+    exact bool_and.comp ((ihφ ha ht hσ).prod (ihψ ha ht hσ))
+  | ex φ ih =>
+    intro γ enc a tables σ ha ht hσ
+    apply anyWithInput (range.comp ha.fst')
+    apply ih (ha.comp (fst enc encUnary)) (ht.comp (fst enc encUnary))
+    intro z
+    cases z with
+    | none => exact snd enc encUnary
+    | some x => exact (hσ x).comp (fst enc encUnary)
+  | @op Γ α k body ts ih =>
+    intro γ enc a tables σ ha ht hσ
+    let tableStep (x : γ) (table : List Bool) :=
+      tableOf (a x).1 k (fun xs => eval v (body 0) (a x) (table :: tables x) (Sum.elim (σ x) xs))
+    have hcount : ComputableInPolyTime (fun x => (a x).1 ^ k) enc encUnary :=
+      (unary_pow k).comp ha.fst'
+    have hstep : ComputableInPolyTime
+        (fun p : γ × List Bool => tableStep p.1 p.2) (encPair enc encBits) encBits := by
+      apply mapToBitsWithInput (range.comp (hcount.comp (fst enc encBits)))
+      have hpar := fst (encPair enc encBits) encUnary
+      have hinput := (fst enc encBits).comp hpar
+      have hn := ha.fst'.comp hinput
+      apply ih 0 (ha.comp hinput)
+        (cons' ((snd enc encBits).comp hpar) (ht.comp hinput))
+      intro z
+      cases z with
+      | inl x => exact (hσ x).comp hinput
+      | inr j =>
+        exact unary_mod.comp ((unary_div.comp
+          ((snd (encPair enc encBits) encUnary).prod ((unary_pow j.val).comp hn))).prod hn)
+    have hiter : ComputableInPolyTime
+        (fun x => (tableStep x)^[(a x).1 ^ k] []) enc encBits := by
+      apply iterateWithInput_of_bounded_growth hcount (const []) hstep
+      refine ⟨hcount.polyBounded, ?_⟩
+      intro x state
+      simp [tableStep, encBits]
+    exact bitsGetDWithInput hiter
+      (valuesIndex_poly ha.fst' (fun j => termValue_poly (ts j) ha.fst' hσ)) false
+
+/-- Every fixed raw formula's bounded evaluator has a native polynomial-time implementation.
+The free variables may be any fixed family of polynomial-time numerical inputs. Formation is
+needed for semantic correctness, and is not needed for the cost bound. -/
+@[fun_prop]
+theorem computableInPolyTime_eval {Γ : List ℕ} {α : Type w}
+    (φ : RawFormula (Ordered.language L) Γ α) {γ : Type} {enc : γ ↪ List Bool}
+    {a : γ → EncodedStructure} {tables : γ → List (List Bool)} {σ : γ → α → ℕ}
+    (ha : ComputableInPolyTime a enc encStructure)
+    (ht : ComputableInPolyTime tables enc (encList encBits))
+    (hσ : ∀ x, ComputableInPolyTime (fun y => σ y x) enc encUnary) :
+    ComputableInPolyTime (fun y => eval v φ (a y) (tables y) (σ y)) enc encBool :=
+  eval_poly v φ ha ht hσ
+
+/-- Decide a fixed sentence, rejecting malformed relation tables and universes smaller than two. -/
+@[expose] def modelChecker (φ : RawFormula (Ordered.language L) [] Empty)
+    (a : EncodedStructure) : Bool :=
+  v.checkShape a && (decide (2 ≤ a.1) && eval v φ a [] Empty.elim)
+
+/-- The complete decision procedure, including its input checks, is native polynomial time. -/
+@[fun_prop] theorem computableInPolyTime_modelChecker
+    (φ : RawFormula (Ordered.language L) [] Empty) :
+    ComputableInPolyTime (modelChecker v φ) encStructure encBool := by
+  apply ComputableInPolyTime.bool_and' v.computableInPolyTime_checkShape
+  apply ComputableInPolyTime.bool_and'
+  · exact unary_le' (const 2) (fst encUnary (encList encBits))
+  · exact computableInPolyTime_eval v φ .id' (.const []) (fun x => x.elim)
+
+end Cslib.Logic.FO.LFP.ModelChecker
+
+namespace Cslib.Logic.FO.Ordered
+
+open Cslib.Complexity LFP.ModelChecker
+
+/-- Every ordered FO(LFP)-definable query is in the native class `P`, using the existing
+source-only structure encoding. The formula is uniform over all canonical finite structures. -/
+theorem LFPDefinable.encodedLanguage_mem_P {L : Language} [L.IsRelational]
+    {K : Query L} (hK : LFPDefinable K) (v : Vocabulary L) :
+    K.encodedLanguage v ∈ P encStructure := by
+  obtain ⟨φ, hφ⟩ := hK
+  refine ⟨modelChecker v φ.val, computableInPolyTime_modelChecker v φ.val, fun a => ?_⟩
+  simp only [Query.encodedLanguage, Set.mem_ofPred_eq, modelChecker, Bool.and_eq_true,
+    Vocabulary.checkShape_eq_true_iff, decide_eq_true_eq]
+  have hrels : @relations [] a.1 [] = @Operator.RelEnv.empty (Fin a.1) := by
+    funext k r
+    exact nomatch r
+  have hempty : (fun x : Empty => (Empty.elim x : Fin a.1).val) = Empty.elim :=
+    Subsingleton.elim _ _
+  constructor
+  · rintro ⟨hshape, hn, hmem⟩
+    refine ⟨hshape, hn, ?_⟩
+    have hreal := (hφ (decoded v a hn)).mp hmem
+    have heval := eval_eq_true_iff v hn φ.val φ.property [] (Empty.elim : Empty → Fin a.1)
+    rw [hrels, hempty] at heval
+    exact heval.mpr hreal
+  · rintro ⟨hshape, hn, heval⟩
+    refine ⟨hshape, hn, (hφ (decoded v a hn)).mpr ?_⟩
+    have hreal := eval_eq_true_iff v hn φ.val φ.property [] (Empty.elim : Empty → Fin a.1)
+    rw [hrels, hempty] at hreal
+    exact hreal.mp heval
+
+end Cslib.Logic.FO.Ordered
diff --git a/Complexity/Computability/Complexity/Classes/P/FirstOrder/ModelChecker.lean b/Complexity/Computability/Complexity/Classes/P/FirstOrder/ModelChecker.lean
new file mode 100644
index 0000000000..49f0ca52c3
--- /dev/null
+++ b/Complexity/Computability/Complexity/Classes/P/FirstOrder/ModelChecker.lean
@@ -0,0 +1,333 @@
+/-
+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.Operator.LeastFixedPoint
+public import Complexity.Logics.FirstOrder.Ordered.Query
+public import Complexity.Logics.FirstOrder.Encoding
+
+/-!
+# A finite model checker for ordered FO(LFP)
+
+The formula is fixed while the finite input structure varies. Each least fixed point is computed
+by iterating its body `n ^ k` times on a truth table, where `n` is the universe size and `k` is
+the relation arity. Outer assignments and relation tables remain fixed throughout the iteration.
+Nested fixed points use the same evaluator recursively.
+
+The evaluator is defined on raw syntax and all encoded inputs. Its agreement with least-fixed-point
+semantics requires the formula's formation certificate and a universe of size at least two, as
+in the library's canonical ordered structures. Malformed input tables are dealt with separately
+by the final decision procedure.
+
+## Main results
+
+* `Cslib.Logic.FO.LFP.ModelChecker.eval_eq_true_iff`: bounded evaluation agrees with realization
+  of every well-formed formula, including nested fixed points and captured parameters.
+* `Cslib.Logic.FO.LFP.ModelChecker.getD_tableOf`: tabulation uses the same tuple numbering as
+  encoded input relations.
+
+## References
+
+* [N. Immerman, *Relational queries computable in polynomial time*][Immerman1986],
+  Section 2, Fact 2.1, for the finite iteration bound.
+-/
+
+public section
+
+universe u v w
+
+open FirstOrder Language
+
+namespace Cslib.Logic.FO.LFP.ModelChecker
+
+variable {L : Language.{u, v}} [L.IsRelational]
+
+/-- The index of a scoped relation variable in the stack of truth tables. -/
+@[expose] def relIndex {Γ : List ℕ} {k : ℕ} : Operator.RelVar Γ k → ℕ
+  | .here => 0
+  | .there r => relIndex r + 1
+
+/-- A term's numerical value. Input vocabularies are relational; numeric functions are constants. -/
+@[expose] def termValue {α : Type w} (n : ℕ) (σ : α → ℕ) :
+    (Ordered.language L).Term α → ℕ
+  | .var x => σ x
+  | .func (.inl f) _ => isEmptyElim f
+  | .func (.inr c) _ => c.index n
+
+/-- The colexicographic truth-table index of a tuple of natural-number coordinates. -/
+@[expose] def valuesIndex (n : ℕ) : {k : ℕ} → (Fin k → ℕ) → ℕ
+  | 0, _ => 0
+  | _ + 1, xs => xs 0 + n * valuesIndex n (fun j => xs j.succ)
+
+/-- Input atoms read the supplied tables; order and BIT are computed from natural indices. -/
+@[expose] def relBit (v : Vocabulary L) (a : EncodedStructure) {k : ℕ}
+    (r : (Ordered.language L).Relations k) (xs : Fin k → ℕ) : Bool :=
+  match r with
+  | .inl r => (v.table a ⟨_, r⟩).getD (valuesIndex a.1 xs) false
+  | .inr .le => decide (xs 0 ≤ xs 1)
+  | .inr .bit => (xs 0).testBit (xs 1)
+
+/-- Evaluate an ordinary bounded formula with separate free and bound assignments. -/
+@[expose] def foEval (v : Vocabulary L) (a : EncodedStructure) {α : Type w} (σ : α → ℕ) :
+    {k : ℕ} → (Ordered.language L).BoundedFormula α k → (Fin k → ℕ) → Bool
+  | _, .falsum, _ => false
+  | _, .equal s t, xs =>
+    termValue a.1 (Sum.elim σ xs) s == termValue a.1 (Sum.elim σ xs) t
+  | _, .rel r ts, xs =>
+    relBit v a r (fun j => termValue a.1 (Sum.elim σ xs) (ts j))
+  | _, .imp φ ψ, xs => !foEval v a σ φ xs || foEval v a σ ψ xs
+  | _, .all φ, xs => (List.range a.1).all (fun x => foEval v a σ φ (Fin.snoc xs x))
+
+/-- Tabulate a Boolean predicate over all tuples, with coordinate zero the least significant. -/
+@[expose] def tableOf (n k : ℕ) (f : (Fin k → ℕ) → Bool) : List Bool :=
+  (List.range (n ^ k)).map (fun i => f (fun j => i / n ^ (j : ℕ) % n))
+
+/-- A raw FO(LFP) evaluator. Bounded iteration gives a total algorithm even for invalid syntax. -/
+@[expose] def eval (v : Vocabulary L) : {Γ : List ℕ} → {α : Type w} →
+    RawFormula (Ordered.language L) Γ α → EncodedStructure → List (List Bool) → (α → ℕ) → Bool
+  | _, _, .ofFO φ, a, _, σ => foEval v a σ φ Fin.elim0
+  | _, _, .rel r ts, a, tables, σ =>
+    (tables.getD (relIndex r) []).getD
+      (valuesIndex a.1 (fun j => termValue a.1 σ (ts j))) false
+  | _, _, .neg φ, a, tables, σ => !eval v φ a tables σ
+  | _, _, .conj φ ψ, a, tables, σ => eval v φ a tables σ && eval v ψ a tables σ
+  | _, _, .ex φ, a, tables, σ =>
+    (List.range a.1).any (fun x => eval v φ a tables (Option.elim · x σ))
+  | _, _, .op k body ts, a, tables, σ =>
+    let step := fun table : List Bool =>
+      tableOf a.1 k (fun xs => eval v (body 0) a (table :: tables) (Sum.elim σ xs))
+    ((step^[a.1 ^ k]) []).getD
+      (valuesIndex a.1 (fun j => termValue a.1 σ (ts j))) false
+
+/-- Read one relation table using the standard tuple numbering. -/
+@[expose] def tableRelation (n k : ℕ) (table : List Bool) : Set (Fin k → Fin n) :=
+  {xs | table.getD (tupleIndex xs) false = true}
+
+/-- Interpret a stack of relation tables at the arities of a scoped context. -/
+@[expose] def relations (Γ : List ℕ) (n : ℕ) (tables : List (List Bool)) :
+    Operator.RelEnv Γ (Fin n) :=
+  fun {k} r => tableRelation n k (tables.getD (relIndex r) [])
+
+/-- An empty table denotes the empty relation, including nullary relations. -/
+@[simp] theorem tableRelation_nil (n k : ℕ) : tableRelation n k [] = ∅ := by
+  ext xs
+  simp [tableRelation]
+
+/-- Extending the table stack agrees with the typed relation binder. -/
+theorem relations_cons (Γ : List ℕ) (n k : ℕ) (table : List Bool) (tables : List (List Bool)) :
+    @relations (k :: Γ) n (table :: tables) =
+      @Operator.RelEnv.cons Γ (Fin n) k (tableRelation n k table) (@relations Γ n tables) := by
+  funext l r
+  cases r with
+  | here => rfl
+  | there r => simp [relations, relIndex, Operator.RelEnv.cons]
+
+/-- A tabulation always has exactly one bit per tuple, including for arity zero. -/
+@[simp] theorem length_tableOf (n k : ℕ) (f : (Fin k → ℕ) → Bool) :
+    (tableOf n k f).length = n ^ k := by
+  simp [tableOf]
+
+/-- Reading a tabulated predicate recovers its value on the given tuple. -/
+theorem getD_tableOf {n k : ℕ} (f : (Fin k → ℕ) → Bool) (xs : Fin k → Fin n) :
+    (tableOf n k f).getD (tupleIndex xs) false = f (fun j => (xs j : ℕ)) := by
+  rw [List.getD_eq_getElem _ _ (by simpa only [length_tableOf] using tupleIndex_lt xs)]
+  simp only [tableOf, List.getElem_map, List.getElem_range]
+  congr 1
+  funext j
+  simpa only [tupleIndex, Equiv.symm_apply_apply] using
+    (finFunctionFinEquiv_symm_apply_val (finFunctionFinEquiv xs) j).symm
+
+/-- Natural coordinates give the standard truth-table index. -/
+theorem valuesIndex_val {n k : ℕ} (xs : Fin k → Fin n) :
+    valuesIndex n (fun j => (xs j : ℕ)) = tupleIndex xs := by
+  induction k with
+  | zero => simp [valuesIndex, tupleIndex_apply]
+  | succ k ih =>
+    rw [valuesIndex, ih, tupleIndex_apply, tupleIndex_apply, Fin.sum_univ_succ,
+      Fin.val_zero, pow_zero, mul_one, Finset.mul_sum]
+    congr 1
+    refine Finset.sum_congr rfl fun j _ => ?_
+    rw [Fin.val_succ, pow_succ]
+    ring
+
+section Correctness
+
+variable (v : Vocabulary L) {a : EncodedStructure}
+  [L.Structure (Fin a.1)] [Fact (2 ≤ a.1)]
+  (hinput : ∀ {k} (r : L.Relations k) (xs : Fin k → Fin a.1),
+    (v.table a ⟨k, r⟩).getD (tupleIndex xs) false = true ↔ Language.Structure.RelMap r xs)
+
+/-- Ordered term evaluation agrees with native Mathlib realization. -/
+private theorem termValue_eq {α : Type w} (σ : α → Fin a.1) (t : (Ordered.language L).Term α) :
+    termValue a.1 (fun x => (σ x : ℕ)) t = Fin.val (t.realize σ) := by
+  cases t with
+  | var x => rfl
+  | func f ts =>
+    cases f with
+    | inl f => exact isEmptyElim f
+    | inr c => rfl
+
+include hinput
+
+omit [L.IsRelational] in
+/-- Atoms read exactly the decoded input relations and canonical numeric relations. -/
+private theorem relBit_eq_true_iff {k : ℕ} (r : (Ordered.language L).Relations k)
+    (xs : Fin k → Fin a.1) :
+    relBit v a r (fun j => (xs j : ℕ)) = true ↔ Language.Structure.RelMap r xs := by
+  cases r with
+  | inl r =>
+    change (v.table a ⟨k, r⟩).getD (valuesIndex a.1 (fun j => (xs j : ℕ))) false = true ↔
+      Language.Structure.RelMap r xs
+    rw [valuesIndex_val]
+    exact hinput r xs
+  | inr r =>
+    cases r with
+    | le => change decide ((xs 0).val ≤ (xs 1).val) = true ↔ xs 0 ≤ xs 1; simp
+    | bit => rfl
+
+/-- The first-order evaluator decides Mathlib's bounded-formula semantics. -/
+private theorem foEval_eq_true_iff {α : Type w} (σ : α → Fin a.1) {k : ℕ}
+    (φ : (Ordered.language L).BoundedFormula α k) (xs : Fin k → Fin a.1) :
+    foEval v a (fun x => (σ x : ℕ)) φ (fun j => (xs j : ℕ)) = true ↔
+      φ.Realize σ xs := by
+  induction φ with
+  | falsum => simp [foEval, BoundedFormula.Realize]
+  | equal s t =>
+    have hσ : Sum.elim (fun x => (σ x : ℕ)) (fun j => (xs j : ℕ)) =
+        fun x => Fin.val (Sum.elim σ xs x) := by funext x; cases x <;> rfl
+    simp only [foEval, hσ, termValue_eq, beq_iff_eq, Fin.val_inj,
+      BoundedFormula.Realize]
+  | rel r ts =>
+    have hσ : Sum.elim (fun x => (σ x : ℕ)) (fun j => (xs j : ℕ)) =
+        fun x => Fin.val (Sum.elim σ xs x) := by funext x; cases x <;> rfl
+    simp only [foEval, hσ, termValue_eq, relBit_eq_true_iff v hinput,
+      BoundedFormula.Realize]
+  | imp φ ψ ihφ ihψ =>
+    simp only [foEval, Bool.or_eq_true, Bool.not_eq_true', ← Bool.not_eq_true, ihφ, ihψ,
+      BoundedFormula.realize_imp]
+    tauto
+  | all φ ih =>
+    simp only [foEval, List.all_eq_true, List.mem_range, BoundedFormula.realize_all]
+    constructor
+    · intro h x
+      apply (ih (Fin.snoc xs x)).mp
+      convert h x x.isLt using 1
+      congr 1
+      funext i
+      exact (Fin.lastCases (by simp) (fun j => by simp) i)
+    · intro h x hx
+      have := (ih (Fin.snoc xs ⟨x, hx⟩)).mpr (h ⟨x, hx⟩)
+      convert this using 1
+      congr 1
+      funext i
+      exact (Fin.lastCases (by simp) (fun j => by simp) i)
+
+/-- The bounded evaluator agrees with the semantics of every well-formed, possibly nested LFP
+formula. Relation variables are interpreted by the supplied truth-table stack. -/
+private theorem eval_correct {Γ : List ℕ} {α : Type w}
+    (φ : RawFormula (Ordered.language L) Γ α) (hφ : φ.wellFormed policy = true)
+    (tables : List (List Bool)) (σ : α → Fin a.1) :
+    eval v φ a tables (fun x => (σ x : ℕ)) = true ↔
+      φ.Realize interpretation (relations Γ a.1 tables) σ := by
+  induction φ generalizing tables with
+  | ofFO φ =>
+    have h := foEval_eq_true_iff v hinput σ φ Fin.elim0
+    have hzero : (fun j : Fin 0 => (Fin.elim0 j : Fin a.1).val) = Fin.elim0 :=
+      Subsingleton.elim _ _
+    have hdefault : (default : Fin 0 → Fin a.1) = Fin.elim0 := Subsingleton.elim _ _
+    simpa only [eval, Operator.Formula.realize_ofFO, FirstOrder.Language.Formula.Realize,
+      hzero, hdefault] using h
+  | rel r ts =>
+    simp only [eval, termValue_eq, valuesIndex_val, Operator.Formula.realize_rel,
+      relations, tableRelation, Set.mem_ofPred_eq]
+  | neg φ ih =>
+    simpa only [eval, Bool.not_eq_true', ← Bool.not_eq_true, Operator.Formula.realize_neg]
+      using not_congr (ih hφ tables σ)
+  | conj φ ψ ihφ ihψ =>
+    have ⟨hφ, hψ⟩ : φ.wellFormed policy = true ∧ ψ.wellFormed policy = true := by
+      simpa only [Operator.Formula.wellFormed, Bool.and_eq_true] using hφ
+    simpa only [eval, Bool.and_eq_true, Operator.Formula.realize_conj] using
+      and_congr (ihφ hφ tables σ) (ihψ hψ tables σ)
+  | ex φ ih =>
+    simp only [eval, List.any_eq_true, List.mem_range, Operator.Formula.realize_ex]
+    constructor
+    · rintro ⟨x, hx, heval⟩
+      refine ⟨⟨x, hx⟩, (ih hφ tables (Option.elim · ⟨x, hx⟩ σ)).mp ?_⟩
+      convert heval using 1
+      congr 1
+      funext y
+      cases y <;> rfl
+    · rintro ⟨x, hx⟩
+      refine ⟨x, x.isLt, ?_⟩
+      have := (ih hφ tables (Option.elim · x σ)).mpr hx
+      convert this using 1
+      congr 1
+      funext y
+      cases y <;> rfl
+  | @op Γ α k body ts ih =>
+    have hop : Operator.Formula.op k body ts = lfp (body 0) ts := by
+      unfold lfp
+      congr 1
+      funext i
+      have hi : i = 0 := Subsingleton.elim i 0
+      subst i
+      rfl
+    rw [hop] at hφ ⊢
+    obtain ⟨hbody, hpos⟩ := (wellFormed_lfp (body 0) ts).mp hφ
+    let tableStep := fun table : List Bool =>
+      tableOf a.1 k (fun xs => eval v (body 0) a (table :: tables)
+        (Sum.elim (fun x => (σ x : ℕ)) xs))
+    have hstep (table : List Bool) :
+        tableRelation a.1 k (tableStep table) =
+          step (body 0) (relations Γ a.1 tables) σ (tableRelation a.1 k table) := by
+      ext xs
+      change (tableStep table).getD (tupleIndex xs) false = true ↔ _
+      rw [show tableStep table = tableOf a.1 k (fun ys =>
+        eval v (body 0) a (table :: tables) (Sum.elim (fun x => (σ x : ℕ)) ys)) from rfl,
+        getD_tableOf]
+      have hσ : Sum.elim (fun x => (σ x : ℕ)) (fun j => (xs j : ℕ)) =
+          fun x => Fin.val (Sum.elim σ xs x) := by funext x; cases x <;> rfl
+      rw [hσ, ih 0 hbody (table :: tables) (Sum.elim σ xs)]
+      exact iff_of_eq (congrArg
+        (fun ρ : Operator.RelEnv (k :: Γ) (Fin a.1) =>
+          (body 0).Realize interpretation ρ (Sum.elim σ xs))
+        (relations_cons Γ a.1 k table tables))
+    have hiter (i : ℕ) :
+        tableRelation a.1 k (tableStep^[i] []) =
+          (step (body 0) (relations Γ a.1 tables) σ)^[i] ∅ := by
+      induction i with
+      | zero => exact tableRelation_nil _ _
+      | succ i hi => rw [Function.iterate_succ_apply', hstep, hi,
+          Function.iterate_succ_apply']
+    rw [realize_lfp (body 0) hpos]
+    change (tableStep^[a.1 ^ k] []).getD
+      (valuesIndex a.1 (fun j => termValue a.1 (fun x => (σ x : ℕ)) (ts j))) false = true ↔ _
+    simp only [termValue_eq, valuesIndex_val]
+    change (fun j => (ts j).realize σ) ∈ tableRelation a.1 k (tableStep^[a.1 ^ k] []) ↔ _
+    rw [hiter]
+    have hfinite := iterate_card_pow_eq_lfp (body 0) hpos (relations Γ a.1 tables) σ
+    rw [show (step (body 0) (relations Γ a.1 tables) σ)^[a.1 ^ k] ∅ =
+      (stepHom (body 0) hpos (relations Γ a.1 tables) σ).lfp by
+        simpa only [Fintype.card_fin] using hfinite]
+
+end Correctness
+
+/-- The bounded evaluator decides the standard realization of every checked formula in the
+canonical ordered expansion of a decoded input. -/
+theorem eval_eq_true_iff (v : Vocabulary L) {a : EncodedStructure} (hn : 2 ≤ a.1)
+    {Γ : List ℕ} {α : Type w} (φ : RawFormula (Ordered.language L) Γ α)
+    (hφ : φ.wellFormed policy = true) (tables : List (List Bool)) (σ : α → Fin a.1) :
+    letI := v.decode a
+    letI : Fact (2 ≤ a.1) := ⟨hn⟩
+    eval v φ a tables (fun x => (σ x : ℕ)) = true ↔
+      φ.Realize interpretation (relations Γ a.1 tables) σ := by
+  let _ := v.decode a
+  let _ : Fact (2 ≤ a.1) := ⟨hn⟩
+  exact eval_correct v (fun _ _ => Iff.rfl) φ hφ tables σ
+
+end Cslib.Logic.FO.LFP.ModelChecker
diff --git a/Complexity/Logics/FirstOrder/Ordered/LeastFixedPoint.lean b/Complexity/Logics/FirstOrder/Ordered/LeastFixedPoint.lean
new file mode 100644
index 0000000000..fbf776174d
--- /dev/null
+++ b/Complexity/Logics/FirstOrder/Ordered/LeastFixedPoint.lean
@@ -0,0 +1,49 @@
+/-
+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 Complexity.Logics.FirstOrder.Operator.LeastFixedPoint
+
+/-!
+# Least-fixed-point definability of ordered queries
+
+An ordered query is `LFPDefinable` if a single checked FO(LFP) sentence defines it on all
+canonically ordered structures. The input relations vary, while order, BIT, and the numeric
+constants retain the meanings supplied by `Ordered.language`. Structures have at least two
+elements, as in the existing ordered-query convention.
+
+This is the logical side of the Immerman–Vardi characterization. The machine side uses the
+existing source-only `Query.encodedLanguage` and native polynomial-time class.
+
+## References
+
+* [N. Immerman, *Relational Queries Computable in Polynomial Time*][Immerman1986], Theorem 1.
+-/
+
+public section
+
+open FirstOrder Language
+
+namespace Cslib.Logic.FO.Ordered
+
+/-- One checked least-fixed-point sentence defines the query uniformly over all ordered inputs. -/
+@[expose] def LFPDefinable {L : Language} (K : Query L) : Prop :=
+  ∃ φ : LFP.Formula (language L) [] Empty,
+    ∀ M : Structure L, M ∈ K ↔ φ.Realize (M := M) Operator.RelEnv.empty Empty.elim
+
+/-- Ordinary ordered first-order definability embeds into least-fixed-point definability. -/
+theorem Definable.lfpDefinable {L : Language} {K : Query L} (hK : Definable K) :
+    LFPDefinable K := by
+  obtain ⟨φ, hφ⟩ := hK
+  refine ⟨⟨.ofFO φ, rfl⟩, fun M => ?_⟩
+  have he : (default : Empty → M) = Empty.elim := Subsingleton.elim _ _
+  simpa only [LFP.Formula.Realize, Operator.Formula.Realize,
+    FirstOrder.Language.Sentence.Realize, he] using hφ M
+
+end Cslib.Logic.FO.Ordered
diff --git a/ComplexityTests/FOLeastFixedPointPolyTime.lean b/ComplexityTests/FOLeastFixedPointPolyTime.lean
new file mode 100644
index 0000000000..71c02114f2
--- /dev/null
+++ b/ComplexityTests/FOLeastFixedPointPolyTime.lean
@@ -0,0 +1,115 @@
+import Complexity.Computability.Complexity.Classes.P.FirstOrder
+import Mathlib.ModelTheory.Graph
+
+/-! Executable ordered FO(LFP) clients: genuine iteration, nested binders, captured parameters,
+numeric atoms, nullary tables, and rejection of malformed or undersized inputs. -/
+
+open FirstOrder Language Cslib.Logic Cslib.Logic.FO
+
+namespace ComplexityTests.FOLeastFixedPointPolyTime
+
+private abbrev L := Ordered.language Language.empty
+
+private def vocabulary : Vocabulary Language.empty where
+  count := 0
+  symbol := Equiv.equivOfIsEmpty _ _
+
+private def truth : LFP.RawFormula L [] Empty := .ofFO ⊤
+
+example : LFP.ModelChecker.modelChecker vocabulary truth (2, []) = true := by decide
+example : LFP.ModelChecker.modelChecker vocabulary truth (0, []) = false := by decide
+example : LFP.ModelChecker.modelChecker vocabulary truth (1, []) = false := by decide
+example : LFP.ModelChecker.modelChecker vocabulary truth (2, [ [true] ]) = false := by decide
+
+-- Every relation is a fixed point of the identity operator; its least fixed point is empty.
+private def identity : LFP.RawFormula L [] Empty :=
+  LFP.lfp (.rel .here ![.var (.inr 0)]) ![Ordered.zero Language.empty]
+
+example : LFP.ModelChecker.modelChecker vocabulary identity (2, []) = false := by decide
+
+-- The second disjunct becomes true only after the first stage inserts zero.
+private def grow : LFP.RawFormula L [1] (Empty ⊕ Fin 1) :=
+  .disj (.ofFO ((Term.var (.inr 0)).equal (Ordered.zero Language.empty)))
+    (.conj (.rel .here ![Ordered.zero Language.empty])
+      (.ofFO ((Term.var (.inr 0)).equal (Ordered.one Language.empty))))
+
+private def reachesOne : LFP.RawFormula L [] Empty :=
+  LFP.lfp grow ![Ordered.one Language.empty]
+
+private def reachesMax : LFP.RawFormula L [] Empty :=
+  LFP.lfp grow ![Ordered.max Language.empty]
+
+example : reachesOne.wellFormed LFP.policy = true := by decide
+example : LFP.ModelChecker.modelChecker vocabulary reachesOne (2, []) = true := by decide
+example : LFP.ModelChecker.modelChecker vocabulary reachesMax (2, []) = true := by decide
+example : LFP.ModelChecker.modelChecker vocabulary reachesMax (3, []) = false := by decide
+
+-- The inner binder reads the outer approximation through `there here`.
+private def nested : LFP.RawFormula L [] Empty :=
+  LFP.lfp
+    (LFP.lfp
+      (.disj (.ofFO ((Term.var (.inr 0)).equal (Ordered.zero Language.empty)))
+        (.rel (.there .here) ![Ordered.zero Language.empty]))
+      ![.var (.inr 0)])
+    ![Ordered.one Language.empty]
+
+example : nested.wellFormed LFP.policy = true := by decide
+example : LFP.ModelChecker.modelChecker vocabulary nested (2, []) = true := by decide
+
+private def parameter : LFP.RawFormula L [] Bool :=
+  LFP.lfp (.ofFO ((Term.var (.inr 0)).equal (.var (.inl false)))) ![.var true]
+
+example : LFP.ModelChecker.eval vocabulary parameter (2, []) []
+    (fun b => if b then 1 else 0) = false := by decide
+example : LFP.ModelChecker.eval vocabulary parameter (2, []) [] (fun _ => 0) = true := by decide
+
+-- The table of a nullary relation still has one bit when the domain is empty.
+private def nullary : LFP.RawFormula L [] Empty := LFP.lfp (.ofFO ⊤) Fin.elim0
+
+example : LFP.ModelChecker.eval vocabulary nullary (0, []) [] Empty.elim = true := by decide
+
+private def numeric : LFP.RawFormula L [] Empty :=
+  .ofFO (Ordered.bit Language.empty (Ordered.max Language.empty) (Ordered.one Language.empty))
+
+example : LFP.ModelChecker.modelChecker vocabulary numeric (2, []) = false := by decide
+example : LFP.ModelChecker.modelChecker vocabulary numeric (3, []) = true := by decide
+
+private def quantified : LFP.RawFormula L [] Empty :=
+  .ex (.ofFO (Ordered.bit Language.empty (.var none) (Ordered.one Language.empty)))
+
+example : LFP.ModelChecker.modelChecker vocabulary quantified (2, []) = false := by decide
+example : LFP.ModelChecker.modelChecker vocabulary quantified (3, []) = true := by decide
+
+private def bounded : LFP.RawFormula L [] Empty :=
+  .ofFO (.all (.rel (.inr .le) ![.var (.inr 0), Ordered.max Language.empty]))
+
+example : LFP.ModelChecker.modelChecker vocabulary bounded (2, []) = true := by decide
+
+private def graphVocabulary : Vocabulary Language.graph where
+  count := 1
+  symbol :=
+    { toFun := fun _ => ⟨2, FirstOrder.Language.adj⟩
+      invFun := fun _ => 0
+      left_inv := fun _ => Subsingleton.elim _ _
+      right_inv := fun ⟨_, .adj⟩ => rfl }
+
+private def forwardEdge : LFP.RawFormula (Ordered.language Language.graph) [] Empty :=
+  .ofFO (Relations.formula₂ (.inl FirstOrder.Language.adj)
+    (Ordered.zero Language.graph) (Ordered.max Language.graph))
+
+private def backwardEdge : LFP.RawFormula (Ordered.language Language.graph) [] Empty :=
+  .ofFO (Relations.formula₂ (.inl FirstOrder.Language.adj)
+    (Ordered.max Language.graph) (Ordered.zero Language.graph))
+
+-- The first coordinate is the least significant truth-table digit.
+example : LFP.ModelChecker.modelChecker graphVocabulary forwardEdge
+    (2, [ [false, false, true, false] ]) = true := by decide
+example : LFP.ModelChecker.modelChecker graphVocabulary backwardEdge
+    (2, [ [false, false, true, false] ]) = false := by decide
+
+-- The native machine certificate is discoverable by the usual automation.
+example : Turing.MultiTapeTM.ComputableInPolyTime
+    (LFP.ModelChecker.modelChecker vocabulary nested) encStructure Turing.MultiTapeTM.encBool := by
+  fun_prop
+
+end ComplexityTests.FOLeastFixedPointPolyTime