From the Krom fragment to FO(TC), through the complement

The formula layer of the converse translation: the implication graph of a Krom program, walked by a DescriptiveComplexity.TCSpec.

DescriptiveComplexity.KromImpl.exists_holds_iff says that a Krom program is satisfiable exactly when no goal clause fires and no literal reaches its own negation and back, and DescriptiveComplexity.TwoCnf.carryReach_iff turns the second condition – a conjunction of two reachabilities – into a single walk of the cycle-witnessing graph, on nodes carrying the start literal, the current one and a flag. This file expresses that walk as first-order data:

• a node's two literals are two modes (a relation variable of the block and a sign, twice) together with two tuples of dimension DescriptiveComplexity.clauseDim, holding the canonically padded arguments of the two atoms – the same encoding the Horn and Krom discharges use;
• the flag is a third component of the mode;
• an edge of the implication graph is DescriptiveComplexity.KromTC.edgeCaseF: for one clause of the program and one choice of which of its literal slots is the source and which the target, the clause's guard holds at some valuation of its k variables, and the two node tuples hold the canonically padded arguments of the two atoms at that valuation. Quantifying the valuation existentially and taking the disjunction over the program gives the transition formula.

The walk starts at a node whose two literals agree and whose flag is down, and accepts when they agree again with the flag up; one extra mode accepts reflexively when a goal clause fires, the empty clause of the 2-CNF. So the specification accepts exactly when the program is unsatisfiable (DescriptiveComplexity.KromTC.accepts_iff_not_exists_holds), which is DescriptiveComplexity.TCDefinable.compl_of_sigmaSOKromDefinable: the complement of an SO-Krom definable problem is FO(TC) definable. With the direction proved in DescriptiveComplexity.TransitiveClosureKrom this is an equivalence, co-NL(Krom) = NL(TC) (DescriptiveComplexity.mem_NL_iff_tcDefinable_compl); what it is not is REACH ∈ NL, which needs the complementation of FO(TC) itself (Immerman–Szelepcsényi).

The two halves of a node's tuple

@[reducible, inline]

abbrev DescriptiveComplexity.KromTC.fstHalf (D : ℕ) : Fin D → Fin (D + D)

The first half of a node's tuple: the arguments of the start literal's atom.

Equations

• DescriptiveComplexity.KromTC.fstHalf D = Fin.castAdd D

@[reducible, inline]

abbrev DescriptiveComplexity.KromTC.sndHalf (D : ℕ) : Fin D → Fin (D + D)

The second half of a node's tuple: the arguments of the current literal's atom.

Equations

• DescriptiveComplexity.KromTC.sndHalf D = Fin.natAdd D

The edge formula

noncomputable def DescriptiveComplexity.KromTC.edgeCaseF {L : FirstOrder.Language} {B : SOBlock} {k : ℕ} {γ : Type} (c : KromClause (L.sum FirstOrder.Language.order) B k) (a₁ a₂ : SOAtom B k) (u w : Fin (clauseDim B k) → γ) : (L.sum FirstOrder.Language.order).Formula γ

One way for a clause to contribute an edge: its guard holds at some valuation of its k universally quantified variables, the coordinates selected by u hold the canonically padded arguments of the source atom at that valuation, and those selected by w hold the arguments of the target atom.

Equations

• One or more equations did not get rendered due to their size.

theorem DescriptiveComplexity.KromTC.realize_edgeCaseF {L : FirstOrder.Language} {B : SOBlock} {k : ℕ} {γ A : Type} [L.Structure A] [LinearOrder A] {v : γ → A} {c : KromClause (L.sum FirstOrder.Language.order) B k} {a₁ a₂ : SOAtom B k} {u w : Fin (clauseDim B k) → γ} : (edgeCaseF c a₁ a₂ u w).Realize v ↔ ∃ (t : Fin (clauseDim B k) → A), (c.guard.Realize fun (j : Fin k) => t (Fin.castLE ⋯ j)) ∧ (PadTup (atomIdx a₁) t fun (j : Fin (clauseDim B k)) => v (u j)) ∧ PadTup (atomIdx a₂) t fun (j : Fin (clauseDim B k)) => v (w j)

