diff --git a/Complexity.lean b/Complexity.lean
index 967229e6c..8c090fd2d 100644
--- a/Complexity.lean
+++ b/Complexity.lean
@@ -2806,7 +2806,10 @@ public import Complexity.Logics.FirstOrder.Operator.Definability
 public import Complexity.Logics.FirstOrder.Operator.Definability.Polarity
 public import Complexity.Logics.FirstOrder.Operator.LeastFixedPoint
 public import Complexity.Logics.FirstOrder.Operator.LeastFixedPoint.Definability
+public import Complexity.Logics.FirstOrder.Operator.LeastFixedPoint.Tuple
+public import Complexity.Logics.FirstOrder.Operator.LeastFixedPoint.Tuple.Semantics
 public import Complexity.Logics.FirstOrder.Operator.Polarity
+public import Complexity.Logics.FirstOrder.Operator.Quantifiers
 public import Complexity.Logics.FirstOrder.Operator.Relabel
 public import Complexity.Logics.FirstOrder.Operator.TransitiveClosure
 public import Complexity.Logics.FirstOrder.Operator.TransitiveClosure.Definability
@@ -2820,10 +2823,13 @@ public import Complexity.Logics.FirstOrder.Ordered.DomainInterpretation
 public import Complexity.Logics.FirstOrder.Ordered.DomainInterpretation.Certificate
 public import Complexity.Logics.FirstOrder.Ordered.DomainInterpretation.Composition
 public import Complexity.Logics.FirstOrder.Ordered.DomainInterpretation.Encoding
+public import Complexity.Logics.FirstOrder.Ordered.Encoding
 public import Complexity.Logics.FirstOrder.Ordered.FullTuple
 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.FullTuple.LeastFixedPoint
+public import Complexity.Logics.FirstOrder.Ordered.FullTuple.Power
 public import Complexity.Logics.FirstOrder.Ordered.Interpretation
 public import Complexity.Logics.FirstOrder.Ordered.LeastFixedPoint
 public import Complexity.Logics.FirstOrder.Ordered.Multiplication
@@ -2838,6 +2844,7 @@ public import Complexity.Logics.FirstOrder.Ordered.Radix.Conversion
 public import Complexity.Logics.FirstOrder.Ordered.Radix.Decode
 public import Complexity.Logics.FirstOrder.Ordered.Radix.Multiplication
 public import Complexity.Logics.FirstOrder.Ordered.Reduction
+public import Complexity.Logics.FirstOrder.Ordered.StrictOrder
 public import Complexity.Logics.FirstOrder.Ordered.Tuple
 public import Complexity.Logics.FirstOrder.Ordered.Tuple.Flatten
 public import Complexity.Logics.FirstOrder.Ordered.TupleBit
diff --git a/Complexity/Computability/Complexity/Fagin/Ordered.lean b/Complexity/Computability/Complexity/Fagin/Ordered.lean
index 0949cd6b7..4b2898ac4 100644
--- a/Complexity/Computability/Complexity/Fagin/Ordered.lean
+++ b/Complexity/Computability/Complexity/Fagin/Ordered.lean
@@ -8,7 +8,7 @@ module
 -- upstream: candidate
 
 public import Complexity.Computability.Complexity.Fagin.Converse
-public import Complexity.Logics.FirstOrder.Ordered.Query
+public import Complexity.Logics.FirstOrder.Ordered.StrictOrder
 public import Complexity.Computability.Complexity.Classes.LogSpace.FirstOrder.Ordered
 import Complexity.Computability.Complexity.Reduction
 
