feat(logic): prove the Immerman–Vardi characterization

Complexity.lean

@@ -1259,6 +1259,13 @@ public import Complexity.Computability.Complexity.FineGrained.Sparsification
 public import Complexity.Computability.Complexity.FineGrained.ThreeOccurrenceReduction
 public import Complexity.Computability.Complexity.HardnessEncoding.PolyTime
 public import Complexity.Computability.Complexity.HardnessEncoding.Program
+public import Complexity.Computability.Complexity.ImmermanVardi
+public import Complexity.Computability.Complexity.ImmermanVardi.Input
+public import Complexity.Computability.Complexity.ImmermanVardi.Tableau.Acceptance
+public import Complexity.Computability.Complexity.ImmermanVardi.Tableau.Correct
+public import Complexity.Computability.Complexity.ImmermanVardi.Tableau.Definability
+public import Complexity.Computability.Complexity.ImmermanVardi.Tableau.FixedPoint
+public import Complexity.Computability.Complexity.ImmermanVardi.Tableau.Step
 public import Complexity.Computability.Complexity.Parameterized
 public import Complexity.Computability.Complexity.Parameterized.Kernelization
 public import Complexity.Computability.Complexity.Parameterized.VertexCover
@@ -2803,6 +2810,7 @@ public import Complexity.Logics.FirstOrder.Interpretation.Tuple
 public import Complexity.Logics.FirstOrder.Interpretation.Unit
 public import Complexity.Logics.FirstOrder.Operator.Basic
 public import Complexity.Logics.FirstOrder.Operator.Definability
+public import Complexity.Logics.FirstOrder.Operator.Definability.Finite
 public import Complexity.Logics.FirstOrder.Operator.Definability.Polarity
 public import Complexity.Logics.FirstOrder.Operator.LeastFixedPoint
 public import Complexity.Logics.FirstOrder.Operator.LeastFixedPoint.Definability

Complexity/Computability/Complexity/ImmermanVardi.lean

