The intended run: the guessing sweeps

The k sweeps of the machine, run against a tuple of block assignments. The whole point is DescriptiveComplexity.valAfter: the truth value the cell of a variable holds once the sweeps below i have run is the disjunction, over the blocks below i marking it, of what they assigned it. At i = k that is DescriptiveComplexity.qbfVal on the nose (DescriptiveComplexity.valAfter_top), which is why one bit per cell suffices even though a variable may carry several block marks.

A sweep runs rightwards writing, turns at ⊣, runs back leftwards unchanged, and hands over at ⊢. The tape during the rightward pass is DescriptiveComplexity.sweepTape: cells strictly below the head already hold the new value, cells at or above still hold the old one. Junk cells – a cell's tag on a tuple that is not a position – are frozen at false, which is what DescriptiveComplexity.AltInp gives them and what the frame condition of every step then preserves.

The value a cell holds between sweeps

noncomputable def DescriptiveComplexity.AltQbf.valAfter {k : ℕ} {A : Type} [(FirstOrder.Language.qbf k).Structure A] (νs : Fin k → A → Prop) (i : ℕ) (x : A) : Bool

The truth value the cell of x holds once the sweeps below i have run.

Equations

• DescriptiveComplexity.AltQbf.valAfter νs i x = decide (∃ (j : Fin k), ↑j < i ∧ DescriptiveComplexity.AltQbf.QbfBlk j x ∧ νs j x)

theorem DescriptiveComplexity.AltQbf.valAfter_eq_true {k : ℕ} {A : Type} [(FirstOrder.Language.qbf k).Structure A] {νs : Fin k → A → Prop} {x : A} {i : ℕ} : valAfter νs i x = true ↔ ∃ (j : Fin k), ↑j < i ∧ QbfBlk j x ∧ νs j x

Reading DescriptiveComplexity.valAfter back.

theorem DescriptiveComplexity.AltQbf.valAfter_zero {k : ℕ} {A : Type} [(FirstOrder.Language.qbf k).Structure A] {νs : Fin k → A → Prop} {x : A} : valAfter νs 0 x = false

theorem DescriptiveComplexity.AltQbf.valAfter_top {k : ℕ} {A : Type} [(FirstOrder.Language.qbf k).Structure A] {νs : Fin k → A → Prop} {x : A} : valAfter νs k x = true ↔ qbfVal νs x

After the last sweep a cell holds the truth value of its variable.

theorem DescriptiveComplexity.AltQbf.valAfter_succ_of_keep {k : ℕ} {A : Type} [(FirstOrder.Language.qbf k).Structure A] {νs : Fin k → A → Prop} {x : A} {i : ℕ} (h : ¬∃ (j : Fin k), ↑j = i ∧ QbfBlk j x ∧ νs j x) : valAfter νs (i + 1) x = valAfter νs i x

A sweep leaves a cell alone when its block does not set it.

theorem DescriptiveComplexity.AltQbf.valAfter_succ_of_set {k : ℕ} {A : Type} [(FirstOrder.Language.qbf k).Structure A] {νs : Fin k → A → Prop} {x : A} {i : ℕ} (h : ∃ (j : Fin k), ↑j = i ∧ QbfBlk j x ∧ νs j x) : valAfter νs (i + 1) x = true

A sweep sets a cell when its block marks the variable and assigns it true.

theorem DescriptiveComplexity.AltQbf.valAfter_mono {k : ℕ} {A : Type} [(FirstOrder.Language.qbf k).Structure A] {νs : Fin k → A → Prop} {x : A} {i i' : ℕ} (hle : i ≤ i') (h : valAfter νs i x = true) : valAfter νs i' x = true

The value of a cell never goes back down.

Changing one block's assignment

The read-off of a round replaces the assignment of the block that has just played, and leaves the others alone. These are the two facts that makes such a replacement invisible to the sweeps below it and exactly visible to its own.

theorem DescriptiveComplexity.AltQbf.valAfter_congr {k : ℕ} {A : Type} [(FirstOrder.Language.qbf k).Structure A] {x : A} {ρ σ : Fin k → A → Prop} {m : ℕ} (h : ∀ (j : Fin k), ↑j < m → (ρ j x ↔ σ j x)) : valAfter ρ m x = valAfter σ m x

