The VAL loop's enumeration

The variable machinery's VAL loop starts at the empty register, increments one address at a time, and stops at the first register content its exhaustion test accepts – the Kin top, the set of the inner-block elements. The enumeration DescriptiveComplexity.Draw.Data.var_run consumes is therefore an initial segment of the binary-counter order on subsets, indexed by Fin (n + 1) – which carries the LinearOrder and Finite instances the run theorem demands, with no subtype order in sight.

This file builds it: DescriptiveComplexity.exists_wmChain – every subset is reachable from the empty one by a finite chain of increments, by strong induction on the address rank (DescriptiveComplexity.bitRank, the same measure DescriptiveComplexity.reaches_of_wideRounds walks) – DescriptiveComplexity.wmChain_lt, the chain's strict monotonicity, and DescriptiveComplexity.Draw.Data.exists_valEnum, the package in exactly the run theorem's hypothesis forms.

theorem DescriptiveComplexity.exists_wmChain {A : Type} [FirstOrder.Language.wide.Structure A] [Finite A] (h : IsLinOrd WMLe) (target : A → Prop) : ∃ (n : ℕ) (mV : Fin (n + 1) → A → Prop), (mV 0 = fun (x : A) => False) ∧ mV (Fin.last n) = target ∧ ∀ (k : Fin n), WMIncr WMLe (mV k.castSucc) (mV k.succ)

Every subset is reachable from the empty one by increments: a finite chain, each step the binary increment of the address, ending at the target. By strong induction on the address rank.

theorem DescriptiveComplexity.wmChain_lt {A : Type} [FirstOrder.Language.wide.Structure A] [Finite A] (h : IsLinOrd WMLe) {n : ℕ} {mV : Fin (n + 1) → A → Prop} (hchain : ∀ (k : Fin n), WMIncr WMLe (mV k.castSucc) (mV k.succ)) {a a' : Fin (n + 1)} (hlt : a < a') : WMSetLt WMLe (mV a) (mV a')

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

def DescriptiveComplexity.Draw.Data.kinTop {L : FirstOrder.Language} (dt : Data L) {A R P : Type} : Univ A R P dt.KIx dt.dd → Prop

The Kin top: the register content the exhaustion test accepts – the set of the inner-block elements.

Equations

• dt.kinTop u = ∃ (j : Fin dt.ki), DescriptiveComplexity.Draw.tagBlk u.1 = some (Sum.inr j)

theorem DescriptiveComplexity.Draw.Data.exists_valEnum {L : FirstOrder.Language} {dt : Data L} {A R P : Type} [LinearOrder A] [LinearOrder R] [LinearOrder P] [FirstOrder.Language.wide.Structure (Univ A R P dt.KIx dt.dd)] [Finite A] [Finite R] [Finite P] (hlin : IsLinOrd WMLe) (hord : ∀ (x y : Univ A R P dt.KIx dt.dd), WMLe x y ↔ tagTupleLe x y) : ∃ (n : ℕ) (mV : Fin (n + 1) → Univ A R P dt.KIx dt.dd → Prop), (mV 0 = fun (x : Univ A R P dt.KIx dt.dd) => False) ∧ (∀ (a a' : Fin (n + 1)), a < a' → (∀ (b : Fin (n + 1)), ¬(a < b ∧ b < a')) → WMIncr WMLe (mV a) (mV a')) ∧ (∀ (u : Univ A R P dt.KIx dt.dd), dt.InnerFull (fun (u : Univ A R P dt.KIx dt.dd) => tagBlk u.1) (mV (Fin.last n)) u) ∧ (∀ a < Fin.last n, ∃ (u : Univ A R P dt.KIx dt.dd), ¬dt.InnerFull (fun (u : Univ A R P dt.KIx dt.dd) => tagBlk u.1) (mV a) u) ∧ ∀ (a : Fin (n + 1)) (t : Tag R P dt.KIx) (w : Fin dt.dd → A), mV a (t, w) → ∃ (j : Fin dt.ki), t = argIn dt.ko j

The VAL loop's enumeration exists: an increment chain over Fin (n + 1) from the empty register to the Kin top, in exactly the forms DescriptiveComplexity.Draw.Data.var_run demands – the covers are machine increments, the top passes the exhaustion test everywhere, every earlier register fails it somewhere, and every register of the chain holds inner cells alone, the Kin blocks being a final segment of the universe (DescriptiveComplexity.Draw.kinSeg, DescriptiveComplexity.subset_of_wmSetLe). That last fact is what the semantic layer reads a register through.