The argument blocks, concretely: outer arguments first, inner variables last

The EXPSPACE program keeps two families of argument blocks (DescriptiveComplexity.Draw.Tag's K): the outer ones hold the arguments of the fixed-point variable at the working cell, the inner ones hold the valuations of the step formula's quantifier prefix, enumerated by the VAL register. This file fixes K := Fin ko ⊕ₗ Fin ki and proves the two facts the choice was made for:

• DescriptiveComplexity.Draw.kinSeg – the inner tags are an order embedding onto a final segment of the whole tag order, which is what hands the inner loop its fold rules (DescriptiveComplexity.Draw.exists_carry_ix and its consequences in DescriptiveComplexity.Problems.Wide.DrawInner);
• the stage dictionary – DescriptiveComplexity.Draw.trackOf, the content of a stage track at an address: the stage of the fixed-point variable at the decoded outer blocks when they decode, False when they do not. It reads only the blocks below the variable's arity (DescriptiveComplexity.Draw.trackOf_of_blocks), so a track may be read at any address with the right prefix – no canonical address, no gating – and the all-blank initial tape is exactly stage 0 (DescriptiveComplexity.Draw.trackOf_botAssign).

DescriptiveComplexity.Draw.outAddr builds the address a family of outer blocks is, with every other block empty; it is what the working cell of the sweep holds, and its non-argument blocks being empty is what puts it in the logical interval (DescriptiveComplexity.Draw.wmSetLe_logicalTop).

The two families of argument tags

def DescriptiveComplexity.Draw.argOut {R P : Type} {ko : ℕ} (ki : ℕ) (k : Fin ko) : Tag R P (Fin ko ⊕ₗ Fin ki)

An outer argument tag: one block per argument of the fixed-point variable.

Equations

• DescriptiveComplexity.Draw.argOut ki k = DescriptiveComplexity.Draw.Tag.arg (Sum.inlₗ k)

def DescriptiveComplexity.Draw.argIn {R P : Type} {ki : ℕ} (ko : ℕ) (j : Fin ki) : Tag R P (Fin ko ⊕ₗ Fin ki)

An inner argument tag: one block per variable of the quantifier prefix.

Equations

• DescriptiveComplexity.Draw.argIn ko j = DescriptiveComplexity.Draw.Tag.arg (Sum.inrₗ j)

theorem DescriptiveComplexity.Draw.kinSeg {R P : Type} {ko ki : ℕ} [LinearOrder R] [LinearOrder P] : IxSeg (fun (x1 x2 : Tag R P (Fin ko ⊕ₗ Fin ki)) => x1 ≤ x2) (argIn ko)

The inner tags are a final segment of the tag order: strictly monotone, and everything strictly above an inner tag is an inner tag – the non-argument tags and the outer arguments all come first. This is the hypothesis pack of the inner loop's fold rules.

The address a family of outer blocks is

def DescriptiveComplexity.Draw.outAddr {A R P : Type} {ko ki dd : ℕ} (V : Fin ko → (Fin dd → A) → Prop) : Univ A R P (Fin ko ⊕ₗ Fin ki) dd → Prop

The address holding given outer blocks and nothing else: what the working cell of the sweep is, its inner and non-argument blocks empty.

Equations

• DescriptiveComplexity.Draw.outAddr V u = ∃ (k : Fin ko), u.1 = DescriptiveComplexity.Draw.argOut ki k ∧ V k u.2

The stage dictionary

def DescriptiveComplexity.Draw.trackOf {R P : Type} {ko ki dd : ℕ} {L : FirstOrder.Language} {X : ExpExpansion L} (ly : EncLayout (PtCode X) (blockArityBound X.B) dd) {A : Type} [L.Structure A] [LinearOrder A] (zero one : A) {d : StepDef (X.E.sum FirstOrder.Language.order)} {i : d.B.ι} (ha : d.B.arity i ≤ ko) (σ : d.B.Assignment (X.Map A)) (s : Univ A R P (Fin ko ⊕ₗ Fin ki) dd → Prop) : Prop

The content of a stage track at an address: the stage of the variable at the decoded outer blocks when the blocks below its arity decode to points, False when they do not. Only those blocks are read, so the track may be read at any address with the right prefix, and the all-blank initial tape is exactly stage 0.

Equations

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

theorem DescriptiveComplexity.Draw.trackOf_of_blocks {R P : Type} {ko ki dd : ℕ} {L : FirstOrder.Language} {X : ExpExpansion L} {ly : EncLayout (PtCode X) (blockArityBound X.B) dd} {A : Type} [L.Structure A] [LinearOrder A] {zero one : A} {d : StepDef (X.E.sum FirstOrder.Language.order)} (hne : zero ≠ one) {i : d.B.ι} (ha : d.B.arity i ≤ ko) (σ : d.B.Assignment (X.Map A)) {s : Univ A R P (Fin ko ⊕ₗ Fin ki) dd → Prop} {x : Fin (d.B.arity i) → X.Map A} (hs : ∀ (ℓ : Fin (d.B.arity i)), wmBlk s (argOut ki (Fin.castLE ha ℓ)) = encMap ly zero one (x ℓ)) : trackOf ly zero one ha σ s ↔ σ i x

The dictionary reads back: at an address whose relevant blocks encode a tuple, the track holds the stage at that tuple.

def DescriptiveComplexity.Draw.tupAddr {R P : Type} {ko ki dd : ℕ} {L : FirstOrder.Language} {X : ExpExpansion L} (ly : EncLayout (PtCode X) (blockArityBound X.B) dd) {A : Type} [L.Structure A] [LinearOrder A] (zero one : A) {d : StepDef (X.E.sum FirstOrder.Language.order)} {i : d.B.ι} (_ha : d.B.arity i ≤ ko) (x : Fin (d.B.arity i) → X.Map A) : Univ A R P (Fin ko ⊕ₗ Fin ki) dd → Prop

The address of a tuple of points: its outer blocks are the tuple's encodings, everything else empty – where the dictionary of a variable at that tuple is read.

Equations

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

def DescriptiveComplexity.Draw.assignOfTrack {R P : Type} {ko ki dd : ℕ} {L : FirstOrder.Language} {X : ExpExpansion L} (ly : EncLayout (PtCode X) (blockArityBound X.B) dd) {A : Type} [L.Structure A] [LinearOrder A] (zero one : A) {d : StepDef (X.E.sum FirstOrder.Language.order)} (ha : ∀ (i : d.B.ι), d.B.arity i ≤ ko) (T : d.B.ι → (Univ A R P (Fin ko ⊕ₗ Fin ki) dd → Prop) → Prop) : d.B.Assignment (X.Map A)

The assignment a track carries: a tuple is in the relation exactly when the address that names it is marked. This is the inverse the forward direction never needs – it writes trackOf of an assignment – and the one a backward reading is built on.

Equations

• DescriptiveComplexity.Draw.assignOfTrack ly zero one ha T i x = T i (DescriptiveComplexity.Draw.tupAddr ly zero one ⋯ x)

theorem DescriptiveComplexity.Draw.wmSetLt_tupAddr_logicalTop {R P : Type} {ko ki dd : ℕ} {L : FirstOrder.Language} {X : ExpExpansion L} {ly : EncLayout (PtCode X) (blockArityBound X.B) dd} {A : Type} [L.Structure A] [LinearOrder A] {zero one : A} {d : StepDef (X.E.sum FirstOrder.Language.order)} [LinearOrder R] [LinearOrder P] [Finite R] [Finite P] [Finite A] (hne : zero ≠ one) (hV : IsLinOrd tupLeLex) {i : d.B.ι} (ha : d.B.arity i ≤ ko) (x : Fin (d.B.arity i) → X.Map A) (ℓ : Fin (d.B.arity i)) : WMSetLt (lexRel (fun (x1 x2 : Tag R P (Fin ko ⊕ₗ Fin ki)) => x1 ≤ x2) tupLeLex) (tupAddr ly zero one ha x) logicalTop

A tuple's address is strictly below the logical top: the top's blocks are full, and an encoding is not (not_encPt_zeroTup). One position of the tuple is enough; at a nullary variable the address is the empty one, which is strictly below any nonempty top.

theorem DescriptiveComplexity.Draw.wmSetLt_logicalTop_of_isPad {R P : Type} {ko ki dd : ℕ} {A : Type} [LinearOrder A] [LinearOrder R] [LinearOrder P] [Finite R] [Finite P] [Finite A] {c : ℕ} {zero one : A} (hne : zero ≠ one) (hV : IsLinOrd tupLeLex) (hc : c < dd) (i : Fin ko ⊕ₗ Fin ki) {s : Univ A R P (Fin ko ⊕ₗ Fin ki) dd → Prop} (hjunk : ∀ (τ : Tag R P (Fin ko ⊕ₗ Fin ki)), (∀ (i : Fin ko ⊕ₗ Fin ki), τ ≠ Tag.arg i) → ∀ (v : Fin dd → A), ¬s (τ, v)) (hpad : ∀ (y : Univ A R P (Fin ko ⊕ₗ Fin ki) dd), s y → IsPad c zero y.2) : WMSetLt (lexRel (fun (x1 x2 : Tag R P (Fin ko ⊕ₗ Fin ki)) => x1 ≤ x2) tupLeLex) s logicalTop

A padded address of argument cells alone is strictly below the logical top: it is at or below it because its non-argument blocks are empty (wmSetLe_logicalTop), and it is not the top itself because the top's blocks are full – they hold the cells whose coordinates beyond the payload are not zero, and a padded address holds none of those. This is what an address a program builds out of padded cells (rather than reads from a register) has to offer, and it needs one coordinate of slack (c < dd) and one argument block to name (i) – the same nonemptiness the interval is given anyway.

theorem DescriptiveComplexity.Draw.wmSetLt_tupAddr_logicalTop' {R P : Type} {ko ki dd : ℕ} {L : FirstOrder.Language} {X : ExpExpansion L} {ly : EncLayout (PtCode X) (blockArityBound X.B) dd} {A : Type} [L.Structure A] [LinearOrder A] {zero one : A} {d : StepDef (X.E.sum FirstOrder.Language.order)} [LinearOrder R] [LinearOrder P] [Finite R] [Finite P] [Finite A] (hne : zero ≠ one) (hV : IsLinOrd tupLeLex) (i₀ : Fin ko ⊕ₗ Fin ki) {i : d.B.ι} (ha : d.B.arity i ≤ ko) (x : Fin (d.B.arity i) → X.Map A) : WMSetLt (lexRel (fun (x1 x2 : Tag R P (Fin ko ⊕ₗ Fin ki)) => x1 ≤ x2) tupLeLex) (tupAddr ly zero one ha x) logicalTop

A tuple's address is strictly below the logical top, at every arity: wmSetLt_tupAddr_logicalTop at a variable of arity ≥ 1, and at a nullary one the address is the empty one, which is strictly below any nonempty top – so what the nullary case asks for is an argument block to name, the same nonemptiness of the interval the run layer is given anyway. This is the form assignment_ext_of_trackOf's hS is discharged in.

theorem DescriptiveComplexity.Draw.assignment_ext_of_trackOf {R P : Type} {ko ki dd : ℕ} {L : FirstOrder.Language} {X : ExpExpansion L} {ly : EncLayout (PtCode X) (blockArityBound X.B) dd} {A : Type} [L.Structure A] [LinearOrder A] {zero one : A} {d : StepDef (X.E.sum FirstOrder.Language.order)} (hne : zero ≠ one) (ha : ∀ (i : d.B.ι), d.B.arity i ≤ ko) {σ σ' : d.B.Assignment (X.Map A)} (S : (Univ A R P (Fin ko ⊕ₗ Fin ki) dd → Prop) → Prop) (hS : ∀ (i : d.B.ι) (x : Fin (d.B.arity i) → X.Map A), S (tupAddr ly zero one ⋯ x)) (hagree : ∀ (s : Univ A R P (Fin ko ⊕ₗ Fin ki) dd → Prop), S s → ∀ (i : d.B.ι), trackOf ly zero one ⋯ σ s ↔ trackOf ly zero one ⋯ σ' s) : σ = σ'

The dictionary determines the stage: two assignments whose tracks agree at every address of a family that carries every tuple's own address are equal. This is what turns the machine's convergence test – the tracks of one stage and the next agreeing over the logical interval – back into «the stages are equal», which is what hnotconv needs.

theorem DescriptiveComplexity.Draw.trackOf_botAssign {R P : Type} {ko ki dd : ℕ} {L : FirstOrder.Language} {X : ExpExpansion L} {ly : EncLayout (PtCode X) (blockArityBound X.B) dd} {A : Type} [L.Structure A] [LinearOrder A] {zero one : A} {d : StepDef (X.E.sum FirstOrder.Language.order)} {i : d.B.ι} (ha : d.B.arity i ≤ ko) (s : Univ A R P (Fin ko ⊕ₗ Fin ki) dd → Prop) : ¬trackOf ly zero one ha (d.B.botAssign (X.Map A)) s

The empty stage writes an empty track: at the bottom assignment nothing holds, whatever the address – the all-blank initial tape is stage 0.