The literal a node denotes

noncomputable def DescriptiveComplexity.KromTC.litAt {B : SOBlock} {k : ℕ} {A : Type} (i : B.ι) (s : Bool) (w : Fin (clauseDim B k) → A) : TwoCnf.Lit (KromImpl.KromAtom B A)

The literal denoted by a relation variable, a sign and a tuple: the atom holds the first B.arity i coordinates.

Equations

• DescriptiveComplexity.KromTC.litAt i s w = (⟨i, DescriptiveComplexity.pref ⋯ w⟩, s)

@[simp]

theorem DescriptiveComplexity.KromTC.litAt_fst_fst {B : SOBlock} {k : ℕ} {A : Type} (i : B.ι) (s : Bool) (w : Fin (clauseDim B k) → A) : (litAt i s w).1.fst = i

@[simp]

theorem DescriptiveComplexity.KromTC.litAt_snd {B : SOBlock} {k : ℕ} {A : Type} (i : B.ι) (s : Bool) (w : Fin (clauseDim B k) → A) : (litAt i s w).2 = s

theorem DescriptiveComplexity.KromTC.litAt_pad {B : SOBlock} {k : ℕ} {A : Type} [LinearOrder A] {a₀ : A} (ha₀ : IsBot a₀) (l : KromLit B k) (t : Fin (clauseDim B k) → A) {x : Fin (clauseDim B k) → A} (hpad : PadTup (atomIdx l.atom) t x) : litAt l.atom.idx l.positive x = KromImpl.litOf l fun (j : Fin k) => t (Fin.castLE ⋯ j)

The literal of a Krom literal, read at the prefix of a clause tuple, is the literal its atom denotes at the canonical padding of its arguments.

The edges a clause contributes

noncomputable def DescriptiveComplexity.KromTC.clauseEdgeF {L : FirstOrder.Language} {B : SOBlock} {k : ℕ} {γ : Type} (c : KromClause (L.sum FirstOrder.Language.order) B k) (i j : B.ι) (s t : Bool) (u w : Fin (clauseDim B k) → γ) : (L.sum FirstOrder.Language.order).Formula γ

All the ways one clause contributes an edge from the literal (i, s) to the literal (j, t).

Equations

• One or more equations did not get rendered due to their size.

theorem DescriptiveComplexity.KromTC.realize_clauseEdgeF {L : FirstOrder.Language} {B : SOBlock} {k : ℕ} {γ A : Type} [L.Structure A] [LinearOrder A] {v : γ → A} {c : KromClause (L.sum FirstOrder.Language.order) B k} {i j : B.ι} {s t : Bool} {u w : Fin (clauseDim B k) → γ} : (clauseEdgeF c i j s t u w).Realize v ↔ ∃ pr ∈ KromImpl.edgePairs c, pr.1.atom.idx = i ∧ pr.1.positive = !s ∧ pr.2.atom.idx = j ∧ pr.2.positive = t ∧ ∃ (tv : Fin (clauseDim B k) → A), (c.guard.Realize fun (m : Fin k) => tv (Fin.castLE ⋯ m)) ∧ (PadTup (atomIdx pr.1.atom) tv fun (m : Fin (clauseDim B k)) => v (u m)) ∧ PadTup (atomIdx pr.2.atom) tv fun (m : Fin (clauseDim B k)) => v (w m)

The edges of the program

The transition formula proper: the disjunction over the program of the edges each clause contributes. Its realization is a step of the implication graph of DescriptiveComplexity.KromImpl.clauseRel, together with the canonicity of the two node tuples – which the formula forces, each disjunct pinning both tuples to the padded arguments of its atoms.

