What one step of the iteration is, on the machine's side of the encoding

The EXPSPACE program computes the next stage of a partial fixed point at every logical address. This file states what it computes, with no machine in sight: one application of a step formula to a stage is an alternating prefix over the block values of an address, gated to the encodings, over the gated matrix.

Two pieces:

• DescriptiveComplexity.Draw.PrenexPack – a step formula with free variables, put once and for all into the prefix normal form of DescriptiveComplexity.altQuantFrom (DescriptiveComplexity.Draw.exists_prenexPack: rebind the free variables as the first bound ones, then FirstOrder.Language.BoundedFormula.toPrenex);
• DescriptiveComplexity.Draw.StepDef.next_iff_gateMat – the chain: one step of DescriptiveComplexity.StepDef.next at a tuple of points is the prefix over block values, read at any valuation whose first coordinates encode the tuple. The quantifiers move from points to block values by DescriptiveComplexity.Draw.altQuantFrom_gateMat, whose gate is DescriptiveComplexity.Draw.IsEnc.

The nullary case – a sentence, whose prefix is played from level 0 – is DescriptiveComplexity.Draw.sentence_iff_gateMat, stated at an arbitrary block and sentence rather than at a fixed-point definition, because two programs need it: the output evaluation of a fixed-point program (DescriptiveComplexity.Draw.StepDef.out_iff_gateMat) and the whole evaluation of a nondeterministic one, whose block is guessed rather than iterated.

The valuation's deeper coordinates are arbitrary – the machine's inner register starts them at whatever is left on its tracks – because a prefix only reads the coordinates below its level (DescriptiveComplexity.altQuantFrom_congr_val).

The linear order on the points is a parameter here (the step formula reads it through the structure); which order the reduction chooses – the pullback of the binary block-value order along the encoding, making order atoms the register comparison the machine can run – is its own decision, discharged where the machine meets the tape.

The prefix normal form of a formula with free variables

structure DescriptiveComplexity.Draw.PrenexPack {M : FirstOrder.Language} {k : ℕ} (φ : M.Formula (Fin k)) : Type 1

A formula in prefix normal form: the polarities and the quantifier-free matrix of an alternating prefix equivalent to φ, the free variables re-bound as the first k coordinates of the valuation. This is the data the machine's control is built from, so it is a structure rather than an existential.

• n : ℕ

  The total number of variables: the free ones first, then the prefix.

• kLe : k ≤ self.n

  The free variables come first.

• pol : ℕ → Bool

  The polarity of each level.

• mat : M.BoundedFormula Empty self.n

  The matrix.

• isQF : self.mat.IsQF

  The matrix is quantifier-free.

• spec (A : Type) [M.Structure A] [Nonempty A] (v : Fin self.n → A) (xs : Fin k → A) : (∀ (i : Fin k), xs i = v (Fin.castLE ⋯ i)) → (φ.Realize xs ↔ altQuantFrom self.pol (fun (w : Fin self.n → A) => self.mat.Realize default w) k v)

  The prefix from level k on, at a valuation whose first k coordinates hold the free variables, is the formula.

theorem DescriptiveComplexity.Draw.exists_prenexPack {M : FirstOrder.Language} {k : ℕ} (φ : M.Formula (Fin k)) : Nonempty (PrenexPack φ)

Every formula has a prefix normal form with its free variables re-bound as the first coordinates: relabel them into the context, take FirstOrder.Language.BoundedFormula.toPrenex, and read the prefix as a walk.

One step of the iteration, over block values

theorem DescriptiveComplexity.Draw.StepDef.next_iff_gateMat {L : FirstOrder.Language} {X : ExpExpansion L} {dd : ℕ} (ly : EncLayout (PtCode X) (blockArityBound X.B) dd) {A : Type} [L.Structure A] [LinearOrder A] [Finite A] [Nonempty A] {zero one : A} [LinearOrder (X.Map A)] {d : StepDef (X.E.sum FirstOrder.Language.order)} (hne : zero ≠ one) {i : d.B.ι} (pk : PrenexPack (d.step i)) (σ : d.B.Assignment (X.Map A)) (x : Fin (d.B.arity i) → X.Map A) {V : Fin pk.n → (Fin dd → A) → Prop} (hV : ∀ (j : Fin (d.B.arity i)), V (Fin.castLE ⋯ j) = encMap ly zero one (x j)) : d.next σ i x ↔ altQuantFrom pk.pol (gateMat (encMap ly zero one) (IsEnc ly zero one) pk.pol fun (w : Fin pk.n → X.Map A) => pk.mat.Realize default w) (d.B.arity i) V

One step of the iteration is the gated prefix over block values. The first coordinates of the valuation encode the argument tuple; the deeper ones are arbitrary, the prefix overwriting every coordinate it reads. This is the statement the machine's inner loop computes, one fold step per increment of its register.

theorem DescriptiveComplexity.Draw.sentence_iff_gateMat {L : FirstOrder.Language} {X : ExpExpansion L} {dd : ℕ} (ly : EncLayout (PtCode X) (blockArityBound X.B) dd) {A : Type} [L.Structure A] [LinearOrder A] [Finite A] [Nonempty A] {zero one : A} [LinearOrder (X.Map A)] (hne : zero ≠ one) {B : SOBlock} {φ : ((X.E.sum FirstOrder.Language.order).sum B.lang).Sentence} (pk : PrenexPack (FirstOrder.Language.Formula.relabel Empty.elim φ)) (σ : B.Assignment (X.Map A)) (V : Fin pk.n → (Fin dd → A) → Prop) : X.Map A ⊨ φ ↔ altQuantFrom pk.pol (gateMat (encMap ly zero one) (IsEnc ly zero one) pk.pol fun (w : Fin pk.n → X.Map A) => pk.mat.Realize default w) 0 V

A sentence is the gated prefix over block values. A sentence has no free level, so the prefix is played from level 0 and the valuation it starts from is arbitrary. This is the nullary case of DescriptiveComplexity.Draw.StepDef.next_iff_gateMat, and it is stated at an arbitrary block and sentence because two programs need it: the output evaluation of a fixed-point program, and the whole evaluation of a nondeterministic one, whose block is guessed rather than iterated.

theorem DescriptiveComplexity.Draw.StepDef.out_iff_gateMat {L : FirstOrder.Language} {X : ExpExpansion L} {dd : ℕ} (ly : EncLayout (PtCode X) (blockArityBound X.B) dd) {A : Type} [L.Structure A] [LinearOrder A] [Finite A] [Nonempty A] {zero one : A} [LinearOrder (X.Map A)] {d : StepDef (X.E.sum FirstOrder.Language.order)} (hne : zero ≠ one) (pk : PrenexPack (FirstOrder.Language.Formula.relabel Empty.elim d.out)) (σ : d.B.Assignment (X.Map A)) (V : Fin pk.n → (Fin dd → A) → Prop) : X.Map A ⊨ d.out ↔ altQuantFrom pk.pol (gateMat (encMap ly zero one) (IsEnc ly zero one) pk.pol fun (w : Fin pk.n → X.Map A) => pk.mat.Realize default w) 0 V

The output sentence is the gated prefix over block values: the previous statement at the fixed-point definition's own block, which is what the output evaluation's machinery computes where the fixed-point variables' computes DescriptiveComplexity.StepDef.next.