What a rule may not write

A forward run constructs the tape it walks: every lemma says the machine reaches a configuration whose tape is a named function of a named tape state, so nothing has to be said about what the rules leave alone. A backward reading is handed an arbitrary run and has to recognize the tape, and there the missing fact bites: a configuration's tape is of the form DescriptiveComplexity.Draw.Data.ixBack of some tape state only because no rule ever writes the slots the channel wrote – the register flag, the two ends, the block one-hots, the name coordinates and the padding flag.

This file states that (Rule.KeepsFile) and proves it of the shapes a rule's write can take: no write at all, an update of a slot that is not one of those, and the guess's own write. With them the outer layer's rules keep the file, which is what an opening's reading needs.

A run as a sequence

theorem DescriptiveComplexity.TMData.exists_seq_of_stepsIn {V : Type} {M : TMData V} {n : ℕ} {c d : Config V} : M.StepsIn n c d → ∃ (g : ℕ → Config V), g 0 = c ∧ (∀ (i : ℕ), n ≤ i → g i = d) ∧ ∀ i < n, M.Step (g i) (g (i + 1))

A run of n steps is a sequence of n + 1 configurations. The StepsIn form is an iterated existential, which is what a forward proof wants; a backward reading has to speak of the configuration at each time, and that is this.

theorem DescriptiveComplexity.TMData.reflTransGen_of_seq {V : Type} {M : TMData V} (g : ℕ → Config V) {n : ℕ} (hstep : ∀ i < n, M.Step (g i) (g (i + 1))) {m : ℕ} : m ≤ n → Relation.ReflTransGen M.Step (g m) (g n)

A stretch of a run, as reachability: from any time to any later one, the steps compose. This is how a backward reading passes the rest of the run – from the entry it found to the accepting configuration – to DescriptiveComplexity.TMData.not_acc_of_reaches_dead_of_uniqueFrom.

The slots the channel writes

def DescriptiveComplexity.Draw.Slot.IsFile {ι : Type} {ko ki dd0 : ℕ} : Slot ι ko ki dd0 → Prop

A slot of the register file: what the channel writes at time zero and no rule may touch – the register flag, the file's two ends, the block one-hots, the name coordinates and the padding flag. Everything else is a track: scratch the program owns.

Equations

• DescriptiveComplexity.Draw.Slot.reg.IsFile = True
• DescriptiveComplexity.Draw.Slot.regFirst.IsFile = True
• DescriptiveComplexity.Draw.Slot.regLast.IsFile = True
• (DescriptiveComplexity.Draw.Slot.blk a).IsFile = True
• (DescriptiveComplexity.Draw.Slot.name a).IsFile = True
• DescriptiveComplexity.Draw.Slot.pdd.IsFile = True
• x✝.IsFile = False

@[simp]

theorem DescriptiveComplexity.Draw.Slot.not_isFile_mir {ι : Type} {ko ki dd0 : ℕ} : ¬mir.IsFile

@[simp]

theorem DescriptiveComplexity.Draw.Slot.not_isFile_tgt {ι : Type} {ko ki dd0 : ℕ} : ¬tgt.IsFile

@[simp]

theorem DescriptiveComplexity.Draw.Slot.not_isFile_sav {ι : Type} {ko ki dd0 : ℕ} : ¬sav.IsFile

@[simp]

theorem DescriptiveComplexity.Draw.Slot.not_isFile_val {ι : Type} {ko ki dd0 : ℕ} : ¬val.IsFile

@[simp]

theorem DescriptiveComplexity.Draw.Slot.not_isFile_wk {ι : Type} {ko ki dd0 : ℕ} : ¬wk.IsFile

@[simp]

theorem DescriptiveComplexity.Draw.Slot.not_isFile_bot {ι : Type} {ko ki dd0 : ℕ} : ¬bot.IsFile

@[simp]

theorem DescriptiveComplexity.Draw.Slot.not_isFile_ltp {ι : Type} {ko ki dd0 : ℕ} : ¬ltp.IsFile

@[simp]

theorem DescriptiveComplexity.Draw.Slot.not_isFile_old {ι : Type} {ko ki dd0 : ℕ} (i : ι) : ¬(old i).IsFile

@[simp]

theorem DescriptiveComplexity.Draw.Slot.not_isFile_new {ι : Type} {ko ki dd0 : ℕ} (i : ι) : ¬(new i).IsFile

Rules that keep the file

def DescriptiveComplexity.Draw.Rule.KeepsFile {L : FirstOrder.Language} (dt : Data L) {A Q P : Type} (ρ : Rule A Q dt.SlotIx P) : Prop

A rule keeps the file: whatever it writes, the slots the channel wrote come out unchanged.

Equations

• DescriptiveComplexity.Draw.Rule.KeepsFile dt ρ = ∀ (f : Q → A) (g : dt.SlotIx → A) (s : dt.SlotIx), DescriptiveComplexity.Draw.Slot.IsFile s → ρ.wr f g s = g s

def DescriptiveComplexity.Draw.Rule.WritesBits {L : FirstOrder.Language} (dt : Data L) {A Q P : Type} (zero one : A) (ρ : Rule A Q dt.SlotIx P) : Prop

A rule writes bits: every slot it leaves is either untouched or one of the two designated elements. This is what keeps a tape readable as an DescriptiveComplexity.Draw.Data.ixBack, whose tracks are bitVals.

Equations

• DescriptiveComplexity.Draw.Rule.WritesBits dt zero one ρ = ∀ (f : Q → A) (g : dt.SlotIx → A) (s : dt.SlotIx), ρ.wr f g s = g s ∨ ρ.wr f g s = zero ∨ ρ.wr f g s = one

def DescriptiveComplexity.Draw.Rule.KeepsCellTracks {L : FirstOrder.Language} (dt : Data L) {A Q P : Type} (ρ : Rule A Q dt.SlotIx P) : Prop

