The machine of a second-order game

The alternating machine emitted by SO-GAME ≤ʳᶠᵒ[≤] ATMAcceptSpace, assembled on the tape of DescriptiveComplexity.Exponential.GameTape with the phases of DescriptiveComplexity.Exponential.GameCtrl.

The shape of a transition

A transition is an element of the emitted universe, so it carries a tag and a tuple. The tag is DescriptiveComplexity.TrTag: the phase it applies in, the phase it moves to, the symbol it reads, the symbol it writes, and its direction. The tuple carries, in one piece,

  coordinates 0 … V-1        the valuation of the question's variables
  coordinates V … V+a-1      the address of the cell the symbol sits in

which is what makes every relation of DescriptiveComplexity.TMData first-order and uniform:

• Src and Dst read the valuation, each up to the arity its own phase declares – so a step of the prefix, whose destination declares one more variable than its source, writes exactly one coordinate, and the existential quantification over transitions is the quantification over the value written;
• Read and Write read the address, and a symbol shape together with an address is a point (DescriptiveComplexity.symPt).

Everything specific to the machine is therefore confined to one predicate, the rule DescriptiveComplexity.TrTag → (Fin dim → A) → Prop saying which tagged transitions are real. This file takes it as a parameter and proves what does not depend on it: the two promises ATMAcceptSpace folds into its yes-instances.

The two promises are rule-independent

DescriptiveComplexity.TMData.WellFormed and DescriptiveComplexity.ATMData.BlocksSplit are proved here once and for all (DescriptiveComplexity.gameMachine_wellFormed, DescriptiveComplexity.gameMachine_blocksSplit), because neither mentions the transitions: the first is about the order, the positions, the input and the blank – all fixed by the layout – and the second is about the marks, which are DescriptiveComplexity.MachPh.IsUniv read off the phase.

Symbols, as a shape and an address

inductive DescriptiveComplexity.SymTag (B : SOBlock) : Type

The shape of a symbol: a sentinel's mark, or a cell's bit together with the region and relation variable of the cell it sits in. The address itself is carried by the transition's tuple, not by the shape.

• mark {B : SOBlock} (b : Bool) : SymTag B

  A sentinel's mark.

• val {B : SOBlock} (b r : Bool) (i : B.ι) : SymTag B

  The bit b in a cell of region r holding the relation variable i.

instance DescriptiveComplexity.SymTag.instFinite {B : SOBlock} : Finite (SymTag B)

The dimension, and the two halves of a tuple

noncomputable def DescriptiveComplexity.gameDim (B : SOBlock) (V : ℕ) : ℕ

The dimension of the emitted universe: room for the valuation of a question's variables, and for the address of a cell.

Equations

• DescriptiveComplexity.gameDim B V = V + DescriptiveComplexity.blockArityBound B

theorem DescriptiveComplexity.blockArityBound_le_gameDim (B : SOBlock) (V : ℕ) : blockArityBound B ≤ gameDim B V

theorem DescriptiveComplexity.le_gameDim (B : SOBlock) (V : ℕ) : V ≤ gameDim B V

noncomputable def DescriptiveComplexity.addrOf {B : SOBlock} {V : ℕ} {A : Type} (w : Fin (gameDim B V) → A) : Fin (blockArityBound B) → A

The address half of a transition's tuple.

Equations

• DescriptiveComplexity.addrOf w l = w ⟨V + ↑l, ⋯⟩

noncomputable def DescriptiveComplexity.argsOf {B : SOBlock} {A : Type} (i : B.ι) (ā : Fin (blockArityBound B) → A) : Fin (B.arity i) → A

The address a symbol shape reads, truncated to the arity of its relation variable.

Equations

• DescriptiveComplexity.argsOf i ā l = ā (Fin.castLE ⋯ l)

noncomputable def DescriptiveComplexity.joinTuple {B : SOBlock} {V : ℕ} {A : Type} (v : Fin V → A) (ā : Fin (blockArityBound B) → A) : Fin (gameDim B V) → A

The tuple of a transition, from the valuation it carries and the address it reads: the two halves, side by side.

Equations