theorem DescriptiveComplexity.KromTC.eq_pad_of_litAt_eq {B : SOBlock} {k : ℕ} {A : Type} [LinearOrder A] {a₀ : A} (ha₀ : IsBot a₀) {i : B.ι} {s : Bool} {x : Fin (clauseDim B k) → A} {l : KromLit B k} {vv : Fin k → A} (hcan : Canon (B.arity i) x) (h : litAt i s x = KromImpl.litOf l vv) : l.atom.idx = i ∧ l.positive = s ∧ x = pad a₀ fun (m : Fin (B.arity l.atom.idx)) => vv (l.atom.args m)

Decoding a node tuple from the literal it denotes: under canonicity, the tuple is the canonical padding of the literal's arguments.

noncomputable def DescriptiveComplexity.KromTC.edgeF {L : FirstOrder.Language} {B : SOBlock} {k : ℕ} {γ : Type} (prog : KromProgram (L.sum FirstOrder.Language.order) B k) (i j : B.ι) (s t : Bool) (u w : Fin (clauseDim B k) → γ) : (L.sum FirstOrder.Language.order).Formula γ

The edge relation of the whole program, from the literal (i, s) to the literal (j, t).

Equations

• One or more equations did not get rendered due to their size.

theorem DescriptiveComplexity.KromTC.realize_edgeF {L : FirstOrder.Language} {B : SOBlock} {k : ℕ} {γ A : Type} [L.Structure A] [LinearOrder A] [Finite A] [Nonempty A] {v : γ → A} {prog : KromProgram (L.sum FirstOrder.Language.order) B k} {i j : B.ι} {s t : Bool} {u w : Fin (clauseDim B k) → γ} : (edgeF prog i j s t u w).Realize v ↔ (Canon (B.arity i) fun (m : Fin (clauseDim B k)) => v (u m)) ∧ (Canon (B.arity j) fun (m : Fin (clauseDim B k)) => v (w m)) ∧ TwoCnf.Step (KromImpl.clauseRel prog) (litAt i s fun (m : Fin (clauseDim B k)) => v (u m)) (litAt j t fun (m : Fin (clauseDim B k)) => v (w m))

The transition formula is the implication graph: it holds exactly when both node tuples are canonically padded and the literals they denote form an edge.

The specification

The nodes of the walk are the nodes of the cycle-witnessing graph of DescriptiveComplexity.TwoCnf.carryReach_iff: the start literal, the current literal and a flag. The two literals' relation variables and signs, and the flag, are the mode; their arguments are the two halves of the tuple. One extra mode accepts reflexively when a goal clause fires.

@[reducible, inline]

abbrev DescriptiveComplexity.KromTC.LitMode (B : SOBlock) : Type

A literal's share of a mode: a relation variable of the block and a sign.

Equations

• DescriptiveComplexity.KromTC.LitMode B = (B.ι × Bool)

@[reducible, inline]

abbrev DescriptiveComplexity.KromTC.Mode (B : SOBlock) : Type

The modes of the walk: the two literals' shares and the flag, or the mode that reports a firing goal clause.

Equations

• DescriptiveComplexity.KromTC.Mode B = (DescriptiveComplexity.KromTC.LitMode B × DescriptiveComplexity.KromTC.LitMode B × Bool ⊕ Unit)

noncomputable def DescriptiveComplexity.KromTC.goalF {L : FirstOrder.Language} {B : SOBlock} {k : ℕ} (prog : KromProgram (L.sum FirstOrder.Language.order) B k) {γ : Type} : (L.sum FirstOrder.Language.order).Formula γ

Some goal clause of the program fires.

Equations

• One or more equations did not get rendered due to their size.

theorem DescriptiveComplexity.KromTC.realize_goalF {L : FirstOrder.Language} {B : SOBlock} {k : ℕ} (prog : KromProgram (L.sum FirstOrder.Language.order) B k) {γ A : Type} [L.Structure A] [LinearOrder A] [Nonempty A] {v : γ → A} : (goalF prog).Realize v ↔ KromImpl.GoalFires prog A

