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.argOut_injective {R P : Type} {ko ki : ℕ} : Function.Injective (argOut ki)

theorem DescriptiveComplexity.Draw.lt_iff_tagKey {R P : Type} [LinearOrder R] [LinearOrder P] {K : Type} [LinearOrder K] (σ τ : Tag R P K) : σ < τ ↔ tagKey σ < tagKey τ

The strict tag order through the key.

theorem DescriptiveComplexity.Draw.arg_lt_arg_iff {R P : Type} [LinearOrder R] [LinearOrder P] {K : Type} [LinearOrder K] (i i' : K) : Tag.arg i < Tag.arg i' ↔ i < i'

Argument tags compare by their block index.

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

theorem DescriptiveComplexity.Draw.wmBlk_outAddr {A R P : Type} {ko ki dd : ℕ} (V : Fin ko → (Fin dd → A) → Prop) (k : Fin ko) : wmBlk (outAddr V) (argOut ki k) = V k

The outer blocks of outAddr are the given family.

theorem DescriptiveComplexity.Draw.outAddr_of_blocks {A R P : Type} {ko ki dd : ℕ} {V : Fin ko → (Fin dd → A) → Prop} {s : Univ A R P (Fin ko ⊕ₗ Fin ki) dd → Prop} (hblk : ∀ (k : Fin ko), wmBlk s (argOut ki k) = V k) (hsupp : ∀ (u : Univ A R P (Fin ko ⊕ₗ Fin ki) dd), s u → ∃ (k : Fin ko), u.1 = argOut ki k) : s = outAddr V

An address that marks outer argument blocks alone is outAddr of its blocks. This is the uniqueness that turns a reading of the blocks into a reading of the address, and with it a set of marked addresses into a stage.

theorem DescriptiveComplexity.Draw.outAddr_junk {A R P : Type} {ko ki dd : ℕ} (V : Fin ko → (Fin dd → A) → Prop) {t : Tag R P (Fin ko ⊕ₗ Fin ki)} (ht : ∀ (i : Fin ko ⊕ₗ Fin ki), t ≠ Tag.arg i) (v : Fin dd → A) : ¬outAddr V (t, v)

The non-argument blocks of outAddr are empty, which is what puts the working cell in the logical interval.

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.

theorem DescriptiveComplexity.Draw.not_trackOf_of_notEnc {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} {ℓ₀ : Fin (d.B.arity i)} (hℓ : ∀ (p : X.Map A), wmBlk s (argOut ki (Fin.castLE ha ℓ₀)) ≠ encMap ly zero one p) : ¬trackOf ly zero one ha σ s

A track is empty at an address that encodes no tuple: one block below the variable's arity holding no point is enough, whatever the stage. This is what the junk addresses of a sweep write, and it is why a program may leave them alone.

theorem DescriptiveComplexity.Draw.nonempty_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)} {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} (ℓ₀ : Fin (d.B.arity i)) (h : trackOf ly zero one ha σ s) : ∃ (y : Univ A R P (Fin ko ⊕ₗ Fin ki) dd), s y

A track marks no empty address: a variable of positive arity has a block below its arity encoding a point, and an encoding always holds its tag's own tuple, so an address the track marks has an element in that block. This is what puts a dictionary entry inside a clocked program's guessed stretch, whose bottom is the file's first register and not the empty address.

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.

theorem DescriptiveComplexity.Draw.wmBlk_tupAddr {R P : Type} {ko ki dd : ℕ} {L : FirstOrder.Language} {X : ExpExpansion L} {A : Type} [L.Structure A] [LinearOrder A] {d : StepDef (X.E.sum FirstOrder.Language.order)} {ly : EncLayout (PtCode X) (blockArityBound X.B) dd} {zero one : A} {i : d.B.ι} (ha : d.B.arity i ≤ ko) (x : Fin (d.B.arity i) → X.Map A) (ℓ : Fin (d.B.arity i)) : wmBlk (tupAddr ly zero one ha x) (argOut ki (Fin.castLE ha ℓ)) = encMap ly zero one (x ℓ)

Its blocks below the variable's arity are the tuple's encodings.

theorem DescriptiveComplexity.Draw.tupAddr_of_blocks {R P : Type} {ko ki dd : ℕ} {L : FirstOrder.Language} {X : ExpExpansion L} {A : Type} [L.Structure A] [LinearOrder A] {d : StepDef (X.E.sum FirstOrder.Language.order)} {ly : EncLayout (PtCode X) (blockArityBound X.B) dd} {zero one : A} {i : d.B.ι} (ha : d.B.arity i ≤ ko) {s : Univ A R P (Fin ko ⊕ₗ Fin ki) dd → Prop} {x : Fin (d.B.arity i) → X.Map A} (hblk : ∀ (ℓ : Fin (d.B.arity i)), wmBlk s (argOut ki (Fin.castLE ha ℓ)) = encMap ly zero one (x ℓ)) (hbeyond : ∀ (k : Fin ko), d.B.arity i ≤ ↑k → ∀ (v : Fin dd → A), ¬wmBlk s (argOut ki k) v) (hsupp : ∀ (u : Univ A R P (Fin ko ⊕ₗ Fin ki) dd), s u → ∃ (k : Fin ko), u.1 = argOut ki k) : s = tupAddr ly zero one ha x

An address whose blocks below the arity are the encodings, and which marks nothing else, is the tuple's address. The addresses a stage atom builds are of that kind – written block by block from named registers – so the dictionary a backward reading needs is asked exactly where trackOf_assignOfTrack answers it.

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.trackOf_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)} (hne : zero ≠ one) (ha : ∀ (i : d.B.ι), d.B.arity i ≤ ko) (T : d.B.ι → (Univ A R P (Fin ko ⊕ₗ Fin ki) dd → Prop) → Prop) {i : d.B.ι} (x : Fin (d.B.arity i) → X.Map A) : trackOf ly zero one ⋯ (assignOfTrack ly zero one ha T) (tupAddr ly zero one ⋯ x) ↔ T i (tupAddr ly zero one ⋯ x)

And it reads back: at the address a tuple names, the track of the assignment a track carries is that track. So a run that left an arbitrary set of addresses marked has left the stage of a definite assignment, as far as the evaluation ever looks.

theorem DescriptiveComplexity.Draw.wmSetLe_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] (hV : IsLinOrd tupLeLex) {i : d.B.ι} (ha : d.B.arity i ≤ ko) (x : Fin (d.B.arity i) → X.Map A) : WMSetLe (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 lies in the logical interval: its non-argument blocks are empty, which is exactly wmSetLe_logicalTop's hypothesis. What is not automatic is that it lies strictly below the top – the reduction owes that where it plants the end marker.

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.