A rule leaves the addressed tracks alone: the mirror, the target, the saved mirror and the valuation are read off the file's registers, so a tape that carries them at an address which is nobody's register is not an ixBack of anything. The opening never writes them.

Equations

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

def DescriptiveComplexity.Draw.Rule.KeepsSlot {L : FirstOrder.Language} (dt : Data L) {A Q P : Type} (t : dt.SlotIx) (ρ : Rule A Q dt.SlotIx P) : Prop

A rule leaves one slot alone. The semantic half of a backward reading is built from these: which slot each rule may touch, and hence what a track still holds after a stretch of the run.

Equations

• DescriptiveComplexity.Draw.Rule.KeepsSlot dt t ρ = ∀ (f : Q → A) (g : dt.SlotIx → A), ρ.wr f g t = g t

def DescriptiveComplexity.Draw.Rule.SetsSlot {L : FirstOrder.Language} (dt : Data L) {A Q P : Type} (one : A) (t : dt.SlotIx) (ρ : Rule A Q dt.SlotIx P) : Prop

A rule sets a slot: whatever it reads, it leaves that slot holding the designated one. The start step does this to the marker and the bottom mark.

Equations

• DescriptiveComplexity.Draw.Rule.SetsSlot dt one t ρ = ∀ (f : Q → A) (g : dt.SlotIx → A), ρ.wr f g t = one

theorem DescriptiveComplexity.Draw.track_after_set {L : FirstOrder.Language} {dt : Data L} {A Q P : Type} {zero one : A} {t : dt.SlotIx} {ρ : Rule A Q dt.SlotIx P} (hset : Rule.SetsSlot dt one t ρ) {U : Type} {rest : U → dt.SlotIx → A} (hzero : ∀ (r : U), rest r t = zero) (f : Q → A) (v s : U) : (if s = v then ρ.wr f (rest v) else rest s) t = bitVal zero one (s = v)

After a rule that sets a slot, that track marks the cell it was written at – provided it was clear before, which at the channel's tape it is (initBackReg_track_zero).

The shapes the outer layer writes with

theorem DescriptiveComplexity.Draw.guessWr_keepsFile {L : FirstOrder.Language} {dt : Data L} {A : Type} (zero one : A) (x : dt.d.B.ι → Bool) (g : dt.SlotIx → A) (s : dt.SlotIx) (hs : Slot.IsFile s) : dt.guessWr zero one x g s = g s

The guess keeps the file: it writes the stage tracks and copies every other slot, the file's included.

theorem DescriptiveComplexity.Draw.nexRule_keepsFile_of_ne_eval {L : FirstOrder.Language} {dt : Data L} {A : Type} [Fintype dt.SlotIx] [DecidableEq dt.SlotIx] {SE PE : Type} {ShE : SE → Type} (one zero : A) (γ : GuessSpec A dt.CtlIx dt.SlotIx (Option dt.KIx) (dt.d.B.ι → Bool)) (hγ : ∀ (b : Option dt.KIx) (x : dt.d.B.ι → Bool), γ.wr b x = fun (x_1 : dt.CtlIx → A) (g : dt.SlotIx → A) => dt.guessWr zero one x g) (ruleE : (e : SE) → ShE e → Rule A dt.CtlIx dt.SlotIx (NexPh (Option dt.KIx) PE)) (evalEntry : PE) (bot : Option dt.KIx) (i : NexSite SE) (ρ : NexSh SE (Option dt.KIx) (dt.d.B.ι → Bool) ShE i) (hi : ∀ (e : SE), i ≠ NexSite.eval e) : Rule.KeepsFile dt (dt.nexRule one (dt.nullSpec (Option dt.KIx)) γ ruleE evalEntry bot i ρ)

The outer layer keeps the file: at every site but the evaluation's, the handed program's rules either write nothing, or write the marker and the bottom mark (the start step), or write the guess's stage tracks – and none of those is a slot the channel wrote. The evaluation's own sites are the parameter ruleE, and a backward opening reading never reaches them.

theorem DescriptiveComplexity.Draw.guessWr_bits {L : FirstOrder.Language} {dt : Data L} {A : Type} (one zero : A) (γ : GuessSpec A dt.CtlIx dt.SlotIx (Option dt.KIx) (dt.d.B.ι → Bool)) (hγ : ∀ (b : Option dt.KIx) (x : dt.d.B.ι → Bool), γ.wr b x = fun (x_1 : dt.CtlIx → A) (g : dt.SlotIx → A) => dt.guessWr zero one x g) (b : Option dt.KIx) (x : dt.d.B.ι → Bool) (f : dt.CtlIx → A) (g : dt.SlotIx → A) (s : dt.SlotIx) : γ.wr b x f g s = g s ∨ γ.wr b x f g s = zero ∨ γ.wr b x f g s = one

The guess's write is a bit at the stage tracks and a copy everywhere else.

theorem DescriptiveComplexity.Draw.guessWr_cellTracks {L : FirstOrder.Language} {dt : Data L} {A : Type} (one zero : A) (γ : GuessSpec A dt.CtlIx dt.SlotIx (Option dt.KIx) (dt.d.B.ι → Bool)) (hγ : ∀ (b : Option dt.KIx) (x : dt.d.B.ι → Bool), γ.wr b x = fun (x_1 : dt.CtlIx → A) (g : dt.SlotIx → A) => dt.guessWr zero one x g) (b : Option dt.KIx) (x : dt.d.B.ι → Bool) (f : dt.CtlIx → A) (g : dt.SlotIx → A) (s : dt.SlotIx) (hs : s = Slot.mir ∨ s = Slot.tgt ∨ s = Slot.sav ∨ s = Slot.val) : γ.wr b x f g s = g s

The guess leaves the addressed tracks alone.

