Levels a prefix's matrix does not read

The EXPSPACE program runs the quantifier prefix of a step formula on its VAL register, one inner argument block per level: level j of the pack is block j, whatever the pack. The register, though, has one block per level of the longest pack (ki), and the enumeration it can run – the binary increment from the empty address to the inner top – plays every block. So the machine plays a prefix that is too long at both ends:

• the levels below the pack's free-variable count are played although the matrix reads them off the working address (the MIRROR register) and not off VAL;
• the levels above the pack's own length are played although nothing reads them at all.

Both are harmless, and this file is why: a level whose matrix ignores it may be skipped, whatever its polarity (DescriptiveComplexity.Draw.altQuantFrom_skip, over a nonempty domain), and a matrix reading only the first n of N coordinates plays as its restriction (DescriptiveComplexity.Draw.altQuantFrom_pad). The third lemma, DescriptiveComplexity.Draw.altQuantFrom_congr_mat, is the one that lets the machine's leaf predicate differ from the pack's away from the valuations the walk can reach: from level j the walk only ever changes coordinates at or above j, so what the matrix does below them is the caller's business.

Everything here is about DescriptiveComplexity.altQuantFrom alone; no machine, no encoding.

The matrix is only read where the walk can go

theorem DescriptiveComplexity.Draw.altQuantFrom_congr_mat {α : Type u_1} {pol : ℕ → Bool} {n : ℕ} {P P' : (Fin n → α) → Prop} {j : ℕ} {v : Fin n → α} (h : ∀ (w : Fin n → α), (∀ (i : Fin n), ↑i < j → w i = v i) → (P w ↔ P' w)) : altQuantFrom pol P j v ↔ altQuantFrom pol P' j v

Two matrices agreeing on the valuations the walk reaches play the same. From level j the prefix only ever changes coordinates at or above j, so the matrix is read only at valuations agreeing with the starting one below j.

Levels the matrix ignores

theorem DescriptiveComplexity.Draw.altQuantFrom_update_irrel {α : Type u_1} {pol : ℕ → Bool} {n : ℕ} {P : (Fin n → α) → Prop} {ℓ : Fin n} (hirr : ∀ (w : Fin n → α) (a : α), P (Function.update w ℓ a) ↔ P w) (j : ℕ) (v : Fin n → α) (a : α) : altQuantFrom pol P j (Function.update v ℓ a) ↔ altQuantFrom pol P j v

A coordinate the matrix ignores may be overwritten at any point of the walk: the prefix's value does not change.

theorem DescriptiveComplexity.Draw.altQuantFrom_skip {α : Type u_1} {pol : ℕ → Bool} [Nonempty α] {n : ℕ} {P : (Fin n → α) → Prop} {j j' : ℕ} (hjj : j ≤ j') (hirr : ∀ (ℓ : Fin n), j ≤ ↑ℓ → ↑ℓ < j' → ∀ (w : Fin n → α) (a : α), P (Function.update w ℓ a) ↔ P w) (v : Fin n → α) : altQuantFrom pol P j v ↔ altQuantFrom pol P j' v

A stretch of levels the matrix ignores may be skipped: playing them changes nothing, whichever player they belong to. This is what lets the machine's inner loop enumerate the blocks the pack's free variables occupy – the matrix reads those off the working address – and the blocks past its prefix.

A prefix padded with unread levels

theorem DescriptiveComplexity.Draw.altQuantFrom_pad {α : Type u_1} {pol : ℕ → Bool} [Nonempty α] {n N : ℕ} (hnN : n ≤ N) {P : (Fin n → α) → Prop} {j : ℕ} (hj : j ≤ n) (v : Fin N → α) : altQuantFrom pol (fun (w : Fin N → α) => P fun (i : Fin n) => w (Fin.castLE hnN i)) j v ↔ altQuantFrom pol P j fun (i : Fin n) => v (Fin.castLE hnN i)

A prefix over more coordinates than its matrix reads plays as its restriction: the machine's register has one block per level of the longest pack, and the extra ones are the innermost quantifiers over variables nothing reads.