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.

def DescriptiveComplexity.SymTag.equivSum {B : SOBlock} : SymTag B ≃ Bool ⊕ Bool × Bool × B.ι

The symbol shapes as a sum, for the Finite instance.

Equations

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

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⟩

theorem DescriptiveComplexity.argsOf_pad {B : SOBlock} {A : Type} (a₀ : A) (i : B.ι) (ā : Fin (B.arity i) → A) : argsOf i (pad a₀ ā) = ā

The address of a cell, read as a symbol's address.

@[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 ā) = ā

theorem DescriptiveComplexity.agree_walkTuple {B : SOBlock} {V : ℕ} {A : Type} {m : ℕ} (hm : m ≤ V) (v : Fin (gameDim B V) → A) (ā : Fin (blockArityBound B) → A) : Agree m (walkTuple v ā) v

A walk step agrees with its own state: it carries the valuation the phase declares, whatever the address it is reading.

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)

theorem DescriptiveComplexity.canon_truncTuple {A : Type} [LinearOrder A] {a₀ : A} (h₀ : IsBot a₀) (m : ℕ) {D : ℕ} (w : Fin D → A) : Canon m (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.

theorem DescriptiveComplexity.truncTuple_succ {A : Type} [LinearOrder A] {a₀ : A} (h₀ : IsBot a₀) {m D : ℕ} {vv w : Fin D → A} (hm : m < D) (hc : Canon m vv) (ha : Agree m w vv) : truncTuple a₀ (m + 1) w = Function.update vv ⟨m, hm⟩ (w ⟨m, hm⟩)

One step of a prefix writes exactly one coordinate: the tuple the next phase keeps is the one it came from, updated at the coordinate just declared. This is the whole of the arithmetic the prefix costs.

theorem DescriptiveComplexity.pref_update {A : Type} {D m : ℕ} (h : m ≤ D) {vv : Fin D → A} {j : ℕ} (hjD : j < D) (hjm : j < m) (a : A) : pref h (Function.update vv ⟨j, hjD⟩ a) = Function.update (pref h vv) ⟨j, hjm⟩ a

Updating a coordinate commutes with taking a prefix, when the coordinate is in the prefix.

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.

def DescriptiveComplexity.TrTag.toProd {B : SOBlock} {V M : ℕ} (t : TrTag B V M) : MachPh V M × MachPh V M × SymTag B × SymTag B × Bool

A transition tag as a tuple, for the Finite instance.

Equations

• t.toProd = (t.src, t.dst, t.rd, t.wr, t.right)

theorem DescriptiveComplexity.TrTag.toProd_injective {B : SOBlock} {V M : ℕ} : Function.Injective toProd

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.isLinOrd_gameLe {B : SOBlock} {V M : ℕ} {A : Type} [LinearOrder A] : IsLinOrd tagTupleLe

The tape order is linear on the whole universe, which is what DescriptiveComplexity.TMData.WellFormed asks of it.

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.

theorem DescriptiveComplexity.gameMachine_isUniv {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) (p : MachPh V M) (w : Fin (gameDim B V) → A) : (gameMachine vars pol a₀ hdim rule).IsUniv true (phasePt p w) ↔ MachPh.IsUniv pol p = true

A state is universal exactly when its phase is.

The two ends, and what a position is

theorem DescriptiveComplexity.posn_cases {B : SOBlock} {V M : ℕ} {A : Type} [LinearOrder A] {vars : GameQuestion → ℕ} {a₀ : A} (h₀ : IsBot a₀) {p : GamePt B V M A} (hp : machPosn p) (hd : machDom (ctrlArity vars) p) : (∃ (b : Bool), p = leftPt a₀ b) ∨ (∃ (r : Bool) (i : B.ι) (ā : Fin (B.arity i) → A), p = cellPt a₀ r i ā) ∨ p = rightPt a₀

What a position is: a left sentinel, a cell, or the right sentinel. This is what a walk's step analysis begins with – the head is one of the three, and the symbol it reads follows.

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.

theorem DescriptiveComplexity.not_ctrlStep_of_walk {B : SOBlock} {V M : ℕ} {vars natoms : GameQuestion → ℕ} {t : TrTag B V M} (h : t.src.kind = PhKind.sweep ∨ t.src.kind = PhKind.rewind ∨ t.src.kind = PhKind.seek) : ¬MachPh.CtrlStep vars natoms t.src t.dst

A rule out of a walk phase is never a control step: the control graph is empty there, so the nine families do not overlap at a walk.

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)