theorem DescriptiveComplexity.Draw.nexRule_writesBits_of_ne_eval {L : FirstOrder.Language} {dt : Data L} {A : Type} [Fintype dt.SlotIx] [DecidableEq dt.SlotIx] {SE PE : Type} {ShE : SE → Type} (one zero : A) (γ : GuessSpec A dt.CtlIx dt.SlotIx (Option dt.KIx) (dt.d.B.ι → Bool)) (hγ : ∀ (b : Option dt.KIx) (x : dt.d.B.ι → Bool), γ.wr b x = fun (x_1 : dt.CtlIx → A) (g : dt.SlotIx → A) => dt.guessWr zero one x g) (ruleE : (e : SE) → ShE e → Rule A dt.CtlIx dt.SlotIx (NexPh (Option dt.KIx) PE)) (evalEntry : PE) (bot : Option dt.KIx) (i : NexSite SE) (ρ : NexSh SE (Option dt.KIx) (dt.d.B.ι → Bool) ShE i) (hi : ∀ (e : SE), i ≠ NexSite.eval e) : Rule.WritesBits dt zero one (dt.nexRule one (dt.nullSpec (Option dt.KIx)) γ ruleE evalEntry bot i ρ)

The outer layer writes bits: the start step writes one, the guess writes a stage bit, and every other site of the opening writes nothing.

theorem DescriptiveComplexity.Draw.nexRule_keepsCellTracks_of_ne_eval {L : FirstOrder.Language} {dt : Data L} {A : Type} [Fintype dt.SlotIx] [DecidableEq dt.SlotIx] {SE PE : Type} {ShE : SE → Type} (one zero : A) (γ : GuessSpec A dt.CtlIx dt.SlotIx (Option dt.KIx) (dt.d.B.ι → Bool)) (hγ : ∀ (b : Option dt.KIx) (x : dt.d.B.ι → Bool), γ.wr b x = fun (x_1 : dt.CtlIx → A) (g : dt.SlotIx → A) => dt.guessWr zero one x g) (ruleE : (e : SE) → ShE e → Rule A dt.CtlIx dt.SlotIx (NexPh (Option dt.KIx) PE)) (evalEntry : PE) (bot : Option dt.KIx) (i : NexSite SE) (ρ : NexSh SE (Option dt.KIx) (dt.d.B.ι → Bool) ShE i) (hi : ∀ (e : SE), i ≠ NexSite.eval e) : Rule.KeepsCellTracks dt (dt.nexRule one (dt.nullSpec (Option dt.KIx)) γ ruleE evalEntry bot i ρ)

The outer layer leaves the addressed tracks alone: the opening writes the marker, the bottom mark and the stage tracks, never the mirror, the target, the saved mirror or the valuation.

theorem DescriptiveComplexity.Draw.nexRule_keepsSlot_wk_bot {L : FirstOrder.Language} {dt : Data L} {A : Type} [Fintype dt.SlotIx] [DecidableEq dt.SlotIx] {SE PE : Type} {ShE : SE → Type} (one zero : A) (γ : GuessSpec A dt.CtlIx dt.SlotIx (Option dt.KIx) (dt.d.B.ι → Bool)) (hγ : ∀ (b : Option dt.KIx) (x : dt.d.B.ι → Bool), γ.wr b x = fun (x_1 : dt.CtlIx → A) (g : dt.SlotIx → A) => dt.guessWr zero one x g) (ruleE : (e : SE) → ShE e → Rule A dt.CtlIx dt.SlotIx (NexPh (Option dt.KIx) PE)) (evalEntry : PE) (bot : Option dt.KIx) (i : NexSite SE) (ρ : NexSh SE (Option dt.KIx) (dt.d.B.ι → Bool) ShE i) (hi : ∀ (e : SE), i ≠ NexSite.eval e) (hstart : i ≠ NexSite.start) (t : dt.SlotIx) (ht : t = Slot.wk ∨ t = Slot.bot) : Rule.KeepsSlot dt t (dt.nexRule one (dt.nullSpec (Option dt.KIx)) γ ruleE evalEntry bot i ρ)

Only the start step writes the marker and the bottom mark: every other site of the opening leaves both alone, so after the first step the working track marks the address the head started on and nothing else.

theorem DescriptiveComplexity.Draw.nexRule_keepsSlot_old {L : FirstOrder.Language} {dt : Data L} {A : Type} [Fintype dt.SlotIx] [DecidableEq dt.SlotIx] {SE PE : Type} {ShE : SE → Type} (one : A) (γ : GuessSpec A dt.CtlIx dt.SlotIx (Option dt.KIx) (dt.d.B.ι → Bool)) (ruleE : (e : SE) → ShE e → Rule A dt.CtlIx dt.SlotIx (NexPh (Option dt.KIx) PE)) (evalEntry : PE) (bot : Option dt.KIx) (i : NexSite SE) (ρ : NexSh SE (Option dt.KIx) (dt.d.B.ι → Bool) ShE i) (hi : ∀ (e : SE), i ≠ NexSite.eval e) (hguess : i ≠ NexSite.guess) (iv : dt.d.B.ι) : Rule.KeepsSlot dt (Slot.old iv) (dt.nexRule one (dt.nullSpec (Option dt.KIx)) γ ruleE evalEntry bot i ρ)

Only the guess writes the stage tracks: every other site of the opening leaves them alone, so what the evaluation reads there is what the guess wrote.

theorem DescriptiveComplexity.Draw.nexRule_setsSlot_start {L : FirstOrder.Language} {dt : Data L} {A : Type} [Fintype dt.SlotIx] [DecidableEq dt.SlotIx] {SE PE : Type} {ShE : SE → Type} (one : A) (γ : GuessSpec A dt.CtlIx dt.SlotIx (Option dt.KIx) (dt.d.B.ι → Bool)) (ruleE : (e : SE) → ShE e → Rule A dt.CtlIx dt.SlotIx (NexPh (Option dt.KIx) PE)) (evalEntry : PE) (bot : Option dt.KIx) (ρ : NexSh SE (Option dt.KIx) (dt.d.B.ι → Bool) ShE NexSite.start) (t : dt.SlotIx) (ht : t = Slot.wk ∨ t = Slot.bot) : Rule.SetsSlot dt one t (dt.nexRule one (dt.nullSpec (Option dt.KIx)) γ ruleE evalEntry bot NexSite.start ρ)

