What the inner loop computes

The VAL register of the EXPSPACE program enumerates addresses supported on the inner argument blocks, from the empty one to the full one, and the control folds one leaf per address. This file says what that fold is worth: at the inner top it is one step of the iteration at the points the working address holds.

The dictionary, fixed here once and for all:

• level j of a variable's pack is inner block j of the register – the free levels included, although the machine reads those off the working address's outer blocks (DescriptiveComplexity.Draw.Data.levelVal);
• the leaf is the gated matrix of DescriptiveComplexity.Problems.Wide.DrawRel at that valuation (DescriptiveComplexity.Draw.Data.leafP), so the encodings' gates are part of the leaf and not of the loop.

DescriptiveComplexity.Draw.Data.altQuantFrom_leafP is the join: the prefix of the leaf predicate over all ki blocks, from level 0, is DescriptiveComplexity.StepDef.next at the encoded arguments. The two ends of the mismatch are paid for by DescriptiveComplexity.Problems.Wide.DrawPad – the free levels and the levels past the pack are skipped, the starting valuation is never read at level 0 – and the middle by DescriptiveComplexity.Draw.StepDef.next_iff_gateMat. foldFrom_leafP_top then reads it off the accumulators, at the address the loop stops at.

The leaf predicate

noncomputable def DescriptiveComplexity.Draw.Data.levelVal {L : FirstOrder.Language} (dt : Data L) {A : Type} (v : dt.VarIx) (mb : Fin dt.ko → (Fin dt.dd → A) → Prop) (w : Fin dt.ki → (Fin dt.dd → A) → Prop) : Fin (dt.nOf v) → (Fin dt.dd → A) → Prop

The valuation the levels of a pack read: the working address's outer blocks below the variable's arity – those are the arguments the stage is being computed at – and the register's inner blocks above it.

Equations

• dt.levelVal v mb w j = if h : ↑j < dt.arOf v then mb ⟨↑j, ⋯⟩ else w ⟨↑j, ⋯⟩

noncomputable def DescriptiveComplexity.Draw.Data.freeVal {L : FirstOrder.Language} (dt : Data L) {A : Type} (v : dt.VarIx) (mb : Fin dt.ko → (Fin dt.dd → A) → Prop) (u : Fin (dt.nOf v) → (Fin dt.dd → A) → Prop) : Fin (dt.nOf v) → (Fin dt.dd → A) → Prop

The same valuation over the pack's own levels: the free ones off the working address, the quantified ones as given.

Equations

• dt.freeVal v mb u j = if h : ↑j < dt.arOf v then mb ⟨↑j, ⋯⟩ else u j

noncomputable def DescriptiveComplexity.Draw.Data.matHolds {L : FirstOrder.Language} (dt : Data L) {A : Type} [L.Structure A] [LinearOrder A] [LinearOrder (dt.X.Map A)] (v : dt.VarIx) (σ : dt.d.B.Assignment (dt.X.Map A)) : (Fin (dt.nOf v) → dt.X.Map A) → Prop

The matrix of a variable's pack, read over points at a stage.

Equations

• dt.matHolds v σ u = (dt.matOf v).Realize default u

noncomputable def DescriptiveComplexity.Draw.Data.gateHolds {L : FirstOrder.Language} (dt : Data L) {A : Type} [L.Structure A] [LinearOrder A] [Finite A] [Nonempty A] [LinearOrder (dt.X.Map A)] (zero one : A) (v : dt.VarIx) (σ : dt.d.B.Assignment (dt.X.Map A)) : (Fin (dt.nOf v) → (Fin dt.dd → A) → Prop) → Prop

The gated matrix over block values: the encodings' gates, then the matrix at the decoded points – the leaf of the relativized prefix.

Equations

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

