The intended run: the guessing sweeps

The k sweeps of the machine, run against a tuple of block assignments. The whole point is DescriptiveComplexity.AltQbf.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 exactly (DescriptiveComplexity.AltQbf.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.AltQbf.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.AltQbf.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_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.

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_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.

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 }

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.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.

One sweep, end to end

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.