The start step sets the marker and the bottom mark.

Reading a tape back as a tape state

theorem DescriptiveComplexity.Draw.Data.exists_ixBack_of_shape {L : FirstOrder.Language} {dt : Data L} {A R' P' I : Type} (lay : Layout dt A R' P' I) {zero one : A} (hzo : zero ≠ one) (rest : (Univ A R' P' dt.KIx dt.dd → Prop) → dt.SlotIx → A) (st₀ : TapeSt dt A R' P' I) (hfile : ∀ (r : Univ A R' P' dt.KIx dt.dd → Prop) (s : Slot dt.d.B.ι dt.ko dt.ki dt.dd0), s.IsFile → rest r s = dt.ixBack lay zero one ⋯ st₀ r s) (hcell : ∀ (r : Univ A R' P' dt.KIx dt.dd → Prop) (s : Slot dt.d.B.ι dt.ko dt.ki dt.dd0), s = Slot.mir ∨ s = Slot.tgt ∨ s = Slot.sav ∨ s = Slot.val → rest r s = zero) (hbits : ∀ (r : Univ A R' P' dt.KIx dt.dd → Prop) (s : Slot dt.d.B.ι dt.ko dt.ki dt.dd0), ¬s.IsFile → rest r s = zero ∨ rest r s = one) : ∃ (st : TapeSt dt A R' P' I), rest = dt.ixBack lay zero one ⋯ st ∧ (st.mir = fun (x : I) => False) ∧ (st.tgt = fun (x : I) => False) ∧ (st.sav = fun (x : I) => False) ∧ st.val = fun (x : I) => False

A tape of the right shape is an ixBack: the file's slots as the layout has them, the four addressed tracks clear, every other track a bit – and the tape state is read off the tape, bit by bit. This is what turns a recognized tape into the object every run lemma is stated against.

structure DescriptiveComplexity.Draw.Data.TapeShape {L : FirstOrder.Language} {dt : Data L} {A R' P' I : Type} (lay : Layout dt A R' P' I) (zero one : A) (st₀ : TapeSt dt A R' P' I) (rest : (Univ A R' P' dt.KIx dt.dd → Prop) → dt.SlotIx → A) : Prop

A tape the reading recognizes: every cell carries a slot vector, the file's slots are the layout's, the four addressed tracks are clear, and every other track is a bit.

• file (r : Univ A R' P' dt.KIx dt.dd → Prop) (s : Slot dt.d.B.ι dt.ko dt.ki dt.dd0) : s.IsFile → rest r s = dt.ixBack lay zero one ⋯ st₀ r s

  The file's slots are the layout's.

• cells (r : Univ A R' P' dt.KIx dt.dd → Prop) (s : Slot dt.d.B.ι dt.ko dt.ki dt.dd0) : s = Slot.mir ∨ s = Slot.tgt ∨ s = Slot.sav ∨ s = Slot.val → rest r s = zero

  The four tracks read at a register are clear.

• bits (r : Univ A R' P' dt.KIx dt.dd → Prop) (s : Slot dt.d.B.ι dt.ko dt.ki dt.dd0) : ¬s.IsFile → rest r s = zero ∨ rest r s = one

  Every other track is a bit.

theorem DescriptiveComplexity.Draw.Data.tapeShape_update {L : FirstOrder.Language} {dt : Data L} {A R' P' I : Type} {lay : Layout dt A R' P' I} {zero one : A} {st₀ : TapeSt dt A R' P' I} {rest : (Univ A R' P' dt.KIx dt.dd → Prop) → dt.SlotIx → A} (hshape : TapeShape lay zero one st₀ rest) {Ph : Type} {ρ : Rule A dt.CtlIx dt.SlotIx Ph} (hfile : Rule.KeepsFile dt ρ) (hcell : Rule.KeepsCellTracks dt ρ) (hbits : Rule.WritesBits dt zero one ρ) (f : dt.CtlIx → A) (v : Univ A R' P' dt.KIx dt.dd → Prop) : TapeShape lay zero one st₀ fun (s : Univ A R' P' dt.KIx dt.dd → Prop) => if s = v then ρ.wr f (rest v) else rest s

A rule that keeps the file, keeps the addressed tracks and writes bits keeps the shape. This is the step of the opening's reading: the cell under the head is the only one that changes, and the three facts say the change stays inside the shape.

theorem DescriptiveComplexity.Draw.Data.ixBack_wk_inv {L : FirstOrder.Language} {dt : Data L} {A R' P' I : Type} (lay : Layout dt A R' P' I) {zero one : A} (hzo : zero ≠ one) (st : TapeSt dt A R' P' I) {P : (Univ A R' P' dt.KIx dt.dd → Prop) → Prop} (hread : ∀ (r : Univ A R' P' dt.KIx dt.dd → Prop), dt.ixBack lay zero one ⋯ st r Slot.wk = bitVal zero one (P r)) : st.wk = P

The marker track, read back.

theorem DescriptiveComplexity.Draw.Data.ixBack_bot_inv {L : FirstOrder.Language} {dt : Data L} {A R' P' I : Type} (lay : Layout dt A R' P' I) {zero one : A} (hzo : zero ≠ one) (st : TapeSt dt A R' P' I) {P : (Univ A R' P' dt.KIx dt.dd → Prop) → Prop} (hread : ∀ (r : Univ A R' P' dt.KIx dt.dd → Prop), dt.ixBack lay zero one ⋯ st r Slot.bot = bitVal zero one (P r)) : st.bot = P