noncomputable def DescriptiveComplexity.KromTC.srcF {L : FirstOrder.Language} {B : SOBlock} {k : ℕ} (prog : KromProgram (L.sum FirstOrder.Language.order) B k) : Mode B → (L.sum FirstOrder.Language.order).Formula (Fin (clauseDim B k + clauseDim B k))

The starting nodes: the current literal is the start, the flag is down, and both halves of the tuple are the same canonical padding – or a firing goal clause, in the reporting mode.

Equations

• One or more equations did not get rendered due to their size.
• DescriptiveComplexity.KromTC.srcF prog (Sum.inr PUnit.unit) = DescriptiveComplexity.KromTC.goalF prog

noncomputable def DescriptiveComplexity.KromTC.tgtF {L : FirstOrder.Language} {B : SOBlock} {k : ℕ} (prog : KromProgram (L.sum FirstOrder.Language.order) B k) : Mode B → (L.sum FirstOrder.Language.order).Formula (Fin (clauseDim B k + clauseDim B k))

The accepting nodes: the current literal is the start again, with the flag up – or a firing goal clause.

Equations

• One or more equations did not get rendered due to their size.
• DescriptiveComplexity.KromTC.tgtF prog (Sum.inr PUnit.unit) = DescriptiveComplexity.KromTC.goalF prog

@[reducible, inline]

abbrev DescriptiveComplexity.KromTC.Walk (B : SOBlock) : Type

The payload of a walk mode: the two literals' shares and the flag.

Equations

• DescriptiveComplexity.KromTC.Walk B = (DescriptiveComplexity.KromTC.LitMode B × DescriptiveComplexity.KromTC.LitMode B × Bool)

noncomputable def DescriptiveComplexity.KromTC.stepWalkF {L : FirstOrder.Language} {B : SOBlock} {k : ℕ} (prog : KromProgram (L.sum FirstOrder.Language.order) B k) (p q : Walk B) : (L.sum FirstOrder.Language.order).Formula (Fin (clauseDim B k + clauseDim B k) ⊕ Fin (clauseDim B k + clauseDim B k))

One step between two walk modes, as a formula on the two nodes' tuples: the start is kept, the current literal moves along an edge of the implication graph, and the flag may go up only on arrival at the negation of the start.

Stated on the payloads rather than on DescriptiveComplexity.KromTC.Mode, so that its realization lemma applies without unfolding a match.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def DescriptiveComplexity.KromTC.stepF {L : FirstOrder.Language} {B : SOBlock} {k : ℕ} (prog : KromProgram (L.sum FirstOrder.Language.order) B k) : Mode B → Mode B → (L.sum FirstOrder.Language.order).Formula (Fin (clauseDim B k + clauseDim B k) ⊕ Fin (clauseDim B k + clauseDim B k))

One step: a step between walk modes, and nothing into or out of the mode that reports a firing goal clause.

Equations

• DescriptiveComplexity.KromTC.stepF prog (Sum.inl p) (Sum.inl q) = DescriptiveComplexity.KromTC.stepWalkF prog p q
• DescriptiveComplexity.KromTC.stepF prog x✝¹ x✝ = ⊥

theorem DescriptiveComplexity.KromTC.realize_stepWalkF {L : FirstOrder.Language} {B : SOBlock} {k : ℕ} (prog : KromProgram (L.sum FirstOrder.Language.order) B k) {A : Type} [L.Structure A] [LinearOrder A] [Finite A] [Nonempty A] {p q : Walk B} {x y : Fin (clauseDim B k + clauseDim B k) → A} : (stepWalkF prog p q).Realize (Sum.elim x y) ↔ (q.1 = p.1 ∧ (q.2.2 = p.2.2 ∨ p.2.2 = false ∧ q.2.2 = true ∧ q.2.1 = (p.1.1, !p.1.2))) ∧ ((fun (m : Fin (clauseDim B k)) => y (fstHalf (clauseDim B k) m)) = fun (m : Fin (clauseDim B k)) => x (fstHalf (clauseDim B k) m)) ∧ (Canon (B.arity p.2.1.1) fun (m : Fin (clauseDim B k)) => x (sndHalf (clauseDim B k) m)) ∧ (Canon (B.arity q.2.1.1) fun (m : Fin (clauseDim B k)) => y (sndHalf (clauseDim B k) m)) ∧ TwoCnf.Step (KromImpl.clauseRel prog) (litAt p.2.1.1 p.2.1.2 fun (m : Fin (clauseDim B k)) => x (sndHalf (clauseDim B k) m)) (litAt q.2.1.1 q.2.1.2 fun (m : Fin (clauseDim B k)) => y (sndHalf (clauseDim B k) m)) ∧ (p.2.2 = false → q.2.2 = true → (fun (m : Fin (clauseDim B k)) => y (sndHalf (clauseDim B k) m)) = fun (m : Fin (clauseDim B k)) => y (fstHalf (clauseDim B k) m))