@@ -76,42 +76,6 @@ theorem Definable.encodedLanguage_mem_NP {L : Language} [L.IsRelational] (v : Vo
   rw [hK', encodedLanguage_sentence]
   exact P_subset_NP (L_subset_P (queryLanguage_mem_L v φ))
 
-/-- The one-dimensional interpretation retaining the input relations and reading strict order
-from canonical non-strict order. -/
-private def strictOrderInterpretation (L : Language.{u, v}) :
-    FO.Interpretation (language L) (L.sum ESO.orderLanguage) Unit where
-  domain := ⊤
-  rel := fun {n} r => match r with
-    | .inl R => Relations.formula (L := language L) (Sum.inl R) fun i => .var (i, ())
-    | .inr r => by
-      rcases r with ⟨⟨⟩, h⟩
-      subst n
-      exact ∼(Relations.formula (L := language L) (Sum.inr NumericRelation.le)
-        fun i => .var (if i = 0 then 1 else 0, ()))
-
-/-- The canonical strict-order structure interpreted above is the original ordered universe. -/
-private def strictOrderEquiv {L : Language.{u, v}} [L.IsRelational] (M : Ordered.Structure L) :
-    letI := ESO.varLanguage.structure (arity := fun _ : Unit => 2)
-      (ESO.orderRelOfEquiv (Equiv.refl M));
-    (strictOrderInterpretation L).Model M ≃[L.sum ESO.orderLanguage] M := by
-  letI := ESO.varLanguage.structure (arity := fun _ : Unit => 2)
-    (ESO.orderRelOfEquiv (Equiv.refl M))
-  refine
-    { toFun := fun x => x.1 ()
-      invFun := fun x => ⟨fun _ => x, Formula.realize_top.2 trivial⟩
-      left_inv := fun _ => FO.Interpretation.Model.ext rfl
-      right_inv := fun _ => rfl
-      map_fun' := fun f => isEmptyElim f
-      map_rel' := ?_ }
-  intro n r x
-  cases r with
-  | inl R => exact Iff.rfl
-  | inr r =>
-    rcases r with ⟨⟨⟩, h⟩
-    subst n
-    change (x 0).1 () < (x 1).1 () ↔ ¬ (x 1).1 () ≤ (x 0).1 ()
-    exact not_le.symm
-
 /-- Pulling a strict-order ESO sentence into the public ordered language preserves its truth
 on the fixed canonical order. -/
 private theorem realize_onESOSentence_strictOrder {L : Language.{u, v}} [L.IsRelational]
diff --git a/Complexity/Logics/FirstOrder/Operator/LeastFixedPoint/Tuple.lean b/Complexity/Logics/FirstOrder/Operator/LeastFixedPoint/Tuple.lean
new file mode 100644
index 000000000..626f5c161
--- /dev/null
+++ b/Complexity/Logics/FirstOrder/Operator/LeastFixedPoint/Tuple.lean
@@ -0,0 +1,164 @@
+/-
+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.Operator.Quantifiers
+public import Mathlib.Logic.Equiv.Fin.Basic
+
+/-!
+# Pulling least-fixed-point formulas back to tuples
+
+An interpretation of target elements by full tuples lifts from ordinary first-order formulas
+to FO(LFP). Relation arities are multiplied by the tuple dimension. Existentially named term
+values let the construction reuse an ordinary first-order pullback, including its handling
+of target constants. It preserves both formation and syntactic polarity.
+
+The semantic theorem uses a bijection between source tuples and target elements. Thus the
+relation spaces are also in bijection, and the intersection of pre-fixed relations is preserved.
+-/
+
+public section
+
+open FirstOrder Language
+
+namespace Cslib.Logic.FO
+
+/-- Replace each argument of a scoped relation variable by `d` coordinates. -/
+@[expose] def Operator.RelVar.scale (d : ℕ) : {Γ : List ℕ} → {k : ℕ} →
+    Operator.RelVar Γ k → Operator.RelVar (Γ.map (· * d)) (k * d)
+  | _, _, .here => .here
+  | _, _, .there r => .there (r.scale d)
+
+namespace LFP.Tuple
+
+variable {L L' : Language} {d : ℕ}
+
+/-- The ordinary first-order part of a full-tuple syntax translation. -/
+abbrev FOMap (L L' : Language) (d : ℕ) :=
+  {α : Type} → L'.Formula α → L.Formula (α × Fin d)
+
+/-- Distribute coordinates over old and newly bound variables, flattening the latter. -/
+@[expose] def scopeMap {α : Type} {k : ℕ} :
+    (α ⊕ Fin k) × Fin d → (α × Fin d) ⊕ Fin (k * d)
+  | (.inl a, i) => .inl (a, i)
+  | (.inr j, i) => .inr (finProdFinEquiv (j, i))
+
+/-- Translate the graph of a tuple of terms, using fresh coordinates for their values. -/
+@[expose] noncomputable def termGraph (f : FOMap L L' d) {α : Type} {k : ℕ}
+    (args : Fin k → L'.Term α) : L.Formula ((α × Fin d) ⊕ Fin (k * d)) :=
+  (f (FirstOrder.Language.Formula.iInf fun i : Fin k =>
+    (Term.var (Sum.inr i)).equal ((args i).relabel Sum.inl))).relabel scopeMap
+
+/-- Apply a formula with fresh coordinate arguments to translated target terms. -/
+@[expose] noncomputable def applyTerms (f : FOMap L L' d) {Γ : List ℕ} {α : Type}
+    {k : ℕ} (args : Fin k → L'.Term α)
+    (φ : RawFormula L Γ ((α × Fin d) ⊕ Fin (k * d))) :
+    RawFormula L Γ (α × Fin d) :=
+  (Operator.Formula.conj (.ofFO (termGraph f args)) φ).exs (k * d)
+
+/-- Extend an ordinary first-order tuple pullback to scoped FO(LFP) syntax. -/
+@[expose] noncomputable def onFormula (f : FOMap L L' d) :
+    {Γ : List ℕ} → {α : Type} → RawFormula L' Γ α →
+      RawFormula L (Γ.map (· * d)) (α × Fin d)
+  | _, _, .ofFO φ => .ofFO (f φ)
+  | _, _, .rel r args =>
+    applyTerms f args (.rel (r.scale d) (fun i => .var (.inr i)))
+  | _, _, .neg φ => .neg (onFormula f φ)
+  | _, _, .conj φ ψ => .conj (onFormula f φ) (onFormula f ψ)
+  | _, _, .ex φ =>
+    ((onFormula f φ).relabel (fun p => match p.1 with
+      | none => .inr p.2
+      | some a => .inl (a, p.2))).exs d
+  | _, _, .op _k body args =>
+    applyTerms f args (lfp
+      (((onFormula f (body 0)).relabel scopeMap).relabel (Sum.map Sum.inl id))
+      (fun i => .var (.inr i)))
+
+variable {Γ : List ℕ} {α : Type}
+
+private theorem scale_outer {k : ℕ} (mark : Operator.Marking (Γ.map (· * d))) :
+    (fun {j} (r : Operator.RelVar (k :: Γ) j) =>
+      mark.outer [k * d] (r.scale d)) =
+      @Operator.Marking.outer Γ [k]
+        (fun {j} (r : Operator.RelVar Γ j) => mark (r.scale d)) := by
+  funext j r
+  cases r <;> rfl
+
+private theorem scale_head {k : ℕ} :
+    (fun {j} (r : Operator.RelVar (k :: Γ) j) => headMark (r.scale d)) =
+      (headMark : Operator.Marking (k :: Γ)) := by
+  funext j r
+  cases r <;> rfl
+
+/-- Naming term values does not change dependence on scoped relations. -/
+@[simp] theorem checkPolarity_applyTerms (f : FOMap L L' d) {k : ℕ}
+    (args : Fin k → L'.Term α) (φ : RawFormula L Γ ((α × Fin d) ⊕ Fin (k * d)))
+    (sign : Bool) (mark : Operator.Marking Γ) :
+    (applyTerms f args φ).checkPolarity policy.variance sign mark =
+      φ.checkPolarity policy.variance sign mark := by
+  simp [applyTerms, Operator.Formula.checkPolarity]
+
+/-- Naming term values does not change formation conditions. -/
+@[simp] theorem wellFormed_applyTerms (f : FOMap L L' d) {k : ℕ}
+    (args : Fin k → L'.Term α) (φ : RawFormula L Γ ((α × Fin d) ⊕ Fin (k * d))) :
+    (applyTerms f args φ).wellFormed policy = φ.wellFormed policy := by
+  simp [applyTerms, Operator.Formula.wellFormed]
+
+/-- Tuple pullback preserves the syntactic polarity check. -/
+@[simp] theorem checkPolarity_onFormula (f : FOMap L L' d) (φ : RawFormula L' Γ α)
+    (sign : Bool) (mark : Operator.Marking (Γ.map (· * d))) :
+    (onFormula f φ).checkPolarity policy.variance sign mark =
+      φ.checkPolarity policy.variance sign (fun {_} r => mark (r.scale d)) := by
+  induction φ generalizing sign with
+  | ofFO φ => rfl
+  | rel r args => simp only [onFormula, checkPolarity_applyTerms, Operator.Formula.checkPolarity]
+  | neg φ ih => exact ih _ _
+  | conj φ ψ ihφ ihψ => simp only [onFormula, Operator.Formula.checkPolarity, ihφ, ihψ]
+  | ex φ ih =>
+    simp only [onFormula, Operator.Formula.checkPolarity_exs,
+      Operator.Formula.checkPolarity_relabel, Operator.Formula.checkPolarity, ih]
+  | op k body args ih =>
+    rename_i Γ' α'
+    rw [onFormula, checkPolarity_applyTerms]
+    change decide (∀ i : Fin 1,
+      ((((onFormula f (body 0)).relabel scopeMap).relabel (Sum.map Sum.inl id)).checkPolarity
+        policy.variance sign (mark.outer [k * d])) = true) =
+      decide (∀ i : Fin 1, (body i).checkPolarity policy.variance sign
+        (Operator.Marking.outer [k] (fun {_} r => mark (r.scale d))) = true)
+    simp only [Operator.Formula.checkPolarity_relabel, ih, Fin.forall_fin_one]
+    have hc := congrArg
+      (fun m : Operator.Marking (k :: Γ') => (body 0).checkPolarity policy.variance sign m)
+      (scale_outer (k := k) mark)
+    exact congrArg (fun b : Bool => decide (b = true)) hc
+
+/-- Tuple pullback preserves the formation check at every nested fixed-point binder. -/
+@[simp] theorem wellFormed_onFormula (f : FOMap L L' d) (φ : RawFormula L' Γ α) :
+    (onFormula f φ).wellFormed policy = φ.wellFormed policy := by
+  induction φ with
+  | ofFO φ => rfl
+  | rel r args => simp only [onFormula, wellFormed_applyTerms, Operator.Formula.wellFormed]
+  | neg φ ih => exact ih
+  | conj φ ψ ihφ ihψ => simp only [onFormula, Operator.Formula.wellFormed, ihφ, ihψ]
+  | ex φ ih =>
+    simp only [onFormula, Operator.Formula.wellFormed_exs,
+      Operator.Formula.wellFormed_relabel, Operator.Formula.wellFormed, ih]
+  | op k body args ih =>
+    rename_i Γ' α'
+    apply Bool.eq_iff_iff.mpr
+    simp only [onFormula, wellFormed_applyTerms, wellFormed_lfp,
+      Operator.Formula.wellFormed_relabel, Positive, Operator.Formula.checkPolarity_relabel,
+      checkPolarity_onFormula, ih, Operator.Formula.wellFormed,
+      decide_eq_true_eq, Fin.forall_fin_one, inner_positive_eq_headMark]
+    have hc := congrArg
+      (fun m : Operator.Marking (k :: Γ') => (body 0).checkPolarity policy.variance true m)
+      (scale_head (Γ := Γ') (d := d) (k := k))
+    exact and_congr Iff.rfl (iff_of_eq (congrArg (fun b : Bool => b = true) hc))
+
+end LFP.Tuple
+end Cslib.Logic.FO
diff --git a/Complexity/Logics/FirstOrder/Operator/LeastFixedPoint/Tuple/Semantics.lean b/Complexity/Logics/FirstOrder/Operator/LeastFixedPoint/Tuple/Semantics.lean
new file mode 100644
index 000000000..8ec43b375
--- /dev/null
+++ b/Complexity/Logics/FirstOrder/Operator/LeastFixedPoint/Tuple/Semantics.lean
@@ -0,0 +1,199 @@
+/-
+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.Tuple
+
+/-!
+# Semantics of tuple pullback for least-fixed-point formulas
+
+The full-tuple compiler preserves truth, including nested least fixed points and captured
+parameters. The proof transports all candidate relations through the tuple bijection; it
+therefore also preserves the total pre-fixed-intersection semantics of unchecked syntax.
+-/
+
+public section
+
+open FirstOrder Language
+
+namespace Cslib.Logic.FO.LFP.Tuple
+
+variable {L L' : Language} {d : ℕ}
+
+/-- Apply an element bijection independently to the blocks of a flattened relation tuple. -/
+def tupleEquiv {M N : Type} (e : (Fin d → M) ≃ N) (k : ℕ) :
+    (Fin (k * d) → M) ≃ (Fin k → N) where
+  toFun xs i := e (fun j => xs (finProdFinEquiv (i, j)))
+  invFun ys p := e.symm (ys (finProdFinEquiv.symm p).1) (finProdFinEquiv.symm p).2
+  left_inv xs := by
+    funext p
+    simp only [Equiv.symm_apply_apply, Prod.mk.eta, Equiv.apply_symm_apply]
+  right_inv ys := by
+    funext i
+    simp only [Equiv.symm_apply_apply, Equiv.apply_symm_apply]
+
+variable {M N : Type} [L.Structure M] [L'.Structure N]
+  (f : FOMap L L' d) (e : (Fin d → M) ≃ N)
+  (hf : ∀ {α : Type} (φ : L'.Formula α) (v : α × Fin d → M),
+    (f φ).Realize v ↔ φ.Realize (fun a => e (fun i => v (a, i))))
+
+include hf in
+/-- The translated term graph identifies precisely the encoded values of its arguments. -/
+theorem realize_termGraph {α : Type} {k : ℕ} (args : Fin k → L'.Term α)
+    (v : α × Fin d → M) (xs : Fin (k * d) → M) :
+    (termGraph f args).Realize (Sum.elim v xs) ↔
+      ∀ i, tupleEquiv e k xs i = (args i).realize (fun a => e (fun j => v (a, j))) := by
+  rw [termGraph, FirstOrder.Language.Formula.realize_relabel, hf,
+    FirstOrder.Language.Formula.realize_iInf]
+  apply forall_congr'
+  intro i
+  simp only [FirstOrder.Language.Formula.realize_equal, Term.realize_var, Term.realize_relabel]
+  rfl
+
+include hf in
+/-- Existential term naming has a unique coordinate witness, even for constants and nullary
+argument tuples. -/
+theorem realize_applyTerms {Γ : List ℕ} {α : Type} {k : ℕ}
+    (args : Fin k → L'.Term α)
+    (φ : RawFormula L Γ ((α × Fin d) ⊕ Fin (k * d)))
+    (ρ : Operator.RelEnv Γ M) (v : α × Fin d → M) :
+    (applyTerms f args φ).Realize interpretation ρ v ↔
+      φ.Realize interpretation ρ (Sum.elim v ((tupleEquiv e k).symm
+        (fun i => (args i).realize (fun a => e (fun j => v (a, j)))))) := by
+  simp only [applyTerms, Operator.Formula.realize_exs, Operator.Formula.realize_conj,
+    Operator.Formula.realize_ofFO, realize_termGraph f e hf]
+  constructor
+  · rintro ⟨xs, hx, hφ⟩
+    have heq := congrArg (tupleEquiv e k).symm (funext hx)
+    rw [Equiv.symm_apply_apply] at heq
+    exact heq ▸ hφ
+  · intro hφ
+    exact ⟨_, fun i => congrFun ((tupleEquiv e k).apply_symm_apply _) i, hφ⟩
+
+private theorem append_singleton {Γ : List ℕ} {A : Type} {k : ℕ}
+    (R : Set (Fin k → A)) (ρ : Operator.RelEnv Γ A) :
+    @Operator.RelEnv.append Γ [k] A (@Operator.RelEnv.cons [] A k R
+      (@Operator.RelEnv.empty A)) ρ = @Operator.RelEnv.cons Γ A k R ρ := by
+  funext n r
+  cases r <;> rfl
+
+private theorem realize_lfp_prefixed {A : Type} [L.Structure A] {Γ : List ℕ}
+    {α : Type} {k : ℕ} (body : RawFormula L (k :: Γ) (α ⊕ Fin k))
+    (args : Fin k → L.Term α) (ρ : Operator.RelEnv Γ A) (v : α → A) :
+    (lfp body args).Realize interpretation ρ v ↔
+      ∀ R : Set (Fin k → A),
+        (∀ xs, body.Realize interpretation (Operator.RelEnv.cons R ρ)
+          (Sum.elim v xs) → xs ∈ R) → (fun i => (args i).realize v) ∈ R := by
+  simp only [lfp, Operator.Formula.Realize, interpretation, append_singleton]
+  rfl
+
+/-- An element bijection carries the intersection of all pre-fixed relations to that of the
+conjugate operator. Monotonicity is not needed for this raw semantic identity. -/
+private theorem prefixed_equiv {A B : Type} (e : A ≃ B)
+    (F : Set A → A → Prop) (G : Set B → B → Prop)
+    (h : ∀ R x, F (e ⁻¹' R) x ↔ G R (e x)) (x : A) :
+    (∀ S, (∀ y, F S y → y ∈ S) → x ∈ S) ↔
+      ∀ R, (∀ y, G R y → y ∈ R) → e x ∈ R := by
+  constructor
+  · intro hF R hR
+    exact hF (e ⁻¹' R) (fun y hy => hR (e y) ((h R y).mp hy))
+  · intro hG S hS
+    let R : Set B := e.symm ⁻¹' S
+    have hRS : e ⁻¹' R = S := by ext y; simp [R]
+    have hx := hG R (fun y hy => by
+      have hy' : F (e ⁻¹' R) (e.symm y) :=
+        (h R (e.symm y)).mpr (by simpa only [Equiv.apply_symm_apply] using hy)
+      rw [hRS] at hy'
+      exact hS (e.symm y) hy')
+    simpa only [R, Set.mem_preimage, Equiv.symm_apply_apply] using hx
+
+include hf in
+/-- Full-tuple pullback preserves truth for arbitrary scoped relation valuations, including
+nested operators. The relation valuations correspond blockwise through `tupleEquiv`. -/
+theorem realize_onFormula {Γ : List ℕ} {α : Type} (φ : RawFormula L' Γ α) :
+    ∀ (ρs : Operator.RelEnv (Γ.map (· * d)) M) (ρt : Operator.RelEnv Γ N),
+      (∀ {k} (r : Operator.RelVar Γ k) xs,
+        xs ∈ ρs (r.scale d) ↔ tupleEquiv e k xs ∈ ρt r) →
+      ∀ v : α × Fin d → M,
+        (onFormula f φ).Realize interpretation ρs v ↔
+          φ.Realize interpretation ρt (fun a => e (fun i => v (a, i))) := by
+  induction φ with
+  | ofFO φ =>
+    intro ρs ρt hρ v
+    exact hf φ v
+  | rel r args =>
+    intro ρs ρt hρ v
+    rw [onFormula, realize_applyTerms f e hf]
+    simpa only [Operator.Formula.Realize, Term.realize_var, Sum.elim_inr,
+      Equiv.apply_symm_apply] using
+      hρ r ((tupleEquiv e _).symm
+        (fun i => (args i).realize (fun a => e (fun j => v (a, j)))))
+  | neg φ ih =>
+    intro ρs ρt hρ v
+    exact not_congr (ih ρs ρt hρ v)
+  | conj φ ψ ihφ ihψ =>
+    intro ρs ρt hρ v
+    exact and_congr (ihφ ρs ρt hρ v) (ihψ ρs ρt hρ v)
+  | ex φ ih =>
+    intro ρs ρt hρ v
+    simp only [onFormula, Operator.Formula.realize_exs, Operator.Formula.realize_relabel,
+      Operator.Formula.realize_ex, ih ρs ρt hρ]
+    constructor
+    · rintro ⟨xs, hx⟩
+      refine ⟨e xs, ?_⟩
+      convert hx using 1
+      funext a
+      cases a <;> rfl
+    · rintro ⟨x, hx⟩
+      refine ⟨e.symm x, ?_⟩
+      convert hx using 1
+      funext a
+      cases a with
+      | none => exact e.apply_symm_apply x
+      | some a => rfl
+  | op k body args ih =>
+    rename_i Γ' α'
+    intro ρs ρt hρ v
+    let vt : α' → N := fun a => e (fun i => v (a, i))
+    let ea := tupleEquiv e k
+    let xs := ea.symm (fun i => (args i).realize vt)
+    let b : RawFormula L ((k * d) :: Γ'.map (· * d))
+        (((α' × Fin d) ⊕ Fin (k * d)) ⊕ Fin (k * d)) :=
+      ((onFormula f (body 0)).relabel scopeMap).relabel (Sum.map Sum.inl id)
+    change (applyTerms f args (lfp b (fun i => .var (.inr i)))).Realize
+      interpretation ρs v ↔ (lfp (body 0) args).Realize interpretation ρt vt
+    rw [realize_applyTerms f e hf, realize_lfp_prefixed, realize_lfp_prefixed]
+    change (∀ S, (∀ ys, b.Realize interpretation (Operator.RelEnv.cons S ρs)
+      (Sum.elim (Sum.elim v xs) ys) → ys ∈ S) → xs ∈ S) ↔
+      ∀ R, (∀ ys, (body 0).Realize interpretation (Operator.RelEnv.cons R ρt)
+        (Sum.elim vt ys) → ys ∈ R) → (fun i => (args i).realize vt) ∈ R
+    have hb (R : Set (Fin k → N)) (ys : Fin (k * d) → M) :
+        b.Realize interpretation (Operator.RelEnv.cons (ea ⁻¹' R) ρs)
+          (Sum.elim (Sum.elim v xs) ys) ↔
+        (body 0).Realize interpretation (Operator.RelEnv.cons R ρt)
+          (Sum.elim vt (ea ys)) := by
+      simp only [b, Operator.Formula.realize_relabel]
+      have hρ' : ∀ {j} (r : Operator.RelVar (k :: Γ') j) zs,
+          zs ∈ Operator.RelEnv.cons (ea ⁻¹' R) ρs (r.scale d) ↔
+            tupleEquiv e j zs ∈ Operator.RelEnv.cons R ρt r := by
+        intro j r zs
+        cases r with
+        | here => rfl
+        | there r => exact hρ r zs
+      rw [ih 0 _ _ hρ']
+      apply iff_of_eq
+      congr 1
+      funext a
+      cases a <;> rfl
+    simpa only [xs, Equiv.apply_symm_apply] using prefixed_equiv ea
+      (fun S ys => b.Realize interpretation (Operator.RelEnv.cons S ρs)
+        (Sum.elim (Sum.elim v xs) ys))
+      (fun R ys => (body 0).Realize interpretation (Operator.RelEnv.cons R ρt)
+        (Sum.elim vt ys)) hb xs
+
+end Cslib.Logic.FO.LFP.Tuple
diff --git a/Complexity/Logics/FirstOrder/Operator/Quantifiers.lean b/Complexity/Logics/FirstOrder/Operator/Quantifiers.lean
new file mode 100644
index 000000000..81a2f7bc9
--- /dev/null
+++ b/Complexity/Logics/FirstOrder/Operator/Quantifiers.lean
@@ -0,0 +1,95 @@
+/-
+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.Polarity
+
+/-!
+# Blocks of quantifiers in operator formulas
+
+`Formula.exs` binds a finite tuple of fresh first-order variables. Its semantics, formation
+check, and polarity check reduce to those of its body. This supplies the quantifier blocks
+needed when pulling fixed-point formulas back along tuple interpretations.
+-/
+
+public section
+
+universe u v w z s
+
+open FirstOrder Language
+
+namespace Cslib.Logic.FO.Operator.Formula
+
+variable {L : Language.{u, v}} {O : Type s} {shape : O → Shape}
+  {Γ : List ℕ} {α : Type w}
+
+/-- Bind all variables in the right summand, in increasing coordinate order. -/
+@[expose] def exs : {α : Type w} → (n : ℕ) →
+    Formula L shape Γ (α ⊕ Fin n) → Formula L shape Γ α
+  | _, 0, φ => φ.relabel (Sum.elim id Fin.elim0)
+  | _, n + 1, φ => .ex (exs n (φ.relabel (Sum.elim
+      (fun a => Sum.inl (some a))
+      (Fin.cases (Sum.inl none) Sum.inr))))
+
+/-- A block of existential quantifiers chooses one complete tuple. -/
+@[simp, fo_realize] theorem realize_exs {M : Type z} [L.Structure M]
+    (I : Interpretation shape M) (n : ℕ) (φ : Formula L shape Γ (α ⊕ Fin n))
+    (ρ : RelEnv Γ M) (v : α → M) :
+    (φ.exs n).Realize I ρ v ↔ ∃ xs, φ.Realize I ρ (Sum.elim v xs) := by
+  induction n generalizing α with
+  | zero =>
+    simp only [exs, realize_relabel]
+    constructor
+    · intro h
+      refine ⟨Fin.elim0, ?_⟩
+      convert h using 1
+      funext y
+      cases y with
+      | inl a => rfl
+      | inr i => exact i.elim0
+    · rintro ⟨xs, h⟩
+      convert h using 1
+      funext y
+      cases y with
+      | inl a => rfl
+      | inr i => exact i.elim0
+  | succ n ih =>
+    simp only [exs, realize_ex, ih, realize_relabel]
+    constructor
+    · rintro ⟨x, xs, h⟩
+      refine ⟨Fin.cons x xs, ?_⟩
+      convert h using 1
+      funext y
+      cases y with
+      | inl a => rfl
+      | inr i => exact Fin.cases rfl (fun _ => rfl) i
+    · rintro ⟨xs, h⟩
+      refine ⟨xs 0, Fin.tail xs, ?_⟩
+      convert h using 1
+      funext y
+      cases y with
+      | inl a => rfl
+      | inr i => exact Fin.cases rfl (fun _ => rfl) i
+
+/-- Quantifying a tuple leaves the formation check unchanged. -/
+@[simp] theorem wellFormed_exs (policy : Policy shape) (n : ℕ)
+    (φ : Formula L shape Γ (α ⊕ Fin n)) :
+    (φ.exs n).wellFormed policy = φ.wellFormed policy := by
+  induction n generalizing α with
+  | zero => simp [exs]
+  | succ n ih => simp only [exs, wellFormed, ih, wellFormed_relabel]
+
+/-- Quantifying a tuple leaves dependence on scoped relations unchanged. -/
+@[simp] theorem checkPolarity_exs (variance : Variances shape) (n : ℕ)
+    (φ : Formula L shape Γ (α ⊕ Fin n)) (sign : Bool) (mark : Marking Γ) :
+    (φ.exs n).checkPolarity variance sign mark = φ.checkPolarity variance sign mark := by
+  induction n generalizing α with
+  | zero => simp [exs]
+  | succ n ih => simp only [exs, checkPolarity, ih, checkPolarity_relabel]
+
+end Cslib.Logic.FO.Operator.Formula
diff --git a/Complexity/Logics/FirstOrder/Ordered/Encoding.lean b/Complexity/Logics/FirstOrder/Ordered/Encoding.lean
new file mode 100644
index 000000000..183a90103
--- /dev/null
+++ b/Complexity/Logics/FirstOrder/Ordered/Encoding.lean
@@ -0,0 +1,347 @@
+/-
+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.Layout
+public import Complexity.Logics.FirstOrder.Ordered.BitArithmetic
+
+/-!
+# First-order access to the native structure encoding
+
+The canonical power structure supplies the original relation tables and their domains. Native
+ordered arithmetic defines the length and every bit of `encStructure` directly, without guessing
+auxiliary relations. The power universe must contain the complete encoded word and its endpoint.
+
+The machine input is the existing unary-cardinality, framed-table encoding. Numeric symbols of
+the power universe have their canonical meanings, rather than being extra input tables.
+
+## Main definitions
+
+* `Cslib.Logic.Vocabulary.inputLength`: the endpoint of the raw native input encoding.
+* `Cslib.Logic.Vocabulary.inputBit`: the set bits of the raw native input encoding.
+
+## Main results
+
+* `Cslib.Logic.Vocabulary.realize_inputLength`, `Cslib.Logic.Vocabulary.realize_inputBit`:
+  exact length and bit semantics, uniformly over sufficiently large power universes.
+
+## References
+
+* [N. Immerman, *Relational Queries Computable in Polynomial Time*][Immerman1986], Section 3,
+  Lemma 3.1: first-order definition of the machine's input. The construction here uses the
+  library's framed encoding and canonical BIT arithmetic.
+-/
+
+public section
+
+namespace Cslib.Logic.Vocabulary
+
+open FirstOrder Language Structure Turing.MultiTapeTM
+open FO.Ordered
+
+variable {L : Language} (v : Vocabulary L)
+
+private abbrev inputLanguage := language v.powerLanguage
+
+private def elementDomain : v.inputLanguage.Formula (Fin 1) :=
+  FO.rel₁ (Sum.inl v.powerIsElem) 0
+
+private def tableDomain (i : Fin v.count) : v.inputLanguage.Formula (Fin 1) :=
+  FO.rel₁ (Sum.inl (v.powerInTable i)) 0
+
+private def tableBit (i : Fin v.count) : v.inputLanguage.Formula (Fin 1) :=
+  FO.rel₁ (Sum.inl (v.powerTableBit i)) 0
+
+private noncomputable def frameEnd {α : Type*}
+    (dom : v.inputLanguage.Formula (Fin 1)) (base last : v.inputLanguage.Term α) :
+    v.inputLanguage.Formula α := Formula.iExs (Fin 3)
+  (FO.isFirstOut (Sum.inl v.powerLt) dom (.inr 0) ⊓
+    scaleEq v.powerLanguage 2 (.var (.inr 0)) (.var (.inr 1)) ⊓
+    addEq v.powerLanguage (base.relabel Sum.inl) (.var (.inr 1)) (.var (.inr 2)) ⊓
+    addEq v.powerLanguage (.var (.inr 2)) (one v.powerLanguage) (last.relabel Sum.inl))
+
+private noncomputable def frameBit {α : Type*}
+    (dom bit : v.inputLanguage.Formula (Fin 1)) (base pos : v.inputLanguage.Term α) :
+    v.inputLanguage.Formula α := Formula.iExs (Fin 3)
+  (FO.atVar dom (.inr 0) ⊓
+    scaleEq v.powerLanguage 2 (.var (.inr 0)) (.var (.inr 1)) ⊓
+    addEq v.powerLanguage (base.relabel Sum.inl) (.var (.inr 1)) (.var (.inr 2)) ⊓
+    ((pos.relabel Sum.inl).equal (.var (.inr 2)) ⊔
+      (FO.atVar bit (.inr 0) ⊓
+        addEq v.powerLanguage (.var (.inr 2)) (one v.powerLanguage) (pos.relabel Sum.inl))))
+
+section Semantics
+
+variable {v} {B : ℕ} [Fact (2 ≤ B)] [v.powerLanguage.Structure (Fin B)]
+
+private theorem realize_frameEnd {α : Type*}
+    (dom : v.inputLanguage.Formula (Fin 1)) (base last : v.inputLanguage.Term α)
+    (env : α → Fin B) (len : ℕ) (hlen : len < B)
+    (hlt : ∀ x : Fin 2 → Fin B,
+      RelMap (L := v.inputLanguage) (Sum.inl v.powerLt) x ↔ x 0 < x 1)
+    (hdom : ∀ j : Fin B, dom.Realize ![j] ↔ (j : ℕ) < len) :
+    (v.frameEnd dom base last).Realize env ↔
+      (base.realize env).val + 2 * len + 1 = (last.realize env).val := by
+  simp only [frameEnd, Formula.realize_iExs, Formula.realize_inf,
+    FO.realize_isFirstOut hlt hlen hdom, realize_scaleEq, realize_addEq,
+    Term.realize_var, Term.realize_relabel, realize_one_val, Function.comp_def,
+    Sum.elim_inl, Sum.elim_inr, and_assoc]
+  constructor
+  · rintro ⟨u, hu, hd, hb, he⟩
+    change (base.realize env).val + (u 1).val = (u 2).val at hb
+    change (u 2).val + 1 = (last.realize env).val at he
+    omega
+  · intro h
+    have hb := (last.realize env).isLt
+    exact ⟨![⟨len, hlen⟩, ⟨2 * len, by omega⟩,
+      ⟨(base.realize env).val + 2 * len, by omega⟩], rfl, rfl, rfl, h⟩
+
+private theorem realize_frameBit {α : Type*}
+    (dom bit : v.inputLanguage.Formula (Fin 1)) (base pos : v.inputLanguage.Term α)
+    (env : α → Fin B) (w : List Bool)
+    (hdom : ∀ j : Fin B, dom.Realize ![j] ↔ (j : ℕ) < w.length)
+    (hbit : ∀ j : Fin B, (j : ℕ) < w.length → (bit.Realize ![j] ↔ w[j.val]? = some true)) :
+    (v.frameBit dom bit base pos).Realize env ↔
+      ∃ j < w.length, (pos.realize env).val = (base.realize env).val + 2 * j ∨
+        (w[j]? = some true ∧ (pos.realize env).val = (base.realize env).val + 2 * j + 1) := by
+  simp only [frameBit, Formula.realize_iExs, Formula.realize_inf, FO.realize_atVar,
+    realize_scaleEq, realize_addEq, Formula.realize_sup, Formula.realize_equal,
+    Term.realize_var, Term.realize_relabel, realize_one_val, Function.comp_def,
+    Sum.elim_inl, Sum.elim_inr, Fin.ext_iff, and_assoc]
+  constructor
+  · rintro ⟨u, hd, hs, hb, he⟩
+    change (base.realize env).val + (u 1).val = (u 2).val at hb
+    have hj := (hdom (u 0)).mp hd
+    refine ⟨(u 0).val, hj, ?_⟩
+    rcases he with he | ⟨hw, he⟩
+    · change (pos.realize env).val = (u 2).val at he
+      exact Or.inl (by omega)
+    · change (u 2).val + 1 = (pos.realize env).val at he
+      exact Or.inr ⟨(hbit (u 0) hj).mp hw, by omega⟩
+  · rintro ⟨j, hj, he⟩
+    have hp := (pos.realize env).isLt
+    have hbound : (base.realize env).val + 2 * j < B := by rcases he with h | ⟨_, h⟩ <;> omega
+    let u : Fin 3 → Fin B :=
+      ![⟨j, by omega⟩, ⟨2 * j, by omega⟩, ⟨(base.realize env).val + 2 * j, hbound⟩]
+    refine ⟨u, (hdom (u 0)).mpr hj, rfl, rfl, ?_⟩
+    rcases he with he | ⟨hw, he⟩
+    · exact Or.inl he
+    · exact Or.inr ⟨(hbit (u 0) hj).mpr hw, he.symm⟩
+
+end Semantics
+
+private noncomputable def prefixEnd : ℕ → {α : Type*} →
+    v.inputLanguage.Term α → v.inputLanguage.Formula α
+  | 0, _, last => v.frameEnd v.elementDomain (zero v.powerLanguage) last
+  | m + 1, _, last => if h : m < v.count then Formula.iExs Unit
+      (prefixEnd m (.var (.inr ())) ⊓
+        v.frameEnd (v.tableDomain ⟨m, h⟩) (.var (.inr ())) (last.relabel Sum.inl))
+    else ⊥
+
+private noncomputable def prefixBit : ℕ → {α : Type*} →
+    v.inputLanguage.Term α → v.inputLanguage.Formula α
+  | 0, _, pos => v.frameBit v.elementDomain ⊤ (zero v.powerLanguage) pos
+  | m + 1, _, pos => if h : m < v.count then prefixBit m pos ⊔ Formula.iExs Unit
+      (v.prefixEnd m (.var (.inr ())) ⊓
+        v.frameBit (v.tableDomain ⟨m, h⟩) (v.tableBit ⟨m, h⟩)
+          (.var (.inr ())) (pos.relabel Sum.inl))
+    else ⊥
+
+/-- The length of the native source-only encoding, inside the canonically ordered power domain. -/
+noncomputable def inputLength : (language v.powerLanguage).Formula (Fin 1) :=
+  v.prefixEnd v.count (.var 0)
+
+/-- A set bit of the native source-only encoding. Positions outside the encoded word are false. -/
+noncomputable def inputBit : (language v.powerLanguage).Formula (Fin 1) :=
+  v.prefixBit v.count (.var 0)
+
+private theorem frame_true_iff (w : List Bool) (p : ℕ) :
+    (frame w)[p]? = some true ↔
+      ∃ j < w.length, p = 2 * j ∨ (w[j]? = some true ∧ p = 2 * j + 1) := by
+  constructor
+  · intro h
+    have hp := (List.getElem?_eq_some_iff.mp h).choose
+    rw [length_frame] at hp
+    have hne : p ≠ 2 * w.length := by
+      intro he
+      rw [he, getElem?_frame_two_mul_length] at h
+      contradiction
+    have hj : p / 2 < w.length := by omega
+    refine ⟨p / 2, hj, ?_⟩
+    rcases Nat.mod_two_eq_zero_or_one p with hm | hm
+    · exact Or.inl (by omega)
+    · have he : p = 2 * (p / 2) + 1 := by omega
+      have hb : (frame w)[2 * (p / 2) + 1]? = some true := by rw [← he]; exact h
+      rw [getElem?_frame_two_mul_add_one hj] at hb
+      exact Or.inr ⟨hb, he⟩
+  · rintro ⟨j, hj, he | ⟨hb, he⟩⟩
+    · rw [he, getElem?_frame_two_mul hj]
+    · rw [he, getElem?_frame_two_mul_add_one hj]
+      exact hb
+
+private theorem shifted_frame_true_iff (w : List Bool) (base p : ℕ) :
+    base ≤ p ∧ (frame w)[p - base]? = some true ↔
+      ∃ j < w.length, p = base + 2 * j ∨
+        (w[j]? = some true ∧ p = base + 2 * j + 1) := by
+  rw [frame_true_iff]
+  constructor
+  · rintro ⟨hp, j, hj, he | ⟨hb, he⟩⟩
+    · exact ⟨j, hj, Or.inl (by omega)⟩
+    · exact ⟨j, hj, Or.inr ⟨hb, by omega⟩⟩
+  · rintro ⟨j, hj, he | ⟨hb, he⟩⟩
+    · exact ⟨by omega, j, hj, Or.inl (by omega)⟩
+    · exact ⟨by omega, j, hj, Or.inr ⟨hb, by omega⟩⟩
+
+private theorem append_true_iff (u w : List Bool) (p : ℕ) :
+    (u ++ w)[p]? = some true ↔
+      u[p]? = some true ∨ (u.length ≤ p ∧ w[p - u.length]? = some true) := by
+  by_cases hp : p < u.length
+  · simp [List.getElem?_append_left hp, Nat.not_le.mpr hp]
+  · simp [List.getElem?_append_right (Nat.le_of_not_gt hp), Nat.le_of_not_gt hp]
+
+private theorem prefix_length_lt {a : EncodedStructure} (ha : v.WellFormed a)
+    {B : ℕ} (hB : (encStructure a).length < B) {m : ℕ} (hm : m ≤ v.count) :
+    (v.encStructurePrefix a m).length < B := by
+  rw [v.length_encStructurePrefix (ha.1.symm ▸ hm) hm]
+  exact (tableStart_le_length a m).trans_lt hB
+
+private theorem realize_prefixEnd {a : EncodedStructure} (ha : v.WellFormed a)
+    {B : ℕ} [Fact (2 ≤ B)] (hB : (encStructure a).length < B)
+    {m : ℕ} (hm : m ≤ v.count) {α : Type*}
+    (last : v.inputLanguage.Term α) (env : α → Fin B) :
+    letI := v.powerStructure a B
+    (v.prefixEnd m last).Realize env ↔
+      (v.encStructurePrefix a m).length = (last.realize env).val := by
+  let _ := v.powerStructure a B
+  have hlt (x : Fin 2 → Fin B) :
+      RelMap (L := v.inputLanguage) (Sum.inl v.powerLt) x ↔ x 0 < x 1 := Iff.rfl
+  induction m generalizing α with
+  | zero =>
+    have hn : a.1 < B := (card_le_length_encStructure a).trans_lt hB
+    rw [prefixEnd, realize_frameEnd _ _ _ _ a.1 hn hlt (fun _ => Iff.rfl)]
+    simp only [realize_zero_val, Nat.zero_add, encStructurePrefix_zero, length_frame,
+      encUnary_apply, List.length_replicate]
+  | succ m ih =>
+    have hm' : m < v.count := by omega
+    let i : Fin v.count := ⟨m, hm'⟩
+    have hp := v.prefix_length_lt ha hB (Nat.le_of_lt hm')
+    have hs := v.prefix_length_lt ha hB hm
+    have hs' : (v.encStructurePrefix a m).length +
+        2 * (v.table a (v.symbol i)).length + 1 < B := by
+      simpa only [show m + 1 = i.val + 1 from rfl, encStructurePrefix_succ,
+        List.length_append, length_frame, Nat.add_assoc] using hs
+    have hlen : (v.table a (v.symbol i)).length < B := by omega
+    have hdom (j : Fin B) : (v.tableDomain i).Realize ![j] ↔
+        j.val < (v.table a (v.symbol i)).length := by
+      rw [ha.length_table]
+      exact Iff.rfl
+    rw [prefixEnd, dite_eq_left hm']
+    simp only [Formula.realize_iExs, Formula.realize_inf]
+    constructor
+    · rintro ⟨u, hu, hf⟩
+      have hb := (ih (Nat.le_of_lt hm') _ (Sum.elim env u)).mp hu
+      have he := (realize_frameEnd _ _ _ _ _ hlen hlt hdom).mp hf
+      simp only [Term.realize_var, Term.realize_relabel, Function.comp_def,
+        Sum.elim_inl, Sum.elim_inr] at hb he
+      change (u ()).val + 2 * (v.table a (v.symbol i)).length + 1 =
+        (last.realize env).val at he
+      rw [show m + 1 = i.val + 1 from rfl, encStructurePrefix_succ, List.length_append,
+        length_frame]
+      change (v.encStructurePrefix a m).length +
+        (2 * (v.table a (v.symbol i)).length + 1) = (last.realize env).val
+      omega
+    · intro he
+      let u : Unit → Fin B := fun _ => ⟨(v.encStructurePrefix a m).length, hp⟩
+      refine ⟨u, (ih (Nat.le_of_lt hm') _ _).mpr rfl, ?_⟩
+      apply (realize_frameEnd _ _ _ _ _ hlen hlt hdom).mpr
+      simp only [Term.realize_var, Term.realize_relabel, Function.comp_def,
+        Sum.elim_inl, Sum.elim_inr]
+      simpa only [show m + 1 = i.val + 1 from rfl, encStructurePrefix_succ,
+        List.length_append, length_frame, Nat.add_assoc] using he
+
+/-- The direct first-order length formula equals the length of the native machine input.
+The endpoint must be an element of the canonical power universe. -/
+@[fo_realize]
+theorem realize_inputLength {a : EncodedStructure} (ha : v.WellFormed a)
+    {B : ℕ} [Fact (2 ≤ B)] (hB : (encStructure a).length < B) (p : Fin B) :
+    letI := v.powerStructure a B
+    v.inputLength.Realize ![p] ↔ (encStructure a).length = p.val := by
+  let _ := v.powerStructure a B
+  simpa only [inputLength, encStructurePrefix_count v ha, Term.realize_var,
+    Matrix.cons_val_zero] using v.realize_prefixEnd ha hB (le_refl v.count) (.var 0) ![p]
+
+private theorem realize_prefixBit {a : EncodedStructure} (ha : v.WellFormed a)
+    {B : ℕ} [Fact (2 ≤ B)] (hB : (encStructure a).length < B)
+    {m : ℕ} (hm : m ≤ v.count) {α : Type*}
+    (pos : v.inputLanguage.Term α) (env : α → Fin B) :
+    letI := v.powerStructure a B
+    (v.prefixBit m pos).Realize env ↔
+      (v.encStructurePrefix a m)[(pos.realize env).val]? = some true := by
+  let _ := v.powerStructure a B
+  induction m generalizing α with
+  | zero =>
+    have hdom (j : Fin B) : v.elementDomain.Realize ![j] ↔ j.val < (encUnary a.1).length := by
+      simp only [encUnary_apply, List.length_replicate]
+      exact Iff.rfl
+    have hbit (j : Fin B) (hj : j.val < (encUnary a.1).length) :
+        (⊤ : v.inputLanguage.Formula (Fin 1)).Realize ![j] ↔
+          (encUnary a.1)[j.val]? = some true := by
+      have hj' : j.val < a.1 := by simpa using hj
+      simp only [encUnary_apply, Formula.realize_top, List.getElem?_replicate, ite_eq_left hj']
+    have hf := realize_frameBit v.elementDomain ⊤ (zero v.powerLanguage) pos env
+      (encUnary a.1) hdom hbit
+    simp only [realize_zero_val, Nat.zero_add] at hf
+    simpa only [prefixBit, encStructurePrefix_zero] using
+      hf.trans (frame_true_iff _ _).symm
+  | succ m ih =>
+    have hm' : m < v.count := by omega
+    let i : Fin v.count := ⟨m, hm'⟩
+    have hp := v.prefix_length_lt ha hB (Nat.le_of_lt hm')
+    have hdom (j : Fin B) : (v.tableDomain i).Realize ![j] ↔
+        j.val < (v.table a (v.symbol i)).length := by
+      rw [ha.length_table]
+      exact Iff.rfl
+    have hbit (j : Fin B) (hj : j.val < (v.table a (v.symbol i)).length) :
+        (v.tableBit i).Realize ![j] ↔ (v.table a (v.symbol i))[j.val]? = some true := by
+      change (j.val < a.1 ^ (v.symbol i).1 ∧
+        (v.table a (v.symbol i)).getD j.val false = true) ↔ _
+      rw [← WellFormed.length_table v ha (v.symbol i)]
+      simp [hj]
+    rw [prefixBit, dite_eq_left hm', Formula.realize_sup, Formula.realize_iExs]
+    simp only [Formula.realize_inf]
+    rw [show m + 1 = i.val + 1 from rfl,
+      encStructurePrefix_succ, append_true_iff]
+    apply or_congr (ih (Nat.le_of_lt hm') pos env)
+    constructor
+    · rintro ⟨u, hu, hf⟩
+      have hb := (v.realize_prefixEnd ha hB (Nat.le_of_lt hm') _ _).mp hu
+      have hf' := (realize_frameBit _ _ _ _ _ _ hdom hbit).mp hf
+      simp only [Term.realize_var, Term.realize_relabel, Function.comp_def,
+        Sum.elim_inl, Sum.elim_inr] at hb hf'
+      rw [← hb] at hf'
+      exact (shifted_frame_true_iff _ _ _).mpr hf'
+    · intro hf
+      let u : Unit → Fin B := fun _ => ⟨(v.encStructurePrefix a m).length, hp⟩
+      refine ⟨u, (v.realize_prefixEnd ha hB (Nat.le_of_lt hm') _ _).mpr rfl, ?_⟩
+      apply (realize_frameBit _ _ _ _ _ _ hdom hbit).mpr
+      simp only [Term.realize_var, Term.realize_relabel, Function.comp_def,
+        Sum.elim_inl, Sum.elim_inr]
+      exact (shifted_frame_true_iff _ _ _).mp hf
+
+/-- The direct first-order input-bit formula recognizes precisely the set bits of the existing
+native machine encoding, including its frame markers and rejecting terminators and padding. -/
+@[fo_realize]
+theorem realize_inputBit {a : EncodedStructure} (ha : v.WellFormed a)
+    {B : ℕ} [Fact (2 ≤ B)] (hB : (encStructure a).length < B) (p : Fin B) :
+    letI := v.powerStructure a B
+    v.inputBit.Realize ![p] ↔ (encStructure a)[p.val]? = some true := by
+  let _ := v.powerStructure a B
+  simpa only [inputBit, encStructurePrefix_count v ha, Term.realize_var,
+    Matrix.cons_val_zero] using v.realize_prefixBit ha hB (le_refl v.count) (.var 0) ![p]
+
+end Cslib.Logic.Vocabulary
diff --git a/Complexity/Logics/FirstOrder/Ordered/FullTuple/LeastFixedPoint.lean b/Complexity/Logics/FirstOrder/Ordered/FullTuple/LeastFixedPoint.lean
new file mode 100644
index 000000000..bd60d9009
--- /dev/null
+++ b/Complexity/Logics/FirstOrder/Ordered/FullTuple/LeastFixedPoint.lean
@@ -0,0 +1,75 @@
+/-
+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.FullTuple
+public import Complexity.Logics.FirstOrder.Ordered.LeastFixedPoint
+public import Complexity.Logics.FirstOrder.Operator.LeastFixedPoint.Tuple.Semantics
+
+/-!
+# Ordered full-tuple interpretations preserve least-fixed-point definability
+
+The ordinary full-tuple interpretation, with its native canonical order, BIT, and constants,
+extends to checked FO(LFP) formulas. Each target relation argument is replaced by a coordinate
+block; positivity and nested binding are preserved. The sentence pullback has exactly the
+truth value of the original sentence on the canonical rank universe.
+
+## References
+
+* [N. Immerman, *Relational Queries Computable in Polynomial Time*][Immerman1986], Section 3:
+  polynomial-sized tableau domains are represented by tuples over the input structure.
+-/
+
+public section
+
+open FirstOrder Language
+
+namespace Cslib.Logic.FO.Ordered.FullTupleInterpretation
+
+variable {L L' : Language} [L'.IsRelational] {k : ℕ}
+  (I : FullTupleInterpretation L L' k)
+
+/-- Pull back checked FO(LFP) syntax, multiplying every relation arity by the tuple dimension. -/
+noncomputable def onLFPFormula {Γ : List ℕ} {α : Type}
+    (φ : LFP.Formula (language L') Γ α) :
+    LFP.Formula (language L) (Γ.map (· * k)) (α × Fin k) :=
+  ⟨LFP.Tuple.onFormula I.onFormula φ.val, by
+    rw [LFP.Tuple.wellFormed_onFormula]
+    exact φ.property⟩
+
+/-- Pull back a checked sentence; its empty free-variable context remains empty. -/
+noncomputable def onLFPSentence (φ : LFP.Formula (language L') [] Empty) :
+    LFP.Formula (language L) [] Empty :=
+  ⟨(I.onLFPFormula φ).val.relabel Prod.fst, by
+    rw [Operator.Formula.wellFormed_relabel]
+    exact (I.onLFPFormula φ).property⟩
+
+variable {n : ℕ} [Fact (2 ≤ n)] [L.Structure (Fin n)]
+
+/-- The sentence pullback preserves truth on the canonical lexicographically ranked universe. -/
+theorem realize_onLFPSentence (hk : 0 < k) (φ : LFP.Formula (language L') [] Empty) :
+    (I.onLFPSentence φ).Realize (M := Fin n) Operator.RelEnv.empty Empty.elim ↔
+      letI := I.inputStructure (n := n)
+      letI : Fact (2 ≤ n ^ k) := ⟨two_le_pow (n := n) hk⟩
+      φ.Realize (M := Fin (n ^ k)) Operator.RelEnv.empty Empty.elim := by
+  let := I.inputStructure (n := n)
+  let : Fact (2 ≤ n ^ k) := ⟨two_le_pow (n := n) hk⟩
+  have hf {α : Type} (ψ : (language L').Formula α) (v : α × Fin k → Fin n) :
+      (I.onFormula ψ).Realize v ↔
+        ψ.Realize (M := Fin (n ^ k)) (fun a => lexEquiv (fun i => v (a, i))) :=
+    I.realize_onFormula hk ψ (fun a i => v (a, i))
+  simp only [onLFPSentence, LFP.Formula.Realize, onLFPFormula,
+    Operator.Formula.realize_relabel]
+  have h := LFP.Tuple.realize_onFormula I.onFormula lexEquiv hf φ.val
+    Operator.RelEnv.empty Operator.RelEnv.empty (fun {_} r => nomatch r)
+    (Empty.elim ∘ Prod.fst)
+  convert h using 1
+  exact iff_of_eq (congrArg (φ.val.Realize LFP.interpretation Operator.RelEnv.empty)
+    (Subsingleton.elim _ _))
+
+end Cslib.Logic.FO.Ordered.FullTupleInterpretation
diff --git a/Complexity/Logics/FirstOrder/Ordered/FullTuple/Power.lean b/Complexity/Logics/FirstOrder/Ordered/FullTuple/Power.lean
new file mode 100644
index 000000000..8833e5781
--- /dev/null
+++ b/Complexity/Logics/FirstOrder/Ordered/FullTuple/Power.lean
@@ -0,0 +1,86 @@
+/-
+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.Power
+public import Complexity.Logics.FirstOrder.Ordered.FullTuple
+public import Complexity.Logics.FirstOrder.Ordered.StrictOrder
+
+/-!
+# Canonical ordered power structures
+
+The existing power interpretation exposes input truth tables on a polynomially enlarged universe.
+This module adapts it to the canonical full-tuple interface, so that target order, BIT and numeric
+constants are defined by the existing tuple formulas. Reversing each tuple block reconciles the
+power interpretation's little-endian indexing with lexicographic ranking.
+
+## Main definitions
+
+* `Cslib.Logic.Vocabulary.orderedPowerInterpretation`: the full-tuple power interpretation.
+
+## Main results
+
+* `Cslib.Logic.Vocabulary.realize_orderedPower_rel`: exact numerical semantics of input relations.
+* `Cslib.Logic.Vocabulary.inputStructure_orderedPowerInterpretation`: the interpreted input
+  structure is the existing `powerStructure`, with no supplied numeric tables.
+
+## References
+
+* [N. Immerman, *Descriptive Complexity*][Immerman1999], Remark 1.32 and Exercise 1.33.
+-/
+
+public section
+
+namespace Cslib.Logic.Vocabulary
+
+open FirstOrder Language Structure FO.Ordered
+
+variable {L : Language} [L.IsRelational] (v : Vocabulary L) (k : ℕ)
+    (har : ∀ i : Fin v.count, v.arity i ≤ k)
+
+/-- Retain the original power-structure input predicates while using canonical lexicographic
+tuple ranks. All target numeric predicates are supplied by the full-tuple interpretation. -/
+noncomputable def orderedPowerInterpretation : FullTupleInterpretation L v.powerLanguage k where
+  rel R := ((strictOrderInterpretation L).onFormula ((v.powerInterpretation k har).rel R)).relabel
+    fun p => (p.1.1, p.1.2.rev)
+
+/-- The original power predicates evaluated on lexicographically ranked tuples. -/
+theorem realize_orderedPower_rel (hk : 1 ≤ k) (M : FO.Ordered.Structure L)
+    {r : ℕ} (R : v.powerLanguage.Relations r) (x : Fin r → Fin k → M) :
+    ((v.orderedPowerInterpretation k har).rel R).Realize (fun p => x p.1 p.2) ↔
+      letI := v.powerStructure (FO.Ordered.encode v M) (M.size ^ k)
+      RelMap R (fun i => lexEquiv (x i)) := by
+  let _ := ESO.varLanguage.structure (arity := fun _ : Unit => 2)
+    (ESO.orderRelOfEquiv (Equiv.refl M))
+  let _ := v.powerStructure (FO.Ordered.encode v M) (M.size ^ k)
+  rw [orderedPowerInterpretation, Formula.realize_relabel]
+  change ((strictOrderInterpretation L).onFormula ((v.powerInterpretation k har).rel R)).Realize
+    (fun p => x p.1.1 p.1.2.rev) ↔ _
+  rw [realize_strictOrder_onFormula M ((v.powerInterpretation k har).rel R)
+    (fun p => x p.1 p.2.rev)]
+  let y : Fin r → (v.powerInterpretation k har).Model M :=
+    fun i => ⟨fun j => x i j.rev, Formula.realize_top.mpr trivial⟩
+  have h := (v.powerEquiv k hk har M (Equiv.refl M)).map_rel R y
+  exact h.symm
+
+/-- The input relations of the full-tuple interpretation agree exactly with the canonical
+power structure of the native input encoding. -/
+theorem inputStructure_orderedPowerInterpretation (hk : 1 ≤ k) (M : FO.Ordered.Structure L) :
+    (v.orderedPowerInterpretation k har).inputStructure (n := M.size) =
+      v.powerStructure (FO.Ordered.encode v M) (M.size ^ k) := by
+  apply FirstOrder.Language.Structure.ext
+  · funext r f
+    exact isEmptyElim f
+  · funext r R x
+    apply propext
+    change ((v.orderedPowerInterpretation k har).rel R).Realize
+      (fun p => lexEquiv.symm (x p.1) p.2) ↔ _
+    have h := v.realize_orderedPower_rel k har hk M R (fun i => lexEquiv.symm (x i))
+    simpa only [Equiv.apply_symm_apply] using h
+
+end Cslib.Logic.Vocabulary
diff --git a/Complexity/Logics/FirstOrder/Ordered/StrictOrder.lean b/Complexity/Logics/FirstOrder/Ordered/StrictOrder.lean
new file mode 100644
index 000000000..9109064f8
--- /dev/null
+++ b/Complexity/Logics/FirstOrder/Ordered/StrictOrder.lean
@@ -0,0 +1,95 @@
+/-
+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.SecondOrder.Projection
+
+/-!
+# Strict-order interpretations of canonical ordered structures
+
+The one-dimensional interpretation retains every input relation and reads strict order from
+canonical non-strict order. It allows order-based relational formulas to be reused with the
+canonical ordered vocabulary, including in the full-tuple power interpretation.
+
+## Main definitions
+
+* `Cslib.Logic.FO.Ordered.strictOrderInterpretation`: the relational strict-order interpretation.
+* `Cslib.Logic.FO.Ordered.strictOrderEquiv`: the isomorphism with the canonical input universe.
+
+## Main results
+
+* `Cslib.Logic.FO.Ordered.realize_strictOrder_onFormula`: arbitrary formula truth is preserved.
+
+## References
+
+* [N. Immerman, *Descriptive Complexity*][Immerman1999], Definition 1.26 and Proposition 3.5.
+-/
+
+@[expose] public section
+
+universe u v
+
+namespace Cslib.Logic.FO.Ordered
+
+open FirstOrder Language Structure
+
+/-- The one-dimensional interpretation retaining the input relations and reading strict order
+from canonical non-strict order. -/
+def strictOrderInterpretation (L : Language.{u, v}) :
+    FO.Interpretation (language L) (L.sum ESO.orderLanguage) Unit where
+  domain := ⊤
+  rel := fun {n} r => match r with
+    | .inl R => Relations.formula (L := language L) (Sum.inl R) fun i => .var (i, ())
+    | .inr r => by
+      rcases r with ⟨⟨⟩, h⟩
+      subst n
+      exact ∼(Relations.formula (L := language L) (Sum.inr NumericRelation.le)
+        fun i => .var (if i = 0 then 1 else 0, ()))
+
+/-- The canonical strict-order structure interpreted above is the original ordered universe. -/
+def strictOrderEquiv {L : Language.{u, v}} [L.IsRelational] (M : Ordered.Structure L) :
+    letI := ESO.varLanguage.structure (arity := fun _ : Unit => 2)
+      (ESO.orderRelOfEquiv (Equiv.refl M));
+    (strictOrderInterpretation L).Model M ≃[L.sum ESO.orderLanguage] M := by
+  letI := ESO.varLanguage.structure (arity := fun _ : Unit => 2)
+    (ESO.orderRelOfEquiv (Equiv.refl M))
+  refine
+    { toFun := fun x => x.1 ()
+      invFun := fun x => ⟨fun _ => x, Formula.realize_top.2 trivial⟩
+      left_inv := fun _ => FO.Interpretation.Model.ext rfl
+      right_inv := fun _ => rfl
+      map_fun' := fun f => isEmptyElim f
+      map_rel' := ?_ }
+  intro n r x
+  cases r with
+  | inl R => exact Iff.rfl
+  | inr r =>
+    rcases r with ⟨⟨⟩, h⟩
+    subst n
+    change (x 0).1 () < (x 1).1 () ↔ ¬ (x 1).1 () ≤ (x 0).1 ()
+    exact not_le.symm
+
+/-- Pulling a relational strict-order formula back to the canonical ordered vocabulary preserves
+its truth for every free-variable assignment. -/
+@[fo_realize]
+theorem realize_strictOrder_onFormula {L : Language.{u, v}} [L.IsRelational]
+    (M : Ordered.Structure L) {α : Type*} (φ : (L.sum ESO.orderLanguage).Formula α)
+    (x : α → M) :
+    ((strictOrderInterpretation L).onFormula φ).Realize (fun p => x p.1) ↔
+      letI := ESO.varLanguage.structure (arity := fun _ : Unit => 2)
+        (ESO.orderRelOfEquiv (Equiv.refl M))
+      φ.Realize x := by
+  let _ := ESO.varLanguage.structure (arity := fun _ : Unit => 2)
+    (ESO.orderRelOfEquiv (Equiv.refl M))
+  let y : α → (strictOrderInterpretation L).Model M :=
+    fun a => ⟨fun _ => x a, Formula.realize_top.mpr trivial⟩
+  rw [(strictOrderInterpretation L).realize_onFormula φ y]
+  exact (StrongHomClass.realize_formula (strictOrderEquiv M) φ).symm
+
+end Cslib.Logic.FO.Ordered
diff --git a/ComplexityTests/FOInputEncoding.lean b/ComplexityTests/FOInputEncoding.lean
new file mode 100644
index 000000000..7543d4aef
--- /dev/null
+++ b/ComplexityTests/FOInputEncoding.lean
@@ -0,0 +1,102 @@
+/-
+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.Logics.FirstOrder.Ordered.Encoding
+import Complexity.Logics.FirstOrder.Ordered.FullTuple.Power
+
+/-! # Native input-layout formulas at markers, payloads, terminators, and padding -/
+
+namespace ComplexityTests.FOInputEncoding
+
+open FirstOrder Language Cslib.Logic Turing.MultiTapeTM
+
+private inductive Relation : ℕ → Type
+  | flag : Relation 0
+  | mark : Relation 1
+
+private abbrev L : Language where
+  Functions _ := Empty
+  Relations := Relation
+
+private def vocabulary : Vocabulary L where
+  count := 2
+  symbol :=
+    { toFun := fun i => if i = 0 then ⟨0, .flag⟩ else ⟨1, .mark⟩
+      invFun := fun ⟨_, r⟩ => match r with | .flag => 0 | .mark => 1
+      left_inv := by intro i; fin_cases i <;> rfl
+      right_inv := by rintro ⟨_, r⟩; cases r <;> rfl }
+
+private def input : EncodedStructure := (2, [ [true], [false, true] ])
+
+private theorem wellFormed : vocabulary.WellFormed input := by decide +kernel
+
+private instance : Fact (2 ≤ 16) := ⟨by decide⟩
+
+private instance : Fact (2 ≤ 2) := ⟨by decide⟩
+
+private instance : vocabulary.powerLanguage.Structure (Fin 16) :=
+  vocabulary.powerStructure input 16
+
+-- The endpoint is 13, after a cardinality frame and nullary and unary relation frames.
+example : vocabulary.inputLength.Realize ![(13 : Fin 16)] := by
+  rw [vocabulary.realize_inputLength wellFormed (by decide)]
+  rfl
+
+example : ¬ vocabulary.inputLength.Realize ![(12 : Fin 16)] := by
+  rw [vocabulary.realize_inputLength wellFormed (by decide)]
+  decide
+
+-- Both the nullary payload and the final true unary payload are preserved.
+example : vocabulary.inputBit.Realize ![(6 : Fin 16)] ∧
+    vocabulary.inputBit.Realize ![(11 : Fin 16)] := by
+  rw [vocabulary.realize_inputBit wellFormed (by decide),
+    vocabulary.realize_inputBit wellFormed (by decide)]
+  decide
+
+-- A marker is true even when the payload that follows it is false.
+example : vocabulary.inputBit.Realize ![(8 : Fin 16)] ∧
+    ¬ vocabulary.inputBit.Realize ![(9 : Fin 16)] := by
+  rw [vocabulary.realize_inputBit wellFormed (by decide),
+    vocabulary.realize_inputBit wellFormed (by decide)]
+  decide
+
+-- The unary-cardinality terminator, table terminator, and out-of-word padding are false.
+example : ¬ vocabulary.inputBit.Realize ![(4 : Fin 16)] ∧
+    ¬ vocabulary.inputBit.Realize ![(12 : Fin 16)] ∧
+    ¬ vocabulary.inputBit.Realize ![(15 : Fin 16)] := by
+  rw [vocabulary.realize_inputBit wellFormed (by decide),
+    vocabulary.realize_inputBit wellFormed (by decide),
+    vocabulary.realize_inputBit wellFormed (by decide)]
+  decide
+
+private def source : FO.Ordered.Structure L where
+  size := 2
+  size_ge_two := by decide
+  input := { RelMap := fun r xs => match r with | .flag => True | .mark => xs 0 = 1 }
+
+private theorem arity_le_two (i : Fin vocabulary.count) : vocabulary.arity i ≤ 2 := by
+  fin_cases i <;> decide
+
+-- The power bridge must preserve lexicographic ranks: (0,1) is 1, while (1,0) is 2.
+example :
+    letI : L.Structure (Fin 2) := source.input
+    ((vocabulary.orderedPowerInterpretation 2 arity_le_two).rel vocabulary.powerIsElem).Realize
+        (fun p => (![0, 1] : Fin 2 → Fin 2) p.2) ∧
+      ¬ ((vocabulary.orderedPowerInterpretation 2 arity_le_two).rel vocabulary.powerIsElem).Realize
+        (fun p => (![1, 0] : Fin 2 → Fin 2) p.2) := by
+  let _ : L.Structure (Fin 2) := source.input
+  constructor
+  · apply (vocabulary.realize_orderedPower_rel 2 arity_le_two (by decide) source
+      vocabulary.powerIsElem (fun _ => (![0, 1] : Fin 2 → Fin 2))).mpr
+    change FO.Ordered.lexRank (![0, 1] : Fin 2 → Fin 2) < 2
+    decide
+  · intro h
+    have hh := (vocabulary.realize_orderedPower_rel 2 arity_le_two (by decide) source
+      vocabulary.powerIsElem (fun _ => (![1, 0] : Fin 2 → Fin 2))).mp h
+    change FO.Ordered.lexRank (![1, 0] : Fin 2 → Fin 2) < 2 at hh
+    exact (by decide : ¬ FO.Ordered.lexRank (![1, 0] : Fin 2 → Fin 2) < 2) hh
+
+end ComplexityTests.FOInputEncoding