• DescriptiveComplexity.joinTuple v ā k = if h : ↑k < V then v ⟨↑k, h⟩ else ā ⟨↑k - V, ⋯⟩

theorem DescriptiveComplexity.joinTuple_of_lt {B : SOBlock} {V : ℕ} {A : Type} (v : Fin V → A) (ā : Fin (blockArityBound B) → A) {k : Fin (gameDim B V)} (h : ↑k < V) : joinTuple v ā k = v ⟨↑k, h⟩

@[simp]

theorem DescriptiveComplexity.addrOf_joinTuple {B : SOBlock} {V : ℕ} {A : Type} (v : Fin V → A) (ā : Fin (blockArityBound B) → A) : addrOf (joinTuple v ā) = ā

noncomputable def DescriptiveComplexity.walkTuple {B : SOBlock} {V : ℕ} {A : Type} (v : Fin (gameDim B V) → A) (ā : Fin (blockArityBound B) → A) : Fin (gameDim B V) → A

The tuple a walk step carries: the valuation its phase already holds, and the address of the cell it is reading. The first half is what Src and Dst compare against the state, the second what Read and Write turn into a symbol.

Equations

• DescriptiveComplexity.walkTuple v ā = DescriptiveComplexity.joinTuple (DescriptiveComplexity.pref ⋯ v) ā

@[simp]

theorem DescriptiveComplexity.addrOf_walkTuple {B : SOBlock} {V : ℕ} {A : Type} (v : Fin (gameDim B V) → A) (ā : Fin (blockArityBound B) → A) : addrOf (walkTuple v ā) = ā

noncomputable def DescriptiveComplexity.truncTuple {A : Type} (a₀ : A) (m : ℕ) {D : ℕ} (w : Fin D → A) : Fin D → A

The valuation a phase keeps: the tuple of the transition entering it, truncated to the coordinates the phase declares and pinned to the minimum elsewhere. This is the destination state a control step builds – any tuple with the same two properties would do, and this is the canonical one.

Equations

• DescriptiveComplexity.truncTuple a₀ m w j = if ↑j < m then w j else a₀

theorem DescriptiveComplexity.agree_truncTuple {A : Type} (a₀ : A) (m : ℕ) {D : ℕ} (w : Fin D → A) : Agree m w (truncTuple a₀ m w)

@[simp]

theorem DescriptiveComplexity.truncTuple_zero {A : Type} (a₀ : A) {D : ℕ} (w : Fin D → A) : truncTuple a₀ 0 w = fun (x : Fin D) => a₀

A phase that declares nothing keeps the constant tuple.

theorem DescriptiveComplexity.eq_truncTuple {A : Type} [LinearOrder A] {a₀ : A} (h₀ : IsBot a₀) {m D : ℕ} {w x : Fin D → A} (hc : Canon m x) (ha : Agree m w x) : x = truncTuple a₀ m w

And it is the only such tuple: a state's tuple is determined by the transition that entered it, because the domain pins everything the phase does not declare.

noncomputable def DescriptiveComplexity.gameSymPt {B : SOBlock} {V : ℕ} {A : Type} (a₀ : A) {C : Type} (s : SymTag B) (ā : Fin (blockArityBound B) → A) : Pt B C (gameDim B V) A

A symbol shape at an address is a point.

Equations

• DescriptiveComplexity.gameSymPt a₀ (DescriptiveComplexity.SymTag.mark b) ā = DescriptiveComplexity.markPt a₀ b
• DescriptiveComplexity.gameSymPt a₀ (DescriptiveComplexity.SymTag.val b r i) ā = DescriptiveComplexity.valPt a₀ b r i (DescriptiveComplexity.argsOf i ā)

theorem DescriptiveComplexity.gameSymPt_val {B : SOBlock} {V : ℕ} {A : Type} (a₀ : A) {C : Type} (b r : Bool) (i : B.ι) (ā : Fin (blockArityBound B) → A) : gameSymPt a₀ (SymTag.val b r i) ā = valPt a₀ b r i (argsOf i ā)