Only the blocks below m matter to what a cell holds after m sweeps.

theorem DescriptiveComplexity.AltQbf.valAfter_update_le {k : ℕ} {A : Type} [(FirstOrder.Language.qbf k).Structure A] {νs : Fin k → A → Prop} {x : A} {i : Fin k} {ν' : A → Prop} {m : ℕ} (hm : m ≤ ↑i) : valAfter (Function.update νs i ν') m x = valAfter νs m x

Replacing block i's assignment does not change what the sweeps below it wrote.

theorem DescriptiveComplexity.AltQbf.valAfter_update_succ {k : ℕ} {A : Type} [(FirstOrder.Language.qbf k).Structure A] {νs : Fin k → A → Prop} {x : A} {i : Fin k} {ν' : A → Prop} : valAfter (Function.update νs i ν') (↑i + 1) x = true ↔ valAfter νs (↑i) x = true ∨ QbfBlk i x ∧ ν' x

Replacing block i's assignment changes exactly what its own sweep writes.

The tape between and during the sweeps

def DescriptiveComplexity.AltQbf.IsCellTup {k : ℕ} {A : Type} [LinearOrder A] (q : AltV k A) : Prop

Whether a tuple carrying a cell's tag is a real cell of the tape.

Equations

• DescriptiveComplexity.AltQbf.IsCellTup q = (↑q.1.2 = 0 ∧ ∀ (a : A), q.2 1 ≤ a)

noncomputable def DescriptiveComplexity.AltQbf.tapeAfter {k : ℕ} {A : Type} [(FirstOrder.Language.qbf k).Structure A] [LinearOrder A] [Finite A] [Nonempty A] (νs : Fin k → A → Prop) (i : ℕ) (q : AltV k A) : AltV k A

The tape once the sweeps below i have run: every real cell holds the value its variable has accumulated, the markers hold their own symbols, junk cells are frozen at false, and everything else reads blank.

Equations

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

noncomputable def DescriptiveComplexity.AltQbf.sweepTape {k : ℕ} {A : Type} [(FirstOrder.Language.qbf k).Structure A] [LinearOrder A] [Finite A] [Nonempty A] (νs : Fin k → A → Prop) (i : ℕ) (p q : AltV k A) : AltV k A

The tape during the rightward pass of the sweep of index i, with the head at p: a real cell strictly below the head already holds the new value.

Equations

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

theorem DescriptiveComplexity.AltQbf.sweepTape_posStart {k : ℕ} {A : Type} [(FirstOrder.Language.qbf k).Structure A] [LinearOrder A] [Finite A] [Nonempty A] (νs : Fin k → A → Prop) (i : ℕ) : sweepTape νs i posStart = tapeAfter νs i

At the left marker nothing has been written yet.

theorem DescriptiveComplexity.AltQbf.sweepTape_posEnd {k : ℕ} {A : Type} [(FirstOrder.Language.qbf k).Structure A] [LinearOrder A] [Finite A] [Nonempty A] (νs : Fin k → A → Prop) (i : ℕ) : sweepTape νs i posEnd = tapeAfter νs (i + 1)

At the right marker the sweep is over.

theorem DescriptiveComplexity.AltQbf.sweepTape_frame {k : ℕ} {A : Type} [(FirstOrder.Language.qbf k).Structure A] [LinearOrder A] [Finite A] [Nonempty A] (νs : Fin k → A → Prop) (i : ℕ) {p q r : AltV k A} (hsucc : SuccPos tagTupleLe AltPosn p q) (hr : r ≠ p) : sweepTape νs i q r = sweepTape νs i p r

The rightward pass 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.

The rightward pass

noncomputable def DescriptiveComplexity.AltQbf.confSweep {k : ℕ} {A : Type} [(FirstOrder.Language.qbf k).Structure A] [LinearOrder A] [Finite A] [Nonempty A] (νs : Fin k → A → Prop) (i : Fin (k + 1)) (p : AltV k A) : Config (AltV k A)

The configuration during the rightward pass of the sweep of index i.

Equations