Realization of a step between walk modes, spelled out.

@[reducible, inline]

noncomputable abbrev DescriptiveComplexity.KromTC.spec {L : FirstOrder.Language} {B : SOBlock} {k : ℕ} (prog : KromProgram (L.sum FirstOrder.Language.order) B k) : TCSpec L

The specification: the cycle-witnessing walk of the program's implication graph, plus the mode reporting a firing goal clause.

Equations

• One or more equations did not get rendered due to their size.

theorem DescriptiveComplexity.KromTC.step_spec_walk_iff {L : FirstOrder.Language} {B : SOBlock} {k : ℕ} (prog : KromProgram (L.sum FirstOrder.Language.order) B k) {A : Type} [L.Structure A] [LinearOrder A] {p q : Walk B} {x y : Fin (clauseDim B k + clauseDim B k) → A} : (spec prog).Step (Sum.inl p, x) (Sum.inl q, y) ↔ (stepWalkF prog p q).Realize (Sum.elim x y)

Realization of a step of the specification, between walk modes.

theorem DescriptiveComplexity.KromTC.not_step_goal_left {L : FirstOrder.Language} {B : SOBlock} {k : ℕ} (prog : KromProgram (L.sum FirstOrder.Language.order) B k) {A : Type} [L.Structure A] [LinearOrder A] {q : Mode B} {x y : Fin (clauseDim B k + clauseDim B k) → A} : ¬(spec prog).Step (Sum.inr (), x) (q, y)

There is no step out of the goal-reporting mode.

theorem DescriptiveComplexity.KromTC.not_step_goal_right {L : FirstOrder.Language} {B : SOBlock} {k : ℕ} (prog : KromProgram (L.sum FirstOrder.Language.order) B k) {A : Type} [L.Structure A] [LinearOrder A] {p : Mode B} {x y : Fin (clauseDim B k + clauseDim B k) → A} : ¬(spec prog).Step (p, x) (Sum.inr (), y)

There is no step into the goal-reporting mode.

Nodes and carry nodes

noncomputable def DescriptiveComplexity.KromTC.decodeNode {B : SOBlock} {k : ℕ} {A : Type} (p : Walk B) (x : Fin (clauseDim B k + clauseDim B k) → A) : TwoCnf.CarryNode (KromImpl.KromAtom B A)

The carry node a walk node denotes.

Equations

• One or more equations did not get rendered due to their size.

def DescriptiveComplexity.KromTC.modeOf {B : SOBlock} {A : Type} (n : TwoCnf.CarryNode (KromImpl.KromAtom B A)) : Walk B

The walk mode of a carry node.

Equations

• DescriptiveComplexity.KromTC.modeOf n = ((n.1.1.fst, n.1.2), (n.2.1.1.fst, n.2.1.2), n.2.2)

noncomputable def DescriptiveComplexity.KromTC.tupleOf {B : SOBlock} {k : ℕ} {A : Type} (a₀ : A) (n : TwoCnf.CarryNode (KromImpl.KromAtom B A)) : Fin (clauseDim B k + clauseDim B k) → A

The tuple of a carry node: the two atoms, canonically padded.

Equations