@@ -0,0 +1,148 @@
+/-
+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
+public import Complexity.Computability.Complexity.ImmermanVardi.Tableau.Acceptance
+public import Complexity.Computability.Complexity.ImmermanVardi.Input
+public import Complexity.Logics.FirstOrder.Ordered.FullTuple.LeastFixedPoint
+public import Complexity.Logics.FirstOrder.Ordered.FullTuple.Power
+import Complexity.Computability.Complexity.Fagin.Converse
+
+/-!
+# The Immerman–Vardi characterization of polynomial time
+
+On the library's canonically ordered finite structures, a query is definable by one checked
+FO(LFP) sentence exactly when its source-only encoded language belongs to native `P`.
+The vocabulary is finite and relational; its fixed enumeration determines truth-table order.
+Universes are `Fin n` with `n ≥ 2`. Order, BIT, zero, one, and maximum are canonical numeric
+symbols, computed from the universe size rather than supplied as input tables.
+
+The forward direction compiles a fixed formula to a native polynomial-time model checker.
+For the converse, a native deterministic machine has a positive local tableau. Its input
+symbols are defined directly from the actual binary encoding. A fixed tuple width bounds the
+machine's time, input length, and finite feature tags for all input sizes. Pullback along the
+canonical full-tuple interpretation gives one sentence over the original input universe.
+
+## Main results
+
+* `FO.Ordered.LFPDefinable.of_encodedLanguage_mem_P`: every native polynomial-time ordered
+  query has a uniform checked FO(LFP) sentence.
+* `FO.Ordered.lfpDefinable_iff_encodedLanguage_mem_P`: FO(LFP) captures native polynomial time.
+
+## References
+
+* [N. Immerman, *Relational Queries Computable in Polynomial Time*][Immerman1986], Theorem 1
+  and Section 3. The theorem is instantiated here at the existing canonical ordered vocabulary
+  and unary-cardinality/full-truth-table encoding. Malformed table shapes and universes below
+  two are rejected.
+-/
+
+public section
+
+open FirstOrder Language Turing Turing.MultiTapeTM
+
+namespace Cslib.Logic
+
+namespace Vocabulary
+
+variable {L : Language} (v : Vocabulary L)
+
+/-- A single tuple dimension contains the input, runtime, and fixed finite feature tags of a
+polynomial-time native machine, uniformly over well-formed ordered structures. -/
+theorem exists_lfp_power_bound (t : ℕ → ℕ) (ht : Cslib.PolynomiallyBounded t) (tags : ℕ) :
+    ∃ k : ℕ, 1 ≤ k ∧ (∀ i : Fin v.count, v.arity i ≤ k) ∧
+      ∀ a : EncodedStructure, v.WellFormed a → 2 ≤ a.1 →
+        (encStructure a).length + 1 < a.1 ^ k ∧
+        t (encStructure a).length < a.1 ^ k ∧ tags ≤ a.1 ^ k := by
+  obtain ⟨c, d, htime⟩ := Cslib.polynomiallyBounded_iff_le.mp ht
+  obtain ⟨k, hk, har, hpow⟩ := v.exists_pow_bound 0 (c + tags) d
+  refine ⟨k, hk, har, fun a ha hn => ?_⟩
+  obtain ⟨hinput, hclock⟩ := hpow a ha hn
+  simp only [Polynomial.eval_zero, Nat.add_zero] at hinput hclock
+  have hlen : (encStructure a).length + 1 ≤ (frame (encStructure a)).length + 1 := by
+    rw [length_frame]
+    omega
+  have ht' : t (encStructure a).length ≤
+      (c + tags) * ((frame (encStructure a)).length + 1) ^ d :=
+    (htime _).trans (Nat.mul_le_mul (Nat.le_add_right c tags)
+      (Nat.pow_le_pow_left hlen d))
+  have hp : 1 ≤ ((frame (encStructure a)).length + 1) ^ d :=
+    Nat.one_le_pow _ _ (by omega)
+  have htags : tags ≤ (c + tags) * ((frame (encStructure a)).length + 1) ^ d :=
+    calc tags ≤ c + tags := Nat.le_add_left _ _
+         _ = (c + tags) * 1 := (Nat.mul_one _).symm
+         _ ≤ _ := Nat.mul_le_mul_left _ hp
+  exact ⟨by omega, by omega, by omega⟩
+
+end Vocabulary
+
+namespace FO.Ordered
+
+open Cslib.Complexity
+
+/-- Every ordered query decided by an actual native polynomial-time machine is defined by one
+checked FO(LFP) sentence over the original ordered input structures. -/
+theorem LFPDefinable.of_encodedLanguage_mem_P {L : Language} [L.IsRelational]
+    (v : Vocabulary L) {K : Query L} (hK : K.encodedLanguage v ∈ P encStructure) :
+    LFPDefinable K := by
+  classical
+  obtain ⟨f, ⟨t, _, ht, _, m, State, hfinite, tm, htm⟩, hdec⟩ := hK
+  let _ := hfinite
+  let _ := Fintype.ofFinite State
+  obtain ⟨k, hk, har, hpow⟩ :=
+    v.exists_lfp_power_bound t ht (Fintype.card (ImmermanVardi.Tableau.Tag m State))
+  let A := {a : EncodedStructure // v.WellFormed a ∧ 2 ≤ a.1}
+  let size (a : A) := a.val.1 ^ k
+  let input (a : A) := encStructure a.val
+  let inst (a : A) : v.powerLanguage.Structure (Fin (size a)) :=
+    v.powerStructure a.val (size a)
+  let instSize (a : A) : Fact (2 ≤ size a) := by
+    let _ : Fact (2 ≤ a.val.1) := ⟨a.property.2⟩
+    exact ⟨FullTupleInterpretation.two_le_pow (n := a.val.1) hk⟩
+  have hb (a : A) :
+      (input a).length + 1 < size a ∧ t (input a).length < size a ∧
+        Fintype.card (ImmermanVardi.Tableau.Tag m State) ≤ size a :=
+    hpow a.val a.property.1 a.property.2
+  obtain ⟨ψ, hψ⟩ := ImmermanVardi.Tableau.exists_acceptance_sentence
+    (L := v.powerLanguage) (size := size) tm input v.inputSymbol
+    (fun a s p => v.realize_inputSymbol a.property.1
+      ((Nat.lt_succ_self _).trans (hb a).1) s p)
+    (fun a => (hb a).1) (fun a => (hb a).2.2)
+  let I := v.orderedPowerInterpretation k har
+  refine ⟨I.onLFPSentence ψ, fun M => ?_⟩
+  let a : A := ⟨encode v M, v.wellFormed_encode M (Equiv.refl M), M.size_ge_two⟩
+  have hm := (htm (encode v M)).runFrom_of_le
+    (show t (input a).length ≤ size a - 1 by have := (hb a).2.1; omega)
+  have haccept : ψ.Realize (M := Fin (size a)) Operator.RelEnv.empty Empty.elim ↔
+      f (encode v M) = true := by
+    have hψ' := hψ a
+    have hv (v : Empty → Fin (size a)) : v = Empty.elim := Subsingleton.elim _ _
+    simp only [hv] at hψ'
+    rw [hψ']
+    change ((tm.runFrom (tm.initCfg (encStructure (encode v M))) (size a - 1)).Halted ∧
+      (tm.runFrom (tm.initCfg (encStructure (encode v M))) (size a - 1)).output = [true]) ↔ _
+    simp only [hm.2, encBool_apply, List.singleton_inj]
+    exact ⟨And.right, fun h => ⟨hm.1, h⟩⟩
+  have hquery : M ∈ K ↔ f (encode v M) = true :=
+    (mem_encodedLanguage_encode v K M).symm.trans (hdec (encode v M))
+  rw [I.realize_onLFPSentence hk ψ]
+  have he := v.inputStructure_orderedPowerInterpretation k har hk M
+  change I.inputStructure (n := M.size) = inst a at he
+  rw [he]
+  exact hquery.trans haccept.symm
+
+/-- **Immerman–Vardi:** a single checked FO(LFP) sentence defines an ordered query exactly
+when its source-only language is decidable in native polynomial time. -/
+theorem lfpDefinable_iff_encodedLanguage_mem_P {L : Language} [L.IsRelational]
+    (v : Vocabulary L) (K : Query L) :
+    LFPDefinable K ↔ K.encodedLanguage v ∈ P encStructure :=
+  ⟨fun h => h.encodedLanguage_mem_P v, LFPDefinable.of_encodedLanguage_mem_P v⟩
+
+end FO.Ordered
+end Cslib.Logic

Complexity/Computability/Complexity/ImmermanVardi/Input.lean

@@ -0,0 +1,113 @@
+/-
+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.Encoding
+public import Complexity.Computability.Machines.Turing.MultiTape.Run
+
+/-!
+# First-order input symbols for native deterministic machines
+
+The direct length and bit formulas for `encStructure` yield formulas for all three native
+input-tape symbols. Position zero is the left endmarker; the first data bit is at position one.
+The formulas include the right endmarker and padding, and use no guessed relations.
+-/
+
+public section
+
+open FirstOrder Language Turing Turing.MultiTapeTM
+
+namespace Cslib.Logic.Vocabulary
+
+open FO.Ordered
+
+variable {L : Language} (v : Vocabulary L)
+
+/-- The native input-tape symbol, including both endmarkers, defined from the encoded input. -/
+noncomputable def inputSymbol : Option Bool → (language v.powerLanguage).Formula (Fin 1)
+  | none => natEq v.powerLanguage 0 (.var 0) ⊔ Formula.iExs (Fin 1)
+      (v.inputLength.relabel (fun _ => .inr 0) ⊓
+        ∼(le v.powerLanguage (.var (.inl 0)) (.var (.inr 0))))
+  | some b => Formula.iExs (Fin 2)
+      (v.inputLength.relabel (fun _ => .inr 1) ⊓
+        ∼(le v.powerLanguage (.var (.inr 1)) (.var (.inr 0))) ⊓
+        addEq v.powerLanguage (.var (.inr 0)) (one v.powerLanguage) (.var (.inl 0)) ⊓
+        (if b then v.inputBit.relabel (fun _ => .inr 0)
+          else ∼(v.inputBit.relabel (fun _ => .inr 0))))
+
+/-- The first-order input-symbol formula agrees exactly with the native machine input lookup. -/
+theorem realize_inputSymbol {a : EncodedStructure} (ha : v.WellFormed a)
+    {B : ℕ} [Fact (2 ≤ B)] (hB : (encStructure a).length < B)
+    (s : Option Bool) (p : Fin B) :
+    letI := v.powerStructure a B
+    (v.inputSymbol s).Realize ![p] ↔ inputAt (encStructure a) p.val = s := by
+  let _ := v.powerStructure a B
+  have hlen (x : Fin B) := v.realize_inputLength ha hB x
+  have hbit (x : Fin B) := v.realize_inputBit ha hB x
+  rcases s with _ | b
+  · simp only [inputSymbol, Formula.realize_sup, realize_natEq, Term.realize_var,
+      Matrix.cons_val_zero, Formula.realize_iExs, Formula.realize_inf,
+      Formula.realize_relabel, Formula.realize_not, realize_le, Function.comp_def,
+      Sum.elim_inl, Sum.elim_inr, not_le]
+    constructor
+    · rintro (hz | ⟨xs, hx, hp⟩)
+      · simp [inputAt, hz]
+      · have hx' : (encStructure a).length = (xs 0).val := by
+          apply (hlen (xs 0)).mp
+          simpa only [Matrix.cons_fin_one] using hx
+        have hn : p.val ≠ 0 := by change (xs 0).val < p.val at hp; omega
+        simp only [inputAt, hn, ite_false, List.getElem?_eq_none_iff]
+        change (xs 0).val < p.val at hp
+        omega
+    · intro h
+      by_cases hp : p.val = 0
+      · exact Or.inl hp
+      · right
+        simp only [inputAt, hp, ite_false, List.getElem?_eq_none_iff] at h
+        let l : Fin B := ⟨(encStructure a).length, hB⟩
+        refine ⟨![l], ?_, ?_⟩
+        · simpa only [Matrix.cons_fin_one] using (hlen l).mpr rfl
+        · change (encStructure a).length < p.val
+          omega
+  · have hdata (q : Fin B) (hq : q.val < (encStructure a).length) :
+        (if b then v.inputBit.Realize ![q] else ¬v.inputBit.Realize ![q]) ↔
+          (encStructure a)[q.val]? = some b := by
+      rw [hbit q, List.getElem?_eq_getElem hq]
+      cases b <;> cases (encStructure a)[q.val] <;> simp
+    have hform : (v.inputSymbol (some b)).Realize ![p] ↔
+        ∃ xs : Fin 2 → Fin B,
+          (encStructure a).length = (xs 1).val ∧
+          (xs 0).val < (xs 1).val ∧ (xs 0).val + 1 = p.val ∧
+          (if b then v.inputBit.Realize ![xs 0] else ¬v.inputBit.Realize ![xs 0]) := by
+      simp only [inputSymbol, Formula.realize_iExs, Formula.realize_inf]
+      apply exists_congr
+      intro xs
+      have hl : v.inputLength.Realize (fun _ : Fin 1 => xs 1) ↔
+          (encStructure a).length = (xs 1).val := by
+        simpa only [Matrix.cons_fin_one] using hlen (xs 1)
+      cases b <;> simp only [Bool.false_eq_true, ↓reduceIte, Formula.realize_relabel,
+        Formula.realize_not, realize_le, realize_addEq, realize_one_val,
+        Term.realize_var, Function.comp_def, Sum.elim_inl, Sum.elim_inr,
+        hl, not_le, Fin.lt_def, Matrix.cons_fin_one, and_assoc]
+    rw [hform]
+    constructor
+    · rintro ⟨xs, hlen, hlt, hs, hb⟩
+      have hq : (xs 0).val < (encStructure a).length := by omega
+      have hp : p.val ≠ 0 := by omega
+      have he : p.val - 1 = (xs 0).val := by omega
+      simpa only [inputAt, hp, ite_false, he] using (hdata (xs 0) hq).mp hb
+    · intro h
+      have hp : p.val ≠ 0 := by intro hp; simp [inputAt, hp] at h
+      simp only [inputAt, hp, ite_false] at h
+      have hq : p.val - 1 < (encStructure a).length :=
+        (List.getElem?_eq_some_iff.mp h).choose
+      let q : Fin B := ⟨p.val - 1, by omega⟩
+      let l : Fin B := ⟨(encStructure a).length, hB⟩
+      exact ⟨![q, l], rfl, hq, by dsimp [q]; omega, (hdata q hq).mpr h⟩
+
+end Cslib.Logic.Vocabulary

Complexity/Computability/Complexity/ImmermanVardi/Tableau/Acceptance.lean

@@ -0,0 +1,110 @@
+/-
+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.ImmermanVardi.Tableau.Definability
+import Mathlib.Tactic.FinCases
+
+/-!
+# FO(LFP) sentences for native machine acceptance
+
+One sentence expresses that a given deterministic native machine has halted with output
+`[true]` by the maximum time in a finite ordered domain. The sentence is uniform in the
+input structure and the domain size. Its input-symbol formulas are ordinary first-order
+formulas, so no computational predicate is hidden in an added relation.
+
+## Main results
+
+* `exists_acceptance_sentence`: native bounded machine acceptance has a single checked
+  FO(LFP) sentence, given the first-order interpretation of its input tape.
+-/
+
+public section
+
+namespace Cslib.Complexity.ImmermanVardi.Tableau
+
+open Turing Turing.MultiTapeTM
+open FirstOrder Language
+open Cslib.Logic.FO
+open Cslib.Logic.FO.Operator
+
+variable {L : Language} {ι : Type} {size : ι → ℕ}
+  [∀ i, L.Structure (Fin (size i))] [∀ i, Fact (2 ≤ size i)]
+  {m : ℕ} {State : Type} [Fintype State]
+
+private def maximum (i : ι) : Fin (size i) :=
+  ⟨size i - 1, Nat.sub_lt (by have := (Fact.out : 2 ≤ size i); omega) (by omega)⟩
+
+private theorem trace_lfp_definable_terms (tm : MultiTapeTM m Bool State)
+    (input : ι → List Bool)
+    (inputFormula : Option Bool → (Ordered.language L).Formula (Fin 1))
+    (hinput : ∀ i s (a : Fin (size i)),
+      (inputFormula s).Realize ![a] ↔ inputAt (input i) a.val = s)
+    {α : Type} (args : Fin 3 → (Ordered.language L).Term α) :
+    Operator.Definable (L := Ordered.language L) LFP.policy
+      (fun i => Fin (size i)) (fun _ => LFP.interpretation) (fun _ => RelEnv.empty)
+      (fun i v => (fun j => (args j).realize v) ∈ (traceStep tm (input i)).lfp) := by
+  apply LFP.definable_lfp (fun i _ => traceStep tm (input i)) args
+  exact traceStep_polarityDefinable tm input inputFormula hinput Sum.inr
+
+private theorem row_at_maximum_definable (tm : MultiTapeTM m Bool State)
+    (input : ι → List Bool)
+    (inputFormula : Option Bool → (Ordered.language L).Formula (Fin 1))
+    (hinput : ∀ i s (a : Fin (size i)),
+      (inputFormula s).Realize ![a] ↔ inputAt (input i) a.val = s)
+    (hn : ∀ i, (input i).length + 1 < size i)
+    (hB : ∀ i, Fintype.card (Tag m State) ≤ size i) (q : Tag m State) :
+    Operator.Definable (L := Ordered.language L) LFP.policy
+      (fun i => Fin (size i)) (fun _ => LFP.interpretation) (fun _ => RelEnv.empty)
+      (fun i (_ : Empty → Fin (size i)) =>
+        row (tm.runFrom (tm.initCfg (input i)) (size i - 1)) q (maximum (size := size) i)) := by
+  have hf : Operator.Definable (L := Ordered.language L) LFP.policy
+      (fun i => Fin (size i)) (fun _ => LFP.interpretation) (fun _ => RelEnv.empty)
+      (fun i (_ : Empty → Fin (size i)) =>
+        traceRow (traceStep tm (input i)).lfp (maximum (size := size) i) q
+          (maximum (size := size) i)) := by
+    apply Definable.ex
+    apply Definable.conj
+    · exact (Definable.ofFO (Ordered.natEq L (tagIndex q) (.var none))).congr
+        fun _ _ => Ordered.realize_natEq _ _ _
+    · apply (trace_lfp_definable_terms tm input inputFormula hinput
+        ![.var none, Ordered.max L, Ordered.max L]).congr
+      intro i v
+      have hm : (Ordered.max L).realize v = maximum (size := size) i :=
+        Fin.ext (Ordered.realize_max_val _)
+      have htuple :
+          (fun j => ((![.var none, Ordered.max L, Ordered.max L] :
+            Fin 3 → (Ordered.language L).Term (Option Empty)) j).realize v) =
+            ![v none, maximum (size := size) i, maximum (size := size) i] := by
+        ext j
+        fin_cases j <;> simp [hm]
+      rw [htuple]
+  exact hf.congr fun i _ => traceRow_lfp tm (input i) (hn i) (hB i)
+    (maximum (size := size) i) q (maximum (size := size) i)
+
+/-- A native deterministic machine's acceptance by the domain's final time is described by one
+checked FO(LFP) sentence. All input symbols are interpreted by ordinary first-order formulas. -/
+theorem exists_acceptance_sentence (tm : MultiTapeTM m Bool State)
+    (input : ι → List Bool)
+    (inputFormula : Option Bool → (Ordered.language L).Formula (Fin 1))
+    (hinput : ∀ i s (a : Fin (size i)),
+      (inputFormula s).Realize ![a] ↔ inputAt (input i) a.val = s)
+    (hn : ∀ i, (input i).length + 1 < size i)
+    (hB : ∀ i, Fintype.card (Tag m State) ≤ size i) :
+    ∃ φ : LFP.Formula (Ordered.language L) [] Empty, ∀ i,
+      φ.Realize (M := Fin (size i)) RelEnv.empty (fun e => nomatch e) ↔
+        (tm.runFrom (tm.initCfg (input i)) (size i - 1)).Halted ∧
+          (tm.runFrom (tm.initCfg (input i)) (size i - 1)).output = [true] := by
+  have hs := row_at_maximum_definable tm input inputFormula hinput hn hB (.state none)
+  have ho := row_at_maximum_definable tm input inputFormula hinput hn hB (.out (.one true))
+  obtain ⟨φ, hwf, hφ⟩ := hs.conj ho
+  refine ⟨⟨φ, hwf⟩, fun i => ?_⟩
+  exact (hφ i (fun e => nomatch e)).trans (by
+    simp only [row, Tag.feature, Feature.Holds, OutView.ofList_eq_one_iff, Cfg.Halted])
+
+end Cslib.Complexity.ImmermanVardi.Tableau