The address primitives of a wide machine

What a wide machine can do to its head, and nothing else: start it on the least position, move it to a neighbor, recognize the last one. Every step of every program a hardness reduction will write is one of these, so they are settled first, at an arbitrary order relation and from finiteness alone.

The one thing to know about them is what an address's neighbor is. An address is a subset read as a binary number whose most significant digit is the Le-least element (DescriptiveComplexity.WMSetLe compares at the least element where two addresses differ), so incrementing flips a run of trailing digits: the greatest element u outside the address enters, and everything above u leaves. DescriptiveComplexity.WMIncr says that relationally – with u existentially quantified rather than chosen – so no choice function enters the statements and the increment is first-order describable as it stands.

primitive	what it is	theorem
the head's start	the empty address	DescriptiveComplexity.minPos_wpLe
the last cell	the whole universe	DescriptiveComplexity.maxPos_wpLe
one step	the binary increment	DescriptiveComplexity.succPos_wpLe_iff

The last of these is the one the programs use: DescriptiveComplexity.TMData.Step moves the head by DescriptiveComplexity.SuccPos, an order-theoretic notion (“no position strictly between”), while a program reasons with the increment. The two agree, which is what lets a machine maintain a mirror of its own head position by incrementing it – the invariant the whole hardness plan rests on, since a head cannot read the digits of its address.

Extremal elements of a definable set

theorem DescriptiveComplexity.exists_least {α : Type} [Finite α] {Le : α → α → Prop} (h : IsLinOrd Le) {P : α → Prop} (hne : ∃ (x : α), P x) : ∃ (x : α), P x ∧ ∀ (y : α), P y → Le x y

A nonempty set has a Le-least element.

theorem DescriptiveComplexity.exists_greatest {α : Type} [Finite α] {Le : α → α → Prop} (h : IsLinOrd Le) {P : α → Prop} (hne : ∃ (x : α), P x) : ∃ (x : α), P x ∧ ∀ (y : α), P y → Le y x

A nonempty set has a Le-greatest element.

The strict order, and the strict comparison of addresses

def DescriptiveComplexity.WMLt {α : Type} (Le : α → α → Prop) (x y : α) : Prop

The strict part of an order relation, in the shape the address layer writes it.

Equations

• DescriptiveComplexity.WMLt Le x y = (Le x y ∧ ¬Le y x)

def DescriptiveComplexity.WMSetLt {α : Type} (Le : α → α → Prop) (s t : α → Prop) : Prop

The strict comparison of two addresses: at some element the first is out of and the second in, they agree at every strictly smaller element. This is the second disjunct of DescriptiveComplexity.WMSetLe, named.

Equations

• DescriptiveComplexity.WMSetLt Le s t = ∃ (x : α), (∀ (y : α), DescriptiveComplexity.WMLt Le y x → (s y ↔ t y)) ∧ ¬s x ∧ t x

theorem DescriptiveComplexity.wmSetLe_iff_wmSetLt {α : Type} (Le : α → α → Prop) (s t : α → Prop) : WMSetLe Le s t ↔ (∀ (x : α), s x ↔ t x) ∨ WMSetLt Le s t

Weak comparison of addresses is agreement or strict comparison, by definition.

theorem DescriptiveComplexity.eq_of_not_wmLt {α : Type} {Le : α → α → Prop} (h : IsLinOrd Le) {x y : α} (h1 : ¬WMLt Le x y) (h2 : ¬WMLt Le y x) : x = y

Two elements neither of which is strictly below the other are equal.

The increment of an address

def DescriptiveComplexity.WMIncr {α : Type} (Le : α → α → Prop) (s t : α → Prop) : Prop

The binary increment of an address: at the greatest element u the address does not contain – so that it contains everything strictly above u – the increment adds u and removes everything strictly above it. The carry position is quantified, not chosen: nothing here needs a choice function, and the relation is first-order in the two addresses.

Equations

• DescriptiveComplexity.WMIncr Le s t = ∃ (u : α), ¬s u ∧ (∀ (v : α), DescriptiveComplexity.WMLt Le u v → s v) ∧ ∀ (v : α), t v ↔ v = u ∨ s v ∧ ¬DescriptiveComplexity.WMLt Le u v