noncomputable def DescriptiveComplexity.Draw.Data.leafP {L : FirstOrder.Language} (dt : Data L) {A : Type} [L.Structure A] [LinearOrder A] [Finite A] [Nonempty A] [LinearOrder (dt.X.Map A)] (zero one : A) (v : dt.VarIx) (σ : dt.d.B.Assignment (dt.X.Map A)) (mb : Fin dt.ko → (Fin dt.dd → A) → Prop) : (Fin dt.ki → (Fin dt.dd → A) → Prop) → Prop

The leaf the machine folds, one per address of the VAL register: the gated matrix at the levels' values.

Equations

• dt.leafP zero one v σ mb w = dt.gateHolds zero one v σ (dt.levelVal v mb w)

theorem DescriptiveComplexity.Draw.Data.leafP_eq_pad {L : FirstOrder.Language} {dt : Data L} {A : Type} [L.Structure A] [LinearOrder A] [Finite A] [Nonempty A] [LinearOrder (dt.X.Map A)] {zero one : A} (v : dt.VarIx) (σ : dt.d.B.Assignment (dt.X.Map A)) (mb : Fin dt.ko → (Fin dt.dd → A) → Prop) (w : Fin dt.ki → (Fin dt.dd → A) → Prop) : dt.leafP zero one v σ mb w = (fun (u : Fin (dt.nOf v) → (Fin dt.dd → A) → Prop) => dt.gateHolds zero one v σ (dt.freeVal v mb u)) fun (j : Fin (dt.nOf v)) => w (Fin.castLE ⋯ j)

The leaf is the pack-level predicate padded to the register's blocks.

theorem DescriptiveComplexity.Draw.Data.leafP_irrel {L : FirstOrder.Language} {dt : Data L} {A : Type} [L.Structure A] [LinearOrder A] [Finite A] [Nonempty A] [LinearOrder (dt.X.Map A)] {zero one : A} (v : dt.VarIx) (σ : dt.d.B.Assignment (dt.X.Map A)) (mb : Fin dt.ko → (Fin dt.dd → A) → Prop) {ℓ : Fin dt.ki} (hℓ : ↑ℓ < dt.arOf v ∨ dt.nOf v ≤ ↑ℓ) (w : Fin dt.ki → (Fin dt.dd → A) → Prop) (a : (Fin dt.dd → A) → Prop) : dt.leafP zero one v σ mb (Function.update w ℓ a) ↔ dt.leafP zero one v σ mb w

The leaf ignores the register blocks the pack does not quantify: those below the variable's arity, whose values it reads off the working address, and those past its prefix, which nothing reads.

theorem DescriptiveComplexity.Draw.Data.leafP_iff_split {L : FirstOrder.Language} {dt : Data L} {A : Type} [L.Structure A] [LinearOrder A] [Finite A] [Nonempty A] [LinearOrder (dt.X.Map A)] {zero one : A} (v : dt.VarIx) (σ : dt.d.B.Assignment (dt.X.Map A)) (mb : Fin dt.ko → (Fin dt.dd → A) → Prop) (w : Fin dt.ki → (Fin dt.dd → A) → Prop) (houter : ∀ (k : Fin dt.ko), ↑k < dt.arOf v → IsEnc dt.ly zero one (mb k)) : dt.leafP zero one v σ mb w ↔ (∀ (j : Fin (dt.nOf v)), dt.arOf v ≤ ↑j → dt.polOf v ↑j = true → IsEnc dt.ly zero one (w ⟨↑j, ⋯⟩)) ∧ ((∀ (j : Fin (dt.nOf v)), dt.arOf v ≤ ↑j → dt.polOf v ↑j = false → IsEnc dt.ly zero one (w ⟨↑j, ⋯⟩)) → dt.matHolds v σ fun (j : Fin (dt.nOf v)) => Function.invFun (encMap dt.ly zero one) (dt.levelVal v mb w j))

The leaf, machine-shaped: at an address whose outer blocks encode points, the leaf splits into the two flags the machinery conjoins – every ∃-level of the register an encoding, and if every ∀-level is one, the matrix at the decoded valuation. The free levels' gates are absorbed by the address's.