• DescriptiveComplexity.KromTC.tupleOf a₀ n i = Fin.addCases (DescriptiveComplexity.pad a₀ n.1.1.snd) (DescriptiveComplexity.pad a₀ n.2.1.1.snd) i

@[simp]

theorem DescriptiveComplexity.KromTC.tupleOf_fstHalf {B : SOBlock} {k : ℕ} {A : Type} (a₀ : A) (n : TwoCnf.CarryNode (KromImpl.KromAtom B A)) (m : Fin (clauseDim B k)) : tupleOf a₀ n (fstHalf (clauseDim B k) m) = pad a₀ n.1.1.snd m

@[simp]

theorem DescriptiveComplexity.KromTC.tupleOf_sndHalf {B : SOBlock} {k : ℕ} {A : Type} (a₀ : A) (n : TwoCnf.CarryNode (KromImpl.KromAtom B A)) (m : Fin (clauseDim B k)) : tupleOf a₀ n (sndHalf (clauseDim B k) m) = pad a₀ n.2.1.1.snd m

@[simp]

theorem DescriptiveComplexity.KromTC.modeOf_fst {B : SOBlock} {A : Type} (n : TwoCnf.CarryNode (KromImpl.KromAtom B A)) : (modeOf n).1 = (n.1.1.fst, n.1.2)

@[simp]

theorem DescriptiveComplexity.KromTC.modeOf_snd_fst {B : SOBlock} {A : Type} (n : TwoCnf.CarryNode (KromImpl.KromAtom B A)) : (modeOf n).2.1 = (n.2.1.1.fst, n.2.1.2)

@[simp]

theorem DescriptiveComplexity.KromTC.modeOf_snd_snd {B : SOBlock} {A : Type} (n : TwoCnf.CarryNode (KromImpl.KromAtom B A)) : (modeOf n).2.2 = n.2.2

@[simp]

theorem DescriptiveComplexity.KromTC.decodeNode_fst {B : SOBlock} {k : ℕ} {A : Type} (p : Walk B) (x : Fin (clauseDim B k + clauseDim B k) → A) : (decodeNode p x).1 = litAt p.1.1 p.1.2 fun (m : Fin (clauseDim B k)) => x (fstHalf (clauseDim B k) m)

@[simp]

theorem DescriptiveComplexity.KromTC.decodeNode_snd_fst {B : SOBlock} {k : ℕ} {A : Type} (p : Walk B) (x : Fin (clauseDim B k + clauseDim B k) → A) : (decodeNode p x).2.1 = litAt p.2.1.1 p.2.1.2 fun (m : Fin (clauseDim B k)) => x (sndHalf (clauseDim B k) m)

@[simp]

theorem DescriptiveComplexity.KromTC.decodeNode_snd_snd {B : SOBlock} {k : ℕ} {A : Type} (p : Walk B) (x : Fin (clauseDim B k + clauseDim B k) → A) : (decodeNode p x).2.2 = p.2.2

theorem DescriptiveComplexity.KromTC.litAt_pad_self {B : SOBlock} {k : ℕ} {A : Type} (a₀ : A) (p : TwoCnf.Lit (KromImpl.KromAtom B A)) : litAt p.1.fst p.2 (pad a₀ p.1.snd) = p

theorem DescriptiveComplexity.KromTC.decodeNode_tupleOf {B : SOBlock} {k : ℕ} {A : Type} (a₀ : A) (n : TwoCnf.CarryNode (KromImpl.KromAtom B A)) : decodeNode (modeOf n) (tupleOf a₀ n) = n

Decoding the encoding gives the carry node back.

theorem DescriptiveComplexity.KromTC.step_of_carryStep {L : FirstOrder.Language} {B : SOBlock} {k : ℕ} (prog : KromProgram (L.sum FirstOrder.Language.order) B k) {A : Type} [L.Structure A] [LinearOrder A] [Finite A] [Nonempty A] {a₀ : A} (ha₀ : IsBot a₀) {n m : TwoCnf.CarryNode (KromImpl.KromAtom B A)} (h : TwoCnf.CarryStep (KromImpl.clauseRel prog) n m) : (spec prog).Step (Sum.inl (modeOf n), tupleOf a₀ n) (Sum.inl (modeOf m), tupleOf a₀ m)