theorem DescriptiveComplexity.gameSymPt_mark {B : SOBlock} {V : ℕ} {A : Type} (a₀ : A) {C : Type} (b : Bool) (ā : Fin (blockArityBound B) → A) : gameSymPt a₀ (SymTag.mark b) ā = markPt a₀ b

The tags of the machine

structure DescriptiveComplexity.TrTag (B : SOBlock) (V M : ℕ) : Type

The tag of a transition: where it applies, where it goes, what it reads and writes, and which way it moves.

• src : MachPh V M

  The phase the transition applies in.

• dst : MachPh V M

  The phase it moves to.

• rd : SymTag B

  The symbol it reads.

• wr : SymTag B

  The symbol it writes.

• right : Bool

  Whether it moves the head right.

instance DescriptiveComplexity.TrTag.instFinite {B : SOBlock} {V M : ℕ} : Finite (TrTag B V M)

@[reducible, inline]

abbrev DescriptiveComplexity.GameCtrlTag (B : SOBlock) (V M : ℕ) : Type

The control's tags: the phases, which are the states, and the rules, which are the transitions.

Equations

• DescriptiveComplexity.GameCtrlTag B V M = (DescriptiveComplexity.MachPh V M ⊕ DescriptiveComplexity.TrTag B V M)

@[reducible, inline]

abbrev DescriptiveComplexity.GameTag (B : SOBlock) (V M : ℕ) : Type

The tags of the emitted machine: the tape's, and the control's.

Equations

• DescriptiveComplexity.GameTag B V M = DescriptiveComplexity.MachTag B (DescriptiveComplexity.GameCtrlTag B V M)

noncomputable def DescriptiveComplexity.ctrlArity (vars : GameQuestion → ℕ) {B : SOBlock} {V M : ℕ} : GameCtrlTag B V M → ℕ

The coordinates a control tag uses: a phase declares its own, a transition uses the whole tuple.

Equations

• DescriptiveComplexity.ctrlArity vars = Sum.elim (DescriptiveComplexity.MachPh.arity vars) fun (x : DescriptiveComplexity.TrTag B V M) => DescriptiveComplexity.gameDim B V

The machine

@[reducible, inline]

abbrev DescriptiveComplexity.GamePt (B : SOBlock) (V M : ℕ) (A : Type) : Type

A point of the emitted universe.

Equations

• DescriptiveComplexity.GamePt B V M A = DescriptiveComplexity.Pt B (DescriptiveComplexity.GameCtrlTag B V M) (DescriptiveComplexity.gameDim B V) A

noncomputable def DescriptiveComplexity.phasePt {B : SOBlock} {V M : ℕ} {A : Type} (p : MachPh V M) (w : Fin (gameDim B V) → A) : GamePt B V M A

The point of a phase, at a given valuation.

Equations

• DescriptiveComplexity.phasePt p w = (Sum.inr (Sum.inl p), w)

noncomputable def DescriptiveComplexity.isUnivPt {B : SOBlock} {V M : ℕ} {A : Type} (pol : GameQuestion → ℕ → Bool) (p : GamePt B V M A) : Prop

A state belongs to the universal player exactly when its phase does.

Equations

• DescriptiveComplexity.isUnivPt pol p = match p.1 with | Sum.inr (Sum.inl ph) => DescriptiveComplexity.MachPh.IsUniv pol ph = true | x => False

def DescriptiveComplexity.startPh (V M : ℕ) : MachPh V M

The state the machine starts in: the initial sweep, writing region 0.

Equations

• DescriptiveComplexity.startPh V M = DescriptiveComplexity.MachPh.sweepPh false false DescriptiveComplexity.SweepCont.start false

noncomputable def DescriptiveComplexity.gameMachine {B : SOBlock} {V M : ℕ} {A : Type} [LinearOrder A] (vars : GameQuestion → ℕ) (pol : GameQuestion → ℕ → Bool) (a₀ : A) (hdim : blockArityBound B ≤ gameDim B V) (rule : TrTag B V M → (Fin (gameDim B V) → A) → Prop) : ATMData (GamePt B V M A)

The machine of a second-order game, with its rules as a parameter.

Equations

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

The two promises