• DescriptiveComplexity.AltQbf.confSweep νs i p = { state := DescriptiveComplexity.AltQbf.stG i true, head := p, tape := DescriptiveComplexity.AltQbf.sweepTape νs (↑i) p }

theorem DescriptiveComplexity.AltQbf.sweepTape_posCell_bot {k : ℕ} {A : Type} [(FirstOrder.Language.qbf k).Structure A] [LinearOrder A] [Finite A] [Nonempty A] (νs : Fin k → A → Prop) (i : ℕ) : sweepTape νs i (posCell qbotA) = tapeAfter νs i

At the first cell nothing has been written yet either: no cell is strictly below the cell of the least element.

theorem DescriptiveComplexity.AltQbf.tape_confSweep_bot {k : ℕ} {A : Type} [(FirstOrder.Language.qbf k).Structure A] [LinearOrder A] [Finite A] [Nonempty A] (νs : Fin k → A → Prop) (i : Fin (k + 1)) : (confSweep νs i (posCell qbotA)).tape = tapeAfter νs ↑i

A sweep starts from the tape the sweeps below it left.

theorem DescriptiveComplexity.AltQbf.isInit_confSweep {k : ℕ} {A : Type} [(FirstOrder.Language.qbf k).Structure A] [LinearOrder A] [Finite A] [Nonempty A] (νs : Fin k → A → Prop) (cnf : Bool) : (altMachine k A cnf).IsInit (confSweep νs 0 posStart)

The run starts at the first sweep.

theorem DescriptiveComplexity.AltQbf.sweepTape_at_head {k : ℕ} {A : Type} [(FirstOrder.Language.qbf k).Structure A] [LinearOrder A] [Finite A] [Nonempty A] {νs : Fin k → A → Prop} {i : ℕ} {p : AltV k A} (hp : AltPosn p) (hb : p.1.1 = AltBase.pCell) : sweepTape νs i p p = symV (valAfter νs i (p.2 0)) (p.2 0)

The value under the head is the old one.

theorem DescriptiveComplexity.AltQbf.sweepTape_written {k : ℕ} {A : Type} [(FirstOrder.Language.qbf k).Structure A] [LinearOrder A] [Finite A] [Nonempty A] {νs : Fin k → A → Prop} {i : ℕ} {p q : AltV k A} (hp : AltPosn p) (hb : p.1.1 = AltBase.pCell) (hsucc : SuccPos tagTupleLe AltPosn p q) : sweepTape νs i q p = symV (valAfter νs (i + 1) (p.2 0)) (p.2 0)

The value written under the head is the new one.

theorem DescriptiveComplexity.AltQbf.step_sweep {k : ℕ} {A : Type} [(FirstOrder.Language.qbf k).Structure A] [LinearOrder A] [Finite A] [Nonempty A] {νs : Fin k → A → Prop} {cnf : Bool} {i : Fin (k + 1)} (hi : ↑i < k) {p q : AltV k A} (hsucc : SuccPos tagTupleLe AltPosn p q) (hb : tagTupleLe q posEnd) (hstart : p.1.1 = AltBase.pStart → ↑i = 0) : (altMachine k A cnf).Step (confSweep νs i p) (confSweep νs i q)

One step of a rightward pass. At a cell the machine writes the value its block gives the variable – keeping the old one, or setting it – and moves on; at the left marker it steps over it.

theorem DescriptiveComplexity.AltQbf.steps_sweepR {k : ℕ} {A : Type} [(FirstOrder.Language.qbf k).Structure A] [LinearOrder A] [Finite A] [Nonempty A] {νs : Fin k → A → Prop} {cnf : Bool} {i : Fin (k + 1)} (hi : ↑i < k) : (altMachine k A cnf).StepsIn (bitRank tagTupleLe AltPosn posEnd - bitRank tagTupleLe AltPosn (posCell qbotA)) (confSweep νs i (posCell qbotA)) (confSweep νs i posEnd)

The whole rightward pass: from the first cell to the right marker, the sweep of index i writes its block's value in every cell.