A carry step lifts to a step of the specification, at the canonically padded nodes.

theorem DescriptiveComplexity.KromTC.carryStep_of_step {L : FirstOrder.Language} {B : SOBlock} {k : ℕ} (prog : KromProgram (L.sum FirstOrder.Language.order) B k) {A : Type} [L.Structure A] [LinearOrder A] [Finite A] [Nonempty A] {p q : Walk B} {x y : Fin (clauseDim B k + clauseDim B k) → A} (h : (spec prog).Step (Sum.inl p, x) (Sum.inl q, y)) : TwoCnf.CarryStep (KromImpl.clauseRel prog) (decodeNode p x) (decodeNode q y)

A step of the specification is a carry step of the decoded nodes.

Walks

theorem DescriptiveComplexity.KromTC.reach_of_carryReach {L : FirstOrder.Language} {B : SOBlock} {k : ℕ} (prog : KromProgram (L.sum FirstOrder.Language.order) B k) {A : Type} [L.Structure A] [LinearOrder A] [Finite A] [Nonempty A] {a₀ : A} (ha₀ : IsBot a₀) {n m : TwoCnf.CarryNode (KromImpl.KromAtom B A)} (h : Relation.ReflTransGen (TwoCnf.CarryStep (KromImpl.clauseRel prog)) n m) : (spec prog).Reach (Sum.inl (modeOf n), tupleOf a₀ n) (Sum.inl (modeOf m), tupleOf a₀ m)

A walk of the cycle-witnessing graph lifts to a walk of the specification, at the canonically padded nodes.

theorem DescriptiveComplexity.KromTC.carryReach_of_reach {L : FirstOrder.Language} {B : SOBlock} {k : ℕ} (prog : KromProgram (L.sum FirstOrder.Language.order) B k) {A : Type} [L.Structure A] [LinearOrder A] [Finite A] [Nonempty A] {p : Walk B} {x : Fin (clauseDim B k + clauseDim B k) → A} {d : (spec prog).Node A} (h : (spec prog).Reach (Sum.inl p, x) d) : ∃ (q : Walk B) (y : Fin (clauseDim B k + clauseDim B k) → A), d = (Sum.inl q, y) ∧ Relation.ReflTransGen (TwoCnf.CarryStep (KromImpl.clauseRel prog)) (decodeNode p x) (decodeNode q y)

A walk of the specification out of a walk mode is one of the cycle-witnessing graph: the goal-reporting mode is never entered, so every node along the way decodes to a carry node.

The endpoints

theorem DescriptiveComplexity.KromTC.isSrc_inl_iff {L : FirstOrder.Language} {B : SOBlock} {k : ℕ} (prog : KromProgram (L.sum FirstOrder.Language.order) B k) {A : Type} [L.Structure A] [LinearOrder A] {i j : B.ι} {s t ph : Bool} {x : Fin (clauseDim B k + clauseDim B k) → A} : (spec prog).IsSrc (Sum.inl ((i, s), (j, t), ph), x) ↔ ((i, s) = (j, t) ∧ ph = false) ∧ ((fun (m : Fin (clauseDim B k)) => x (sndHalf (clauseDim B k) m)) = fun (m : Fin (clauseDim B k)) => x (fstHalf (clauseDim B k) m)) ∧ (Canon (B.arity i) fun (m : Fin (clauseDim B k)) => x (fstHalf (clauseDim B k) m)) ∧ Canon (B.arity i) fun (m : Fin (clauseDim B k)) => x (sndHalf (clauseDim B k) m)

A walk node is a starting node exactly when its current literal is its start, its flag is down, and its two halves are the same canonical tuple.