theorem DescriptiveComplexity.gameMachine_wellFormed {B : SOBlock} {V M : ℕ} {A : Type} [LinearOrder A] {vars : GameQuestion → ℕ} {pol : GameQuestion → ℕ → Bool} {a₀ : A} (hdim : blockArityBound B ≤ gameDim B V) (rule : TrTag B V M → (Fin (gameDim B V) → A) → Prop) (h₀ : IsBot a₀) : (gameMachine vars pol a₀ hdim rule).WellFormed

The machine is well formed, whatever its rules: the order is linear, there is a position, the input is functional and total, and there is exactly one blank.

theorem DescriptiveComplexity.gameMachine_blocksSplit {B : SOBlock} {V M : ℕ} {A : Type} [LinearOrder A] {vars : GameQuestion → ℕ} {pol : GameQuestion → ℕ → Bool} {a₀ : A} (hdim : blockArityBound B ≤ gameDim B V) (rule : TrTag B V M → (Fin (gameDim B V) → A) → Prop) : (gameMachine vars pol a₀ hdim rule).BlocksSplit

The two marks split the states, whatever the rules: a point is universal exactly when it is a state whose phase is.

The two ends, and what a position is

The rules

def DescriptiveComplexity.gameRule {B : SOBlock} {V M : ℕ} {A : Type} (vars natoms : GameQuestion → ℕ) (concOk : MachPh V M → (Fin (gameDim B V) → A) → Prop) (isTarget : MachPh V M → SymTag B → (Fin (gameDim B V) → A) → Prop) (t : TrTag B V M) (w : Fin (gameDim B V) → A) : Prop

The rules of the machine, all nine families.

Two of them are still parameters, and for the same reason the rules themselves were one: they are the only places where the machine consults the source structure rather than its own tape.

• concOk is the guard of a concluding transition – the residual formula of DescriptiveComplexity.QuestionData, which mentions no block atom and is therefore a first-order condition on the valuation;
• isTarget is the test a seek makes at a cell: is the symbol I am reading the one the challenged atom addresses, carrying the bit that was claimed? Both the address and the claim come from the phase and the tuple.

The control's own steps (family A) are DescriptiveComplexity.MachPh.CtrlStep, which is False at every walk phase, so no family overlaps another except where the design means it to: family C at a cell of the swept region, where the two choices of the written bit are the guess.

Equations

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

The machine of a specification

structure DescriptiveComplexity.GameProg (K : FirstOrder.Language) (B : SOBlock) (V M : ℕ) : Type

What a machine needs to know about a specification: one DescriptiveComplexity.QuestionData per question, and the two bounds that let the phases carry a common prefix index and a common claim vector. Nothing is padded – each question keeps its own vars and natoms, and the tuples are restricted with Fin.castLE.

• data : GameQuestion → QuestionData K B

  The machine-ready form of each of the six questions.

• vars_le (q : GameQuestion) : (self.data q).vars ≤ V

  Every question's prefix fits in the phase's index.

• natoms_le (q : GameQuestion) : (self.data q).natoms ≤ M

  Every question's atoms fit in the phase's claim vector.

def DescriptiveComplexity.GameProg.vars {K : FirstOrder.Language} {B : SOBlock} {V M : ℕ} (prog : GameProg K B V M) : GameQuestion → ℕ

The length of each question's prefix.

Equations

• prog.vars q = (prog.data q).vars

def DescriptiveComplexity.GameProg.natoms {K : FirstOrder.Language} {B : SOBlock} {V M : ℕ} (prog : GameProg K B V M) : GameQuestion → ℕ

The number of block atoms in each question's matrix.

Equations

• prog.natoms q = (prog.data q).natoms

def DescriptiveComplexity.GameProg.pol {K : FirstOrder.Language} {B : SOBlock} {V M : ℕ} (prog : GameProg K B V M) : GameQuestion → ℕ → Bool

Whose turn each prefix variable is.

Equations

• prog.pol q = (prog.data q).pol

theorem DescriptiveComplexity.GameProg.vars_le_gameDim {K : FirstOrder.Language} {B : SOBlock} {V M : ℕ} (prog : GameProg K B V M) (q : GameQuestion) : (prog.data q).vars ≤ gameDim B V