theorem DescriptiveComplexity.AltQbf.step_sweepStart {k : ℕ} {A : Type} [(FirstOrder.Language.qbf k).Structure A] [LinearOrder A] [Finite A] [Nonempty A] {νs : Fin k → A → Prop} {cnf : Bool} (hk : 0 < k) : (altMachine k A cnf).Step (confSweep νs 0 posStart) (confSweep νs 0 (posCell qbotA))

The first sweep steps over the left marker. Later sweeps do not: they enter at the first cell, the handover at ⊢ having already moved the head.

The turn, the leftward pass and the handover

noncomputable def DescriptiveComplexity.AltQbf.confBack {k : ℕ} {A : Type} [(FirstOrder.Language.qbf k).Structure A] [LinearOrder A] [Finite A] [Nonempty A] (νs : Fin k → A → Prop) (i : Fin (k + 1)) (p : AltV k A) : Config (AltV k A)

The configuration during the leftward pass of the sweep of index i: the tape is the one the sweep has just finished writing, and does not change again.

Equations

• DescriptiveComplexity.AltQbf.confBack νs i p = { state := DescriptiveComplexity.AltQbf.stG i false, head := p, tape := DescriptiveComplexity.AltQbf.tapeAfter νs (↑i + 1) }

theorem DescriptiveComplexity.AltQbf.tapeAfter_posEnd {k : ℕ} {A : Type} [(FirstOrder.Language.qbf k).Structure A] [LinearOrder A] [Finite A] [Nonempty A] {νs : Fin k → A → Prop} (i : ℕ) : tapeAfter νs i posEnd = symEnd

The tape reads its own symbol at each marker.

theorem DescriptiveComplexity.AltQbf.tapeAfter_posStart {k : ℕ} {A : Type} [(FirstOrder.Language.qbf k).Structure A] [LinearOrder A] [Finite A] [Nonempty A] {νs : Fin k → A → Prop} (i : ℕ) : tapeAfter νs i posStart = symStart

The tape reads its own symbol at each marker.

theorem DescriptiveComplexity.AltQbf.tapeAfter_at_cell {k : ℕ} {A : Type} [(FirstOrder.Language.qbf k).Structure A] [LinearOrder A] [Finite A] [Nonempty A] {νs : Fin k → A → Prop} {m : ℕ} {p : AltV k A} (hp : AltPosn p) (hb : p.1.1 = AltBase.pCell) : tapeAfter νs m p = symV (valAfter νs m (p.2 0)) (p.2 0)

The tape reads a real cell as the value its variable has accumulated.

theorem DescriptiveComplexity.AltQbf.tapeAfter_posCell {k : ℕ} {A : Type} [(FirstOrder.Language.qbf k).Structure A] [LinearOrder A] [Finite A] [Nonempty A] {νs : Fin k → A → Prop} (i : ℕ) (x : A) : tapeAfter νs i (posCell x) = symV (valAfter νs i x) x

theorem DescriptiveComplexity.AltQbf.step_turnBack {k : ℕ} {A : Type} [(FirstOrder.Language.qbf k).Structure A] [LinearOrder A] [Finite A] [Nonempty A] {νs : Fin k → A → Prop} {cnf : Bool} {i : Fin (k + 1)} (hi : ↑i < k) : (altMachine k A cnf).Step (confSweep νs i posEnd) (confBack νs i (posCell qtopA))

The turn at the right marker: the sweep has written every cell and turns round.

theorem DescriptiveComplexity.AltQbf.step_back {k : ℕ} {A : Type} [(FirstOrder.Language.qbf k).Structure A] [LinearOrder A] [Finite A] [Nonempty A] {νs : Fin k → A → Prop} {cnf : Bool} {i : Fin (k + 1)} (hi : ↑i < k) {p q : AltV k A} (hsucc : SuccPos tagTupleLe AltPosn p q) (hlb : tagTupleLe posStart p) (hub : tagTupleLe q (posCell qtopA)) : (altMachine k A cnf).Step (confBack νs i q) (confBack νs i p)

One step of the leftward pass: the head steps back over a cell, changing nothing.