theorem DescriptiveComplexity.GameProg.machine_wellFormed {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) (h₀ : IsBot a₀) : (prog.machine a₀ hdim).WellFormed

The machine is well formed.

theorem DescriptiveComplexity.GameProg.machine_blocksSplit {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) : (prog.machine a₀ hdim).BlocksSplit

The two marks split its states.

theorem DescriptiveComplexity.exists_gameProg {L : FirstOrder.Language} [L.IsRelational] (spec : SOGameSpec L) : ∃ (V : ℕ) (M : ℕ) (prog : GameProg (L.sum FirstOrder.Language.order) spec.B V M), ∀ (q : GameQuestion), (prog.data q).Plays (spec.question q)

Every specification has such a program. The six questions are read in one language and normalized independently; the phases' index types are the maxima, and nothing is padded.

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.exists_trPt_of_tr {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} {τ : GamePt B V M A} (h : (gameMachine vars pol a₀ hdim rule).Tr τ) : ∃ (t : TrTag B V M) (w : Fin (gameDim B V) → A), τ = trPt t w ∧ rule t w

Every transition is a tagged tuple, and its rule holds of it. This is the one place the tag of a transition is destructured; everything downstream reads the five lemmas below.

@[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

theorem DescriptiveComplexity.game_step_iff {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} (c c' : Config (GamePt B V M A)) : (gameMachine vars pol a₀ hdim rule).Step c c' ↔ ∃ (t : TrTag B V M) (w : Fin (gameDim B V) → A), rule t w ∧ (c.state.1 = Sum.inr (Sum.inl t.src) ∧ Canon (MachPh.arity vars t.src) c.state.2 ∧ Agree (MachPh.arity vars t.src) w c.state.2) ∧ c.tape c.head = gameSymPt a₀ t.rd (addrOf w) ∧ (c'.state.1 = Sum.inr (Sum.inl t.dst) ∧ Canon (MachPh.arity vars t.dst) c'.state.2 ∧ Agree (MachPh.arity vars t.dst) w c'.state.2) ∧ c'.tape c.head = gameSymPt a₀ t.wr (addrOf w) ∧ (∀ (p : GamePt B V M A), p ≠ c.head → c'.tape p = c.tape p) ∧ (t.right = true ∧ SuccPos (gameMachine vars pol a₀ hdim rule).Le (gameMachine vars pol a₀ hdim rule).Posn c.head c'.head ∨ t.right = false ∧ SuccPos (gameMachine vars pol a₀ hdim rule).Le (gameMachine vars pol a₀ hdim rule).Posn c'.head c.head)

A step, read off its transition. The tuple w of the transition is what carries the value a prefix step writes and the address a walk step reads; the five clauses about it are exactly the five attributes of DescriptiveComplexity.TMData.Step.

Building one step

theorem DescriptiveComplexity.step_of_rule {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} (hrule : rule t w) (c : Config (GamePt B V M A)) (q' h' : GamePt B V M A) (hsrc : c.state.1 = Sum.inr (Sum.inl t.src)) (hcs : Canon (MachPh.arity vars t.src) c.state.2) (has : Agree (MachPh.arity vars t.src) w c.state.2) (hdst : q'.1 = Sum.inr (Sum.inl t.dst)) (hcd : Canon (MachPh.arity vars t.dst) q'.2) (had : Agree (MachPh.arity vars t.dst) w q'.2) (hread : c.tape c.head = gameSymPt a₀ t.rd (addrOf w)) (hmove : t.right = true ∧ SuccPos (gameMachine vars pol a₀ hdim rule).Le (gameMachine vars pol a₀ hdim rule).Posn c.head h' ∨ t.right = false ∧ SuccPos (gameMachine vars pol a₀ hdim rule).Le (gameMachine vars pol a₀ hdim rule).Posn h' c.head) : (gameMachine vars pol a₀ hdim rule).Step c { state := q', head := h', tape := Function.update c.tape c.head (gameSymPt a₀ t.wr (addrOf w)) }

One step, built from a rule. The destination configuration is forced: the state is whatever Dst allows, the head is the neighbor, and the tape is the old one with the written symbol at the head. Every case of every walk goes through this, so the frame condition is discharged once.

What a walk may do

theorem DescriptiveComplexity.sweep_cases {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} (hk : t.src.kind = PhKind.sweep) (h : gameRule vars natoms concOk isTarget t w) : t.dst = t.src ∧ t.rd = SymTag.mark false ∧ t.wr = SymTag.mark false ∧ t.right = true ∨ (t.dst = t.src ∧ t.right = true ∧ ∃ (b : Bool) (b' : Bool) (rr : Bool) (i : B.ι), t.rd = SymTag.val b rr i ∧ t.wr = SymTag.val b' rr i ∧ (rr = t.src.tgt ∨ b' = b)) ∨ t.dst = MachPh.rewindPh t.src.r t.src.tgt t.src.cont false ∧ t.rd = SymTag.mark true ∧ t.wr = SymTag.mark true ∧ t.right = false

The three things a sweep may do, and nothing else: cross a left sentinel, act at a cell – guessing the bit in the swept region, copying it back elsewhere – or reach the right mark and hand over to its rewind. The other six families die on the phase's kind, and the control's own family dies because DescriptiveComplexity.MachPh.CtrlStep is empty at a walk.

theorem DescriptiveComplexity.rewind_cases {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} (hk : t.src.kind = PhKind.rewind) (h : gameRule vars natoms concOk isTarget t w) : (t.dst = t.src ∧ t.rd = t.wr ∧ t.right = false ∧ ∃ (b : Bool) (rr : Bool) (i : B.ι), t.rd = SymTag.val b rr i) ∨ t.dst = t.src.rewindTarget ∧ t.rd = SymTag.mark false ∧ t.wr = SymTag.mark false ∧ t.right = false

The two things a rewind may do: cross a cell without changing it, or reach the left mark and hand over to its continuation. Both move left, so it really does walk back.

theorem DescriptiveComplexity.seek_cases {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} (hk : t.src.kind = PhKind.seek) (h : gameRule vars natoms concOk isTarget t w) : t.dst = t.src ∧ t.rd = SymTag.mark false ∧ t.wr = SymTag.mark false ∧ t.right = true ∨ t.dst = t.src ∧ t.rd = t.wr ∧ t.right = true ∧ (∃ (b : Bool) (rr : Bool) (i : B.ι), t.rd = SymTag.val b rr i) ∧ ¬isTarget t.src t.rd w ∨ t.dst = MachPh.accPh false ∧ t.rd = t.wr ∧ t.right = true ∧ isTarget t.src t.rd w

The three things a seek may do: cross a left sentinel, cross a cell that is not its target, or stop at the one that is. Every one of them writes back what it read, so a seek never changes the tape; and the last is the only way out of the phase, so a seek that never meets its target simply runs off the tape and loses.

theorem DescriptiveComplexity.ctrl_cases {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} (hs : t.src.kind ≠ PhKind.sweep) (hr : t.src.kind ≠ PhKind.rewind) (hk : t.src.kind ≠ PhKind.seek) (h : gameRule vars natoms concOk isTarget t w) : t.rd = SymTag.mark false ∧ t.wr = SymTag.mark false ∧ t.right = !t.src.par ∧ MachPh.CtrlStep vars natoms t.src t.dst ∧ (t.src.kind = PhKind.conc → concOk t.src w)

The only thing a control phase may do is a step of the control graph. The eight tape families all name a walk kind, so at any other phase they are empty and family (A) is what is left – with the guard of a concluding transition, which is the one thing the control graph does not carry.

theorem DescriptiveComplexity.rewind_writes_back {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} (hk : t.src.kind = PhKind.rewind) (h : gameRule vars natoms concOk isTarget t w) : t.rd = t.wr

A rewind never changes the tape.

The two steps of a sweep

theorem DescriptiveComplexity.sweep_step_left {B : SOBlock} {V M : ℕ} {A : Type} [LinearOrder 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₀) (c : Config (GamePt B V M A)) (hstate : c.state = phasePt (MachPh.sweepPh r tgt cont par) fun (x : Fin (gameDim B V)) => a₀) (hread : c.tape c.head = markPt a₀ false) {h' : GamePt B V M A} (hsucc : SuccPos (gameMachine vars pol a₀ hdim (gameRule vars natoms concOk isTarget)).Le (gameMachine vars pol a₀ hdim (gameRule vars natoms concOk isTarget)).Posn c.head h') : (gameMachine vars pol a₀ hdim (gameRule vars natoms concOk isTarget)).Step c { state := c.state, head := h', tape := Function.update c.tape c.head (markPt a₀ false) }

A sweep crosses a sentinel, changing nothing.

theorem DescriptiveComplexity.sweep_step_cell {B : SOBlock} {V M : ℕ} {A : Type} [LinearOrder 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₀) (c : Config (GamePt B V M A)) (hstate : c.state = phasePt (MachPh.sweepPh r tgt cont par) fun (x : Fin (gameDim B V)) => a₀) {b rr b' : Bool} {i : B.ι} {ā : Fin (B.arity i) → A} (hread : c.tape c.head = valPt a₀ b rr i ā) (hb : rr = tgt ∨ b' = b) {h' : GamePt B V M A} (hsucc : SuccPos (gameMachine vars pol a₀ hdim (gameRule vars natoms concOk isTarget)).Le (gameMachine vars pol a₀ hdim (gameRule vars natoms concOk isTarget)).Posn c.head h') : (gameMachine vars pol a₀ hdim (gameRule vars natoms concOk isTarget)).Step c { state := c.state, head := h', tape := Function.update c.tape c.head (valPt a₀ b' rr i ā) }

A sweep acts at a cell: in the region it is writing it may put either bit there, and elsewhere it writes back what it read.

theorem DescriptiveComplexity.sweep_step_right {B : SOBlock} {V M : ℕ} {A : Type} [LinearOrder 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₀) (c : Config (GamePt B V M A)) (hstate : c.state = phasePt (MachPh.sweepPh r tgt cont par) fun (x : Fin (gameDim B V)) => a₀) (hread : c.tape c.head = markPt a₀ true) {h' : GamePt B V M A} (hsucc : SuccPos (gameMachine vars pol a₀ hdim (gameRule vars natoms concOk isTarget)).Le (gameMachine vars pol a₀ hdim (gameRule vars natoms concOk isTarget)).Posn h' c.head) : (gameMachine vars pol a₀ hdim (gameRule vars natoms concOk isTarget)).Step c { state := phasePt (MachPh.rewindPh r tgt cont false) fun (x : Fin (gameDim B V)) => a₀, head := h', tape := c.tape }

A sweep reaches the right mark and hands over to its rewind, moving left in the same step – so the rewind starts strictly below the right sentinel.

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.

theorem DescriptiveComplexity.exists_reach_stop {U : Type} [Finite U] {M : TMData U} (hlin : IsLinOrd M.Le) {Inv Stop Guard : Config U → Prop} (hguard : ∀ (c : Config U), Inv c → ¬MaxPos M.Le M.Posn c.head → ¬Stop c → Guard c) (hstep : ∀ (c : Config U), Inv c → M.Posn c.head → ¬MaxPos M.Le M.Posn c.head → ¬Stop c → ∃ (c' : Config U), M.Step c c' ∧ SuccPos M.Le M.Posn c.head c'.head ∧ Inv c') (c : Config U) : Inv c → M.Posn c.head → ∃ (c' : Config U), Relation.ReflTransGen (fun (x y : Config U) => M.Step x y ∧ Guard x) c c' ∧ (Stop c' ∨ MaxPos M.Le M.Posn c'.head) ∧ Inv c'

A rightward walk runs until something stops it, or to the end of the tape. A sweep is stopped by nothing and so reaches the right sentinel; a seek is stopped by the cell it is looking for, and reaching the sentinel instead is how it learns there was none.

theorem DescriptiveComplexity.exists_reach_maxPos {U : Type} [Finite U] {M : TMData U} (hlin : IsLinOrd M.Le) {Inv Guard : Config U → Prop} (hguard : ∀ (c : Config U), Inv c → ¬MaxPos M.Le M.Posn c.head → Guard c) (hstep : ∀ (c : Config U), Inv c → M.Posn c.head → ¬MaxPos M.Le M.Posn c.head → ∃ (c' : Config U), M.Step c c' ∧ SuccPos M.Le M.Posn c.head c'.head ∧ Inv c') (c : Config U) : Inv c → M.Posn c.head → ∃ (c' : Config U), Relation.ReflTransGen (fun (x y : Config U) => M.Step x y ∧ Guard x) c c' ∧ MaxPos M.Le M.Posn c'.head ∧ Inv c'

A rightward walk reaches the highest position, when nothing stops it.

theorem DescriptiveComplexity.exists_reach_minPos {U : Type} [Finite U] {M : TMData U} (hlin : IsLinOrd M.Le) {Inv Guard : Config U → Prop} (hguard : ∀ (c : Config U), Inv c → ¬MinPos M.Le M.Posn c.head → Guard c) (hstep : ∀ (c : Config U), Inv c → M.Posn c.head → ¬MinPos M.Le M.Posn c.head → ∃ (c' : Config U), M.Step c c' ∧ SuccPos M.Le M.Posn c'.head c.head ∧ Inv c') (c : Config U) : Inv c → M.Posn c.head → ∃ (c' : Config U), Relation.ReflTransGen (fun (x y : Config U) => M.Step x y ∧ Guard x) c c' ∧ MinPos M.Le M.Posn c'.head ∧ Inv c'

A leftward walk reaches the lowest position.

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.

theorem DescriptiveComplexity.below_succPos {U : Type} {Le : U → U → Prop} {Posn : U → Prop} (hlin : IsLinOrd Le) {h h' : U} (hs : SuccPos Le Posn h h') {p : U} (hp : Posn p) : Le p h' ∧ p ≠ h' ↔ Le p h ∧ p ≠ h ∨ p = h

A step of the walk moves exactly one position from ahead to behind: the positions strictly below the successor are those strictly below the head, together with the head itself.

theorem DescriptiveComplexity.succPos_right_unique {U : Type} {Le : U → U → Prop} {Posn : U → Prop} (hlin : IsLinOrd Le) {p q q' : U} (h : SuccPos Le Posn p q) (h' : SuccPos Le Posn p q') : q = q'

The element immediately above a given one is unique – the mirror of DescriptiveComplexity.succPos_left_unique, and what pins the head a control step lands on.

The control's own step

theorem DescriptiveComplexity.ctrl_step {B : SOBlock} {V M : ℕ} {A : Type} [LinearOrder 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} (h₀ : IsBot a₀) {p p' : MachPh V M} {w vv : Fin (gameDim B V) → A} (hcs : MachPh.CtrlStep vars natoms p p') (hconc : p.kind = PhKind.conc → concOk p w) (c : Config (GamePt B V M A)) (hstate : c.state = phasePt p vv) (hcv : Canon (MachPh.arity vars p) vv) (hag : Agree (MachPh.arity vars p) w vv) (hhead : c.head = leftPt a₀ p.par) (hread : c.tape c.head = markPt a₀ false) : (gameMachine vars pol a₀ hdim (gameRule vars natoms concOk isTarget)).Step c { state := phasePt p' (truncTuple a₀ (MachPh.arity vars p') w), head := leftPt a₀ !p.par, tape := c.tape }

A step of the control graph, built. The head bounces between the two left sentinels – which is what DescriptiveComplexity.MachPh.par records, and why every such step flips it – and the tape is untouched. The destination keeps the transition's tuple up to the arity it declares, so a prefix step writes exactly one coordinate and the choice of the transition is the choice of the value written.

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_step_cell {B : SOBlock} {V M : ℕ} {A : Type} [LinearOrder 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₀) (c : Config (GamePt B V M A)) (hstate : c.state = phasePt (MachPh.rewindPh r tgt cont par) fun (x : Fin (gameDim B V)) => a₀) {b rr : Bool} {i : B.ι} {ā : Fin (B.arity i) → A} (hread : c.tape c.head = valPt a₀ b rr i ā) {h' : GamePt B V M A} (hsucc : SuccPos (gameMachine vars pol a₀ hdim (gameRule vars natoms concOk isTarget)).Le (gameMachine vars pol a₀ hdim (gameRule vars natoms concOk isTarget)).Posn h' c.head) : (gameMachine vars pol a₀ hdim (gameRule vars natoms concOk isTarget)).Step c { state := c.state, head := h', tape := c.tape }

A rewind crosses a cell, changing nothing.

theorem DescriptiveComplexity.rewind_step_left {B : SOBlock} {V M : ℕ} {A : Type} [LinearOrder 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₀) (c : Config (GamePt B V M A)) (hstate : c.state = phasePt (MachPh.rewindPh r tgt cont par) fun (x : Fin (gameDim B V)) => a₀) (hread : c.tape c.head = markPt a₀ false) {h' : GamePt B V M A} (hsucc : SuccPos (gameMachine vars pol a₀ hdim (gameRule vars natoms concOk isTarget)).Le (gameMachine vars pol a₀ hdim (gameRule vars natoms concOk isTarget)).Posn h' c.head) : (gameMachine vars pol a₀ hdim (gameRule vars natoms concOk isTarget)).Step c { state := phasePt (MachPh.rewindPh r tgt cont par).rewindTarget fun (x : Fin (gameDim B V)) => a₀, head := h', tape := c.tape }

A rewind reads the left mark and hands over, moving left in the same step – which is why it has to be the second sentinel it reads it on.

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_leftPt {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} (b : Bool) : ¬SeekHit a₀ isTarget ph v tape (leftPt a₀ b)

A sentinel is never the cell a seek is looking for.

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_step_left {B : SOBlock} {V M : ℕ} {A : Type} [LinearOrder 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} (hk : ph.kind = PhKind.seek) (harity : MachPh.arity vars ph ≤ V) (c : Config (GamePt B V M A)) (hstate : c.state = phasePt ph v) (hcv : Canon (MachPh.arity vars ph) v) (hread : c.tape c.head = markPt a₀ false) {h' : GamePt B V M A} (hsucc : SuccPos (gameMachine vars pol a₀ hdim (gameRule vars natoms concOk isTarget)).Le (gameMachine vars pol a₀ hdim (gameRule vars natoms concOk isTarget)).Posn c.head h') : (gameMachine vars pol a₀ hdim (gameRule vars natoms concOk isTarget)).Step c { state := c.state, head := h', tape := c.tape }

A seek crosses a sentinel, changing nothing.

theorem DescriptiveComplexity.seek_step_miss {B : SOBlock} {V M : ℕ} {A : Type} [LinearOrder 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} (hk : ph.kind = PhKind.seek) (harity : MachPh.arity vars ph ≤ V) (c : Config (GamePt B V M A)) (hstate : c.state = phasePt ph v) (hcv : Canon (MachPh.arity vars ph) v) {b rr : Bool} {i : B.ι} {ā : Fin (B.arity i) → A} (hread : c.tape c.head = valPt a₀ b rr i ā) (hmiss : ¬isTarget ph (SymTag.val b rr i) (walkTuple v (pad a₀ ā))) {h' : GamePt B V M A} (hsucc : SuccPos (gameMachine vars pol a₀ hdim (gameRule vars natoms concOk isTarget)).Le (gameMachine vars pol a₀ hdim (gameRule vars natoms concOk isTarget)).Posn c.head h') : (gameMachine vars pol a₀ hdim (gameRule vars natoms concOk isTarget)).Step c { state := c.state, head := h', tape := c.tape }

A seek crosses a cell that is not the one it is looking for, changing nothing.

theorem DescriptiveComplexity.seek_step_hit {B : SOBlock} {V M : ℕ} {A : Type} [LinearOrder 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) (c : Config (GamePt B V M A)) (hstate : c.state = phasePt ph v) (hcv : Canon (MachPh.arity vars ph) v) {b rr : Bool} {i : B.ι} {ā : Fin (B.arity i) → A} (hread : c.tape c.head = valPt a₀ b rr i ā) (hhit : isTarget ph (SymTag.val b rr i) (walkTuple v (pad a₀ ā))) {h' : GamePt B V M A} (hsucc : SuccPos (gameMachine vars pol a₀ hdim (gameRule vars natoms concOk isTarget)).Le (gameMachine vars pol a₀ hdim (gameRule vars natoms concOk isTarget)).Posn c.head h') : (gameMachine vars pol a₀ hdim (gameRule vars natoms concOk isTarget)).Step c { state := phasePt (MachPh.accPh false) fun (x : Fin (gameDim B V)) => a₀, head := h', tape := c.tape }

A seek stops at the cell it is looking for, and accepts.

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.