noncomputable def DescriptiveComplexity.GameProg.valOf {K : FirstOrder.Language} {B : SOBlock} {V M : ℕ} (prog : GameProg K B V M) {A : Type} (q : GameQuestion) (w : Fin (gameDim B V) → A) : Fin (prog.data q).vars → A

The valuation a tuple gives the variables of a question.

Equations

• prog.valOf q w l = w (Fin.castLE ⋯ l)

def DescriptiveComplexity.GameProg.concOk {K : FirstOrder.Language} {B : SOBlock} {V M : ℕ} (prog : GameProg K B V M) {A : Type} [K.Structure A] (p : MachPh V M) (w : Fin (gameDim B V) → A) : Prop

The guard of a concluding transition: the residual formula of the question, under the claims the phase carries, read at the valuation the tuple carries. It mentions no block atom, so it is a condition on the source structure – written by the interpretation, never computed by the machine.

Equations

• prog.concOk p w = ((prog.data p.q).sub fun (j : Fin (prog.data p.q).natoms) => p.claims (Fin.castLE ⋯ j)).Realize default (prog.valOf p.q w)

def DescriptiveComplexity.GameProg.isTarget {K : FirstOrder.Language} {B : SOBlock} {V M : ℕ} (prog : GameProg K B V M) {A : Type} (p : MachPh V M) (s : SymTag B) (w : Fin (gameDim B V) → A) : Prop

The test a seek makes at a cell: is the symbol I am reading the one the challenged atom addresses, carrying the bit that was claimed? The region and the relation variable are named by the atom – the copy being read against the region the game sits in – and the address is the atom's arguments applied to the valuation.

Equations

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

noncomputable def DescriptiveComplexity.GameProg.machine {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) : ATMData (GamePt B V M A)

The machine of a specification, complete: the layout, the control, the nine rule families, and the two guards that read the source structure.

Equations

• prog.machine a₀ hdim = DescriptiveComplexity.gameMachine prog.vars prog.pol a₀ hdim (DescriptiveComplexity.gameRule prog.vars prog.natoms prog.concOk prog.isTarget)

Reading a step off its transition

def DescriptiveComplexity.trPt {B : SOBlock} {V M : ℕ} {A : Type} (t : TrTag B V M) (w : Fin (gameDim B V) → A) : GamePt B V M A

The point of a transition: its tag, and its tuple.

Equations

• DescriptiveComplexity.trPt t w = (Sum.inr (Sum.inr t), w)

theorem DescriptiveComplexity.tag_inj {B : SOBlock} {V M : ℕ} {A : Type} {t t' : TrTag B V M} {w : Fin (gameDim B V) → A} (h : (trPt t w).1 = Sum.inr (Sum.inr t')) : t' = t

@[simp]

theorem DescriptiveComplexity.tr_trPt {B : SOBlock} {V M : ℕ} {A : Type} [LinearOrder A] {vars : GameQuestion → ℕ} {pol : GameQuestion → ℕ → Bool} {a₀ : A} {hdim : blockArityBound B ≤ gameDim B V} {rule : TrTag B V M → (Fin (gameDim B V) → A) → Prop} (t : TrTag B V M) (w : Fin (gameDim B V) → A) : (gameMachine vars pol a₀ hdim rule).Tr (trPt t w) ↔ rule t w

@[simp]

theorem DescriptiveComplexity.right_trPt {B : SOBlock} {V M : ℕ} {A : Type} [LinearOrder A] {vars : GameQuestion → ℕ} {pol : GameQuestion → ℕ → Bool} {a₀ : A} {hdim : blockArityBound B ≤ gameDim B V} {rule : TrTag B V M → (Fin (gameDim B V) → A) → Prop} (t : TrTag B V M) (w : Fin (gameDim B V) → A) : (gameMachine vars pol a₀ hdim rule).Right (trPt t w) ↔ t.right = true

@[simp]