theorem DescriptiveComplexity.AltQbf.steps_back {k : ℕ} {A : Type} [(FirstOrder.Language.qbf k).Structure A] [LinearOrder A] [Finite A] [Nonempty A] {νs : Fin k → A → Prop} {cnf : Bool} {i : Fin (k + 1)} (hi : ↑i < k) : (altMachine k A cnf).StepsIn (bitRank tagTupleLe AltPosn (posCell qtopA) - bitRank tagTupleLe AltPosn posStart) (confBack νs i (posCell qtopA)) (confBack νs i posStart)

The whole leftward pass: from the last cell back to the left marker.

theorem DescriptiveComplexity.AltQbf.step_next {k : ℕ} {A : Type} [(FirstOrder.Language.qbf k).Structure A] [LinearOrder A] [Finite A] [Nonempty A] {νs : Fin k → A → Prop} {cnf : Bool} {i : Fin (k + 1)} (hi : ↑i + 1 < k) : (altMachine k A cnf).Step (confBack νs i posStart) (confSweep νs (i + 1) (posCell qbotA))

The handover to the next sweep: at the left marker the machine steps right into the first cell and the next block takes over.

theorem DescriptiveComplexity.AltQbf.step_toChk {k : ℕ} {A : Type} [(FirstOrder.Language.qbf k).Structure A] [LinearOrder A] [Finite A] [Nonempty A] {νs : Fin k → A → Prop} {cnf : Bool} {i : Fin (k + 1)} (hlast : ↑i + 1 = k) {c₀ : A} (hc₀ : QbfMinCl k c₀) : (altMachine k A cnf).Step (confBack νs i posStart) { state := stChk false true c₀, head := posCell qbotA, tape := tapeAfter νs k }

The handover to the check phase: after the last sweep the machine takes the lowest clause with an empty flag and sweeps rightwards.

theorem DescriptiveComplexity.AltQbf.step_toAcc {k : ℕ} {A : Type} [(FirstOrder.Language.qbf k).Structure A] [LinearOrder A] [Finite A] [Nonempty A] {νs : Fin k → A → Prop} {cnf : Bool} {i : Fin (k + 1)} (hlast : ↑i + 1 = k) (hcnf : cnf = true) (hno : ∀ (e : A), ¬QbfCl k e) : (altMachine k A cnf).Step (confBack νs i posStart) { state := stAcc, head := posCell qbotA, tape := tapeAfter νs k }

The handover to acceptance: an instance with no clause at all is vacuously satisfied by a conjunctive matrix, and the machine accepts.

One sweep, end to end

theorem DescriptiveComplexity.AltQbf.stepsIn_add {k : ℕ} {A : Type} {M : TMData (AltV k A)} {m n : ℕ} {c d e : Config (AltV k A)} : M.StepsIn m c d → M.StepsIn n d e → M.StepsIn (m + n) c e

Two runs compose. (DescriptiveComplexity.TMData.stepsIn_split is the converse; this direction is not in DescriptiveComplexity.Machines and could be hoisted there.)

noncomputable def DescriptiveComplexity.AltQbf.sweepLen (k : ℕ) (A : Type) [LinearOrder A] [Finite A] [Nonempty A] : ℕ

The number of steps a sweep takes: right to the marker, turn, back to the other marker, and over it.

Equations

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

theorem DescriptiveComplexity.AltQbf.steps_sweep {k : ℕ} {A : Type} [(FirstOrder.Language.qbf k).Structure A] [LinearOrder A] [Finite A] [Nonempty A] {νs : Fin k → A → Prop} {cnf : Bool} {i : Fin (k + 1)} (hi : ↑i + 1 < k) : (altMachine k A cnf).StepsIn (sweepLen k A) (confSweep νs i (posCell qbotA)) (confSweep νs (i + 1) (posCell qbotA))

The whole of sweep i, from the first cell to the first cell of the sweep that follows it: the round of block i is exactly this run.

theorem DescriptiveComplexity.AltQbf.steps_sweep_zero {k : ℕ} {A : Type} [(FirstOrder.Language.qbf k).Structure A] [LinearOrder A] [Finite A] [Nonempty A] {νs : Fin k → A → Prop} {cnf : Bool} (hk : 1 + 1 ≤ k) : (altMachine k A cnf).StepsIn (1 + sweepLen k A) (confSweep νs 0 posStart) (confSweep νs (0 + 1) (posCell qbotA))

The first sweep, which begins at the left marker.