The machine of a CNF formula

The program half of SAT ≤ᶠᵒ[≤] NTMAccept: the states, symbols and transitions of the machine M_φ built inside an ordered SAT instance, on the tape laid out in DescriptiveComplexity.Problems.Machine.Tape.

The program

  guess :  ⊢ →  at each cell (x,U) write (x,T) or (x,F), moving right  → ⊣
  check c: sweep back over the cells, accumulating
             flag := flag ∨ (posIn c x ∧ b) ∨ (negIn c x ∧ ¬b)
           at the far marker: if flag, take the next clause and turn round;
                              if not, no transition exists and the run dies
  accept:  when the clause just checked was the last one

Two things make this small. The check is an first-order test on the source structure – DescriptiveComplexity.SatLit – evaluated by the formula that will define the transition relation, so no clause-width bound and no occurrence machinery are needed and the source can be plain SAT rather than 3SAT. And the sweeps alternate direction instead of rewinding, so a clause costs one pass and there are no rewind states; the markers are what tell the machine a pass has ended.

The machine is nondeterministic in exactly one place, the choice of (x,T) or (x,F) in the guess phase. That is a deliberate design decision, and it is what will make the ⇒ half of correctness a corollary of uniqueness rather than a second invariant induction.

Semantics first

Everything here is a plain predicate on tagged tuples, as DescriptiveComplexity.SatPosn and DescriptiveComplexity.SatInp are: the machine is assembled as a DescriptiveComplexity.TMData and reasoned about directly. Only once its correctness is proved does the first-order transcription happen, one realization lemma per relFormula. A transition table type-checks whatever it says, so it has to be validated by a proof, not by elaboration.

The instance, read

def DescriptiveComplexity.SatCl {A : Type} [FirstOrder.Language.sat.Structure A] (c : A) : Prop

Being a clause of the CNF instance.

Equations

• DescriptiveComplexity.SatCl c = FirstOrder.Language.Structure.RelMap FirstOrder.Language.satIsClause ![c]

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

The variable x occurs positively in the clause c.

Equations

• DescriptiveComplexity.SatPos c x = FirstOrder.Language.Structure.RelMap FirstOrder.Language.satPosIn ![c, x]

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

The variable x occurs negatively in the clause c.

Equations

• DescriptiveComplexity.SatNeg c x = FirstOrder.Language.Structure.RelMap FirstOrder.Language.satNegIn ![c, x]

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

The literal test: the cell x, holding the truth value v, satisfies the clause c. This is the first-order test on the source structure that the transition relation performs; it is the whole of the check phase.

Equations

• DescriptiveComplexity.SatLit c x v = (DescriptiveComplexity.SatPos c x ∧ v = true ∨ DescriptiveComplexity.SatNeg c x ∧ v = false)

def DescriptiveComplexity.SatMinCl {A : Type} [FirstOrder.Language.sat.Structure A] [LinearOrder A] (c : A) : Prop

c is the lowest clause.

Equations

• DescriptiveComplexity.SatMinCl c = (DescriptiveComplexity.SatCl c ∧ ∀ (e : A), DescriptiveComplexity.SatCl e → c ≤ e)

def DescriptiveComplexity.SatMaxCl {A : Type} [FirstOrder.Language.sat.Structure A] [LinearOrder A] (c : A) : Prop

c is the highest clause.

Equations

• DescriptiveComplexity.SatMaxCl c = (DescriptiveComplexity.SatCl c ∧ ∀ (e : A), DescriptiveComplexity.SatCl e → e ≤ c)

def DescriptiveComplexity.SatNextCl {A : Type} [FirstOrder.Language.sat.Structure A] [LinearOrder A] (c c' : A) : Prop

c' is the clause immediately above c.

Equations

• DescriptiveComplexity.SatNextCl c c' = (DescriptiveComplexity.SatCl c ∧ DescriptiveComplexity.SatCl c' ∧ c < c' ∧ ∀ (e : A), DescriptiveComplexity.SatCl e → c < e → c' ≤ e)

The elements of the machine

noncomputable def DescriptiveComplexity.botA {A : Type} [LinearOrder A] [Finite A] [Nonempty A] : A

The least element of the instance, to which every constant of the machine is pinned.

Equations

• DescriptiveComplexity.botA = ⋯.choose

theorem DescriptiveComplexity.botA_le {A : Type} [LinearOrder A] [Finite A] [Nonempty A] (a : A) : botA ≤ a

theorem DescriptiveComplexity.isMinTup_bot {A : Type} [LinearOrder A] [Finite A] [Nonempty A] : IsMinTup fun (x : Fin 2) => botA

@[reducible, inline]

abbrev DescriptiveComplexity.SatV (A : Type) : Type

The universe of the machine: tagged pairs.

Equations

• DescriptiveComplexity.SatV A = (DescriptiveComplexity.SatTag × (Fin 2 → A))

noncomputable def DescriptiveComplexity.cst {A : Type} [LinearOrder A] [Finite A] [Nonempty A] (t : SatTag) : SatV A

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

Equations

• DescriptiveComplexity.cst t = (t, fun (x : Fin 2) => DescriptiveComplexity.botA)

noncomputable def DescriptiveComplexity.one {A : Type} [LinearOrder A] [Finite A] [Nonempty A] (t : SatTag) (a : A) : SatV A

A tag carrying one element, pinned in the second coordinate.

Equations

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

Symbols

@[reducible, inline]

noncomputable abbrev DescriptiveComplexity.symStart {A : Type} [LinearOrder A] [Finite A] [Nonempty A] : SatV A

The left-marker symbol.

Equations

• DescriptiveComplexity.symStart = DescriptiveComplexity.cst DescriptiveComplexity.SatTag.sStart

@[reducible, inline]

noncomputable abbrev DescriptiveComplexity.symEnd {A : Type} [LinearOrder A] [Finite A] [Nonempty A] : SatV A

The right-marker symbol.

Equations

• DescriptiveComplexity.symEnd = DescriptiveComplexity.cst DescriptiveComplexity.SatTag.sEnd

@[reducible, inline]

noncomputable abbrev DescriptiveComplexity.symBlank {A : Type} [LinearOrder A] [Finite A] [Nonempty A] : SatV A

The blank symbol.

Equations

• DescriptiveComplexity.symBlank = DescriptiveComplexity.cst DescriptiveComplexity.SatTag.sBlank

@[reducible, inline]

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

The symbol of an unassigned cell.

Equations

• DescriptiveComplexity.symU x = DescriptiveComplexity.one DescriptiveComplexity.SatTag.sU x

@[reducible, inline]

noncomputable abbrev DescriptiveComplexity.symV {A : Type} [LinearOrder A] [Finite A] [Nonempty A] (v : Bool) (x : A) : SatV A

The symbol of a cell assigned the truth value v.

Equations