theorem DescriptiveComplexity.read_trPt {B : SOBlock} {V M : ℕ} {A : Type} [LinearOrder A] {vars : GameQuestion → ℕ} {pol : GameQuestion → ℕ → Bool} {a₀ : A} {hdim : blockArityBound B ≤ gameDim B V} {rule : TrTag B V M → (Fin (gameDim B V) → A) → Prop} (t : TrTag B V M) (w : Fin (gameDim B V) → A) (x : GamePt B V M A) : (gameMachine vars pol a₀ hdim rule).Read (trPt t w) x ↔ x = gameSymPt a₀ t.rd (addrOf w)

@[simp]

theorem DescriptiveComplexity.write_trPt {B : SOBlock} {V M : ℕ} {A : Type} [LinearOrder A] {vars : GameQuestion → ℕ} {pol : GameQuestion → ℕ → Bool} {a₀ : A} {hdim : blockArityBound B ≤ gameDim B V} {rule : TrTag B V M → (Fin (gameDim B V) → A) → Prop} (t : TrTag B V M) (w : Fin (gameDim B V) → A) (x : GamePt B V M A) : (gameMachine vars pol a₀ hdim rule).Write (trPt t w) x ↔ x = gameSymPt a₀ t.wr (addrOf w)

@[simp]

theorem DescriptiveComplexity.src_trPt {B : SOBlock} {V M : ℕ} {A : Type} [LinearOrder A] {vars : GameQuestion → ℕ} {pol : GameQuestion → ℕ → Bool} {a₀ : A} {hdim : blockArityBound B ≤ gameDim B V} {rule : TrTag B V M → (Fin (gameDim B V) → A) → Prop} (t : TrTag B V M) (w : Fin (gameDim B V) → A) (q : GamePt B V M A) : (gameMachine vars pol a₀ hdim rule).Src (trPt t w) q ↔ q.1 = Sum.inr (Sum.inl t.src) ∧ Canon (MachPh.arity vars t.src) q.2 ∧ Agree (MachPh.arity vars t.src) w q.2

@[simp]

theorem DescriptiveComplexity.dst_trPt {B : SOBlock} {V M : ℕ} {A : Type} [LinearOrder A] {vars : GameQuestion → ℕ} {pol : GameQuestion → ℕ → Bool} {a₀ : A} {hdim : blockArityBound B ≤ gameDim B V} {rule : TrTag B V M → (Fin (gameDim B V) → A) → Prop} (t : TrTag B V M) (w : Fin (gameDim B V) → A) (q : GamePt B V M A) : (gameMachine vars pol a₀ hdim rule).Dst (trPt t w) q ↔ q.1 = Sum.inr (Sum.inl t.dst) ∧ Canon (MachPh.arity vars t.dst) q.2 ∧ Agree (MachPh.arity vars t.dst) w q.2

Building one step

What a walk may do

The two steps of a sweep

A walk along the positions

The induction the three walks run on, stated for an arbitrary machine: each step moves the head to the neighboring position and preserves an invariant, so the walk reaches the end of the tape. The measure is DescriptiveComplexity.bitRank, which increases by one along DescriptiveComplexity.SuccPos (DescriptiveComplexity.bitRank_succPos) and is bounded by the number of positions (DescriptiveComplexity.bitRank_lt_card), so nothing here depends on which position follows which – the successor is whatever the step produces. That is the payoff of §2.1a: a walk needs no address of its own.

What a walk has already passed

A walk's invariant has to say what it has already rewritten, and the only handle on that is the order: the cells strictly below the head. The two facts below are all it needs, and neither mentions the tape's layout – so the sweep's invariant never has to compare two cells, and the order on cells (cellPt r i ā against cellPt r' i' ā') does not have to be characterized at all.

The control's own step

The run of a sweep

