The unit-propagation machine of a Horn formula

The program half of HORNSAT ≤ᶠᵒ[≤] DTMAccept, stage 4 of the machine bridge: the states, symbols and transitions of the deterministic machine computing the unit-propagation closure of a CNF instance and verifying it, on the tape laid out in DescriptiveComplexity.Problems.Machine.HornTape.

The program

  init:      at ⊢, dispatch – first check sweep if a clause exists, else accept
  chk(r, c):  sweep right, f := f ∧ (negIn c x → marked x)
  mark(r, c): sweep back left; if the check succeeded, mark the positive
              literal of c in passing
  … next clause; after the last clause, next round; after the last round …
  ver(c):     sweep, f := f ∨ (posIn c x ∧ marked x) ∨ (negIn c x ∧ ¬marked x),
              alternating direction; a failed clause leaves no transition
  accept     after the last verified clause – gated on the Horn condition

n rounds of one check-and-mark pass per clause compute the propagation closure DescriptiveComplexity.Forced (DescriptiveComplexity.forced_forcedIn_card is the stabilization), and the verification phase accepts exactly when the closure, read as an assignment, satisfies every clause – which for a Horn instance is satisfiability itself (DescriptiveComplexity.satisfiable_iff_forced_model).

The machine is deterministic everywhere – there is no guess phase – and DescriptiveComplexity.TMData.Deterministic for the constructed machine is part of the statement, not bookkeeping: it is what makes the image a potential yes-instance of DTMAccept at all. The instance is read exactly as in stage 3 (DescriptiveComplexity.SatCl, DescriptiveComplexity.SatPos, …, imported from DescriptiveComplexity.Problems.Machine.Hardness together with the clause-order machinery), and the only two additions are the element order (rounds walk it) and the Horn gate on the accept transition.

The elements of the machine

@[reducible, inline]

abbrev DescriptiveComplexity.HV (A : Type) : Type

The universe of the machine: tagged triples.

Equations

• DescriptiveComplexity.HV A = (DescriptiveComplexity.UPTag × (Fin 3 → A))

noncomputable def DescriptiveComplexity.cstH {A : Type} [LinearOrder A] [Finite A] [Nonempty A] (t : UPTag) : HV A

A constant of the machine: a tag on the triple of least elements.

Equations

• DescriptiveComplexity.cstH t = (t, fun (x : Fin 3) => DescriptiveComplexity.botA)

noncomputable def DescriptiveComplexity.oneH {A : Type} [LinearOrder A] [Finite A] [Nonempty A] (t : UPTag) (a : A) : HV A

A tag carrying one element.

Equations

• DescriptiveComplexity.oneH t a = (t, ![a, DescriptiveComplexity.botA, DescriptiveComplexity.botA])

noncomputable def DescriptiveComplexity.twoH {A : Type} [LinearOrder A] [Finite A] [Nonempty A] (t : UPTag) (a b : A) : HV A

A tag carrying two elements.

Equations

• DescriptiveComplexity.twoH t a b = (t, ![a, b, DescriptiveComplexity.botA])

theorem DescriptiveComplexity.isMinTup3_bot {A : Type} [LinearOrder A] [Finite A] [Nonempty A] : IsMinTup3 fun (x : Fin 3) => botA

Symbols

@[reducible, inline]

noncomputable abbrev DescriptiveComplexity.symHStart {A : Type} [LinearOrder A] [Finite A] [Nonempty A] : HV A

The left-marker symbol.

Equations

• DescriptiveComplexity.symHStart = DescriptiveComplexity.cstH DescriptiveComplexity.UPTag.sStart

@[reducible, inline]

noncomputable abbrev DescriptiveComplexity.symHEnd {A : Type} [LinearOrder A] [Finite A] [Nonempty A] : HV A

The right-marker symbol.

Equations

• DescriptiveComplexity.symHEnd = DescriptiveComplexity.cstH DescriptiveComplexity.UPTag.sEnd

@[reducible, inline]

noncomputable abbrev DescriptiveComplexity.symHBlank {A : Type} [LinearOrder A] [Finite A] [Nonempty A] : HV A

The blank symbol.

Equations

• DescriptiveComplexity.symHBlank = DescriptiveComplexity.cstH DescriptiveComplexity.UPTag.sBlank

@[reducible, inline]

noncomputable abbrev DescriptiveComplexity.symCell {A : Type} [LinearOrder A] [Finite A] [Nonempty A] (m : Bool) (x : A) : HV A

The symbol of the cell of x, with mark m.

Equations

• DescriptiveComplexity.symCell m x = DescriptiveComplexity.oneH (if m = true then DescriptiveComplexity.UPTag.sM else DescriptiveComplexity.UPTag.sU) x

Positions

@[reducible, inline]

noncomputable abbrev DescriptiveComplexity.posHStart {A : Type} [LinearOrder A] [Finite A] [Nonempty A] : HV A

The left-marker cell.

Equations

• DescriptiveComplexity.posHStart = DescriptiveComplexity.cstH DescriptiveComplexity.UPTag.pStart

@[reducible, inline]

noncomputable abbrev DescriptiveComplexity.posHCell {A : Type} [LinearOrder A] [Finite A] [Nonempty A] (x : A) : HV A

The cell of the element x.

Equations

• DescriptiveComplexity.posHCell x = DescriptiveComplexity.oneH DescriptiveComplexity.UPTag.pCell x

@[reducible, inline]

noncomputable abbrev DescriptiveComplexity.posHEnd {A : Type} [LinearOrder A] [Finite A] [Nonempty A] : HV A

The right-marker cell.

Equations

• DescriptiveComplexity.posHEnd = DescriptiveComplexity.cstH DescriptiveComplexity.UPTag.pEnd

States

@[reducible, inline]

noncomputable abbrev DescriptiveComplexity.stHInit {A : Type} [LinearOrder A] [Finite A] [Nonempty A] : HV A

The dispatch state.

Equations

• DescriptiveComplexity.stHInit = DescriptiveComplexity.cstH DescriptiveComplexity.UPTag.qInit

@[reducible, inline]

noncomputable abbrev DescriptiveComplexity.stHChk {A : Type} [LinearOrder A] [Finite A] [Nonempty A] (f : Bool) (r c : A) : HV A

Checking the clause c in round r, flag f.

Equations

• DescriptiveComplexity.stHChk f r c = DescriptiveComplexity.twoH (DescriptiveComplexity.UPTag.qChk f) r c

@[reducible, inline]

noncomputable abbrev DescriptiveComplexity.stHMark {A : Type} [LinearOrder A] [Finite A] [Nonempty A] (m : Bool) (r c : A) : HV A

The return sweep of clause c in round r, marking iff m.

Equations

• DescriptiveComplexity.stHMark m r c = DescriptiveComplexity.twoH (DescriptiveComplexity.UPTag.qMark m) r c

@[reducible, inline]

noncomputable abbrev DescriptiveComplexity.stHVer {A : Type} [LinearOrder A] [Finite A] [Nonempty A] (f d : Bool) (c : A) : HV A

Verifying the clause c, flag f, sweeping in direction d.

Equations

• DescriptiveComplexity.stHVer f d c = DescriptiveComplexity.oneH (DescriptiveComplexity.UPTag.qVer f d) c

@[reducible, inline]

noncomputable abbrev DescriptiveComplexity.stHAcc {A : Type} [LinearOrder A] [Finite A] [Nonempty A] : HV A

The accepting state.

Equations

• DescriptiveComplexity.stHAcc = DescriptiveComplexity.cstH DescriptiveComplexity.UPTag.qAcc

Reading the order of the elements

def DescriptiveComplexity.MinElt {A : Type} [LinearOrder A] (a : A) : Prop

a is the least element.

Equations

• DescriptiveComplexity.MinElt a = ∀ (b : A), a ≤ b

def DescriptiveComplexity.MaxElt {A : Type} [LinearOrder A] (a : A) : Prop

a is the greatest element.

Equations

• DescriptiveComplexity.MaxElt a = ∀ (b : A), b ≤ a

def DescriptiveComplexity.SuccElt {A : Type} [LinearOrder A] (a b : A) : Prop

b is the successor of a in the order of the elements: rounds walk this relation.

Equations

• DescriptiveComplexity.SuccElt a b = (a < b ∧ ∀ (z : A), a < z → b ≤ z)

def DescriptiveComplexity.MLit {A : Type} [FirstOrder.Language.sat.Structure A] (c x : A) (m : Bool) : Prop

The satisfaction test of the verification phase: the cell x, with mark m, satisfies the clause c under the marked assignment. This is DescriptiveComplexity.SatLit with the marks as the valuation.

Equations

• DescriptiveComplexity.MLit c x m = (DescriptiveComplexity.SatPos c x ∧ m = true ∨ DescriptiveComplexity.SatNeg c x ∧ m = false)

The transition table

def DescriptiveComplexity.HTr {A : Type} [FirstOrder.Language.sat.Structure A] [LinearOrder A] (τ : HV A) : Prop

Which tagged triples are transitions: the payload promises. Coordinates not pinned by the source state or the symbol read are pinned here, so that no junk element is a transition.

Equations

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

def DescriptiveComplexity.HSrc {A : Type} [LinearOrder A] [Finite A] [Nonempty A] (τ q : HV A) : Prop