• DescriptiveComplexity.symV v x = DescriptiveComplexity.one (if v = true then DescriptiveComplexity.SatTag.sT else DescriptiveComplexity.SatTag.sF) x

Positions

@[reducible, inline]

noncomputable abbrev DescriptiveComplexity.posStart {A : Type} [LinearOrder A] [Finite A] [Nonempty A] : SatV A

The left-marker cell.

Equations

• DescriptiveComplexity.posStart = DescriptiveComplexity.cst DescriptiveComplexity.SatTag.pStart

@[reducible, inline]

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

The cell of the element x.

Equations

• DescriptiveComplexity.posCell x = DescriptiveComplexity.one DescriptiveComplexity.SatTag.pCell x

@[reducible, inline]

noncomputable abbrev DescriptiveComplexity.posEnd {A : Type} [LinearOrder A] [Finite A] [Nonempty A] : SatV A

The right-marker cell.

Equations

• DescriptiveComplexity.posEnd = DescriptiveComplexity.cst DescriptiveComplexity.SatTag.pEnd

States

@[reducible, inline]

noncomputable abbrev DescriptiveComplexity.stGuess {A : Type} [LinearOrder A] [Finite A] [Nonempty A] : SatV A

The guessing state.

Equations

• DescriptiveComplexity.stGuess = DescriptiveComplexity.cst DescriptiveComplexity.SatTag.qGuess

@[reducible, inline]

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

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

Equations

• DescriptiveComplexity.stChk f d c = DescriptiveComplexity.one (DescriptiveComplexity.SatTag.qChk f d) c

@[reducible, inline]

noncomputable abbrev DescriptiveComplexity.stAcc {A : Type} [LinearOrder A] [Finite A] [Nonempty A] : SatV A

The accepting state.

Equations

• DescriptiveComplexity.stAcc = DescriptiveComplexity.cst DescriptiveComplexity.SatTag.qAcc

The transition table

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

Which tagged tuples are transitions. The payload is pinned exactly as far as the transition needs it, and the clause coordinates are required to be clauses, so that no junk element is ever a transition.

Equations

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

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

The state a transition applies in.

Equations

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

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

The symbol a transition reads.

Equations

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

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

The state a transition moves to. The only place the instance is consulted is the check clause, where the new flag depends on DescriptiveComplexity.SatLit.

Equations

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

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

The symbol a transition writes: everything but the guess phase leaves the tape as it found it.

Equations

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

def DescriptiveComplexity.SatRight {A : Type} (τ : SatV A) : Prop

Which transitions move the head right: the guess phase always does, a check sweep goes in its own direction, and a turn – whether it takes the next clause or accepts – reverses. A turn must reverse even when accepting: it fires at a marker, and there is no position beyond one.

Equations

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

def DescriptiveComplexity.SatAcc {A : Type} (q : SatV A) : Prop

Accepting states: just DescriptiveComplexity.stAcc.

Equations

• DescriptiveComplexity.SatAcc q = (q.1 = DescriptiveComplexity.SatTag.qAcc)

def DescriptiveComplexity.SatStart {A : Type} [LinearOrder A] (q : SatV A) : Prop

Start states: just DescriptiveComplexity.stGuess.

Equations

• DescriptiveComplexity.SatStart q = (q.1 = DescriptiveComplexity.SatTag.qGuess ∧ DescriptiveComplexity.IsMinTup q.2)

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

The machine of a CNF instance.

Equations

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

The table is a table

Before any run is considered: each transition has exactly one destination and symbol written, and the two places where two tags could otherwise both apply are exclusive. A mistake in the table shows up here first, which is why these come before the correctness proof. (Sources and symbols read need no functionality lemma of their own: DescriptiveComplexity.satTr_unique pins the whole transition from them.)

theorem DescriptiveComplexity.one_eq_one_iff {A : Type} [LinearOrder A] [Finite A] [Nonempty A] {t t' : SatTag} {a a' : A} : one t a = one t' a' ↔ t = t' ∧ a = a'