theorem DescriptiveComplexity.sweep_run {B : SOBlock} {V M : ℕ} {A : Type} [LinearOrder A] [Finite A] {vars natoms : GameQuestion → ℕ} {pol : GameQuestion → ℕ → Bool} {a₀ : A} {hdim : blockArityBound B ≤ gameDim B V} {concOk : MachPh V M → (Fin (gameDim B V) → A) → Prop} {isTarget : MachPh V M → SymTag B → (Fin (gameDim B V) → A) → Prop} {r tgt : Bool} {cont : SweepCont} {par : Bool} (h₀ : IsBot a₀) {ρ σ ρ' σ' : B.Assignment A} (hkeep : ∀ (rr : Bool), rr ≠ tgt → (bif rr then σ' else ρ') = bif rr then σ else ρ) (c : Config (GamePt B V M A)) (hstate : c.state = phasePt (MachPh.sweepPh r tgt cont par) fun (x : Fin (gameDim B V)) => a₀) {bhd : Bool} (hhead : c.head = leftPt a₀ bhd) (htape : ∀ (p : GamePt B V M A), (gameMachine vars pol a₀ hdim (gameRule vars natoms concOk isTarget)).Posn p → c.tape p = tapeOfAssign a₀ hdim ρ σ p) : ∃ (c' : Config (GamePt B V M A)), Relation.ReflTransGen (fun (x y : Config (GamePt B V M A)) => (gameMachine vars pol a₀ hdim (gameRule vars natoms concOk isTarget)).Step x y ∧ x.state = c.state) c c' ∧ c'.state = c.state ∧ c'.head = rightPt a₀ ∧ ∀ (p : GamePt B V M A), (gameMachine vars pol a₀ hdim (gameRule vars natoms concOk isTarget)).Posn p → c'.tape p = tapeOfAssign a₀ hdim ρ' σ' p

A sweep writes an arbitrary assignment into its region. Starting at the lowest position with the tape holding ρ and σ, it reaches the right sentinel with the tape holding any ρ', σ' that agree with them outside the swept region – and, since the phase owns the choice, every play of the sweep is such a run, which is what a universal sweep needs.

The tape is controlled only at the positions: a cell tag with a non-canonical tuple is not one, and is never read.

The run of a rewind

A rewind changes nothing – both its rules write back what they read – so its invariant is about the state, not the tape. Unlike a sweep it does not end in the phase it began: its last step, at the second left sentinel, both moves to the lowest position and hands over to DescriptiveComplexity.MachPh.rewindTarget. So the invariant it runs on is

(the tape is unchanged) ∧ (the head is not the right sentinel) ∧
  (the state is the rewind, or it is the target and the head is lowest)

and closing it needs the two order facts of the layout: the two left sentinels are adjacent (DescriptiveComplexity.succPos_leftPt), so the handover really does land on the lowest position; and a cell is never next to the first sentinel (DescriptiveComplexity.succPos_ne_leftPt), so the walk cannot reach the lowest position without reading the mark first.

theorem DescriptiveComplexity.rewind_run {B : SOBlock} {V M : ℕ} {A : Type} [LinearOrder A] [Finite A] {vars natoms : GameQuestion → ℕ} {pol : GameQuestion → ℕ → Bool} {a₀ : A} {hdim : blockArityBound B ≤ gameDim B V} {concOk : MachPh V M → (Fin (gameDim B V) → A) → Prop} {isTarget : MachPh V M → SymTag B → (Fin (gameDim B V) → A) → Prop} {r tgt : Bool} {cont : SweepCont} {par : Bool} (h₀ : IsBot a₀) {ρ σ : B.Assignment A} (c : Config (GamePt B V M A)) (hstate : c.state = phasePt (MachPh.rewindPh r tgt cont par) fun (x : Fin (gameDim B V)) => a₀) (hpos : (gameMachine vars pol a₀ hdim (gameRule vars natoms concOk isTarget)).Posn c.head) (hne : c.head ≠ rightPt a₀) (hlow : c.head ≠ leftPt a₀ false) (htape : ∀ (p : GamePt B V M A), (gameMachine vars pol a₀ hdim (gameRule vars natoms concOk isTarget)).Posn p → c.tape p = tapeOfAssign a₀ hdim ρ σ p) : ∃ (c' : Config (GamePt B V M A)), Relation.ReflTransGen (fun (x y : Config (GamePt B V M A)) => (gameMachine vars pol a₀ hdim (gameRule vars natoms concOk isTarget)).Step x y ∧ x.state = c.state) c c' ∧ (c'.state = phasePt (MachPh.rewindPh r tgt cont par).rewindTarget fun (x : Fin (gameDim B V)) => a₀) ∧ c'.head = leftPt a₀ false ∧ ∀ (p : GamePt B V M A), (gameMachine vars pol a₀ hdim (gameRule vars natoms concOk isTarget)).Posn p → c'.tape p = tapeOfAssign a₀ hdim ρ σ p

A rewind walks back to the lowest position and hands over. It starts anywhere strictly below the right sentinel – which is where the sweep's last step leaves it – changes nothing, and ends on the lowest position in the phase DescriptiveComplexity.MachPh.rewindTarget names.

The run of a seek

A seek walks right, writing back everything it reads, and stops at the cell whose symbol answers its test – the address and the claimed bit, which is why a wrong claim is not a stop. It therefore either meets its cell and accepts, or runs off the tape and, having no rule at the right sentinel, is stuck. Since a seek is an existential phase, that is a loss: asking an unprovable question costs the player who asked.

def DescriptiveComplexity.SeekHit {B : SOBlock} {V M : ℕ} {A : Type} (a₀ : A) (isTarget : MachPh V M → SymTag B → (Fin (gameDim B V) → A) → Prop) (ph : MachPh V M) (v : Fin (gameDim B V) → A) (tape : GamePt B V M A → GamePt B V M A) (p : GamePt B V M A) : Prop

The cell a seek is looking for: a cell whose symbol – the bit included – answers the phase's test at the address the valuation gives. The bit is read off the tape, so this is where a claim being right or wrong is decided.

Equations

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

theorem DescriptiveComplexity.not_seekHit_rightPt {B : SOBlock} {V M : ℕ} {A : Type} {a₀ : A} {isTarget : MachPh V M → SymTag B → (Fin (gameDim B V) → A) → Prop} {ph : MachPh V M} {v : Fin (gameDim B V) → A} {tape : GamePt B V M A → GamePt B V M A} : ¬SeekHit a₀ isTarget ph v tape (rightPt a₀)

theorem DescriptiveComplexity.seek_run {B : SOBlock} {V M : ℕ} {A : Type} [LinearOrder A] [Finite A] {vars natoms : GameQuestion → ℕ} {pol : GameQuestion → ℕ → Bool} {a₀ : A} {hdim : blockArityBound B ≤ gameDim B V} {concOk : MachPh V M → (Fin (gameDim B V) → A) → Prop} {isTarget : MachPh V M → SymTag B → (Fin (gameDim B V) → A) → Prop} {ph : MachPh V M} {v : Fin (gameDim B V) → A} (h₀ : IsBot a₀) (hk : ph.kind = PhKind.seek) (harity : MachPh.arity vars ph ≤ V) (hcv : Canon (MachPh.arity vars ph) v) {ρ σ : B.Assignment A} (c : Config (GamePt B V M A)) (hstate : c.state = phasePt ph v) {bhd : Bool} (hhead : c.head = leftPt a₀ bhd) (htape : ∀ (p : GamePt B V M A), (gameMachine vars pol a₀ hdim (gameRule vars natoms concOk isTarget)).Posn p → c.tape p = tapeOfAssign a₀ hdim ρ σ p) : ∃ (c' : Config (GamePt B V M A)), Relation.ReflTransGen (fun (x y : Config (GamePt B V M A)) => (gameMachine vars pol a₀ hdim (gameRule vars natoms concOk isTarget)).Step x y ∧ x.state = c.state) c c' ∧ c'.tape = c.tape ∧ ((c'.state = phasePt (MachPh.accPh false) fun (x : Fin (gameDim B V)) => a₀) ∨ c'.state = c.state ∧ c'.head = rightPt a₀ ∧ ∀ (p : GamePt B V M A), (gameMachine vars pol a₀ hdim (gameRule vars natoms concOk isTarget)).Posn p → ¬SeekHit a₀ isTarget ph v (tapeOfAssign a₀ hdim ρ σ) p)

A seek either meets its cell and accepts, or runs off the tape – and then no cell at all answered its test, which is how a false claim is punished. It starts on a sentinel, where nothing below it can have been passed.