The game, read back

The backward simulation of the game itself: a winning configuration of the machine is a winning state of the game. It is one induction on DescriptiveComplexity.ATMData.AltWin, whose motive is a conjunction with one clause per phase the game proper can be in.

What each phase proves

The conclusions at play, splitEx and splitAll are all spec.Wins ρ, because what a split proves is exactly the premises of the matching constructor of DescriptiveComplexity.SOGameSpec.Wins. The others are the DescriptiveComplexity.ContGoal a sweep's continuation names:

start   ⟶ IsStart ρ ∧ Wins ρ            certify ⟶ Move ρ σ
exMove  ⟶ Move ρ σ ∧ Wins σ             allMove ⟶ ¬ Move ρ σ ∨ Wins σ

In each case of the induction most clauses are one line: at acc no phase of the game is accepting, and at ex/all the clauses of the other polarity are killed by IsUniv.

The one trap, and the motive that avoids it

A universal sweep cannot be read backwards: its clause is every candidate is answered, and at a half-finished sweep that is false – the cells already written cannot be changed. So the motive is strengthened to

Sound c : for every d reachable from c by steps whose sources are universal sweeps, the clauses hold at d.

The clauses at c follow by the reflexive chain, and in the all case the chain's first step is a successor, so the induction hypothesis covers the rest of it. That lets the universal sweep be proved forward: its run supplies the chain, the handover the last step, and the motive delivers the clauses at the rewind configuration – whose clause is the ContGoal wanted.

def DescriptiveComplexity.WalkCfg {B : SOBlock} {V M : ℕ} {A : Type} [LinearOrder A] (a₀ : A) (hdim : blockArityBound B ≤ gameDim B V) (vars : GameQuestion → ℕ) (ρ σ : B.Assignment A) (p : MachPh V M) (c : Config (GamePt B V M A)) : Prop

A configuration in the middle of a walk: the phase at the constant valuation, the head anywhere among the positions, and the tape holding the two assignments. Unlike DescriptiveComplexity.CtrlCfg it does not pin the head to a sentinel, which is exactly what a rewind needs.

Equations

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

def DescriptiveComplexity.ContGoal {L : FirstOrder.Language} (spec : SOGameSpec L) {A : Type} [L.Structure A] [LinearOrder A] (cont : SweepCont) (r : Bool) (ρ σ : spec.B.Assignment A) : Prop

What a sweep's continuation has to prove, one clause per place the control guesses an assignment.

Equations

• DescriptiveComplexity.ContGoal spec DescriptiveComplexity.SweepCont.start r ρ σ = (spec.IsStart (bif r then σ else ρ) ∧ spec.Wins (bif r then σ else ρ))
• DescriptiveComplexity.ContGoal spec DescriptiveComplexity.SweepCont.exMove r ρ σ = (spec.Move (bif r then σ else ρ) (bif !r then σ else ρ) ∧ spec.Wins (bif !r then σ else ρ))
• DescriptiveComplexity.ContGoal spec DescriptiveComplexity.SweepCont.certify r ρ σ = spec.Move (bif r then σ else ρ) (bif !r then σ else ρ)
• DescriptiveComplexity.ContGoal spec DescriptiveComplexity.SweepCont.allMove r ρ σ = (¬spec.Move (bif r then σ else ρ) (bif !r then σ else ρ) ∨ spec.Wins (bif !r then σ else ρ))

structure DescriptiveComplexity.GameStmt {L : FirstOrder.Language} (spec : SOGameSpec L) {V M : ℕ} (prog : GameProg (L.sum FirstOrder.Language.order) spec.B V M) {A : Type} [L.Structure A] [LinearOrder A] (a₀ : A) (hdim : blockArityBound spec.B ≤ gameDim spec.B V) (d : Config (GamePt spec.B V M A)) : Prop

What a win proves, phase by phase.

• play (ρ₀ σ₀ : spec.B.Assignment A) (r par : Bool) : CtrlCfg a₀ hdim prog.vars ρ₀ σ₀ (MachPh.playPh r par) (fun (x : Fin (gameDim spec.B V)) => a₀) d → spec.Wins (bif r then σ₀ else ρ₀)

  A position of the game is winning.

• splitEx (ρ₀ σ₀ : spec.B.Assignment A) (r par : Bool) : CtrlCfg a₀ hdim prog.vars ρ₀ σ₀ (MachPh.splitExPh r par) (fun (x : Fin (gameDim spec.B V)) => a₀) d → spec.Wins (bif r then σ₀ else ρ₀)

  So is the existential clause.

• splitAll (ρ₀ σ₀ : spec.B.Assignment A) (r par : Bool) : CtrlCfg a₀ hdim prog.vars ρ₀ σ₀ (MachPh.splitAllPh r par) (fun (x : Fin (gameDim spec.B V)) => a₀) d → spec.Wins (bif r then σ₀ else ρ₀)

  And the universal one.

• splitMove (ρ₀ σ₀ : spec.B.Assignment A) (r par : Bool) : CtrlCfg a₀ hdim prog.vars ρ₀ σ₀ (MachPh.splitMovePh r par) (fun (x : Fin (gameDim spec.B V)) => a₀) d → ContGoal spec SweepCont.exMove r ρ₀ σ₀

  After an existential move: it is legal, and the play goes on.

• allStep (ρ₀ σ₀ : spec.B.Assignment A) (r par : Bool) : CtrlCfg a₀ hdim prog.vars ρ₀ σ₀ (MachPh.allStepPh r par) (fun (x : Fin (gameDim spec.B V)) => a₀) d → ContGoal spec SweepCont.allMove r ρ₀ σ₀

  After a universal move: it is refuted, or the play goes on.