The join

theorem DescriptiveComplexity.Draw.Data.altQuantFrom_leafP {L : FirstOrder.Language} {dt : Data L} {A : Type} [L.Structure A] [LinearOrder A] [Finite A] [Nonempty A] [LinearOrder (dt.X.Map A)] {zero one : A} (hzo : zero ≠ one) (i : dt.d.B.ι) (σ : dt.d.B.Assignment (dt.X.Map A)) (mb : Fin dt.ko → (Fin dt.dd → A) → Prop) (x : Fin (dt.d.B.arity i) → dt.X.Map A) (hx : ∀ (ℓ : Fin (dt.d.B.arity i)), mb (Fin.castLE ⋯ ℓ) = encMap dt.ly zero one (x ℓ)) (w : Fin dt.ki → (Fin dt.dd → A) → Prop) : altQuantFrom (dt.polOf (some i)) (dt.leafP zero one (some i) σ mb) 0 w ↔ dt.d.next σ i x

The inner loop computes the step formula. The prefix of the leaf predicate over every block of the register, played from level 0, is one step of the iteration at the points the working address's outer blocks encode – whatever the register held when the loop began, since level 0 reads nothing.

The three mismatches between what the machine plays and what the pack asks for are exactly the three lemmas of DescriptiveComplexity.Problems.Wide.DrawPad: the free levels are skipped, the levels past the prefix are padding, and below the prefix's start the machine's leaf reads the working address where the pack reads its valuation.

theorem DescriptiveComplexity.Draw.Data.altQuantFrom_leafP_out {L : FirstOrder.Language} {dt : Data L} {A : Type} [L.Structure A] [LinearOrder A] [Finite A] [Nonempty A] [LinearOrder (dt.X.Map A)] {zero one : A} (hzo : zero ≠ one) (σ : dt.d.B.Assignment (dt.X.Map A)) (mb : Fin dt.ko → (Fin dt.dd → A) → Prop) (w : Fin dt.ki → (Fin dt.dd → A) → Prop) : altQuantFrom (dt.polOf none) (dt.leafP zero one none σ mb) 0 w ↔ dt.X.Map A ⊨ dt.d.out

The inner loop at the output variable computes the output sentence. The same three mismatches as altQuantFrom_leafP, minus the free levels: a sentence has none, so the prefix starts where the machine starts it and only the padding past the pack has to be skipped.

Read off the accumulators

theorem DescriptiveComplexity.Draw.Data.foldFrom_leafP_top {L : FirstOrder.Language} {dt : Data L} {A : Type} [L.Structure A] [LinearOrder A] [Finite A] [Nonempty A] [LinearOrder (dt.X.Map A)] {zero one : A} {R' P' : Type} (hzo : zero ≠ one) {LeV : (Fin dt.dd → A) → (Fin dt.dd → A) → Prop} (hLeV : IsLinOrd LeV) (i : dt.d.B.ι) (σ : dt.d.B.Assignment (dt.X.Map A)) (mb : Fin dt.ko → (Fin dt.dd → A) → Prop) (x : Fin (dt.d.B.arity i) → dt.X.Map A) (hx : ∀ (ℓ : Fin (dt.d.B.arity i)), mb (Fin.castLE ⋯ ℓ) = encMap dt.ly zero one (x ℓ)) {s : Univ A R' P' dt.KIx dt.dd → Prop} (hfull : ∀ (j : Fin dt.ki) (v : Fin dt.dd → A), wmBlk s (argIn dt.ko j) v) : foldFrom (dt.polOf (some i)) (dt.leafP zero one (some i) σ mb) (WMSetLe LeV) 0 (ixBlk (argIn dt.ko) s) ↔ dt.d.next σ i x

At the inner top the fold holds the step's value. The loop stops when every inner block of the register is full; there the accumulator at level 0 is the whole prefix (DescriptiveComplexity.Draw.foldFrom_top_of_ix), hence one step of the iteration at the working address's points.