theorem DescriptiveComplexity.satWrite_functional {A : Type} [LinearOrder A] [Finite A] [Nonempty A] {τ a a' : SatV A} (h : SatWrite τ a) (h' : SatWrite τ a') : a = a'

A transition writes exactly one symbol.

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

A transition moves to exactly one state. The only case with a choice is the check clause, whose two branches are separated by the flag and by DescriptiveComplexity.SatLit.

theorem DescriptiveComplexity.satTr_guessEnd_excl {A : Type} [FirstOrder.Language.sat.Structure A] [LinearOrder A] {τ τ' : SatV A} (h : SatTr τ) (h' : SatTr τ') (hτ : τ.1 = SatTag.tGuessEndAcc) (hτ' : τ'.1 = SatTag.tGuessEndChk) : False

The end of the guess phase is not ambiguous: an instance either has a clause to check or has none.

theorem DescriptiveComplexity.satTr_turn_excl {A : Type} [FirstOrder.Language.sat.Structure A] [LinearOrder A] {τ τ' : SatV A} {d d' : Bool} (h : SatTr τ) (h' : SatTr τ') (hτ : τ.1 = SatTag.tTurnNext d) (hτ' : τ'.1 = SatTag.tTurnAcc d') (hc : τ.2 0 = τ'.2 0) : False

A turn is not ambiguous: the clause just checked either has a successor or is the last one.

def DescriptiveComplexity.stateTag : SatTag → SatTag

The tag of the state a transition applies in, as a function of its own tag. Junk tags are sent to themselves; they are never transitions.

Equations

• DescriptiveComplexity.stateTag DescriptiveComplexity.SatTag.tGuessStart = DescriptiveComplexity.SatTag.qGuess
• DescriptiveComplexity.stateTag (DescriptiveComplexity.SatTag.tGuessVal b) = DescriptiveComplexity.SatTag.qGuess
• DescriptiveComplexity.stateTag DescriptiveComplexity.SatTag.tGuessEndAcc = DescriptiveComplexity.SatTag.qGuess
• DescriptiveComplexity.stateTag DescriptiveComplexity.SatTag.tGuessEndChk = DescriptiveComplexity.SatTag.qGuess
• DescriptiveComplexity.stateTag (DescriptiveComplexity.SatTag.tChk b f d) = DescriptiveComplexity.SatTag.qChk f d
• DescriptiveComplexity.stateTag (DescriptiveComplexity.SatTag.tTurnNext d) = DescriptiveComplexity.SatTag.qChk true d
• DescriptiveComplexity.stateTag (DescriptiveComplexity.SatTag.tTurnAcc d) = DescriptiveComplexity.SatTag.qChk true d
• DescriptiveComplexity.stateTag x✝ = x✝

def DescriptiveComplexity.readTag : SatTag → SatTag

The tag of the symbol a transition reads, as a function of its own tag.

Equations

• DescriptiveComplexity.readTag DescriptiveComplexity.SatTag.tGuessStart = DescriptiveComplexity.SatTag.sStart
• DescriptiveComplexity.readTag (DescriptiveComplexity.SatTag.tGuessVal b) = DescriptiveComplexity.SatTag.sU
• DescriptiveComplexity.readTag DescriptiveComplexity.SatTag.tGuessEndAcc = DescriptiveComplexity.SatTag.sEnd
• DescriptiveComplexity.readTag DescriptiveComplexity.SatTag.tGuessEndChk = DescriptiveComplexity.SatTag.sEnd
• DescriptiveComplexity.readTag (DescriptiveComplexity.SatTag.tChk b f d) = if b = true then DescriptiveComplexity.SatTag.sT else DescriptiveComplexity.SatTag.sF
• DescriptiveComplexity.readTag (DescriptiveComplexity.SatTag.tTurnNext d) = if d = true then DescriptiveComplexity.SatTag.sEnd else DescriptiveComplexity.SatTag.sStart
• DescriptiveComplexity.readTag (DescriptiveComplexity.SatTag.tTurnAcc d) = if d = true then DescriptiveComplexity.SatTag.sEnd else DescriptiveComplexity.SatTag.sStart
• DescriptiveComplexity.readTag x✝ = x✝

theorem DescriptiveComplexity.satSrc_tag {A : Type} [FirstOrder.Language.sat.Structure A] [LinearOrder A] [Finite A] [Nonempty A] {τ q : SatV A} (hτ : SatTr τ) (hs : SatSrc τ q) : q.1 = stateTag τ.1

The state pins the transition's tag.

theorem DescriptiveComplexity.satRead_tag {A : Type} [FirstOrder.Language.sat.Structure A] [LinearOrder A] [Finite A] [Nonempty A] {τ a : SatV A} (hτ : SatTr τ) (hr : SatRead τ a) : a.1 = readTag τ.1

The symbol read pins the transition's tag.

def DescriptiveComplexity.isTrTag : SatTag → Bool

Being the tag of a transition.

Equations

• DescriptiveComplexity.isTrTag DescriptiveComplexity.SatTag.tGuessStart = true
• DescriptiveComplexity.isTrTag (DescriptiveComplexity.SatTag.tGuessVal b) = true
• DescriptiveComplexity.isTrTag DescriptiveComplexity.SatTag.tGuessEndAcc = true
• DescriptiveComplexity.isTrTag DescriptiveComplexity.SatTag.tGuessEndChk = true
• DescriptiveComplexity.isTrTag (DescriptiveComplexity.SatTag.tChk b f d) = true
• DescriptiveComplexity.isTrTag (DescriptiveComplexity.SatTag.tTurnNext d) = true
• DescriptiveComplexity.isTrTag (DescriptiveComplexity.SatTag.tTurnAcc d) = true
• DescriptiveComplexity.isTrTag x✝ = false

def DescriptiveComplexity.isGuessVal : SatTag → Bool

The tag of a guess-phase write.

Equations

• DescriptiveComplexity.isGuessVal (DescriptiveComplexity.SatTag.tGuessVal b) = true
• DescriptiveComplexity.isGuessVal x✝ = false

def DescriptiveComplexity.isEndAcc : SatTag → Bool

The tag ending the guess phase with no clause to check.

Equations

• DescriptiveComplexity.isEndAcc DescriptiveComplexity.SatTag.tGuessEndAcc = true
• DescriptiveComplexity.isEndAcc x✝ = false

def DescriptiveComplexity.isEndChk : SatTag → Bool

The tag ending the guess phase with a clause to check.

Equations

• DescriptiveComplexity.isEndChk DescriptiveComplexity.SatTag.tGuessEndChk = true
• DescriptiveComplexity.isEndChk x✝ = false

def DescriptiveComplexity.isTurnNext : SatTag → Bool

The tag turning to the next clause.

Equations

• DescriptiveComplexity.isTurnNext (DescriptiveComplexity.SatTag.tTurnNext d) = true
• DescriptiveComplexity.isTurnNext x✝ = false

def DescriptiveComplexity.isTurnAcc : SatTag → Bool

The tag accepting after the last clause.

Equations

• DescriptiveComplexity.isTurnAcc (DescriptiveComplexity.SatTag.tTurnAcc d) = true
• DescriptiveComplexity.isTurnAcc x✝ = false

theorem DescriptiveComplexity.tag_cases (t t' : SatTag) : isTrTag t = true → isTrTag t' = true → stateTag t = stateTag t' → readTag t = readTag t' → t = t' ∨ isGuessVal t = true ∧ isGuessVal t' = true ∨ isEndAcc t = true ∧ isEndChk t' = true ∨ isEndChk t = true ∧ isEndAcc t' = true ∨ isTurnNext t = true ∧ isTurnAcc t' = true ∨ isTurnAcc t = true ∧ isTurnNext t' = true

The state and the symbol determine the transition's tag, up to the three known ambiguities: the guess itself, the end of the guess phase, and a turn. A finite check over the tags – no case analysis by hand.

theorem DescriptiveComplexity.satV_ext {A : Type} {τ τ' : SatV A} (ht : τ.1 = τ'.1) (h0 : τ.2 0 = τ'.2 0) (h1 : τ.2 1 = τ'.2 1) : τ = τ'

Two elements agree when their tag and both coordinates do.

theorem DescriptiveComplexity.satTr_isTrTag {A : Type} [FirstOrder.Language.sat.Structure A] [LinearOrder A] {τ : SatV A} (hτ : SatTr τ) : isTrTag τ.1 = true

Only transitions have transition tags.

theorem DescriptiveComplexity.isGuessVal_iff {t : SatTag} : isGuessVal t = true ↔ ∃ (v : Bool), t = SatTag.tGuessVal v

theorem DescriptiveComplexity.isEndAcc_iff {t : SatTag} : isEndAcc t = true ↔ t = SatTag.tGuessEndAcc

theorem DescriptiveComplexity.isEndChk_iff {t : SatTag} : isEndChk t = true ↔ t = SatTag.tGuessEndChk

theorem DescriptiveComplexity.isTurnNext_iff {t : SatTag} : isTurnNext t = true ↔ ∃ (d : Bool), t = SatTag.tTurnNext d

theorem DescriptiveComplexity.isTurnAcc_iff {t : SatTag} : isTurnAcc t = true ↔ ∃ (d : Bool), t = SatTag.tTurnAcc d

theorem DescriptiveComplexity.satTr_payload {A : Type} [FirstOrder.Language.sat.Structure A] [LinearOrder A] [Finite A] [Nonempty A] {τ τ' q a : SatV A} (hτ : SatTr τ) (hτ' : SatTr τ') (hs : SatSrc τ q) (hs' : SatSrc τ' q) (hr : SatRead τ a) (hr' : SatRead τ' a) (ht : τ.1 = τ'.1) : τ = τ'

Equal tags force equal payloads: the state and symbol pin one coordinate, the promises in DescriptiveComplexity.SatTr pin the other.

theorem DescriptiveComplexity.satSrc_guessVal {A : Type} [LinearOrder A] [Finite A] [Nonempty A] {τ q : SatV A} {v : Bool} (h : τ.1 = SatTag.tGuessVal v) (hs : SatSrc τ q) : q = stGuess

Reading off DescriptiveComplexity.SatSrc at a guess-write tag.

theorem DescriptiveComplexity.satRead_guessVal {A : Type} [LinearOrder A] [Finite A] [Nonempty A] {τ a : SatV A} {v : Bool} (h : τ.1 = SatTag.tGuessVal v) (hr : SatRead τ a) : a = symU (τ.2 0)

Reading off DescriptiveComplexity.SatRead at a guess-write tag.

theorem DescriptiveComplexity.satSrc_turnNext {A : Type} [LinearOrder A] [Finite A] [Nonempty A] {τ q : SatV A} {d : Bool} (h : τ.1 = SatTag.tTurnNext d) (hs : SatSrc τ q) : q = stChk true d (τ.2 0)

Reading off DescriptiveComplexity.SatSrc at a turn-to-next tag.

theorem DescriptiveComplexity.satSrc_turnAcc {A : Type} [LinearOrder A] [Finite A] [Nonempty A] {τ q : SatV A} {d : Bool} (h : τ.1 = SatTag.tTurnAcc d) (hs : SatSrc τ q) : q = stChk true d (τ.2 0)

Reading off DescriptiveComplexity.SatSrc at a turn-to-accept tag.

theorem DescriptiveComplexity.satTr_unique {A : Type} [FirstOrder.Language.sat.Structure A] [LinearOrder A] [Finite A] [Nonempty A] {τ τ' q a : SatV A} (hτ : SatTr τ) (hτ' : SatTr τ') (hs : SatSrc τ q) (hs' : SatSrc τ' q) (hr : SatRead τ a) (hr' : SatRead τ' a) (hguess : ¬(q = stGuess ∧ ∃ (x : A), a = symU x)) : τ = τ'

At most one transition applies, away from the one nondeterministic choice of the guess phase: the state and the symbol read pin the tag (DescriptiveComplexity.tag_cases), the tag pins the payload (DescriptiveComplexity.satTr_payload), and the three ambiguities are the guess itself and the two exclusive branch points.

The positions of the tape, concretely

theorem DescriptiveComplexity.satPosn_posStart {A : Type} [LinearOrder A] [Finite A] [Nonempty A] : SatPosn posStart

The left marker is a position.

theorem DescriptiveComplexity.satPosn_posCell {A : Type} [LinearOrder A] [Finite A] [Nonempty A] (x : A) : SatPosn (posCell x)

The cell of an element is a position.

theorem DescriptiveComplexity.satPosn_posEnd {A : Type} [LinearOrder A] [Finite A] [Nonempty A] : SatPosn posEnd

The right marker is a position.

theorem DescriptiveComplexity.tagTupleLe_refl {A : Type} [LinearOrder A] (p : SatV A) : tagTupleLe p p

The tape order is reflexive.

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

A tag strictly below another puts its tuples below all of theirs.

theorem DescriptiveComplexity.pStart_lt {t : SatTag} (h : t ≠ SatTag.pStart) : SatTag.pStart < t

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

theorem DescriptiveComplexity.eq_posStart_of_posn {A : Type} [LinearOrder A] [Finite A] [Nonempty A] {p : SatV A} (hp : SatPosn p) (h : p.1 = SatTag.pStart) : p = posStart

There is only one left marker.

theorem DescriptiveComplexity.minPos_posStart {A : Type} [LinearOrder A] [Finite A] [Nonempty A] : MinPos tagTupleLe SatPosn posStart

The left marker is the lowest position: the head starts there.

theorem DescriptiveComplexity.posStart_le_posCell {A : Type} [LinearOrder A] [Finite A] [Nonempty A] (x : A) : tagTupleLe posStart (posCell x)

The left marker precedes every cell.

theorem DescriptiveComplexity.posCell_le_posEnd {A : Type} [LinearOrder A] [Finite A] [Nonempty A] (x : A) : tagTupleLe (posCell x) posEnd

Every cell precedes the right marker.

theorem DescriptiveComplexity.posStart_le_posEnd {A : Type} [LinearOrder A] [Finite A] [Nonempty A] : tagTupleLe posStart posEnd

The left marker precedes the right marker.

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

The tape order refines the tag order.

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

Cells are ordered as their elements are. The tape order between two cells is the source order between the elements they belong to – which is what makes a sweep over the cells a walk along the instance.

theorem DescriptiveComplexity.tag_le_pCell {t : SatTag} (h : t ≤ SatTag.pCell) : t = SatTag.pStart ∨ t = SatTag.pCell

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

theorem DescriptiveComplexity.eq_posCell_of_posn {A : Type} [LinearOrder A] [Finite A] [Nonempty A] {p : SatV A} (hp : SatPosn p) (h : p.1 = SatTag.pCell) : p = posCell (p.2 0)

A cell is the cell of the element it carries.

theorem DescriptiveComplexity.succPos_posStart_posCell {A : Type} [LinearOrder A] [Finite A] [Nonempty A] : SuccPos tagTupleLe SatPosn posStart (posCell botA)

The head's first move. The cell of the least element follows the left marker immediately: the guess sweep starts by stepping over ⊢.

noncomputable def DescriptiveComplexity.topA {A : Type} [LinearOrder A] [Finite A] [Nonempty A] : A

The greatest element of the instance: the last cell of the tape.

Equations

• DescriptiveComplexity.topA = ⋯.choose

theorem DescriptiveComplexity.le_topA {A : Type} [LinearOrder A] [Finite A] [Nonempty A] (a : A) : a ≤ topA

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

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

theorem DescriptiveComplexity.eq_posEnd_of_posn {A : Type} [LinearOrder A] [Finite A] [Nonempty A] {p : SatV A} (hp : SatPosn p) (h : p.1 = SatTag.pEnd) : p = posEnd

There is only one right marker.

theorem DescriptiveComplexity.succPos_posCell_posEnd {A : Type} [LinearOrder A] [Finite A] [Nonempty A] : SuccPos tagTupleLe SatPosn (posCell topA) posEnd

The head's last move of a sweep. The right marker follows the cell of the greatest element: this is where the guess sweep stops.

theorem DescriptiveComplexity.step_functional_off_guess {A : Type} [FirstOrder.Language.sat.Structure A] [LinearOrder A] [Finite A] [Nonempty A] {c c₁ c₂ : Config (SatV A)} (hguess : ¬(c.state = stGuess ∧ ∃ (x : A), c.tape c.head = symU x)) (h₁ : (satMachine A).Step c c₁) (h₂ : (satMachine A).Step c c₂) : c₁ = c₂

The machine is deterministic away from the guess. Once the transition is pinned (DescriptiveComplexity.satTr_unique), the successor configuration is too: its state by satDst_functional, the cell under the head by satWrite_functional, every other cell by the frame condition, and the head itself by uniqueness of the neighbour in the direction the transition names.

This is a deliberate design decision: with only the guess phase branching, the ⇒ half of correctness becomes a corollary of uniqueness rather than a second invariant induction.

The intended run: the guess phase

noncomputable def DescriptiveComplexity.guessTape {A : Type} [LinearOrder A] [Finite A] [Nonempty A] (ν : A → Bool) (p q : SatV A) : SatV A

The tape during the guess sweep, with the head at p: the markers hold their own symbols, a cell strictly below the head has been assigned its value under ν, a cell at or above the head is still unassigned, and every other element reads blank.

A tuple carrying a cell's tag but a junk second coordinate is not a position, and the machine never visits it – but the frame condition of a step quantifies over it all the same, so its value must not move as the head advances. Hence the guard ∀ a, q.2 1 ≤ a: junk cells read unassigned forever, which is also what DescriptiveComplexity.SatInp says they hold initially.

Equations

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

noncomputable def DescriptiveComplexity.confGuess {A : Type} [LinearOrder A] [Finite A] [Nonempty A] (ν : A → Bool) (p : SatV A) : Config (SatV A)

The configuration during the guess sweep, with the head at p.

Equations

• DescriptiveComplexity.confGuess ν p = { state := DescriptiveComplexity.stGuess, head := p, tape := DescriptiveComplexity.guessTape ν p }

theorem DescriptiveComplexity.guessTape_frame {A : Type} [LinearOrder A] [Finite A] [Nonempty A] (ν : A → Bool) {p q r : SatV A} (hsucc : SuccPos tagTupleLe SatPosn p q) (hr : r ≠ p) : guessTape ν q r = guessTape ν p r

The guess sweep only ever changes the cell under the head. Every other element reads the same before and after: markers and non-cells do not depend on the head at all, junk cells are frozen, and a real cell is below the new head exactly when it was below the old one – by the between-condition of DescriptiveComplexity.SuccPos in one direction and transitivity in the other.

theorem DescriptiveComplexity.isInit_confGuess {A : Type} [FirstOrder.Language.sat.Structure A] [LinearOrder A] [Finite A] [Nonempty A] (ν : A → Bool) : (satMachine A).IsInit (confGuess ν posStart)

The guess sweep starts from an initial configuration: at the left marker no cell is below the head, so every cell still reads unassigned – which is exactly the input DescriptiveComplexity.SatInp describes.

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

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

theorem DescriptiveComplexity.step_guess {A : Type} [FirstOrder.Language.sat.Structure A] [LinearOrder A] [Finite A] [Nonempty A] (ν : A → Bool) {p q : SatV A} (hsucc : SuccPos tagTupleLe SatPosn p q) (hb : tagTupleLe q posEnd) : (satMachine A).Step (confGuess ν p) (confGuess ν q)

One step of the guess sweep. At the left marker the machine steps over it; at a cell it writes the guessed value and moves on; past the right marker the segment bound leaves nothing to prove.

theorem DescriptiveComplexity.steps_guess {A : Type} [FirstOrder.Language.sat.Structure A] [LinearOrder A] [Finite A] [Nonempty A] (ν : A → Bool) : (satMachine A).StepsIn (bitRank tagTupleLe SatPosn posEnd - bitRank tagTupleLe SatPosn posStart) (confGuess ν posStart) (confGuess ν posEnd)

The whole guess sweep. From the left marker to the right one, the machine writes a truth value in every cell, in as many steps as there are positions strictly between the markers – plus the two markers themselves.

theorem DescriptiveComplexity.step_turnChk {A : Type} [FirstOrder.Language.sat.Structure A] [LinearOrder A] [Finite A] [Nonempty A] (ν : A → Bool) {c₀ : A} (hc₀ : SatMinCl c₀) : (satMachine A).Step (confGuess ν posEnd) { state := stChk false false c₀, head := posCell topA, tape := guessTape ν posEnd }

The turn out of the guess phase, when there is a clause to check: the machine reads the right marker, takes the lowest clause with an empty flag, and turns round to sweep leftwards.

theorem DescriptiveComplexity.step_turnAcc {A : Type} [FirstOrder.Language.sat.Structure A] [LinearOrder A] [Finite A] [Nonempty A] (ν : A → Bool) (hno : ∀ (e : A), ¬SatCl e) : (satMachine A).Step (confGuess ν posEnd) { state := stAcc, head := posCell topA, tape := guessTape ν posEnd }

The turn out of the guess phase, when the instance has no clause at all: the formula is vacuously satisfiable and the machine accepts. Without this tag the run would die and the reduction would be wrong on the empty CNF.

The intended run: a check sweep

noncomputable def DescriptiveComplexity.doneTape {A : Type} [LinearOrder A] [Finite A] [Nonempty A] (ν : A → Bool) : SatV A → SatV A

The tape once the guess sweep has finished: every cell assigned. It does not change again, so the frame condition of every later step is rfl.

Equations

• DescriptiveComplexity.doneTape ν = DescriptiveComplexity.guessTape ν DescriptiveComplexity.posEnd

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

The flag of a leftward check sweep with the head at p: some cell already visited – that is, strictly above p – satisfies the clause c.

Equations

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

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

The configuration during a leftward check sweep of the clause c.

Equations

• DescriptiveComplexity.confChkL ν c p = { state := DescriptiveComplexity.stChk (DescriptiveComplexity.chkFlagL ν c p) false c, head := p, tape := DescriptiveComplexity.doneTape ν }

theorem DescriptiveComplexity.chkFlagL_top {A : Type} [FirstOrder.Language.sat.Structure A] [LinearOrder A] [Finite A] [Nonempty A] (ν : A → Bool) (c : A) : chkFlagL ν c (posCell topA) = false

A check sweep starts with an empty flag: at the highest cell nothing has been visited yet.

theorem DescriptiveComplexity.chkFlagL_succ {A : Type} [FirstOrder.Language.sat.Structure A] [LinearOrder A] [Finite A] [Nonempty A] (ν : A → Bool) (c : A) {p q : SatV A} (hsucc : SuccPos tagTupleLe SatPosn p q) (hq : q.1 = SatTag.pCell) : chkFlagL ν c p = true ↔ chkFlagL ν c q = true ∨ SatLit c (q.2 0) (ν (q.2 0))

Stepping down adds exactly one literal to the flag. Moving the head from q to the position below it brings q's own cell into view and nothing else, because DescriptiveComplexity.SuccPos leaves no room between them. This is the whole content of a check sweep.

theorem DescriptiveComplexity.doneTape_cell {A : Type} [LinearOrder A] [Finite A] [Nonempty A] (ν : A → Bool) {q : SatV A} (hq : q.1 = SatTag.pCell) (hpos : ∀ (a : A), q.2 1 ≤ a) : doneTape ν q = symV (ν (q.2 0)) (q.2 0)

After the guess sweep every real cell holds its assigned value.

theorem DescriptiveComplexity.step_chkL {A : Type} [FirstOrder.Language.sat.Structure A] [LinearOrder A] [Finite A] [Nonempty A] (ν : A → Bool) {c : A} (hc : SatCl c) {p q : SatV A} (hsucc : SuccPos tagTupleLe SatPosn p q) (hq : q.1 = SatTag.pCell) : (satMachine A).Step (confChkL ν c q) (confChkL ν c p)

One step of a leftward check sweep. The machine reads the cell it is on, folds that literal into the flag, and moves one place left. Which of the two DescriptiveComplexity.SatDst branches applies is exactly DescriptiveComplexity.chkFlagL_succ.

theorem DescriptiveComplexity.steps_chkL {A : Type} [FirstOrder.Language.sat.Structure A] [LinearOrder A] [Finite A] [Nonempty A] (ν : A → Bool) {c : A} (hc : SatCl c) : (satMachine A).StepsIn (bitRank tagTupleLe SatPosn (posCell topA) - bitRank tagTupleLe SatPosn posStart) (confChkL ν c (posCell topA)) (confChkL ν c posStart)

A whole leftward check sweep. From the highest cell down to the left marker, the flag accumulating the literals of c satisfied along the way.

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

The flag of a rightward check sweep with the head at p: some cell already visited – strictly below p – satisfies c.

Equations

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

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

The configuration during a rightward check sweep of the clause c.

Equations

• DescriptiveComplexity.confChkR ν c p = { state := DescriptiveComplexity.stChk (DescriptiveComplexity.chkFlagR ν c p) true c, head := p, tape := DescriptiveComplexity.doneTape ν }

theorem DescriptiveComplexity.chkFlagR_bot {A : Type} [FirstOrder.Language.sat.Structure A] [LinearOrder A] [Finite A] [Nonempty A] (ν : A → Bool) (c : A) : chkFlagR ν c (posCell botA) = false

A rightward sweep also starts with an empty flag: nothing lies below the lowest cell.

theorem DescriptiveComplexity.doneTape_start {A : Type} [LinearOrder A] [Finite A] [Nonempty A] (ν : A → Bool) : doneTape ν posStart = symStart

The left marker keeps its symbol throughout.

theorem DescriptiveComplexity.step_turnNextL {A : Type} [FirstOrder.Language.sat.Structure A] [LinearOrder A] [Finite A] [Nonempty A] (ν : A → Bool) {c c' : A} (hnext : SatNextCl c c') (hflag : chkFlagL ν c posStart = true) : (satMachine A).Step (confChkL ν c posStart) (confChkR ν c' (posCell botA))

The turn at the left marker, when another clause follows: the flag is set, so the machine takes the next clause, empties the flag and reverses to sweep rightwards.

theorem DescriptiveComplexity.chkFlagR_succ {A : Type} [FirstOrder.Language.sat.Structure A] [LinearOrder A] [Finite A] [Nonempty A] (ν : A → Bool) (c : A) {p q : SatV A} (hsucc : SuccPos tagTupleLe SatPosn p q) (hp : p.1 = SatTag.pCell) : chkFlagR ν c q = true ↔ chkFlagR ν c p = true ∨ SatLit c (p.2 0) (ν (p.2 0))

Stepping up adds exactly one literal to the flag – the mirror of DescriptiveComplexity.chkFlagL_succ.

theorem DescriptiveComplexity.step_chkR {A : Type} [FirstOrder.Language.sat.Structure A] [LinearOrder A] [Finite A] [Nonempty A] (ν : A → Bool) {c : A} (hc : SatCl c) {p q : SatV A} (hsucc : SuccPos tagTupleLe SatPosn p q) (hp : p.1 = SatTag.pCell) : (satMachine A).Step (confChkR ν c p) (confChkR ν c q)

One step of a rightward check sweep – the mirror of DescriptiveComplexity.step_chkL.

theorem DescriptiveComplexity.doneTape_end {A : Type} [LinearOrder A] [Finite A] [Nonempty A] (ν : A → Bool) : doneTape ν posEnd = symEnd

The right marker keeps its symbol throughout.

theorem DescriptiveComplexity.steps_chkR {A : Type} [FirstOrder.Language.sat.Structure A] [LinearOrder A] [Finite A] [Nonempty A] (ν : A → Bool) {c : A} (hc : SatCl c) : (satMachine A).StepsIn (bitRank tagTupleLe SatPosn posEnd - bitRank tagTupleLe SatPosn (posCell botA)) (confChkR ν c (posCell botA)) (confChkR ν c posEnd)

A whole rightward check sweep – the mirror of DescriptiveComplexity.steps_chkL.

theorem DescriptiveComplexity.step_turnNextR {A : Type} [FirstOrder.Language.sat.Structure A] [LinearOrder A] [Finite A] [Nonempty A] (ν : A → Bool) {c c' : A} (hnext : SatNextCl c c') (hflag : chkFlagR ν c posEnd = true) : (satMachine A).Step (confChkR ν c posEnd) (confChkL ν c' (posCell topA))

The turn at the right marker, when another clause follows – the mirror of DescriptiveComplexity.step_turnNextL.

theorem DescriptiveComplexity.step_turnAccL {A : Type} [FirstOrder.Language.sat.Structure A] [LinearOrder A] [Finite A] [Nonempty A] (ν : A → Bool) {c : A} (hmax : SatMaxCl c) (hflag : chkFlagL ν c posStart = true) : (satMachine A).Step (confChkL ν c posStart) { state := stAcc, head := posCell botA, tape := doneTape ν }

Accepting at the left marker: the flag is set and the clause just checked was the last one.

theorem DescriptiveComplexity.step_turnAccR {A : Type} [FirstOrder.Language.sat.Structure A] [LinearOrder A] [Finite A] [Nonempty A] (ν : A → Bool) {c : A} (hmax : SatMaxCl c) (hflag : chkFlagR ν c posEnd = true) : (satMachine A).Step (confChkR ν c posEnd) { state := stAcc, head := posCell topA, tape := doneTape ν }

Accepting at the right marker – the mirror.

theorem DescriptiveComplexity.chkFlagL_posStart {A : Type} [FirstOrder.Language.sat.Structure A] [LinearOrder A] [Finite A] [Nonempty A] (ν : A → Bool) (c : A) : chkFlagL ν c posStart = true ↔ ∃ (y : A), SatLit c y (ν y)

A completed leftward sweep has seen every cell: its flag says exactly that some element satisfies the clause.

theorem DescriptiveComplexity.chkFlagR_posEnd {A : Type} [FirstOrder.Language.sat.Structure A] [LinearOrder A] [Finite A] [Nonempty A] (ν : A → Bool) (c : A) : chkFlagR ν c posEnd = true ↔ ∃ (y : A), SatLit c y (ν y)

A completed rightward sweep has seen every cell – the same statement, which is why the alternating directions never have to be reconciled inside the induction over clauses.

One clause, checked end to end

Each of these is a sweep followed by its turn. They are the step and the base case of the induction over clauses; the induction itself only has to choose between them. Each carries its step count, bounded by the rank of the right marker: that is the honest per-clause cost, roughly the size of the instance, and what lets the whole run fit the budget of DescriptiveComplexity.TMData.Accepts.

theorem DescriptiveComplexity.bitRank_posStart {A : Type} [LinearOrder A] [Finite A] [Nonempty A] : bitRank tagTupleLe SatPosn posStart = 0

The left marker has rank 0: it is the lowest position.

theorem DescriptiveComplexity.bitRank_posEnd_eq {A : Type} [LinearOrder A] [Finite A] [Nonempty A] : bitRank tagTupleLe SatPosn posEnd = bitRank tagTupleLe SatPosn (posCell topA) + 1

The right marker sits one step above the last cell.

theorem DescriptiveComplexity.bitRank_posCell_botA {A : Type} [LinearOrder A] [Finite A] [Nonempty A] : bitRank tagTupleLe SatPosn (posCell botA) = 1

The first cell has rank 1: it follows the left marker.

theorem DescriptiveComplexity.steps_clauseL {A : Type} [FirstOrder.Language.sat.Structure A] [LinearOrder A] [Finite A] [Nonempty A] (ν : A → Bool) {c c' : A} (hc : SatCl c) (hnext : SatNextCl c c') (hsat : ∃ (y : A), SatLit c y (ν y)) : ∃ k ≤ bitRank tagTupleLe SatPosn posEnd, (satMachine A).StepsIn k (confChkL ν c (posCell topA)) (confChkR ν c' (posCell botA))

Checking c leftwards and moving on to the next clause.

theorem DescriptiveComplexity.steps_clauseR {A : Type} [FirstOrder.Language.sat.Structure A] [LinearOrder A] [Finite A] [Nonempty A] (ν : A → Bool) {c c' : A} (hc : SatCl c) (hnext : SatNextCl c c') (hsat : ∃ (y : A), SatLit c y (ν y)) : ∃ k ≤ bitRank tagTupleLe SatPosn posEnd, (satMachine A).StepsIn k (confChkR ν c (posCell botA)) (confChkL ν c' (posCell topA))

Checking c rightwards and moving on to the next clause.

theorem DescriptiveComplexity.steps_clauseAccL {A : Type} [FirstOrder.Language.sat.Structure A] [LinearOrder A] [Finite A] [Nonempty A] (ν : A → Bool) {c : A} (hc : SatCl c) (hmax : SatMaxCl c) (hsat : ∃ (y : A), SatLit c y (ν y)) : ∃ k ≤ bitRank tagTupleLe SatPosn posEnd, ∃ (cfin : Config (SatV A)), (satMachine A).StepsIn k (confChkL ν c (posCell topA)) cfin ∧ SatAcc cfin.state

Checking the last clause leftwards, and accepting.

theorem DescriptiveComplexity.steps_clauseAccR {A : Type} [FirstOrder.Language.sat.Structure A] [LinearOrder A] [Finite A] [Nonempty A] (ν : A → Bool) {c : A} (hc : SatCl c) (hmax : SatMaxCl c) (hsat : ∃ (y : A), SatLit c y (ν y)) : ∃ k ≤ bitRank tagTupleLe SatPosn posEnd, ∃ (cfin : Config (SatV A)), (satMachine A).StepsIn k (confChkR ν c (posCell botA)) cfin ∧ SatAcc cfin.state

Checking the last clause rightwards, and accepting.

theorem DescriptiveComplexity.bitRank_posEnd_le {A : Type} [LinearOrder A] [Finite A] [Nonempty A] : bitRank tagTupleLe SatPosn posEnd ≤ Nat.card A + 1

A sweep is short. Only the left marker and the cells lie below the right marker, so a sweep of the tape takes about as many steps as the instance has elements – not as many as the tape has positions, which is what makes the run fit the budget. Proved by injecting into Option A rather than by counting.

theorem DescriptiveComplexity.exists_satNextCl {A : Type} [FirstOrder.Language.sat.Structure A] [LinearOrder A] [Finite A] {c : A} (hc : SatCl c) (hnmax : ¬SatMaxCl c) : ∃ (c' : A), SatNextCl c c'

Every clause but the last has a next one. The clause the machine turns to is the least one above the current one, which is what DescriptiveComplexity.SatNextCl asserts.

theorem DescriptiveComplexity.ncard_clauses_next {A : Type} [FirstOrder.Language.sat.Structure A] [LinearOrder A] [Finite A] {c c' : A} (hnext : SatNextCl c c') : {e : A | SatCl e ∧ c ≤ e}.ncard = {e : A | SatCl e ∧ c' ≤ e}.ncard + 1

Passing to the next clause removes exactly one clause from the ones still to be checked.

theorem DescriptiveComplexity.accepts_from_chk {A : Type} [FirstOrder.Language.sat.Structure A] [LinearOrder A] [Finite A] [Nonempty A] (ν : A → Bool) (hsat : ∀ (e : A), SatCl e → ∃ (y : A), SatLit e y (ν y)) (c : A) : SatCl c → (∃ (n : ℕ) (cfin : Config (SatV A)), n ≤ {e : A | SatCl e ∧ c ≤ e}.ncard * bitRank tagTupleLe SatPosn posEnd ∧ (satMachine A).StepsIn n (confChkL ν c (posCell topA)) cfin ∧ SatAcc cfin.state) ∧ ∃ (n : ℕ) (cfin : Config (SatV A)), n ≤ {e : A | SatCl e ∧ c ≤ e}.ncard * bitRank tagTupleLe SatPosn posEnd ∧ (satMachine A).StepsIn n (confChkR ν c (posCell botA)) cfin ∧ SatAcc cfin.state

The machine checks every remaining clause and accepts, in at most one sweep's worth of steps per clause. Induction along the clauses from c upwards: if c is the last one the machine accepts at the marker it reaches, and otherwise it turns to the next clause, reversing direction – which is why the statement carries both orientations at once.

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

The machine is well formed, which is all of DescriptiveComplexity.TMData.WellFormed – the order is linear, there is a position, the input is functional and the blank is unique. Every conjunct was proved on the tape layer, before any transition existed.

Correctness, the chaining half

theorem DescriptiveComplexity.satMachine_accepts_of_sat {A : Type} [FirstOrder.Language.sat.Structure A] [LinearOrder A] [Finite A] [Nonempty A] (ν : A → Bool) (hsat : ∀ (e : A), SatCl e → ∃ (y : A), SatLit e y (ν y)) : (satMachine A).Accepts

A satisfying assignment makes the machine accept, within the budget. The run is the guess sweep, the turn into the lowest clause, and one sweep per clause; its length is at most (m + 1) · (n + 2) steps for n elements and m clauses, which DescriptiveComplexity.sat_budget puts strictly below the number of filler positions alone.

Correctness, from an accepting run to an assignment

By design, the machine branches only at the guess, so an accepting run is the intended run of the assignment it wrote, and the flag conditions along it force every clause to be satisfied. The analysis is one induction on the length of the run, with one case per tag of the head position. At each non-guess configuration the transition that fired is identified through its tag – a decide over the finite tag type – and the actual step is equated with the intended one by DescriptiveComplexity.step_functional_off_guess; at a guess configuration the transition itself says which value was written.

theorem DescriptiveComplexity.trTag_guess_sU (t : SatTag) : isTrTag t = true → stateTag t = SatTag.qGuess → readTag t = SatTag.sU → ∃ (v : Bool), t = SatTag.tGuessVal v

In the guessing state over an unassigned cell, only a guess write can fire.

theorem DescriptiveComplexity.trTag_guess_sEnd (t : SatTag) : isTrTag t = true → stateTag t = SatTag.qGuess → readTag t = SatTag.sEnd → t = SatTag.tGuessEndAcc ∨ t = SatTag.tGuessEndChk

In the guessing state over the right marker, only the two turns out of the guess phase can fire.

theorem DescriptiveComplexity.trTag_chk_sStart (t : SatTag) (f d : Bool) : isTrTag t = true → stateTag t = SatTag.qChk f d → readTag t = SatTag.sStart → f = true ∧ d = false ∧ (t = SatTag.tTurnNext false ∨ t = SatTag.tTurnAcc false)

In a check state over the left marker, only a leftward turn can fire, and only with the flag set.

theorem DescriptiveComplexity.trTag_chk_sEnd (t : SatTag) (f d : Bool) : isTrTag t = true → stateTag t = SatTag.qChk f d → readTag t = SatTag.sEnd → f = true ∧ d = true ∧ (t = SatTag.tTurnNext true ∨ t = SatTag.tTurnAcc true)

In a check state over the right marker, only a rightward turn can fire, and only with the flag set.

theorem DescriptiveComplexity.trTag_read_ne_sBlank (t : SatTag) : isTrTag t = true → readTag t ≠ SatTag.sBlank

No transition reads the blank symbol: the head never leaves the bracketed tape, so a run that somehow stood on a filler could not move.

theorem DescriptiveComplexity.guessTape_congr {A : Type} [LinearOrder A] [Finite A] [Nonempty A] {ν ν' : A → Bool} {p : SatV A} (h : ∀ (y : A), tagTupleLe (posCell y) p → posCell y ≠ p → ν y = ν' y) (r : SatV A) : guessTape ν p r = guessTape ν' p r

Changing the assignment anywhere but strictly below the head leaves the guess tape unchanged: only the cells already passed read it.

theorem DescriptiveComplexity.isInit_eq_confGuess {A : Type} [FirstOrder.Language.sat.Structure A] [LinearOrder A] [Finite A] [Nonempty A] {c : Config (SatV A)} (h : (satMachine A).IsInit c) (ν : A → Bool) : c = confGuess ν posStart

The initial configuration is unique: the start state and the lowest position are pinned, and the initial tape is functional, so any initial configuration starts a guess run – of every assignment at once, no cell of the guess tape at the left marker reading the assignment at all.

theorem DescriptiveComplexity.sat_of_chk {A : Type} [FirstOrder.Language.sat.Structure A] [LinearOrder A] [Finite A] [Nonempty A] (k : ℕ) : (∀ (ν : A → Bool) (c : A) (p : SatV A) (cfin : Config (SatV A)), SatCl c → SatPosn p → (satMachine A).StepsIn k (confChkL ν c p) cfin → SatAcc cfin.state → ∀ (e : A), SatCl e → c ≤ e → ∃ (y : A), SatLit e y (ν y)) ∧ ∀ (ν : A → Bool) (c : A) (p : SatV A) (cfin : Config (SatV A)), SatCl c → SatPosn p → (satMachine A).StepsIn k (confChkR ν c p) cfin → SatAcc cfin.state → ∀ (e : A), SatCl e → c ≤ e → ∃ (y : A), SatLit e y (ν y)

The check-phase analysis, both directions at once: an accepting run from a check configuration forces every clause from the current one upwards to be satisfied. The only live positions are the cells – where the step is pinned by determinism and the sweep continues – and the marker the sweep is headed to, where the transition that fired says the flag was set, hence the clause satisfied, and either names the next clause or certifies this one was last.

theorem DescriptiveComplexity.sat_of_guess {A : Type} [FirstOrder.Language.sat.Structure A] [LinearOrder A] [Finite A] [Nonempty A] (k : ℕ) (ν : A → Bool) (p : SatV A) (cfin : Config (SatV A)) : SatPosn p → tagTupleLe p posEnd → (satMachine A).StepsIn k (confGuess ν p) cfin → SatAcc cfin.state → ∃ (ν' : A → Bool), ∀ (e : A), SatCl e → ∃ (y : A), SatLit e y (ν' y)

The guess-phase analysis: an accepting run from a guess configuration yields a satisfying assignment. Walking the guess sweep, the assignment is rebuilt one cell at a time from the values the run chose to write; at the right marker the run either accepts – no clause exists – or enters the check phase, where DescriptiveComplexity.sat_of_chk takes over.

The machine accepts exactly the satisfiable instances

theorem DescriptiveComplexity.satisfiable_iff_exists_bool {A : Type} [FirstOrder.Language.sat.Structure A] : Satisfiable A ↔ ∃ (ν : A → Bool), ∀ (e : A), SatCl e → ∃ (y : A), SatLit e y (ν y)

Satisfiability with a Bool-valued assignment, the form the machine manipulates.

theorem DescriptiveComplexity.satMachine_accepts_iff_satisfiable {A : Type} [FirstOrder.Language.sat.Structure A] [LinearOrder A] [Finite A] [Nonempty A] : (satMachine A).Accepts ↔ Satisfiable A

Correctness of the machine of a CNF formula: it accepts – within the budget – exactly the satisfiable instances.