A question, read back

The mirror of DescriptiveComplexity.GameProg.altWin_ask: if the machine wins from the entry of a question's prefix, the question holds.

What the bridge has to say, backwards

• an arrival is a correct claim. DescriptiveComplexity.SeekArrives gives a cell whose symbol answered the test; unfolding DescriptiveComplexity.GameProg.isTarget says the symbol's bit is the claim, its region is the one the atom's copy names, and its address is the atom's arguments at the valuation. Since the tape's cell carries the bit the assignment gives it, the claim is right – and the region bookkeeping is DescriptiveComplexity.GameProg.cond_copy again, read the other way;
• the seek's test never fires on a mark, which the parametric layer had to assume and the program discharges by unfolding one existential;
• the tuple SeekArrives carries is not the one the forward direction builds, so the address it names has to be recovered from argsOf and the agreement with the phase's valuation – which is the only place the two halves of a transition's tuple are pulled apart backwards.

theorem DescriptiveComplexity.GameProg.not_isTarget_mark {K : FirstOrder.Language} {B : SOBlock} {V M : ℕ} {prog : GameProg K B V M} {A : Type} (p : MachPh V M) (b : Bool) (w : Fin (gameDim B V) → A) : ¬prog.isTarget p (SymTag.mark b) w

The seek's test never fires on a mark: it asks for the symbol of a cell, which a sentinel's mark is not.

theorem DescriptiveComplexity.GameProg.concOk_congr {K : FirstOrder.Language} {B : SOBlock} {V M : ℕ} {prog : GameProg K B V M} {A : Type} [K.Structure A] {p : MachPh V M} {w vv : Fin (gameDim B V) → A} (hp : p.kind = PhKind.conc) (hag : Agree (MachPh.arity prog.vars p) w vv) (h : prog.concOk p w) : prog.concOk p vv

The guard of a concluding transition reads only the valuation the phase declares.

theorem DescriptiveComplexity.GameProg.holds_of_seekArrives {K : FirstOrder.Language} {B : SOBlock} {V M : ℕ} {prog : GameProg K B V M} {A : Type} [LinearOrder A] {a₀ : A} {hdim : blockArityBound B ≤ gameDim B V} {ρ σ : B.Assignment A} (q : GameQuestion) (r par : Bool) {b : Fin M → Bool} {vv : Fin (gameDim B V) → A} {k : Fin (M + 1)} (hk : ↑k < (prog.data q).natoms) {pos : GamePt B V M A} (harr : SeekArrives a₀ prog.isTarget prog.vars (MachPh.seekPh q r b k par) vv (tapeOfAssign a₀ hdim ρ σ) pos) : b (Fin.castLE ⋯ ⟨↑k, hk⟩) = true ↔ ((prog.data q).atoms ⟨↑k, hk⟩).Holds (bif r then σ else ρ) (bif !r then σ else ρ) (prog.valOf q vv)

An arrival is a correct claim. The cell the seek stopped at holds the atom the challenge named, its bit is the one that was claimed, and the tape gives that bit by the assignment of the region the atom's copy points to.

theorem DescriptiveComplexity.GameProg.matrixHolds_of_altWin {K : FirstOrder.Language} {B : SOBlock} {V M : ℕ} {prog : GameProg K B V M} {A : Type} [K.Structure A] [LinearOrder A] {a₀ : A} {hdim : blockArityBound B ≤ gameDim B V} {ρ σ : B.Assignment A} (h₀ : IsBot a₀) {q : GameQuestion} {r par : Bool} {vv : Fin (gameDim B V) → A} {c : Config (GamePt B V M A)} (h : CtrlCfg a₀ hdim prog.vars ρ σ (MachPh.claimPh q r par) vv c) (hw : (gameMachine prog.vars prog.pol a₀ hdim (gameRule prog.vars prog.natoms prog.concOk prog.isTarget)).AltWin true c) : (prog.data q).MatrixHolds (bif r then σ else ρ) (bif !r then σ else ρ) (prog.valOf q vv)

The matrix holds, read back from a winning claim phase: the vector the existential player claimed is correct at every atom the universal player could have challenged, and the residue it leaves holds.

theorem DescriptiveComplexity.GameProg.ask_of_altWin {K : FirstOrder.Language} {B : SOBlock} {V M : ℕ} {prog : GameProg K B V M} {A : Type} [K.Structure A] [LinearOrder A] {a₀ : A} {hdim : blockArityBound B ≤ gameDim B V} {ρ σ : B.Assignment A} (h₀ : IsBot a₀) (q : GameQuestion) {φ : ((K.sum B.lang).sum B.lang).Sentence} (hplays : (prog.data q).Plays φ) {r par : Bool} {jj : Fin (V + 1)} (hjj : ↑jj = 0) {vv : Fin (gameDim B V) → A} {c : Config (GamePt B V M A)} (h : CtrlCfg a₀ hdim prog.vars ρ σ (MachPh.prePh q r jj par) vv c) (hw : (gameMachine prog.vars prog.pol a₀ hdim (gameRule prog.vars prog.natoms prog.concOk prog.isTarget)).AltWin true c) : A ⊨ φ

A question holds, read back: if the machine wins from the entry of a question's prefix, the question's sentence is true of the two assignments the tape carries. This is the converse of DescriptiveComplexity.GameProg.altWin_ask.