The bottom mark, read back.

theorem DescriptiveComplexity.Draw.Data.passTracksAt_of_mir_zero {L : FirstOrder.Language} {dt : Data L} {A R' P' : Type} [Fintype dt.SlotIx] {J : Type} (cell : J → Univ A R' P' dt.KIx dt.dd → Prop) {PR : Prog A R' P' dt.CtlIx dt.SlotIx dt.KIx dt.dd} [DecidableEq dt.SlotIx] (rest : (Univ A R' P' dt.KIx dt.dd → Prop) → dt.SlotIx → A) (hz : ∀ (r : Univ A R' P' dt.KIx dt.dd → Prop), rest r Slot.mir = PR.zero) : (PR.passTracksAt cell Slot.mir rest fun (x : J) => False) = rest

A tape whose mirror track is clear is its own pass tape: the run layer writes its tapes as passTracksAt, which overwrites the walked track with the mark the head carries; where the head carries no mark and the track is clear, the two agree. This is the bridge from the shape a reading recovers to the tape the run lemmas are stated over.

One step of the machine, seen from the tape

theorem DescriptiveComplexity.Draw.Data.step_tape_of_shape_tr {A R P K : Type} {dd : ℕ} [LinearOrder A] [LinearOrder R] [LinearOrder P] [LinearOrder K] [FirstOrder.Language.wide.Structure (Univ A R P K dd)] {Q W : Type} [Fintype Q] [Fintype W] {PR : Prog A R P Q W K dd} (hR : PR.table.Reads) {x y : Config (WPoint (Univ A R P K dd))} {rest : (Univ A R P K dd → Prop) → W → A} {v : Univ A R P K dd → Prop} (hhead : x.head = Sum.inl v) (htape : x.tape = wideTape (fun (r : Univ A R P K dd → Prop) => PR.syElt (rest r)) (PR.syElt PR.blank)) {r : R} {w : Fin dd → A} (hread : (wideData (Univ A R P K dd)).Read (Sum.inr (Tag.ctrl r, w)) (x.tape x.head)) (hwrite : (wideData (Univ A R P K dd)).Write (Sum.inr (Tag.ctrl r, w)) (y.tape x.head)) (hframe : ∀ (p : WPoint (Univ A R P K dd)), p ≠ x.head → y.tape p = x.tape p) : y.tape = wideTape (fun (s : Univ A R P K dd → Prop) => PR.syElt (if s = v then (PR.rules r).wr (fun (q : Q) => unslot (unpad ⋯ w) (Sum.inl q)) (rest v) else rest s)) (PR.syElt PR.blank)

What a step does to the tape: it leaves every cell but the one under the head, and there it writes what the fired rule's wr makes of the control's payload and the cell's own tracks. Read backwards – from an arbitrary step to the tape it produces – this is what a recognizing argument walks along, and it is the converse of the run layer's Prog.step_* lemmas, which write the cell they already know.

The reading, along a run

def DescriptiveComplexity.Draw.Data.ShapedAt {L : FirstOrder.Language} {dt : Data L} {A R' P' I : Type} [Fintype dt.SlotIx] (PR : Prog A R' P' dt.CtlIx dt.SlotIx dt.KIx dt.dd) (lay : Layout dt A R' P' I) (st₀ : TapeSt dt A R' P' I) (c : Config (WPoint (Univ A R' P' dt.KIx dt.dd))) : Prop

A configuration the reading recognizes: its tape carries a slot vector at every cell, of the shape TapeShape describes.

Equations

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