The state a transition applies in.

Equations

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

def DescriptiveComplexity.HRead {A : Type} [LinearOrder A] [Finite A] [Nonempty A] (τ a : HV A) : Prop

The symbol a transition reads.

Equations

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

def DescriptiveComplexity.HDst {A : Type} [FirstOrder.Language.sat.Structure A] [LinearOrder A] [Finite A] [Nonempty A] (τ q : HV A) : Prop

The state a transition moves to. The check and verification sweeps branch on a first-order test of the source instance; each pair of branches is exclusive, which is what keeps the table functional.

Equations

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

def DescriptiveComplexity.HWrite {A : Type} [FirstOrder.Language.sat.Structure A] [LinearOrder A] [Finite A] [Nonempty A] (τ a : HV A) : Prop

The symbol a transition writes: only the return sweep of a successful check writes anything new, and only at the positive literal of its clause.

Equations

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

def DescriptiveComplexity.HRight {A : Type} (τ : HV A) : Prop

Which transitions move the head right.

Equations

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

def DescriptiveComplexity.HAcc {A : Type} (q : HV A) : Prop

Accepting states.

Equations

• DescriptiveComplexity.HAcc q = (q.1 = DescriptiveComplexity.UPTag.qAcc)

def DescriptiveComplexity.HStart {A : Type} [LinearOrder A] (q : HV A) : Prop

Start states: the dispatch state alone.

Equations

• DescriptiveComplexity.HStart q = (q.1 = DescriptiveComplexity.UPTag.qInit ∧ DescriptiveComplexity.IsMinTup3 q.2)

def DescriptiveComplexity.hornMachine (A : Type) [FirstOrder.Language.sat.Structure A] [LinearOrder A] [Finite A] [Nonempty A] : TMData (HV A)

The unit-propagation machine of a CNF instance.

Equations

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

The machine is well formed

theorem DescriptiveComplexity.hornMachine_wellFormed {A : Type} [FirstOrder.Language.sat.Structure A] [LinearOrder A] [Finite A] [Nonempty A] : (hornMachine A).WellFormed

The machine is well formed: every conjunct comes from the tape layer.

The machine is deterministic

There is no guess phase, so – unlike stage 3 – the whole table is functional: the state and the symbol read pin the transition's tag up to promise-exclusive alternatives, the tag pins the payload, and the branching destinations and writes are separated by their first-order tests. This discharges the DescriptiveComplexity.TMData.Deterministic promise of the constructed instance, which is part of the correctness of the reduction.