• splitStart (ρ₀ σ₀ : spec.B.Assignment A) (r par : Bool) : CtrlCfg a₀ hdim prog.vars ρ₀ σ₀ (MachPh.splitStartPh r par) (fun (x : Fin (gameDim spec.B V)) => a₀) d → ContGoal spec SweepCont.start r ρ₀ σ₀

  At the start: the position starts the game, and wins it.

• rewind (ρ₀ σ₀ : spec.B.Assignment A) (r tgt : Bool) (cont : SweepCont) (par : Bool) : WalkCfg a₀ hdim prog.vars ρ₀ σ₀ (MachPh.rewindPh r tgt cont par) d → ContGoal spec cont r ρ₀ σ₀

  A rewind proves what its continuation must.

• sweepEx (ρ₀ σ₀ : spec.B.Assignment A) (r tgt : Bool) (cont : SweepCont) (par : Bool) : cont ≠ SweepCont.allMove → SweptCfg a₀ hdim prog.vars ρ₀ σ₀ tgt (MachPh.sweepPh r tgt cont par) d → ∃ (ρ' : spec.B.Assignment A) (σ' : spec.B.Assignment A), (∀ (rr : Bool), rr ≠ tgt → (bif rr then σ' else ρ') = bif rr then σ₀ else ρ₀) ∧ ContGoal spec cont r ρ' σ'

  An existential sweep proves it for some assignment of its region.

• sweepAll (ρ₀ σ₀ : spec.B.Assignment A) (r tgt par : Bool) : SweptCfg a₀ hdim prog.vars ρ₀ σ₀ tgt (MachPh.sweepPh r tgt SweepCont.allMove par) d → d.head = leftPt a₀ par → ∀ (ρ' σ' : spec.B.Assignment A), (∀ (rr : Bool), rr ≠ tgt → (bif rr then σ' else ρ') = bif rr then σ₀ else ρ₀) → ContGoal spec SweepCont.allMove r ρ' σ'

  A universal sweep proves it for every assignment of its region – but only at its entry, the head on the sentinel its parity names.

Small conversions between the three shapes of a configuration

theorem DescriptiveComplexity.WalkCfg.of_ctrlCfg {L : FirstOrder.Language} {spec : SOGameSpec L} {V M : ℕ} {prog : GameProg (L.sum FirstOrder.Language.order) spec.B V M} {A : Type} [LinearOrder A] {a₀ : A} {hdim : blockArityBound spec.B ≤ gameDim spec.B V} {ρ₀ σ₀ : spec.B.Assignment A} {p : MachPh V M} {d : Config (GamePt spec.B V M A)} (h₀ : IsBot a₀) (h : CtrlCfg a₀ hdim prog.vars ρ₀ σ₀ p (fun (x : Fin (gameDim spec.B V)) => a₀) d) : WalkCfg a₀ hdim prog.vars ρ₀ σ₀ p d

theorem DescriptiveComplexity.CtrlCfg.of_walkCfg {L : FirstOrder.Language} {spec : SOGameSpec L} {V M : ℕ} {prog : GameProg (L.sum FirstOrder.Language.order) spec.B V M} {A : Type} [LinearOrder A] {a₀ : A} {hdim : blockArityBound spec.B ≤ gameDim spec.B V} {ρ₀ σ₀ : spec.B.Assignment A} {p : MachPh V M} {d : Config (GamePt spec.B V M A)} (h₀ : IsBot a₀) (h : WalkCfg a₀ hdim prog.vars ρ₀ σ₀ p d) (hhead : d.head = leftPt a₀ p.par) : CtrlCfg a₀ hdim prog.vars ρ₀ σ₀ p (fun (x : Fin (gameDim spec.B V)) => a₀) d

theorem DescriptiveComplexity.SweptCfg.of_ctrlCfg {L : FirstOrder.Language} {spec : SOGameSpec L} {V M : ℕ} {prog : GameProg (L.sum FirstOrder.Language.order) spec.B V M} {A : Type} [LinearOrder A] {a₀ : A} {hdim : blockArityBound spec.B ≤ gameDim spec.B V} {ρ₀ σ₀ : spec.B.Assignment A} {tgt : Bool} {p : MachPh V M} {d : Config (GamePt spec.B V M A)} (h₀ : IsBot a₀) (h : CtrlCfg a₀ hdim prog.vars ρ₀ σ₀ p (fun (x : Fin (gameDim spec.B V)) => a₀) d) : SweptCfg a₀ hdim prog.vars ρ₀ σ₀ tgt p d

The three cases of the induction

The induction, and the entry

theorem DescriptiveComplexity.altAcceptsSpace_iff_accepts {L : FirstOrder.Language} {spec : SOGameSpec L} {V M : ℕ} {prog : GameProg (L.sum FirstOrder.Language.order) spec.B V M} {A : Type} [L.Structure A] [LinearOrder A] [Finite A] {a₀ : A} {hdim : blockArityBound spec.B ≤ gameDim spec.B V} (h₀ : IsBot a₀) (hplays : ∀ (q : GameQuestion), (prog.data q).Plays (spec.question q)) : (gameMachine prog.vars prog.pol a₀ hdim (gameRule prog.vars prog.natoms prog.concOk prog.isTarget)).AltAcceptsSpace true ↔ spec.Accepts A

The machine accepts exactly when the game does. Both halves of the simulation, in one statement – and the whole of what SO-GAME ≤ʳᶠᵒ[≤] ATMAcceptSpace needs of the machine.