theorem DescriptiveComplexity.Draw.Data.shapedAt_step_of_phase {L : FirstOrder.Language} {dt : Data L} {A R' P' I : Type} [LinearOrder A] [LinearOrder R'] [LinearOrder P'] [LinearOrder dt.KIx] [FirstOrder.Language.wide.Structure (Univ A R' P' dt.KIx dt.dd)] [Fintype dt.SlotIx] {PR : Prog A R' P' dt.CtlIx dt.SlotIx dt.KIx dt.dd} (hR : PR.table.Reads) {lay : Layout dt A R' P' I} {st₀ : TapeSt dt A R' P' I} {Ph : P' → Prop} {x y : Config (WPoint (Univ A R' P' dt.KIx dt.dd))} {v : Univ A R' P' dt.KIx dt.dd → Prop} (hhead : x.head = Sum.inl v) (hfacts : ∀ (r : R'), Ph (PR.table.srcPh r) → Rule.KeepsFile dt (PR.rules r) ∧ Rule.KeepsCellTracks dt (PR.rules r) ∧ Rule.WritesBits dt PR.zero PR.one (PR.rules r)) (hph : ∀ (p : P') (f : Fin (Fintype.card (dt.CtlIx ⊕ dt.SlotIx)) → A), x.state = Sum.inr (stateElt PR.zero p f) → Ph p) (hx : ShapedAt PR lay st₀ x) (hstep : (wideData (Univ A R' P' dt.KIx dt.dd)).Step x y) : ShapedAt PR lay st₀ y

One step keeps the shape, when the rule that fires is one of the phases the caller vouches for. A step's transition carries its rule, and the state it fires from carries that rule's source phase, so vouching for the phases a run passes through is vouching for the rules it fires.

theorem DescriptiveComplexity.Draw.Data.shapedAt_of_reaches_of_phase {L : FirstOrder.Language} {dt : Data L} {A R' P' I : Type} [LinearOrder A] [LinearOrder R'] [LinearOrder P'] [LinearOrder dt.KIx] [FirstOrder.Language.wide.Structure (Univ A R' P' dt.KIx dt.dd)] [Fintype dt.SlotIx] {PR : Prog A R' P' dt.CtlIx dt.SlotIx dt.KIx dt.dd} (hR : PR.table.Reads) {lay : Layout dt A R' P' I} {st₀ : TapeSt dt A R' P' I} {Ph : P' → Prop} {c₀ : Config (WPoint (Univ A R' P' dt.KIx dt.dd))} (hfacts : ∀ (r : R'), Ph (PR.table.srcPh r) → Rule.KeepsFile dt (PR.rules r) ∧ Rule.KeepsCellTracks dt (PR.rules r) ∧ Rule.WritesBits dt PR.zero PR.one (PR.rules r)) (hhead : ∀ (x : Config (WPoint (Univ A R' P' dt.KIx dt.dd))), ∃ (v : Univ A R' P' dt.KIx dt.dd → Prop), x.head = Sum.inl v) (h0 : ShapedAt PR lay st₀ c₀) {c : Config (WPoint (Univ A R' P' dt.KIx dt.dd))} (hreach : Relation.ReflTransGen (wideData (Univ A R' P' dt.KIx dt.dd)).Step c₀ c) (hpre : ∀ (x y : Config (WPoint (Univ A R' P' dt.KIx dt.dd))), Relation.ReflTransGen (wideData (Univ A R' P' dt.KIx dt.dd)).Step c₀ x → (wideData (Univ A R' P' dt.KIx dt.dd)).Step x y → Relation.ReflTransGen (wideData (Univ A R' P' dt.KIx dt.dd)).Step y c → ∀ (p : P') (f : Fin (Fintype.card (dt.CtlIx ⊕ dt.SlotIx)) → A), x.state = Sum.inr (stateElt PR.zero p f) → Ph p) : ShapedAt PR lay st₀ c

A run keeps the shape, as long as the caller vouches for the phases it passes through – all of them but the last, since it is the fired rules that matter. This is the form an opening's reading uses: the phases before the evaluation's entry are the outer layer's, and those are the rules nexRule_keepsFile_of_ne_eval and its two siblings are about.

theorem DescriptiveComplexity.Draw.Data.shapedAt_of_seq {L : FirstOrder.Language} {dt : Data L} {A R' P' I : Type} [LinearOrder A] [LinearOrder R'] [LinearOrder P'] [LinearOrder dt.KIx] [FirstOrder.Language.wide.Structure (Univ A R' P' dt.KIx dt.dd)] [Fintype dt.SlotIx] {PR : Prog A R' P' dt.CtlIx dt.SlotIx dt.KIx dt.dd} (hR : PR.table.Reads) {lay : Layout dt A R' P' I} {st₀ : TapeSt dt A R' P' I} {Ph : P' → Prop} (hfacts : ∀ (r : R'), Ph (PR.table.srcPh r) → Rule.KeepsFile dt (PR.rules r) ∧ Rule.KeepsCellTracks dt (PR.rules r) ∧ Rule.WritesBits dt PR.zero PR.one (PR.rules r)) (g : ℕ → Config (WPoint (Univ A R' P' dt.KIx dt.dd))) (hhead : ∀ (i : ℕ), ∃ (v : Univ A R' P' dt.KIx dt.dd → Prop), (g i).head = Sum.inl v) (h0 : ShapedAt PR lay st₀ (g 0)) (n : ℕ) (hstep : ∀ i < n, (wideData (Univ A R' P' dt.KIx dt.dd)).Step (g i) (g (i + 1))) (hph : ∀ i < n, ∀ (p : P') (f : Fin (Fintype.card (dt.CtlIx ⊕ dt.SlotIx)) → A), (g i).state = Sum.inr (stateElt PR.zero p f) → Ph p) : ShapedAt PR lay st₀ (g n)

The reading along a sequence: the configuration at each time is recognized, as long as the phases up to that time are ones the caller vouches for. This is shapedAt_of_reaches_of_phase in the form a backward reading actually has its run in – time by time, so that «the phases before the entry» is a statement about indices.

theorem DescriptiveComplexity.Draw.Data.step_track_const {L : FirstOrder.Language} {dt : Data L} {A R' P' : Type} [LinearOrder A] [LinearOrder R'] [LinearOrder P'] [LinearOrder dt.KIx] [FirstOrder.Language.wide.Structure (Univ A R' P' dt.KIx dt.dd)] [Fintype dt.SlotIx] {PR : Prog A R' P' dt.CtlIx dt.SlotIx dt.KIx dt.dd} (hR : PR.table.Reads) {Ph : P' → Prop} {t : dt.SlotIx} {x y : Config (WPoint (Univ A R' P' dt.KIx dt.dd))} {rest : (Univ A R' P' dt.KIx dt.dd → Prop) → dt.SlotIx → A} {v : Univ A R' P' dt.KIx dt.dd → Prop} (hhead : x.head = Sum.inl v) (htape : x.tape = wideTape (fun (r : Univ A R' P' dt.KIx dt.dd → Prop) => PR.syElt (rest r)) (PR.syElt PR.blank)) (hkeep : ∀ (r : R'), Ph (PR.table.srcPh r) → Rule.KeepsSlot dt t (PR.rules r)) (hph : ∀ (p : P') (f : Fin (Fintype.card (dt.CtlIx ⊕ dt.SlotIx)) → A), x.state = Sum.inr (stateElt PR.zero p f) → Ph p) (hstep : (wideData (Univ A R' P' dt.KIx dt.dd)).Step x y) : ∃ (rest' : (Univ A R' P' dt.KIx dt.dd → Prop) → dt.SlotIx → A), y.tape = wideTape (fun (r : Univ A R' P' dt.KIx dt.dd → Prop) => PR.syElt (rest' r)) (PR.syElt PR.blank) ∧ ∀ (r : Univ A R' P' dt.KIx dt.dd → Prop), rest' r t = rest r t

A step that fires a rule keeping a slot leaves that track alone, at every address: at the head because the rule keeps it, elsewhere because a step writes nowhere else.

theorem DescriptiveComplexity.Draw.Data.head_isAddr_of_step {L : FirstOrder.Language} {dt : Data L} {A R' P' : Type} [FirstOrder.Language.wide.Structure (Univ A R' P' dt.KIx dt.dd)] {x y : Config (WPoint (Univ A R' P' dt.KIx dt.dd))} (hstep : (wideData (Univ A R' P' dt.KIx dt.dd)).Step x y) : ∃ (v : Univ A R' P' dt.KIx dt.dd → Prop), y.head = Sum.inl v

After a step the head is on an address: a move lands on a position, and the positions of a wide machine are its addresses. The head of the initial configuration is one by construction, so along a run every head is – which is what a reading needs before it can speak of the cell under the head.

theorem DescriptiveComplexity.Draw.Data.step_rule {L : FirstOrder.Language} {dt : Data L} {A R' P' : Type} [LinearOrder A] [LinearOrder R'] [LinearOrder P'] [LinearOrder dt.KIx] [FirstOrder.Language.wide.Structure (Univ A R' P' dt.KIx dt.dd)] [Fintype dt.SlotIx] {PR : Prog A R' P' dt.CtlIx dt.SlotIx dt.KIx dt.dd} (hR : PR.table.Reads) {x y : Config (WPoint (Univ A R' P' dt.KIx dt.dd))} (hstep : (wideData (Univ A R' P' dt.KIx dt.dd)).Step x y) : ∃ (r : R') (f : dt.CtlIx → A) (g : dt.SlotIx → A), (PR.rules r).guard f g ∧ x.state = Sum.inr (stateElt PR.zero (PR.rules r).srcPh (stPl PR.zero f)) ∧ y.state = Sum.inr (stateElt PR.zero (PR.rules r).dstPh (stPl PR.zero ((PR.rules r).dstSt f g)))

A step, inverted: the rule that fired, the data it fired on, that its guard held, and the two phases it went between. step_state_dst is its destination half; a reading that has to know which rule fired – because the guard of every other one is false – needs the guard too.

theorem DescriptiveComplexity.Draw.Data.rest_eq_of_tape {L : FirstOrder.Language} {dt : Data L} {A R' P' : Type} [Fintype dt.SlotIx] {PR : Prog A R' P' dt.CtlIx dt.SlotIx dt.KIx dt.dd} {rest rest' : (Univ A R' P' dt.KIx dt.dd → Prop) → dt.SlotIx → A} (h : wideTape (fun (r : Univ A R' P' dt.KIx dt.dd → Prop) => PR.syElt (rest r)) (PR.syElt PR.blank) = wideTape (fun (r : Univ A R' P' dt.KIx dt.dd → Prop) => PR.syElt (rest' r)) (PR.syElt PR.blank)) : rest = rest'

A symbol determines its tracks: the payload is the packed track vector and the packing is injective, so two recognized tapes that are equal carry equal tracks. That is what lets a reading combine facts proved of different recognitions of the same run – the shape's, and the marker's.

theorem DescriptiveComplexity.Draw.Data.step_state_dst {L : FirstOrder.Language} {dt : Data L} {A R' P' : Type} [LinearOrder A] [LinearOrder R'] [LinearOrder P'] [LinearOrder dt.KIx] [FirstOrder.Language.wide.Structure (Univ A R' P' dt.KIx dt.dd)] [Fintype dt.SlotIx] {PR : Prog A R' P' dt.CtlIx dt.SlotIx dt.KIx dt.dd} (hR : PR.table.Reads) {x y : Config (WPoint (Univ A R' P' dt.KIx dt.dd))} (hstep : (wideData (Univ A R' P' dt.KIx dt.dd)).Step x y) : ∃ (r : R') (f : Fin (Fintype.card (dt.CtlIx ⊕ dt.SlotIx)) → A), y.state = Sum.inr (stateElt PR.zero (PR.rules r).dstPh f)

The state a step lands in is a rule's destination: which is how a reading learns that a phase no rule enters – the start phase – occurs at time zero and never again.

theorem DescriptiveComplexity.Draw.Data.step_track_set {L : FirstOrder.Language} {dt : Data L} {A R' P' : Type} [LinearOrder A] [LinearOrder R'] [LinearOrder P'] [LinearOrder dt.KIx] [FirstOrder.Language.wide.Structure (Univ A R' P' dt.KIx dt.dd)] [Fintype dt.SlotIx] {PR : Prog A R' P' dt.CtlIx dt.SlotIx dt.KIx dt.dd} (hR : PR.table.Reads) {Ph : P' → Prop} {t : dt.SlotIx} {x y : Config (WPoint (Univ A R' P' dt.KIx dt.dd))} {rest : (Univ A R' P' dt.KIx dt.dd → Prop) → dt.SlotIx → A} {v : Univ A R' P' dt.KIx dt.dd → Prop} (hhead : x.head = Sum.inl v) (htape : x.tape = wideTape (fun (r : Univ A R' P' dt.KIx dt.dd → Prop) => PR.syElt (rest r)) (PR.syElt PR.blank)) (hset : ∀ (r : R'), Ph (PR.table.srcPh r) → Rule.SetsSlot dt PR.one t (PR.rules r)) (hzero : ∀ (r : Univ A R' P' dt.KIx dt.dd → Prop), rest r t = PR.zero) (hph : ∀ (p : P') (f : Fin (Fintype.card (dt.CtlIx ⊕ dt.SlotIx)) → A), x.state = Sum.inr (stateElt PR.zero p f) → Ph p) (hstep : (wideData (Univ A R' P' dt.KIx dt.dd)).Step x y) : ∃ (rest' : (Univ A R' P' dt.KIx dt.dd → Prop) → dt.SlotIx → A), y.tape = wideTape (fun (r : Univ A R' P' dt.KIx dt.dd → Prop) => PR.syElt (rest' r)) (PR.syElt PR.blank) ∧ ∀ (s : Univ A R' P' dt.KIx dt.dd → Prop), rest' s t = bitVal PR.zero PR.one (s = v)

A step that fires a rule setting a slot leaves that track marking the cell it was written at – provided the track was clear before, which at the channel's tape it is (initBackReg_track_zero). This is the one write of the opening a backward reading has to read, rather than merely skip: the start step's marker, which every later rule keeps (nexRule_keepsSlot_wk_bot).

theorem DescriptiveComplexity.Draw.Data.track_const_of_seq {L : FirstOrder.Language} {dt : Data L} {A R' P' : Type} [LinearOrder A] [LinearOrder R'] [LinearOrder P'] [LinearOrder dt.KIx] [FirstOrder.Language.wide.Structure (Univ A R' P' dt.KIx dt.dd)] [Fintype dt.SlotIx] {PR : Prog A R' P' dt.CtlIx dt.SlotIx dt.KIx dt.dd} (hR : PR.table.Reads) {Ph : P' → Prop} {t : dt.SlotIx} (hkeep : ∀ (r : R'), Ph (PR.table.srcPh r) → Rule.KeepsSlot dt t (PR.rules r)) (g : ℕ → Config (WPoint (Univ A R' P' dt.KIx dt.dd))) (hhead : ∀ (i : ℕ), ∃ (v : Univ A R' P' dt.KIx dt.dd → Prop), (g i).head = Sum.inl v) {rest₀ : (Univ A R' P' dt.KIx dt.dd → Prop) → dt.SlotIx → A} (h0 : (g 0).tape = wideTape (fun (r : Univ A R' P' dt.KIx dt.dd → Prop) => PR.syElt (rest₀ r)) (PR.syElt PR.blank)) (n : ℕ) (hstep : ∀ i < n, (wideData (Univ A R' P' dt.KIx dt.dd)).Step (g i) (g (i + 1))) (hph : ∀ i < n, ∀ (p : P') (f : Fin (Fintype.card (dt.CtlIx ⊕ dt.SlotIx)) → A), (g i).state = Sum.inr (stateElt PR.zero p f) → Ph p) : ∃ (rest : (Univ A R' P' dt.KIx dt.dd → Prop) → dt.SlotIx → A), (g n).tape = wideTape (fun (r : Univ A R' P' dt.KIx dt.dd → Prop) => PR.syElt (rest r)) (PR.syElt PR.blank) ∧ ∀ (r : Univ A R' P' dt.KIx dt.dd → Prop), rest r t = rest₀ r t

A track the opening never writes still holds what it held: the same induction as the shape's, carried on one slot. Together with nexRule_keepsSlot_wk_bot and nexRule_keepsSlot_old this is how a backward reading learns what the tracks hold, not merely that they hold bits.

theorem DescriptiveComplexity.Draw.Data.track_set_of_seq {L : FirstOrder.Language} {dt : Data L} {A R' P' : Type} [LinearOrder A] [LinearOrder R'] [LinearOrder P'] [LinearOrder dt.KIx] [FirstOrder.Language.wide.Structure (Univ A R' P' dt.KIx dt.dd)] [Fintype dt.SlotIx] {PR : Prog A R' P' dt.CtlIx dt.SlotIx dt.KIx dt.dd} (hR : PR.table.Reads) {Ph Ph₀ : P' → Prop} {t : dt.SlotIx} (hset : ∀ (r : R'), Ph₀ (PR.table.srcPh r) → Rule.SetsSlot dt PR.one t (PR.rules r)) (hkeep : ∀ (r : R'), Ph (PR.table.srcPh r) → Rule.KeepsSlot dt t (PR.rules r)) (g : ℕ → Config (WPoint (Univ A R' P' dt.KIx dt.dd))) (hhead : ∀ (i : ℕ), ∃ (v : Univ A R' P' dt.KIx dt.dd → Prop), (g i).head = Sum.inl v) {rest₀ : (Univ A R' P' dt.KIx dt.dd → Prop) → dt.SlotIx → A} (h0 : (g 0).tape = wideTape (fun (r : Univ A R' P' dt.KIx dt.dd → Prop) => PR.syElt (rest₀ r)) (PR.syElt PR.blank)) (hzero : ∀ (r : Univ A R' P' dt.KIx dt.dd → Prop), rest₀ r t = PR.zero) {v₀ : Univ A R' P' dt.KIx dt.dd → Prop} (hhead0 : (g 0).head = Sum.inl v₀) (n : ℕ) (hn : 0 < n) (hstep : ∀ i < n, (wideData (Univ A R' P' dt.KIx dt.dd)).Step (g i) (g (i + 1))) (hph₀ : ∀ (p : P') (f : Fin (Fintype.card (dt.CtlIx ⊕ dt.SlotIx)) → A), (g 0).state = Sum.inr (stateElt PR.zero p f) → Ph₀ p) (hph : ∀ (i : ℕ), 0 < i → i < n → ∀ (p : P') (f : Fin (Fintype.card (dt.CtlIx ⊕ dt.SlotIx)) → A), (g i).state = Sum.inr (stateElt PR.zero p f) → Ph p) : ∃ (rest : (Univ A R' P' dt.KIx dt.dd → Prop) → dt.SlotIx → A), (g n).tape = wideTape (fun (r : Univ A R' P' dt.KIx dt.dd → Prop) => PR.syElt (rest r)) (PR.syElt PR.blank) ∧ ∀ (s : Univ A R' P' dt.KIx dt.dd → Prop), rest s t = bitVal PR.zero PR.one (s = v₀)

The marker, along a run: the first step writes it at the cell the head began on and every later step keeps it, so at any time after the first the track marks that cell and nothing else. With ixBack_wk_inv this is «the working track marks the address the machine started at», the first of the hypotheses the evaluation's entry state is asked for.