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.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)

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.

Read off the accumulators