theorem DescriptiveComplexity.wmIncr_carry_unique {α : Type} {Le : α → α → Prop} (h : IsLinOrd Le) {s : α → Prop} {u u' : α} (hu : ¬s u) (hau : ∀ (v : α), WMLt Le u v → s v) (hu' : ¬s u') (hau' : ∀ (v : α), WMLt Le u' v → s v) : u = u'

The carry position of an increment is unique: it is the greatest element outside the address, and an address has only one such.

theorem DescriptiveComplexity.wmIncr_functional {α : Type} {Le : α → α → Prop} (h : IsLinOrd Le) {s t t' : α → Prop} (hi : WMIncr Le s t) (hi' : WMIncr Le s t') : t = t'

The increment is unique, so a program stepping by it is deterministic.

theorem DescriptiveComplexity.wmSetLe_of_wmIncr {α : Type} {Le : α → α → Prop} {s t : α → Prop} (hi : WMIncr Le s t) : WMSetLe Le s t

The increment is above the address: they differ at the carry position, and agree at every element below it – that is, above it in significance.

theorem DescriptiveComplexity.ne_of_wmIncr {α : Type} {Le : α → α → Prop} {s t : α → Prop} (hi : WMIncr Le s t) : s ≠ t

The increment differs from the address, at the carry position.

theorem DescriptiveComplexity.exists_wmIncr {α : Type} {Le : α → α → Prop} [Finite α] (h : IsLinOrd Le) {s : α → Prop} (hne : ∃ (x : α), ¬s x) : ∃ (t : α → Prop), WMIncr Le s t

Every address but the last has an increment.

theorem DescriptiveComplexity.exists_wmPred {α : Type} {Le : α → α → Prop} [Finite α] (h : IsLinOrd Le) {s : α → Prop} (hne : ∃ (x : α), s x) : ∃ (t : α → Prop), WMIncr Le t s

Every address but the first has a predecessor. The carry position of the step into an address is the greatest element that address contains: everything above it leaves, and it is what the increment put there. A program walking its mirror downwards – which is what an increment does, the least significant digit being the Le-greatest element – needs this end of the statement.

theorem DescriptiveComplexity.wmSetLt_iff {α : Type} {Le : α → α → Prop} (s t : α → Prop) : WMSetLt Le s t ↔ WMSetLe Le s t ∧ s ≠ t

Strict comparison of addresses is weak comparison plus difference.

theorem DescriptiveComplexity.subset_of_wmSetLe {α : Type} {Le : α → α → Prop} (h : IsLinOrd Le) {s t : α → Prop} (hup : ∀ (x y : α), t x → WMLt Le x y → t y) (hle : WMSetLe Le s t) {x : α} (hx : s x) : t x

A set below an upward-closed address is contained in it: at the element where they first differ the smaller one says no, and everything above that element is in the larger by closure – so nothing the smaller holds escapes. This is what says a register enumerated up to a region (the address whose elements are exactly a final segment's cells) never holds a cell outside it.

theorem DescriptiveComplexity.wmSetLe_of_empty {α : Type} {Le : α → α → Prop} [Finite α] (h : IsLinOrd Le) {s : α → Prop} (hs : ∀ (x : α), ¬s x) (t : α → Prop) : WMSetLe Le s t

An address holding nothing is below every address.

theorem DescriptiveComplexity.wmSetLe_of_subset {α : Type} {Le : α → α → Prop} [Finite α] (h : IsLinOrd Le) {s t : α → Prop} (hsub : ∀ (x : α), s x → t x) : WMSetLe Le s t

A sub-address is below the address containing it. The least element where two addresses differ decides the comparison, and if one is contained in the other that element is in the larger – so a program that only ever clears cells moves its address down the tape, and one that only sets them moves it up.

theorem DescriptiveComplexity.wmSetLe_of_full {α : Type} {Le : α → α → Prop} [Finite α] (h : IsLinOrd Le) {t : α → Prop} (ht : ∀ (x : α), t x) (s : α → Prop) : WMSetLe Le s t

An address holding everything is above every address.

theorem DescriptiveComplexity.wmLt_wmSetLe_iff {α : Type} {Le : α → α → Prop} [Finite α] (h : IsLinOrd Le) (s t : α → Prop) : WMLt (WMSetLe Le) s t ↔ WMSetLt Le s t

The strict part of the address order is the strict comparison of addresses: the fold of DescriptiveComplexity.Problems.Wide.Fold writes its strict order as DescriptiveComplexity.WMLt of whatever relation it is given, and at addresses that is DescriptiveComplexity.WMSetLt.

theorem DescriptiveComplexity.eq_of_between_wmIncr {α : Type} {Le : α → α → Prop} [Finite α] (h : IsLinOrd Le) {s t r : α → Prop} (hi : WMIncr Le s t) (h1 : WMSetLe Le s r) (h2 : WMSetLe Le r t) : r = s ∨ r = t

Nothing lies strictly between an address and its increment: an address weakly between them agrees with one of the two. This is the half that makes the increment an immediate successor, and the only place the linearity of the address order is used.

theorem DescriptiveComplexity.wmSetLt_iff_of_wmIncr {α : Type} {Le : α → α → Prop} [Finite α] (h : IsLinOrd Le) {t t' : α → Prop} (hi : WMIncr Le t t') (s : α → Prop) : WMSetLt Le s t' ↔ WMSetLe Le s t

An address is below the increment of another exactly when it is at or below that other: the increment is the immediate successor, so < t' and ≤ t are the same. This is the hypothesis the fold of DescriptiveComplexity.Problems.Wide.Fold asks about the successor, discharged for addresses.

theorem DescriptiveComplexity.wmSetLe_succ_bot_of_nonempty {α : Type} {Le : α → α → Prop} [Finite α] (h : IsLinOrd Le) {s₀ s : α → Prop} (hs₀ : WMIncr Le (fun (x : α) => False) s₀) (hne : ∃ (x : α), s x) : WMSetLe Le s₀ s

The empty address's successor is at or below every nonempty address: an address strictly below it is at or below the empty one, hence empty. This is what puts a program's data – every address it marks anything at – inside a stretch that starts one step above the cell its head began on.

theorem DescriptiveComplexity.wmSetLe_of_wmIncr_of_lt {α : Type} {Le : α → α → Prop} [Finite α] (h : IsLinOrd Le) {t t' s : α → Prop} (hi : WMIncr Le t t') (hlt : WMSetLt Le t s) : WMSetLe Le t' s

An increment cannot overshoot: the successor of an address strictly below another is still at or below it. A walk that stops at the first address a marker sits on reads this at every round.

Every address is reached from the empty one by increments

The chain and its monotonicity, over an arbitrary linearly ordered index. The universe of a wide machine is one such index and so is the index of a file, which is what a program handed its file counts its rounds over.

theorem DescriptiveComplexity.exists_wmChainOf {α : Type} {Le : α → α → Prop} [Finite α] (h : IsLinOrd Le) (target : α → Prop) : ∃ (n : ℕ) (mV : Fin (n + 1) → α → Prop), (mV 0 = fun (x : α) => False) ∧ mV (Fin.last n) = target ∧ ∀ (k : Fin n), WMIncr Le (mV k.castSucc) (mV k.succ)

Every address is reached from the empty one by increments: a finite chain, each step the binary increment, ending at the target. This is DescriptiveComplexity.exists_wmChain over an arbitrary index.

theorem DescriptiveComplexity.wmChainOf_lt {α : Type} {Le : α → α → Prop} [Finite α] (h : IsLinOrd Le) {n : ℕ} {mV : Fin (n + 1) → α → Prop} (hchain : ∀ (k : Fin n), WMIncr Le (mV k.castSucc) (mV k.succ)) {a a' : Fin (n + 1)} (hlt : a < a') : WMSetLt Le (mV a) (mV a')

The chain is strictly increasing: two positions compare as their addresses do, by induction on the distance.

The three primitives, on the universe of a wide machine

theorem DescriptiveComplexity.wpPosn_iff {A : Type} (p : WPoint A) : wpPosn p ↔ ∃ (s : A → Prop), p = Sum.inl s

Only addresses are positions, so both ends of a step are addresses.

theorem DescriptiveComplexity.minPos_wpLe {A : Type} [FirstOrder.Language.wide.Structure A] [Finite A] (h : IsLinOrd WMLe) : MinPos wpLe wpPosn (Sum.inl fun (x : A) => False)

The head of a wide machine starts on the empty address.

theorem DescriptiveComplexity.maxPos_wpLe {A : Type} [FirstOrder.Language.wide.Structure A] [Finite A] (h : IsLinOrd WMLe) : MaxPos wpLe wpPosn (Sum.inl fun (x : A) => True)

The last cell of a wide machine is the full address.

theorem DescriptiveComplexity.succPos_wpLe_iff {A : Type} [FirstOrder.Language.wide.Structure A] [Finite A] (h : IsLinOrd WMLe) (s t : A → Prop) : SuccPos wpLe wpPosn (Sum.inl s) (Sum.inl t) ↔ WMIncr WMLe s t

A step of a wide machine is the binary increment of its address. The machine's own primitive is DescriptiveComplexity.SuccPos, which says only that no position lies strictly between; this identifies it with the increment, which is what a program can maintain.