theorem DescriptiveComplexity.KromTC.isTgt_inl_iff {L : FirstOrder.Language} {B : SOBlock} {k : ℕ} (prog : KromProgram (L.sum FirstOrder.Language.order) B k) {A : Type} [L.Structure A] [LinearOrder A] {i j : B.ι} {s t ph : Bool} {x : Fin (clauseDim B k + clauseDim B k) → A} : (spec prog).IsTgt (Sum.inl ((i, s), (j, t), ph), x) ↔ ((i, s) = (j, t) ∧ ph = true) ∧ (fun (m : Fin (clauseDim B k)) => x (sndHalf (clauseDim B k) m)) = fun (m : Fin (clauseDim B k)) => x (fstHalf (clauseDim B k) m)

A walk node is accepting exactly when its current literal is its start again, with the flag up.

theorem DescriptiveComplexity.KromTC.isSrc_inr_iff {L : FirstOrder.Language} {B : SOBlock} {k : ℕ} (prog : KromProgram (L.sum FirstOrder.Language.order) B k) {A : Type} [L.Structure A] [LinearOrder A] [Nonempty A] {x : Fin (clauseDim B k + clauseDim B k) → A} : (spec prog).IsSrc (Sum.inr (), x) ↔ KromImpl.GoalFires prog A

The goal-reporting mode is a starting mode exactly when a goal clause fires.

theorem DescriptiveComplexity.KromTC.isTgt_inr_iff {L : FirstOrder.Language} {B : SOBlock} {k : ℕ} (prog : KromProgram (L.sum FirstOrder.Language.order) B k) {A : Type} [L.Structure A] [LinearOrder A] [Nonempty A] {x : Fin (clauseDim B k + clauseDim B k) → A} : (spec prog).IsTgt (Sum.inr (), x) ↔ KromImpl.GoalFires prog A

The goal-reporting mode is accepting exactly when a goal clause fires.

Correctness

theorem DescriptiveComplexity.KromTC.accepts_iff_not_exists_holds {L : FirstOrder.Language} {B : SOBlock} {k : ℕ} (prog : KromProgram (L.sum FirstOrder.Language.order) B k) {A : Type} [L.Structure A] [LinearOrder A] [Finite A] [Nonempty A] : (spec prog).Accepts A ↔ ¬∃ (ρ : B.Assignment A), prog.Holds ρ

Correctness: the specification accepts exactly when the program is unsatisfiable – either a goal clause fires, in the reporting mode, or some literal of the implication graph reaches its own negation and back, which the cycle-witnessing walk sees as a walk from (p, p, false) to (p, p, true).

theorem DescriptiveComplexity.TCDefinable.compl_of_sigmaSOKromDefinable {L : FirstOrder.Language} {P : DecisionProblem L} (h : SigmaSOKromDefinable P) : TCDefinable Pᶜ

The complement of an SO-Krom definable problem is FO(TC) definable: a Krom program instantiated in a structure is a 2-CNF on the atoms of its block, so it is unsatisfiable exactly when a goal clause fires or some literal reaches its own negation and back, and the second condition is a single walk of the cycle-witnessing graph – whose nodes are a pair of literals and a flag, i.e. a mode and two canonically padded tuples. Together with DescriptiveComplexity.SigmaSOKromDefinable.compl_of_tcDefinable this gives co-NL(Krom) = NL(TC); it is upgraded to NL = coNL by Immerman–Szelepcsényi (DescriptiveComplexity.NL_eq_coNL).

theorem DescriptiveComplexity.sigmaSOKromDefinable_iff_tcDefinable_compl {L : FirstOrder.Language} (P : DecisionProblem L) : SigmaSOKromDefinable P ↔ TCDefinable Pᶜ

The two translations compose: a problem is SO-Krom definable exactly when its complement is FO(TC) definable, co-NL(Krom) = NL(TC).

theorem DescriptiveComplexity.mem_NL_iff_tcDefinable_compl {L : FirstOrder.Language} (P : DecisionProblem L) : NL.Mem P ↔ TCDefinable Pᶜ

NL is the complements of the FO(TC) definable problems.