theorem DescriptiveComplexity.hV_ext {A : Type} {τ τ' : HV A} (ht : τ.1 = τ'.1) (h0 : τ.2 0 = τ'.2 0) (h1 : τ.2 1 = τ'.2 1) (h2 : τ.2 2 = τ'.2 2) : τ = τ'

Two elements agree when their tag and all three coordinates do.

theorem DescriptiveComplexity.oneH_eq_oneH_iff {A : Type} [LinearOrder A] [Finite A] [Nonempty A] {t t' : UPTag} {a a' : A} : oneH t a = oneH t' a' ↔ t = t' ∧ a = a'

theorem DescriptiveComplexity.twoH_eq_twoH_iff {A : Type} [LinearOrder A] [Finite A] [Nonempty A] {t t' : UPTag} {a a' b b' : A} : twoH t a b = twoH t' a' b' ↔ t = t' ∧ a = a' ∧ b = b'

def DescriptiveComplexity.hStateTag : UPTag → UPTag

The tag of the state a transition applies in.

Equations

• DescriptiveComplexity.hStateTag DescriptiveComplexity.UPTag.tInitChk = DescriptiveComplexity.UPTag.qInit
• DescriptiveComplexity.hStateTag DescriptiveComplexity.UPTag.tInitAcc = DescriptiveComplexity.UPTag.qInit
• DescriptiveComplexity.hStateTag (DescriptiveComplexity.UPTag.tChk m f) = DescriptiveComplexity.UPTag.qChk f
• DescriptiveComplexity.hStateTag (DescriptiveComplexity.UPTag.tChkEnd f) = DescriptiveComplexity.UPTag.qChk f
• DescriptiveComplexity.hStateTag (DescriptiveComplexity.UPTag.tMark m mk) = DescriptiveComplexity.UPTag.qMark mk
• DescriptiveComplexity.hStateTag (DescriptiveComplexity.UPTag.tMarkEndNext mk) = DescriptiveComplexity.UPTag.qMark mk
• DescriptiveComplexity.hStateTag (DescriptiveComplexity.UPTag.tMarkEndRound mk) = DescriptiveComplexity.UPTag.qMark mk
• DescriptiveComplexity.hStateTag (DescriptiveComplexity.UPTag.tMarkEndVer mk) = DescriptiveComplexity.UPTag.qMark mk
• DescriptiveComplexity.hStateTag (DescriptiveComplexity.UPTag.tVer m f d) = DescriptiveComplexity.UPTag.qVer f d
• DescriptiveComplexity.hStateTag (DescriptiveComplexity.UPTag.tVerNext d) = DescriptiveComplexity.UPTag.qVer true d
• DescriptiveComplexity.hStateTag (DescriptiveComplexity.UPTag.tVerAcc d) = DescriptiveComplexity.UPTag.qVer true d
• DescriptiveComplexity.hStateTag x✝ = x✝

def DescriptiveComplexity.hReadTag : UPTag → UPTag

The tag of the symbol a transition reads.

Equations

• DescriptiveComplexity.hReadTag DescriptiveComplexity.UPTag.tInitChk = DescriptiveComplexity.UPTag.sStart
• DescriptiveComplexity.hReadTag DescriptiveComplexity.UPTag.tInitAcc = DescriptiveComplexity.UPTag.sStart
• DescriptiveComplexity.hReadTag (DescriptiveComplexity.UPTag.tChk m f) = if m = true then DescriptiveComplexity.UPTag.sM else DescriptiveComplexity.UPTag.sU
• DescriptiveComplexity.hReadTag (DescriptiveComplexity.UPTag.tChkEnd f) = DescriptiveComplexity.UPTag.sEnd
• DescriptiveComplexity.hReadTag (DescriptiveComplexity.UPTag.tMark m mk) = if m = true then DescriptiveComplexity.UPTag.sM else DescriptiveComplexity.UPTag.sU
• DescriptiveComplexity.hReadTag (DescriptiveComplexity.UPTag.tMarkEndNext mk) = DescriptiveComplexity.UPTag.sStart
• DescriptiveComplexity.hReadTag (DescriptiveComplexity.UPTag.tMarkEndRound mk) = DescriptiveComplexity.UPTag.sStart
• DescriptiveComplexity.hReadTag (DescriptiveComplexity.UPTag.tMarkEndVer mk) = DescriptiveComplexity.UPTag.sStart
• DescriptiveComplexity.hReadTag (DescriptiveComplexity.UPTag.tVer m f d) = if m = true then DescriptiveComplexity.UPTag.sM else DescriptiveComplexity.UPTag.sU
• DescriptiveComplexity.hReadTag (DescriptiveComplexity.UPTag.tVerNext d) = if d = true then DescriptiveComplexity.UPTag.sEnd else DescriptiveComplexity.UPTag.sStart
• DescriptiveComplexity.hReadTag (DescriptiveComplexity.UPTag.tVerAcc d) = if d = true then DescriptiveComplexity.UPTag.sEnd else DescriptiveComplexity.UPTag.sStart
• DescriptiveComplexity.hReadTag x✝ = x✝

def DescriptiveComplexity.isHTrTag : UPTag → Bool

Being the tag of a transition.

Equations

• DescriptiveComplexity.isHTrTag DescriptiveComplexity.UPTag.tInitChk = true
• DescriptiveComplexity.isHTrTag DescriptiveComplexity.UPTag.tInitAcc = true
• DescriptiveComplexity.isHTrTag (DescriptiveComplexity.UPTag.tChk m f) = true
• DescriptiveComplexity.isHTrTag (DescriptiveComplexity.UPTag.tChkEnd f) = true
• DescriptiveComplexity.isHTrTag (DescriptiveComplexity.UPTag.tMark m mk) = true
• DescriptiveComplexity.isHTrTag (DescriptiveComplexity.UPTag.tMarkEndNext mk) = true
• DescriptiveComplexity.isHTrTag (DescriptiveComplexity.UPTag.tMarkEndRound mk) = true
• DescriptiveComplexity.isHTrTag (DescriptiveComplexity.UPTag.tMarkEndVer mk) = true
• DescriptiveComplexity.isHTrTag (DescriptiveComplexity.UPTag.tVer m f d) = true
• DescriptiveComplexity.isHTrTag (DescriptiveComplexity.UPTag.tVerNext d) = true
• DescriptiveComplexity.isHTrTag (DescriptiveComplexity.UPTag.tVerAcc d) = true
• DescriptiveComplexity.isHTrTag x✝ = false

theorem DescriptiveComplexity.hTr_isHTrTag {A : Type} [FirstOrder.Language.sat.Structure A] [LinearOrder A] {τ : HV A} (hτ : HTr τ) : isHTrTag τ.1 = true

Only transitions have transition tags.

theorem DescriptiveComplexity.hSrc_tag {A : Type} [LinearOrder A] [Finite A] [Nonempty A] {τ q : HV A} (hs : HSrc τ q) : q.1 = hStateTag τ.1

The state pins the transition's tag.

theorem DescriptiveComplexity.hRead_tag {A : Type} [LinearOrder A] [Finite A] [Nonempty A] {τ a : HV A} (hr : HRead τ a) : a.1 = hReadTag τ.1

The symbol read pins the transition's tag.

def DescriptiveComplexity.isInitChk : UPTag → Bool

Tag classes for the promise-exclusive alternatives.

Equations

• DescriptiveComplexity.isInitChk DescriptiveComplexity.UPTag.tInitChk = true
• DescriptiveComplexity.isInitChk x✝ = false

def DescriptiveComplexity.isInitAcc : UPTag → Bool

Tag classes for the promise-exclusive alternatives.

Equations

• DescriptiveComplexity.isInitAcc DescriptiveComplexity.UPTag.tInitAcc = true
• DescriptiveComplexity.isInitAcc x✝ = false

def DescriptiveComplexity.isMarkEndNext : UPTag → Bool

Tag classes for the promise-exclusive alternatives.

Equations

• DescriptiveComplexity.isMarkEndNext (DescriptiveComplexity.UPTag.tMarkEndNext mk) = true
• DescriptiveComplexity.isMarkEndNext x✝ = false

def DescriptiveComplexity.isMarkEndRound : UPTag → Bool

Tag classes for the promise-exclusive alternatives.

Equations

• DescriptiveComplexity.isMarkEndRound (DescriptiveComplexity.UPTag.tMarkEndRound mk) = true
• DescriptiveComplexity.isMarkEndRound x✝ = false

def DescriptiveComplexity.isMarkEndVer : UPTag → Bool

Tag classes for the promise-exclusive alternatives.

Equations

• DescriptiveComplexity.isMarkEndVer (DescriptiveComplexity.UPTag.tMarkEndVer mk) = true
• DescriptiveComplexity.isMarkEndVer x✝ = false

def DescriptiveComplexity.isVerNext : UPTag → Bool

Tag classes for the promise-exclusive alternatives.

Equations

• DescriptiveComplexity.isVerNext (DescriptiveComplexity.UPTag.tVerNext d) = true
• DescriptiveComplexity.isVerNext x✝ = false

def DescriptiveComplexity.isVerAcc : UPTag → Bool

Tag classes for the promise-exclusive alternatives.

Equations

• DescriptiveComplexity.isVerAcc (DescriptiveComplexity.UPTag.tVerAcc d) = true
• DescriptiveComplexity.isVerAcc x✝ = false

theorem DescriptiveComplexity.hTag_cases (t t' : UPTag) : isHTrTag t = true → isHTrTag t' = true → hStateTag t = hStateTag t' → hReadTag t = hReadTag t' → t = t' ∨ (isInitChk t = true ∨ isInitAcc t = true) ∧ (isInitChk t' = true ∨ isInitAcc t' = true) ∨ (isMarkEndNext t = true ∨ isMarkEndRound t = true ∨ isMarkEndVer t = true) ∧ (isMarkEndNext t' = true ∨ isMarkEndRound t' = true ∨ isMarkEndVer t' = true) ∨ (isVerNext t = true ∨ isVerAcc t = true) ∧ (isVerNext t' = true ∨ isVerAcc t' = true)

The state and the symbol determine the transition's tag, up to the promise-exclusive alternatives: the two dispatches, the three ends of a return sweep, and the two ends of a verification sweep. A finite check over the tags.

theorem DescriptiveComplexity.satMinCl_unique {A : Type} [FirstOrder.Language.sat.Structure A] [LinearOrder A] {c c' : A} (h : SatMinCl c) (h' : SatMinCl c') : c = c'

The lowest clause is unique.

theorem DescriptiveComplexity.satMaxCl_unique {A : Type} [FirstOrder.Language.sat.Structure A] [LinearOrder A] {c c' : A} (h : SatMaxCl c) (h' : SatMaxCl c') : c = c'

The highest clause is unique.

theorem DescriptiveComplexity.satNextCl_unique {A : Type} [FirstOrder.Language.sat.Structure A] [LinearOrder A] {c c' c'' : A} (h : SatNextCl c c') (h' : SatNextCl c c'') : c' = c''

The next clause is unique.

theorem DescriptiveComplexity.minElt_unique {A : Type} [LinearOrder A] {a a' : A} (h : MinElt a) (h' : MinElt a') : a = a'

The least element is unique.

theorem DescriptiveComplexity.succElt_unique {A : Type} [LinearOrder A] {a b b' : A} (h : SuccElt a b) (h' : SuccElt a b') : b = b'

The successor of an element is unique.

theorem DescriptiveComplexity.hTr_payload {A : Type} [FirstOrder.Language.sat.Structure A] [LinearOrder A] [Finite A] [Nonempty A] {τ τ' q a : HV A} (hτ : HTr τ) (hτ' : HTr τ') (hs : HSrc τ q) (hs' : HSrc τ' q) (hr : HRead τ a) (hr' : HRead τ' a) (ht : τ.1 = τ'.1) : τ = τ'

Equal tags force equal payloads: the source state and the symbol read pin two coordinates, the promises the rest.

The promise-exclusive alternatives

theorem DescriptiveComplexity.hTr_init_excl {A : Type} [FirstOrder.Language.sat.Structure A] [LinearOrder A] {τ τ' : HV A} (h : HTr τ) (h' : HTr τ') (hτ : τ.1 = UPTag.tInitChk) (hτ' : τ'.1 = UPTag.tInitAcc) : False

The two dispatches exclude each other.

theorem DescriptiveComplexity.hTr_next_max_excl {A : Type} [FirstOrder.Language.sat.Structure A] [LinearOrder A] {c c' cm : A} (hnext : SatNextCl c c') (hmax : SatMaxCl cm) (hc : c = cm) : False

A clause with a next one is not the last.

theorem DescriptiveComplexity.succElt_maxElt_excl {A : Type} [LinearOrder A] {r r' rm : A} (hsucc : SuccElt r r') (hmax : MaxElt rm) (hr : r = rm) : False

An element with a successor is not the greatest.

theorem DescriptiveComplexity.isInitChk_iff {t : UPTag} : isInitChk t = true ↔ t = UPTag.tInitChk

theorem DescriptiveComplexity.isInitAcc_iff {t : UPTag} : isInitAcc t = true ↔ t = UPTag.tInitAcc

theorem DescriptiveComplexity.isMarkEndNext_iff {t : UPTag} : isMarkEndNext t = true ↔ ∃ (mrk : Bool), t = UPTag.tMarkEndNext mrk

theorem DescriptiveComplexity.isMarkEndRound_iff {t : UPTag} : isMarkEndRound t = true ↔ ∃ (mrk : Bool), t = UPTag.tMarkEndRound mrk

theorem DescriptiveComplexity.isMarkEndVer_iff {t : UPTag} : isMarkEndVer t = true ↔ ∃ (mrk : Bool), t = UPTag.tMarkEndVer mrk

theorem DescriptiveComplexity.isVerNext_iff {t : UPTag} : isVerNext t = true ↔ ∃ (d : Bool), t = UPTag.tVerNext d

theorem DescriptiveComplexity.isVerAcc_iff {t : UPTag} : isVerAcc t = true ↔ ∃ (d : Bool), t = UPTag.tVerAcc d

theorem DescriptiveComplexity.hSrc_eq {A : Type} [LinearOrder A] [Finite A] [Nonempty A] {τ q : HV A} (hs : HSrc τ q) (t' : UPTag) : τ.1 = t' → match t' with | UPTag.tInitChk => q = stHInit | UPTag.tInitAcc => q = stHInit | UPTag.tChk m f => q = stHChk f (τ.2 0) (τ.2 1) | UPTag.tChkEnd f => q = stHChk f (τ.2 0) (τ.2 1) | UPTag.tMark m mrk => q = stHMark mrk (τ.2 0) (τ.2 1) | UPTag.tMarkEndNext mrk => q = stHMark mrk (τ.2 0) (τ.2 1) | UPTag.tMarkEndRound mrk => q = stHMark mrk (τ.2 0) (τ.2 2) | UPTag.tMarkEndVer mrk => q = stHMark mrk (τ.2 0) (τ.2 1) | UPTag.tVer m f d => q = stHVer f d (τ.2 0) | UPTag.tVerNext d => q = stHVer true d (τ.2 0) | UPTag.tVerAcc d => q = stHVer true d (τ.2 0) | x => False

Reading DescriptiveComplexity.HSrc off a concrete tag: the payload equations all flow through this.

theorem DescriptiveComplexity.hTr_at {A : Type} [FirstOrder.Language.sat.Structure A] [LinearOrder A] {τ : HV A} (hτ : HTr τ) (t' : UPTag) : τ.1 = t' → match t' with | UPTag.tInitChk => MinElt (τ.2 0) ∧ SatMinCl (τ.2 1) ∧ ∀ (a : A), τ.2 2 ≤ a | UPTag.tInitAcc => IsMinTup3 τ.2 ∧ ∀ (e : A), ¬SatCl e | UPTag.tChk m f => SatCl (τ.2 1) | UPTag.tChkEnd f => SatCl (τ.2 1) ∧ ∀ (a : A), τ.2 2 ≤ a | UPTag.tMark m mk => SatCl (τ.2 1) | UPTag.tMarkEndNext mk => SatNextCl (τ.2 1) (τ.2 2) | UPTag.tMarkEndRound mk => SuccElt (τ.2 0) (τ.2 1) ∧ SatMaxCl (τ.2 2) | UPTag.tMarkEndVer mk => MaxElt (τ.2 0) ∧ SatMaxCl (τ.2 1) ∧ ∀ (a : A), τ.2 2 ≤ a | UPTag.tVer m f d => SatCl (τ.2 0) ∧ ∀ (a : A), τ.2 2 ≤ a | UPTag.tVerNext d => SatNextCl (τ.2 0) (τ.2 1) ∧ ∀ (a : A), τ.2 2 ≤ a | UPTag.tVerAcc d => SatMaxCl (τ.2 0) ∧ (∀ (a : A), τ.2 1 ≤ a) ∧ (∀ (a : A), τ.2 2 ≤ a) ∧ AtMostOnePositive A | x => False

Reading DescriptiveComplexity.HTr off a concrete tag.

theorem DescriptiveComplexity.hTr_unique {A : Type} [FirstOrder.Language.sat.Structure A] [LinearOrder A] [Finite A] [Nonempty A] {τ τ' q a : HV A} (hτ : HTr τ) (hτ' : HTr τ') (hs : HSrc τ q) (hs' : HSrc τ' q) (hr : HRead τ a) (hr' : HRead τ' a) : τ = τ'

At most one transition applies, everywhere: the machine has no guess phase, so this is the whole of transition-level determinism. The three ambiguity classes left by DescriptiveComplexity.hTag_cases are separated by their promises: a clause with a next one is not the last, an element with a successor is not the greatest, and an instance either has a clause or has none.

theorem DescriptiveComplexity.hDst_functional {A : Type} [FirstOrder.Language.sat.Structure A] [LinearOrder A] [Finite A] [Nonempty A] {τ q q' : HV A} (h : HDst τ q) (h' : HDst τ q') : q = q'

A transition moves to exactly one state: the branching destinations are separated by their flags and their first-order tests, and the two relational destinations are pinned by uniqueness of the lowest clause.

theorem DescriptiveComplexity.hWrite_functional {A : Type} [FirstOrder.Language.sat.Structure A] [LinearOrder A] [Finite A] [Nonempty A] {τ a a' : HV A} (h : HWrite τ a) (h' : HWrite τ a') : a = a'

A transition writes exactly one symbol: the marking write's two branches are separated by the marking bit and the positive-literal test.

theorem DescriptiveComplexity.hornMachine_deterministic {A : Type} [FirstOrder.Language.sat.Structure A] [LinearOrder A] [Finite A] [Nonempty A] : (hornMachine A).Deterministic

The machine is deterministic – the promise DescriptiveComplexity.DTMAccept folds into its yes-instances, discharged here for every image of the reduction, Horn or not.

The positions of the tape, concretely

The dimension-3 mirror of stage 3's marker and cell lemmas: the left marker is the lowest position, cells follow in the order of their elements, the right marker closes the chain, and ranks are what the budget compares.

theorem DescriptiveComplexity.hPosn_posHStart {A : Type} [LinearOrder A] [Finite A] [Nonempty A] : HPosn posHStart

theorem DescriptiveComplexity.hPosn_posHCell {A : Type} [LinearOrder A] [Finite A] [Nonempty A] (x : A) : HPosn (posHCell x)

theorem DescriptiveComplexity.hPosn_posHEnd {A : Type} [LinearOrder A] [Finite A] [Nonempty A] : HPosn posHEnd

theorem DescriptiveComplexity.hTagTupleLe_refl {A : Type} [LinearOrder A] (p : HV A) : tagTupleLe p p

theorem DescriptiveComplexity.hTagTupleLe_of_tag_lt {A : Type} [LinearOrder A] {p q : HV A} (h : p.1 < q.1) : tagTupleLe p q

theorem DescriptiveComplexity.hTagTupleLe_tag_le {A : Type} [LinearOrder A] {p q : HV A} (h : tagTupleLe p q) : p.1 ≤ q.1

theorem DescriptiveComplexity.hpStart_lt {t : UPTag} (h : t ≠ UPTag.pStart) : UPTag.pStart < t

Every tag other than the left marker's is above it.

theorem DescriptiveComplexity.eq_posHStart_of_posn {A : Type} [LinearOrder A] [Finite A] [Nonempty A] {p : HV A} (hp : HPosn p) (h : p.1 = UPTag.pStart) : p = posHStart

There is only one left marker.

theorem DescriptiveComplexity.eq_posHEnd_of_posn {A : Type} [LinearOrder A] [Finite A] [Nonempty A] {p : HV A} (hp : HPosn p) (h : p.1 = UPTag.pEnd) : p = posHEnd

There is only one right marker.

theorem DescriptiveComplexity.eq_posHCell_of_posn {A : Type} [LinearOrder A] [Finite A] [Nonempty A] {p : HV A} (hp : HPosn p) (h : p.1 = UPTag.pCell) : p = posHCell (p.2 0)

A cell is the cell of the element it carries.

theorem DescriptiveComplexity.minPos_posHStart {A : Type} [LinearOrder A] [Finite A] [Nonempty A] : MinPos tagTupleLe HPosn posHStart

The left marker is the lowest position.

theorem DescriptiveComplexity.posHStart_le_posHCell {A : Type} [LinearOrder A] [Finite A] [Nonempty A] (x : A) : tagTupleLe posHStart (posHCell x)

theorem DescriptiveComplexity.posHCell_le_posHEnd {A : Type} [LinearOrder A] [Finite A] [Nonempty A] (x : A) : tagTupleLe (posHCell x) posHEnd

theorem DescriptiveComplexity.posHStart_le_posHEnd {A : Type} [LinearOrder A] [Finite A] [Nonempty A] : tagTupleLe posHStart posHEnd

theorem DescriptiveComplexity.posHCell_le_iff {A : Type} [LinearOrder A] [Finite A] [Nonempty A] {x y : A} : tagTupleLe (posHCell x) (posHCell y) ↔ x ≤ y

Cells are ordered as their elements are.

theorem DescriptiveComplexity.htag_le_pCell {t : UPTag} (h : t ≤ UPTag.pCell) : t = UPTag.pStart ∨ t = UPTag.pCell

Only the two lowest tags are at or below a cell's.

theorem DescriptiveComplexity.htag_le_pEnd {t : UPTag} (h : t ≤ UPTag.pEnd) : t = UPTag.pStart ∨ t = UPTag.pCell ∨ t = UPTag.pEnd

Only the three bracketing tags are at or below the right marker's.

theorem DescriptiveComplexity.htag_between {t : UPTag} (h₁ : UPTag.pCell ≤ t) (h₂ : t ≤ UPTag.pEnd) : t = UPTag.pCell ∨ t = UPTag.pEnd

Only the two highest bracketing tags lie between a cell's and the right marker's.

theorem DescriptiveComplexity.succPos_posHStart_posHCell {A : Type} [LinearOrder A] [Finite A] [Nonempty A] : SuccPos tagTupleLe HPosn posHStart (posHCell botA)

The head's first move: the cell of the least element follows ⊢.

theorem DescriptiveComplexity.succPos_posHCell_posHCell {A : Type} [LinearOrder A] [Finite A] [Nonempty A] {x x' : A} (hsucc : SuccElt x x') : SuccPos tagTupleLe HPosn (posHCell x) (posHCell x')

The head moves from cell to cell along the instance.

theorem DescriptiveComplexity.succPos_posHCell_posHEnd {A : Type} [LinearOrder A] [Finite A] [Nonempty A] : SuccPos tagTupleLe HPosn (posHCell topA) posHEnd

The head's last move of a sweep: ⊣ follows the last cell.

The intended run: marks and tapes

The machine's working state is a set of marked elements, as a Bool-valued assignment. Processing one clause – a check sweep and a return sweep – applies DescriptiveComplexity.procB to it: unconditionally, because when the check fails the inner conjunction is false and nothing is added, exactly as the machine's return sweep writes nothing when its marking bit is off.

noncomputable def DescriptiveComplexity.procB {A : Type} [FirstOrder.Language.sat.Structure A] (M : A → Bool) (c : A) : A → Bool

One clause processed on a marked set: if every negative literal of c is marked, its positive literals join the marks.

Equations

• DescriptiveComplexity.procB M c x = (M x || decide (DescriptiveComplexity.SatPos c x) && decide (∀ (y : A), DescriptiveComplexity.SatNeg c y → M y = true))

theorem DescriptiveComplexity.le_procB {A : Type} [FirstOrder.Language.sat.Structure A] (M : A → Bool) (c : A) {x : A} (h : M x = true) : procB M c x = true

Processing a clause only adds marks.

noncomputable def DescriptiveComplexity.hTape {A : Type} [LinearOrder A] [Finite A] [Nonempty A] (M : A → Bool) : HV A → HV A

The tape carrying the marked set M: markers and blanks in place, the cell of y holding (y, M y). A junk cell tuple reads its initial, unmarked symbol forever – it is never written, so its value must not depend on M.

Equations

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

theorem DescriptiveComplexity.hTape_posHStart {A : Type} [LinearOrder A] [Finite A] [Nonempty A] (M : A → Bool) : hTape M posHStart = symHStart

The markers hold their symbols on every marked tape.

theorem DescriptiveComplexity.hTape_posHEnd {A : Type} [LinearOrder A] [Finite A] [Nonempty A] (M : A → Bool) : hTape M posHEnd = symHEnd

theorem DescriptiveComplexity.hTape_posHCell {A : Type} [LinearOrder A] [Finite A] [Nonempty A] (M : A → Bool) (y : A) : hTape M (posHCell y) = symCell (M y) y

A real cell reads its element's mark.

theorem DescriptiveComplexity.hTape_congr {A : Type} [LinearOrder A] [Finite A] [Nonempty A] {M M' : A → Bool} (p : HV A) (h : ∀ (y : A), M y = M' y) : hTape M p = hTape M' p

Marked tapes agree wherever the marks do – in particular junk cells never notice a change of marks.

noncomputable def DescriptiveComplexity.markTape {A : Type} [FirstOrder.Language.sat.Structure A] [LinearOrder A] [Finite A] [Nonempty A] (M : A → Bool) (c : A) (p : HV A) : HV A → HV A

The tape during a return sweep of the clause c with the head at p, moving left: the cells strictly above the head have been processed, the rest still carry the old marks.

Equations

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

theorem DescriptiveComplexity.markTape_posHStart {A : Type} [FirstOrder.Language.sat.Structure A] [LinearOrder A] [Finite A] [Nonempty A] (M : A → Bool) (c : A) (p : HV A) : markTape M c p posHStart = symHStart

theorem DescriptiveComplexity.markTape_posHEnd {A : Type} [FirstOrder.Language.sat.Structure A] [LinearOrder A] [Finite A] [Nonempty A] (M : A → Bool) (c : A) (p : HV A) : markTape M c p posHEnd = symHEnd

The intended run: configurations

noncomputable def DescriptiveComplexity.chkFlag {A : Type} [FirstOrder.Language.sat.Structure A] [LinearOrder A] [Finite A] [Nonempty A] (M : A → Bool) (c : A) (p : HV A) : Bool

The flag of a check sweep with the head at p: every negative literal of c strictly below the head is marked.

Equations

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

noncomputable def DescriptiveComplexity.confHChk {A : Type} [FirstOrder.Language.sat.Structure A] [LinearOrder A] [Finite A] [Nonempty A] (M : A → Bool) (r c : A) (p : HV A) : Config (HV A)

The configuration during the check sweep of clause c in round r.

Equations

• DescriptiveComplexity.confHChk M r c p = { state := DescriptiveComplexity.stHChk (DescriptiveComplexity.chkFlag M c p) r c, head := p, tape := DescriptiveComplexity.hTape M }

noncomputable def DescriptiveComplexity.confHMark {A : Type} [FirstOrder.Language.sat.Structure A] [LinearOrder A] [Finite A] [Nonempty A] (M : A → Bool) (m : Bool) (r c : A) (p : HV A) : Config (HV A)

The configuration during the return sweep of clause c in round r, with marking bit m.

Equations

• DescriptiveComplexity.confHMark M m r c p = { state := DescriptiveComplexity.stHMark m r c, head := p, tape := DescriptiveComplexity.markTape M c p }

noncomputable def DescriptiveComplexity.verFlagL {A : Type} [FirstOrder.Language.sat.Structure A] [LinearOrder A] [Finite A] [Nonempty A] (M : A → Bool) (c : A) (p : HV A) : Bool

The flag of a verification sweep, leftwards, with the head at p: some cell strictly above the head satisfies c under the marks – stage 3's DescriptiveComplexity.chkFlagL with the marks as valuation.

Equations

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

noncomputable def DescriptiveComplexity.verFlagR {A : Type} [FirstOrder.Language.sat.Structure A] [LinearOrder A] [Finite A] [Nonempty A] (M : A → Bool) (c : A) (p : HV A) : Bool

The flag of a verification sweep, rightwards.

Equations

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

noncomputable def DescriptiveComplexity.confHVerL {A : Type} [FirstOrder.Language.sat.Structure A] [LinearOrder A] [Finite A] [Nonempty A] (M : A → Bool) (c : A) (p : HV A) : Config (HV A)

The configuration during a leftward verification sweep.

Equations

• DescriptiveComplexity.confHVerL M c p = { state := DescriptiveComplexity.stHVer (DescriptiveComplexity.verFlagL M c p) false c, head := p, tape := DescriptiveComplexity.hTape M }

noncomputable def DescriptiveComplexity.confHVerR {A : Type} [FirstOrder.Language.sat.Structure A] [LinearOrder A] [Finite A] [Nonempty A] (M : A → Bool) (c : A) (p : HV A) : Config (HV A)

The configuration during a rightward verification sweep.

Equations

• DescriptiveComplexity.confHVerR M c p = { state := DescriptiveComplexity.stHVer (DescriptiveComplexity.verFlagR M c p) true c, head := p, tape := DescriptiveComplexity.hTape M }

noncomputable def DescriptiveComplexity.confHInit {A : Type} [LinearOrder A] [Finite A] [Nonempty A] : Config (HV A)

The initial configuration: the dispatch state at the left marker, all cells unmarked.

Equations

• DescriptiveComplexity.confHInit = { state := DescriptiveComplexity.stHInit, head := DescriptiveComplexity.posHStart, tape := DescriptiveComplexity.hTape fun (x : A) => false }

theorem DescriptiveComplexity.isInit_confHInit {A : Type} [FirstOrder.Language.sat.Structure A] [LinearOrder A] [Finite A] [Nonempty A] : (hornMachine A).IsInit confHInit

The machine starts at the dispatch configuration: the unmarked tape is the initial tape.

The flags and tapes along a sweep

theorem DescriptiveComplexity.chkFlag_botA {A : Type} [FirstOrder.Language.sat.Structure A] [LinearOrder A] [Finite A] [Nonempty A] (M : A → Bool) (c : A) : chkFlag M c (posHCell botA) = true

A check sweep starts with a vacuously true flag: no cell lies strictly below the first one.

theorem DescriptiveComplexity.chkFlag_succ {A : Type} [FirstOrder.Language.sat.Structure A] [LinearOrder A] [Finite A] [Nonempty A] (M : A → Bool) (c : A) {p q : HV A} (hsucc : SuccPos tagTupleLe HPosn p q) (hp : p.1 = UPTag.pCell) : chkFlag M c q = true ↔ chkFlag M c p = true ∧ (SatNeg c (p.2 0) → M (p.2 0) = true)

Stepping right folds one cell into the check flag.

theorem DescriptiveComplexity.chkFlag_posHEnd {A : Type} [FirstOrder.Language.sat.Structure A] [LinearOrder A] [Finite A] [Nonempty A] (M : A → Bool) (c : A) : chkFlag M c posHEnd = true ↔ ∀ (y : A), SatNeg c y → M y = true

A completed check sweep has seen every cell: at the right marker the flag says every negative literal of the clause is marked.

theorem DescriptiveComplexity.verFlagL_topA {A : Type} [FirstOrder.Language.sat.Structure A] [LinearOrder A] [Finite A] [Nonempty A] (M : A → Bool) (c : A) : verFlagL M c (posHCell topA) = false

A leftward verification sweep starts with an empty flag.

theorem DescriptiveComplexity.verFlagR_botA {A : Type} [FirstOrder.Language.sat.Structure A] [LinearOrder A] [Finite A] [Nonempty A] (M : A → Bool) (c : A) : verFlagR M c (posHCell botA) = false

A rightward verification sweep starts with an empty flag.

theorem DescriptiveComplexity.verFlagL_succ {A : Type} [FirstOrder.Language.sat.Structure A] [LinearOrder A] [Finite A] [Nonempty A] (M : A → Bool) (c : A) {p q : HV A} (hsucc : SuccPos tagTupleLe HPosn p q) (hq : q.1 = UPTag.pCell) : verFlagL M c p = true ↔ verFlagL M c q = true ∨ MLit c (q.2 0) (M (q.2 0))

Stepping down folds one cell into the leftward verification flag.

theorem DescriptiveComplexity.verFlagR_succ {A : Type} [FirstOrder.Language.sat.Structure A] [LinearOrder A] [Finite A] [Nonempty A] (M : A → Bool) (c : A) {p q : HV A} (hsucc : SuccPos tagTupleLe HPosn p q) (hp : p.1 = UPTag.pCell) : verFlagR M c q = true ↔ verFlagR M c p = true ∨ MLit c (p.2 0) (M (p.2 0))

Stepping up folds one cell into the rightward verification flag.

theorem DescriptiveComplexity.verFlagL_posHStart {A : Type} [FirstOrder.Language.sat.Structure A] [LinearOrder A] [Finite A] [Nonempty A] (M : A → Bool) (c : A) : verFlagL M c posHStart = true ↔ ∃ (y : A), MLit c y (M y)

A completed leftward verification sweep has seen every cell.

theorem DescriptiveComplexity.verFlagR_posHEnd {A : Type} [FirstOrder.Language.sat.Structure A] [LinearOrder A] [Finite A] [Nonempty A] (M : A → Bool) (c : A) : verFlagR M c posHEnd = true ↔ ∃ (y : A), MLit c y (M y)

A completed rightward verification sweep has seen every cell.

theorem DescriptiveComplexity.markTape_topA {A : Type} [FirstOrder.Language.sat.Structure A] [LinearOrder A] [Finite A] [Nonempty A] (M : A → Bool) (c : A) (r : HV A) : markTape M c (posHCell topA) r = hTape M r

At the top of the return sweep nothing has been processed: the tape still carries the old marks.

theorem DescriptiveComplexity.markTape_posHStart_eq {A : Type} [FirstOrder.Language.sat.Structure A] [LinearOrder A] [Finite A] [Nonempty A] (M : A → Bool) (c : A) (r : HV A) : markTape M c posHStart r = hTape (procB M c) r

At the bottom of the return sweep everything has been processed: the tape carries the new marks.

theorem DescriptiveComplexity.markTape_frame' {A : Type} [FirstOrder.Language.sat.Structure A] [LinearOrder A] [Finite A] [Nonempty A] (M : A → Bool) (c : A) {p q r : HV A} (hsucc : SuccPos tagTupleLe HPosn q p) (hrne : r ≠ p) : markTape M c q r = markTape M c p r

The return sweep only ever changes the cell under the head, exactly as stage 3's guess sweep: moving the head down brings its own cell into the processed region and nothing else.

theorem DescriptiveComplexity.markTape_at_head {A : Type} [FirstOrder.Language.sat.Structure A] [LinearOrder A] [Finite A] [Nonempty A] (M : A → Bool) (c : A) {p : HV A} (hp : HPosn p) (hcell : p.1 = UPTag.pCell) : markTape M c p p = symCell (M (p.2 0)) (p.2 0)

What the return sweep reads at its own head: the old mark.

The intended run: single steps

theorem DescriptiveComplexity.step_hInitChk {A : Type} [FirstOrder.Language.sat.Structure A] [LinearOrder A] [Finite A] [Nonempty A] {c₀ : A} (hc₀ : SatMinCl c₀) : (hornMachine A).Step confHInit (confHChk (fun (x : A) => false) botA c₀ (posHCell botA))

The dispatch, when a clause exists: into the first check sweep of the lowest round and clause, with everything unmarked.

theorem DescriptiveComplexity.step_hInitAcc {A : Type} [FirstOrder.Language.sat.Structure A] [LinearOrder A] [Finite A] [Nonempty A] (hno : ∀ (e : A), ¬SatCl e) : (hornMachine A).Step confHInit { state := stHAcc, head := posHCell botA, tape := hTape fun (x : A) => false }

The dispatch, when there is no clause at all: accept.

theorem DescriptiveComplexity.step_hChk {A : Type} [FirstOrder.Language.sat.Structure A] [LinearOrder A] [Finite A] [Nonempty A] (M : A → Bool) {r c : A} (hc : SatCl c) {p q : HV A} (hsucc : SuccPos tagTupleLe HPosn p q) (hp : p.1 = UPTag.pCell) : (hornMachine A).Step (confHChk M r c p) (confHChk M r c q)

One step of a check sweep: fold the cell under the head into the flag and move right.

theorem DescriptiveComplexity.step_hChkEnd {A : Type} [FirstOrder.Language.sat.Structure A] [LinearOrder A] [Finite A] [Nonempty A] (M : A → Bool) {r c : A} (hc : SatCl c) : (hornMachine A).Step (confHChk M r c posHEnd) (confHMark M (chkFlag M c posHEnd) r c (posHCell topA))

The turn at the right marker: the check sweep is over, the return sweep begins with the accumulated verdict as its marking bit.

theorem DescriptiveComplexity.step_hMark {A : Type} [FirstOrder.Language.sat.Structure A] [LinearOrder A] [Finite A] [Nonempty A] (M : A → Bool) {m : Bool} {r c : A} (hc : SatCl c) (hm : m = true ↔ ∀ (y : A), SatNeg c y → M y = true) {p q : HV A} (hsucc : SuccPos tagTupleLe HPosn q p) (hp : p.1 = UPTag.pCell) : (hornMachine A).Step (confHMark M m r c p) (confHMark M m r c q)

One step of a return sweep: process the cell under the head – marking it if it is the positive literal of a successfully checked clause – and move left.

theorem DescriptiveComplexity.step_hMarkEndNext {A : Type} [FirstOrder.Language.sat.Structure A] [LinearOrder A] [Finite A] [Nonempty A] (M : A → Bool) {m : Bool} {r c c' : A} (hnext : SatNextCl c c') : (hornMachine A).Step (confHMark M m r c posHStart) (confHChk (procB M c) r c' (posHCell botA))

The turn at the left marker, next clause: the processed marks become the working marks, and the next check sweep starts.

theorem DescriptiveComplexity.step_hMarkEndRound {A : Type} [FirstOrder.Language.sat.Structure A] [LinearOrder A] [Finite A] [Nonempty A] (M : A → Bool) {m : Bool} {r r' c c₀ : A} (hsucc : SuccElt r r') (hmax : SatMaxCl c) (hmin : SatMinCl c₀) : (hornMachine A).Step (confHMark M m r c posHStart) (confHChk (procB M c) r' c₀ (posHCell botA))

The turn at the left marker, next round: last clause processed, the round counter advances and the checks restart at the lowest clause.

theorem DescriptiveComplexity.step_hMarkEndVer {A : Type} [FirstOrder.Language.sat.Structure A] [LinearOrder A] [Finite A] [Nonempty A] (M : A → Bool) {m : Bool} {r c c₀ : A} (hmaxr : MaxElt r) (hmax : SatMaxCl c) (hmin : SatMinCl c₀) : (hornMachine A).Step (confHMark M m r c posHStart) (confHVerR (procB M c) c₀ (posHCell botA))

The turn at the left marker, into verification: the last clause of the last round is processed, and the final marks are verified clause by clause, starting rightwards at the lowest clause.

theorem DescriptiveComplexity.step_hVerR {A : Type} [FirstOrder.Language.sat.Structure A] [LinearOrder A] [Finite A] [Nonempty A] (M : A → Bool) {c : A} (hc : SatCl c) {p q : HV A} (hsucc : SuccPos tagTupleLe HPosn p q) (hp : p.1 = UPTag.pCell) : (hornMachine A).Step (confHVerR M c p) (confHVerR M c q)

One step of a rightward verification sweep.

theorem DescriptiveComplexity.step_hVerL {A : Type} [FirstOrder.Language.sat.Structure A] [LinearOrder A] [Finite A] [Nonempty A] (M : A → Bool) {c : A} (hc : SatCl c) {p q : HV A} (hsucc : SuccPos tagTupleLe HPosn p q) (hq : q.1 = UPTag.pCell) : (hornMachine A).Step (confHVerL M c q) (confHVerL M c p)

One step of a leftward verification sweep.

theorem DescriptiveComplexity.step_hVerNextR {A : Type} [FirstOrder.Language.sat.Structure A] [LinearOrder A] [Finite A] [Nonempty A] (M : A → Bool) {c c' : A} (hnext : SatNextCl c c') (hflag : verFlagR M c posHEnd = true) : (hornMachine A).Step (confHVerR M c posHEnd) (confHVerL M c' (posHCell topA))

The verification turn at the right marker, another clause following: reverse into a leftward sweep of the next clause.

theorem DescriptiveComplexity.step_hVerNextL {A : Type} [FirstOrder.Language.sat.Structure A] [LinearOrder A] [Finite A] [Nonempty A] (M : A → Bool) {c c' : A} (hnext : SatNextCl c c') (hflag : verFlagL M c posHStart = true) : (hornMachine A).Step (confHVerL M c posHStart) (confHVerR M c' (posHCell botA))

The verification turn at the left marker – the mirror.

theorem DescriptiveComplexity.step_hVerAccR {A : Type} [FirstOrder.Language.sat.Structure A] [LinearOrder A] [Finite A] [Nonempty A] (M : A → Bool) {c : A} (hmax : SatMaxCl c) (hhorn : AtMostOnePositive A) (hflag : verFlagR M c posHEnd = true) : (hornMachine A).Step (confHVerR M c posHEnd) { state := stHAcc, head := posHCell topA, tape := hTape M }

Accepting at the right marker: the last clause is verified, and the instance is Horn – the gate.

theorem DescriptiveComplexity.step_hVerAccL {A : Type} [FirstOrder.Language.sat.Structure A] [LinearOrder A] [Finite A] [Nonempty A] (M : A → Bool) {c : A} (hmax : SatMaxCl c) (hhorn : AtMostOnePositive A) (hflag : verFlagL M c posHStart = true) : (hornMachine A).Step (confHVerL M c posHStart) { state := stHAcc, head := posHCell botA, tape := hTape M }

Accepting at the left marker – the mirror.

Ranks, sweeps, and one whole clause

theorem DescriptiveComplexity.bitRank_posHStart {A : Type} [LinearOrder A] [Finite A] [Nonempty A] : bitRank tagTupleLe HPosn posHStart = 0

The left marker has rank 0.

theorem DescriptiveComplexity.bitRank_posHEnd_eq {A : Type} [LinearOrder A] [Finite A] [Nonempty A] : bitRank tagTupleLe HPosn posHEnd = bitRank tagTupleLe HPosn (posHCell topA) + 1

The right marker sits one step above the last cell.

theorem DescriptiveComplexity.bitRank_posHCell_botA {A : Type} [LinearOrder A] [Finite A] [Nonempty A] : bitRank tagTupleLe HPosn (posHCell botA) = 1

The first cell has rank 1.

theorem DescriptiveComplexity.bitRank_posHEnd_le {A : Type} [LinearOrder A] [Finite A] [Nonempty A] : bitRank tagTupleLe HPosn posHEnd ≤ Nat.card A + 1

A sweep is short: only the left marker and the cells lie below the right marker, by injection into Option A.

theorem DescriptiveComplexity.steps_hChkAll {A : Type} [FirstOrder.Language.sat.Structure A] [LinearOrder A] [Finite A] [Nonempty A] (M : A → Bool) {r c : A} (hc : SatCl c) : (hornMachine A).StepsIn (bitRank tagTupleLe HPosn posHEnd - bitRank tagTupleLe HPosn (posHCell botA)) (confHChk M r c (posHCell botA)) (confHChk M r c posHEnd)

A whole check sweep, from the first cell to the right marker.

theorem DescriptiveComplexity.steps_hMarkAll {A : Type} [FirstOrder.Language.sat.Structure A] [LinearOrder A] [Finite A] [Nonempty A] (M : A → Bool) {m : Bool} {r c : A} (hc : SatCl c) (hm : m = true ↔ ∀ (y : A), SatNeg c y → M y = true) : (hornMachine A).StepsIn (bitRank tagTupleLe HPosn (posHCell topA) - bitRank tagTupleLe HPosn posHStart) (confHMark M m r c (posHCell topA)) (confHMark M m r c posHStart)

A whole return sweep, from the last cell down to the left marker.

theorem DescriptiveComplexity.steps_hVerRAll {A : Type} [FirstOrder.Language.sat.Structure A] [LinearOrder A] [Finite A] [Nonempty A] (M : A → Bool) {c : A} (hc : SatCl c) : (hornMachine A).StepsIn (bitRank tagTupleLe HPosn posHEnd - bitRank tagTupleLe HPosn (posHCell botA)) (confHVerR M c (posHCell botA)) (confHVerR M c posHEnd)

A whole rightward verification sweep.

theorem DescriptiveComplexity.steps_hVerLAll {A : Type} [FirstOrder.Language.sat.Structure A] [LinearOrder A] [Finite A] [Nonempty A] (M : A → Bool) {c : A} (hc : SatCl c) : (hornMachine A).StepsIn (bitRank tagTupleLe HPosn (posHCell topA) - bitRank tagTupleLe HPosn posHStart) (confHVerL M c (posHCell topA)) (confHVerL M c posHStart)

A whole leftward verification sweep.

theorem DescriptiveComplexity.steps_hOneClause {A : Type} [FirstOrder.Language.sat.Structure A] [LinearOrder A] [Finite A] [Nonempty A] (M : A → Bool) {r c : A} (hc : SatCl c) : ∃ k ≤ 2 * bitRank tagTupleLe HPosn posHEnd, (hornMachine A).StepsIn k (confHChk M r c (posHCell botA)) (confHMark M (chkFlag M c posHEnd) r c posHStart)

One whole clause: check sweep, turn, return sweep, back at the left marker with the processed marks, in exactly 2 R steps for R the right marker's rank.

The folds: what the rounds compute

inductive DescriptiveComplexity.ClauseFold {A : Type} [FirstOrder.Language.sat.Structure A] [LinearOrder A] : A → (A → Bool) → (A → Bool) → Prop

Processing the clauses from c to the last one, relationally: the marked set each clause leaves behind.

• last {A : Type} [FirstOrder.Language.sat.Structure A] [LinearOrder A] {c : A} {M : A → Bool} : SatMaxCl c → ClauseFold c M (procB M c)
• step {A : Type} [FirstOrder.Language.sat.Structure A] [LinearOrder A] {c c' : A} {M M' : A → Bool} : SatNextCl c c' → ClauseFold c' (procB M c) M' → ClauseFold c M M'

inductive DescriptiveComplexity.RoundFold {A : Type} [FirstOrder.Language.sat.Structure A] [LinearOrder A] (c₀ : A) : A → (A → Bool) → (A → Bool) → Prop

Processing the rounds from r to the last one, each a pass over all the clauses from c₀.

• last {A : Type} [FirstOrder.Language.sat.Structure A] [LinearOrder A] {c₀ r : A} {M M' : A → Bool} : MaxElt r → ClauseFold c₀ M M' → RoundFold c₀ r M M'
• step {A : Type} [FirstOrder.Language.sat.Structure A] [LinearOrder A] {c₀ r r' : A} {M M' M'' : A → Bool} : SuccElt r r' → ClauseFold c₀ M M' → RoundFold c₀ r' M' M'' → RoundFold c₀ r M M''

theorem DescriptiveComplexity.ClauseFold.mono {A : Type} [FirstOrder.Language.sat.Structure A] [LinearOrder A] {c : A} {M M' : A → Bool} (h : ClauseFold c M M') {x : A} (hx : M x = true) : M' x = true

The clause fold only adds marks.

theorem DescriptiveComplexity.RoundFold.mono {A : Type} [FirstOrder.Language.sat.Structure A] [LinearOrder A] {c₀ r : A} {M M' : A → Bool} (h : RoundFold c₀ r M M') {x : A} (hx : M x = true) : M' x = true

The round fold only adds marks.

theorem DescriptiveComplexity.ClauseFold.subset_forced {A : Type} [FirstOrder.Language.sat.Structure A] [LinearOrder A] [Finite A] {c : A} {M M' : A → Bool} (h : ClauseFold c M M') (hM : ∀ (x : A), M x = true → Forced x) (x : A) : M' x = true → Forced x

Soundness of the fold: marks stay inside the propagation closure.

theorem DescriptiveComplexity.RoundFold.subset_forced {A : Type} [FirstOrder.Language.sat.Structure A] [LinearOrder A] [Finite A] {c₀ r : A} {M M' : A → Bool} (h : RoundFold c₀ r M M') (hM : ∀ (x : A), M x = true → Forced x) (x : A) : M' x = true → Forced x

Soundness for the rounds.

theorem DescriptiveComplexity.ClauseFold.dominates {A : Type} [FirstOrder.Language.sat.Structure A] [LinearOrder A] {c₀ : A} {M M' : A → Bool} (h : ClauseFold c₀ M M') {c x : A} (hc : SatCl c) (hpos : SatPos c x) : c₀ ≤ c → (∀ (y : A), SatNeg c y → M y = true) → M' x = true

One round dominates one propagation step: a clause whose negative literals are all marked at the start of the round has its positive literals marked at its end – the marks only grow until the clause's turn comes.

theorem DescriptiveComplexity.RoundFold.forcedIn_subset {A : Type} [FirstOrder.Language.sat.Structure A] [LinearOrder A] [Finite A] {c₀ : A} (hmin : SatMinCl c₀) {r : A} {M M' : A → Bool} (h : RoundFold c₀ r M M') (j : ℕ) : (∀ (y : A), ForcedIn j y → M y = true) → ∀ (x : A), ForcedIn (j + {e : A | r ≤ e}.ncard) x → M' x = true

The rounds reach every propagation stage: seed marks containing stage j become, after the remaining rounds, marks containing stage j + #rounds. Each round dominates one step because its marks only grow.

The machine walks the folds

theorem DescriptiveComplexity.exists_succElt {A : Type} [LinearOrder A] [Finite A] {r : A} (hnmax : ¬MaxElt r) : ∃ (r' : A), SuccElt r r'

Every element that is not the greatest has a successor.

theorem DescriptiveComplexity.ncard_ge_succElt {A : Type} [LinearOrder A] [Finite A] {r r' : A} (hsucc : SuccElt r r') : {e : A | r ≤ e}.ncard = {e : A | r' ≤ e}.ncard + 1

Passing to the next round removes exactly one round from those left.

theorem DescriptiveComplexity.steps_hClauses {A : Type} [FirstOrder.Language.sat.Structure A] [LinearOrder A] [Finite A] [Nonempty A] {c₀ : A} (hmin : SatMinCl c₀) (r c : A) : SatCl c → ∀ (M : A → Bool), ∃ (M' : A → Bool), ClauseFold c M M' ∧ (∀ (r' : A), SuccElt r r' → ∃ k ≤ {e : A | SatCl e ∧ c ≤ e}.ncard * (2 * bitRank tagTupleLe HPosn posHEnd + 1), (hornMachine A).StepsIn k (confHChk M r c (posHCell botA)) (confHChk M' r' c₀ (posHCell botA))) ∧ (MaxElt r → ∃ k ≤ {e : A | SatCl e ∧ c ≤ e}.ncard * (2 * bitRank tagTupleLe HPosn posHEnd + 1), (hornMachine A).StepsIn k (confHChk M r c (posHCell botA)) (confHVerR M' c₀ (posHCell botA)))

The machine processes the clauses from c to the last one: it computes the clause fold, and then turns – to the next round if one follows, into verification otherwise – in at most 2R + 1 steps per clause.

theorem DescriptiveComplexity.steps_hRounds {A : Type} [FirstOrder.Language.sat.Structure A] [LinearOrder A] [Finite A] [Nonempty A] {c₀ : A} (hmin : SatMinCl c₀) (r : A) (M : A → Bool) : ∃ (M' : A → Bool), RoundFold c₀ r M M' ∧ ∃ k ≤ {e : A | r ≤ e}.ncard * ({e : A | SatCl e ∧ c₀ ≤ e}.ncard * (2 * bitRank tagTupleLe HPosn posHEnd + 1)), (hornMachine A).StepsIn k (confHChk M r c₀ (posHCell botA)) (confHVerR M' c₀ (posHCell botA))

The machine runs all the rounds: from any round to the start of the verification phase, computing the round fold.

The verification phase

theorem DescriptiveComplexity.steps_hVerClauseR {A : Type} [FirstOrder.Language.sat.Structure A] [LinearOrder A] [Finite A] [Nonempty A] (M : A → Bool) {c c' : A} (hc : SatCl c) (hnext : SatNextCl c c') (hsat : ∃ (y : A), MLit c y (M y)) : ∃ k ≤ bitRank tagTupleLe HPosn posHEnd, (hornMachine A).StepsIn k (confHVerR M c (posHCell botA)) (confHVerL M c' (posHCell topA))

Verifying c rightwards and moving on to the next clause.

theorem DescriptiveComplexity.steps_hVerClauseL {A : Type} [FirstOrder.Language.sat.Structure A] [LinearOrder A] [Finite A] [Nonempty A] (M : A → Bool) {c c' : A} (hc : SatCl c) (hnext : SatNextCl c c') (hsat : ∃ (y : A), MLit c y (M y)) : ∃ k ≤ bitRank tagTupleLe HPosn posHEnd, (hornMachine A).StepsIn k (confHVerL M c (posHCell topA)) (confHVerR M c' (posHCell botA))

Verifying c leftwards and moving on to the next clause.

theorem DescriptiveComplexity.steps_hVerClauseAccR {A : Type} [FirstOrder.Language.sat.Structure A] [LinearOrder A] [Finite A] [Nonempty A] (M : A → Bool) {c : A} (hc : SatCl c) (hmax : SatMaxCl c) (hhorn : AtMostOnePositive A) (hsat : ∃ (y : A), MLit c y (M y)) : ∃ k ≤ bitRank tagTupleLe HPosn posHEnd, ∃ (cfin : Config (HV A)), (hornMachine A).StepsIn k (confHVerR M c (posHCell botA)) cfin ∧ HAcc cfin.state

Verifying the last clause rightwards, and accepting.

theorem DescriptiveComplexity.steps_hVerClauseAccL {A : Type} [FirstOrder.Language.sat.Structure A] [LinearOrder A] [Finite A] [Nonempty A] (M : A → Bool) {c : A} (hc : SatCl c) (hmax : SatMaxCl c) (hhorn : AtMostOnePositive A) (hsat : ∃ (y : A), MLit c y (M y)) : ∃ k ≤ bitRank tagTupleLe HPosn posHEnd, ∃ (cfin : Config (HV A)), (hornMachine A).StepsIn k (confHVerL M c (posHCell topA)) cfin ∧ HAcc cfin.state

Verifying the last clause leftwards, and accepting.

theorem DescriptiveComplexity.hVer_accepts {A : Type} [FirstOrder.Language.sat.Structure A] [LinearOrder A] [Finite A] [Nonempty A] (M : A → Bool) (hhorn : AtMostOnePositive A) (hsat : ∀ (e : A), SatCl e → ∃ (y : A), MLit e y (M y)) (c : A) : SatCl c → (∃ (n : ℕ) (cfin : Config (HV A)), n ≤ {e : A | SatCl e ∧ c ≤ e}.ncard * bitRank tagTupleLe HPosn posHEnd ∧ (hornMachine A).StepsIn n (confHVerR M c (posHCell botA)) cfin ∧ HAcc cfin.state) ∧ ∃ (n : ℕ) (cfin : Config (HV A)), n ≤ {e : A | SatCl e ∧ c ≤ e}.ncard * bitRank tagTupleLe HPosn posHEnd ∧ (hornMachine A).StepsIn n (confHVerL M c (posHCell topA)) cfin ∧ HAcc cfin.state

The verification phase accepts: every remaining clause is satisfied by the marks, so the sweeps run through and the machine accepts after the last one – stage 3's clause induction, verbatim, with the marks as valuation.

The machine accepts every Horn-satisfiable instance

theorem DescriptiveComplexity.roundFold_marks_eq_forced {A : Type} [FirstOrder.Language.sat.Structure A] [LinearOrder A] [Finite A] [Nonempty A] {c₀ : A} (hmin : SatMinCl c₀) {M' : A → Bool} (h : RoundFold c₀ botA (fun (x : A) => false) M') (x : A) : M' x = true ↔ Forced x

The final marks are exactly the propagation closure.

theorem DescriptiveComplexity.hornMachine_accepts_of {A : Type} [FirstOrder.Language.sat.Structure A] [LinearOrder A] [Finite A] [Nonempty A] (hhorn : AtMostOnePositive A) (hsat : Satisfiable A) : (hornMachine A).Accepts

The machine accepts every yes-instance of HORN-SAT, within the budget: dispatch, n rounds of propagation, and a verification pass that the closure – which satisfiability makes a model – lets run to acceptance.

The machine accepts only Horn-satisfiable instances

Determinism replaces stage 3's run-analysis induction: the run from the unique initial configuration is the intended trajectory, so it suffices that on a non-Horn-satisfiable instance the trajectory never carries an accepting state – either because no accept transition exists at all (the Horn gate), or because the trajectory gets stuck at the first failing verification sweep.

theorem DescriptiveComplexity.hTag_no_stateTag_qAcc (t : UPTag) : isHTrTag t = true → hStateTag t ≠ UPTag.qAcc

No transition applies in an accepting state: once accepted, the machine halts, so an accepting run cannot be a strict prefix of another.

theorem DescriptiveComplexity.hTag_verFalse_no_marker (t : UPTag) (d : Bool) : isHTrTag t = true → hStateTag t = UPTag.qVer false d → hReadTag t ≠ UPTag.sStart ∧ hReadTag t ≠ UPTag.sEnd

No transition applies in a failed verification state on a marker: the run dies there.

theorem DescriptiveComplexity.hDst_acc_cases {A : Type} [FirstOrder.Language.sat.Structure A] [LinearOrder A] [Finite A] [Nonempty A] {τ q : HV A} (hd : HDst τ q) (hq : q.1 = UPTag.qAcc) : τ.1 = UPTag.tInitAcc ∨ ∃ (d : Bool), τ.1 = UPTag.tVerAcc d

The only transitions into an accepting state are the two accept transitions.

theorem DescriptiveComplexity.no_step_verR_false {A : Type} [FirstOrder.Language.sat.Structure A] [LinearOrder A] [Finite A] [Nonempty A] (M : A → Bool) {c : A} (hflag : verFlagR M c posHEnd = false) (d : Config (HV A)) : ¬(hornMachine A).Step (confHVerR M c posHEnd) d

A failed rightward verification sweep is stuck at the right marker.

theorem DescriptiveComplexity.no_step_verL_false {A : Type} [FirstOrder.Language.sat.Structure A] [LinearOrder A] [Finite A] [Nonempty A] (M : A → Bool) {c : A} (hflag : verFlagL M c posHStart = false) (d : Config (HV A)) : ¬(hornMachine A).Step (confHVerL M c posHStart) d

A failed leftward verification sweep is stuck at the left marker.

theorem DescriptiveComplexity.hVer_stuck {A : Type} [FirstOrder.Language.sat.Structure A] [LinearOrder A] [Finite A] [Nonempty A] (M : A → Bool) {cf : A} (hcf : SatCl cf) (hfail : ¬∃ (y : A), MLit cf y (M y)) (c : A) : SatCl c → c ≤ cf → (∀ (e : A), SatCl e → c ≤ e → e < cf → ∃ (y : A), MLit e y (M y)) → (∃ (N : ℕ) (S : Config (HV A)), (hornMachine A).StepsIn N (confHVerR M c (posHCell botA)) S ∧ (∀ (d : Config (HV A)), ¬(hornMachine A).Step S d) ∧ S.state.1 ≠ UPTag.qAcc) ∧ ∃ (N : ℕ) (S : Config (HV A)), (hornMachine A).StepsIn N (confHVerL M c (posHCell topA)) S ∧ (∀ (d : Config (HV A)), ¬(hornMachine A).Step S d) ∧ S.state.1 ≠ UPTag.qAcc

The trajectory of an unsatisfiable Horn instance gets stuck: the verification sweeps run through the satisfied clauses and die at the first failing one, in a configuration that is not accepting and admits no step.

theorem DescriptiveComplexity.hornMachine_accepts_iff {A : Type} [FirstOrder.Language.sat.Structure A] [LinearOrder A] [Finite A] [Nonempty A] : (hornMachine A).Accepts ↔ HornSatisfiable A

Correctness of the unit-propagation machine: it accepts exactly the yes-instances of HORN-SAT.