One variable's machinery, instantiated: the gates' and the matrix's legs

The two abstract machineries of DescriptiveComplexity.Draw.Data.var_run – the gates' run to the verdict checkpoint and the per-round matrix pass – discharged at the program's own rules (DescriptiveComplexity.Draw.Data.varRuleF at DescriptiveComplexity.Draw.Data.varArgsOf): each is a walk-back into the sub-machinery's first checkpoint, the assembled run (DescriptiveComplexity.Draw.Data.gates_run, DescriptiveComplexity.Draw.Data.matrix_run), and the walk-back at the landing checkpoint.

theorem DescriptiveComplexity.Draw.Data.varGates_run {L : FirstOrder.Language} (dt : Data L) {A R P : Type} [Fintype dt.SlotIx] [LinearOrder A] [LinearOrder R] [LinearOrder P] [FirstOrder.Language.wide.Structure (Univ A R P dt.KIx dt.dd)] [Finite A] [Finite R] [Finite P] {PR : Prog A R P dt.CtlIx dt.SlotIx dt.KIx dt.dd} (RF : RegFile (Univ A R P dt.KIx dt.dd)) (hord : ∀ (x y : Univ A R P dt.KIx dt.dd), WMLe x y ↔ tagTupleLe x y) [Nonempty A] [L.IsRelational] [L.Structure A] (vi : dt.VarIx) (st : TapeStD dt A R P) {v : Univ A R P dt.KIx dt.dd → Prop} {emb : dt.VarPhF vi → P} {exitPh : P} {rEmb : (i : dt.VarSiteF vi) → dt.VarShF vi i → R} [Finite dt.KIx] (hrules : ∀ (i : dt.VarSiteF vi) (ρ : dt.VarShF vi i), PR.rules (rEmb i ρ) = dt.varRuleF PR.zero PR.one vi (dt.varArgsOf PR.zero PR.one vi) emb exitPh i ρ) (hR : PR.table.Reads) (hlin : IsLinOrd WMLe) {gtop gbot : Univ A R P dt.KIx dt.dd} (htop : ∀ (y : Univ A R P dt.KIx dt.dd), WMLe y gtop) (hbot : ∀ (y : Univ A R P dt.KIx dt.dd), WMLe gbot y) {v' : Univ A R P dt.KIx dt.dd → Prop} (hv : WMSetLt WMLe v (RF.cell gbot)) (hvi : WMIncr WMLe v v') (hwkSt : st.wk = fun (r : Univ A R P dt.KIx dt.dd → Prop) => r = v) (TestOf : Fin (dt.arOf vi) → Univ A R P dt.KIx dt.dd → Prop) (hcompatOf : ∀ (ℓ : Fin (dt.arOf vi)) (u : Univ A R P dt.KIx dt.dd), dt.wellShapedG PR.zero PR.one (Sum.inl (Fin.castLE ⋯ ℓ)) (PR.passTracksAt RF.cell Slot.mir (dt.back RF.cell PR.zero PR.one ⋯ st) st.mir (RF.cell u)) ↔ TestOf ℓ u) (tOf : Fin (dt.arOf vi) → dt.X.Tag) (htagOf : ∀ (ℓ : Fin (dt.arOf vi)), dt.dspTagOf PR.zero PR.one (wmBlk st.mir (Tag.arg (toLex (Sum.inl (Fin.castLE ⋯ ℓ))))) = tOf ℓ) (hTestOf : ∀ (ℓ : Fin (dt.arOf vi)) (u : Univ A R P dt.KIx dt.dd), TestOf ℓ u) (f₀ : dt.CtlIx → A) : Relation.ReflTransGen (wideData (Univ A R P dt.KIx dt.dd)).Step { state := Sum.inr (PR.stElt (emb (VarPh.gatesP (SeqPh.chk 0))) f₀), head := Sum.inl v', tape := wideTape (PR.trackTapeAt RF.cell Slot.val (dt.back RF.cell PR.zero PR.one ⋯ st) st.val) (PR.syElt PR.blank) } { state := Sum.inr (PR.stElt (emb VarPh.vchk1) (dt.gatesFs RF PR.zero PR.one vi st v (fun (ℓ : Fin (dt.arOf vi)) => Sum.inl (Fin.castLE ⋯ ℓ)) ⋯ ⋯ ⋯ tOf (dt.varArgsOf PR.zero PR.one vi).enterBlockSt f₀ (dt.arOf vi))), head := Sum.inl v, tape := wideTape (PR.trackTapeAt RF.cell Slot.val (dt.back RF.cell PR.zero PR.one ⋯ st) st.val) (PR.syElt PR.blank) }

The gates' leg of one variable's machinery: from the dispatch's landing one cell right of the marker, the walk-back, the whole gate sequence at a gated address, and the walk-back at the verdict checkpoint.

noncomputable def DescriptiveComplexity.Draw.Data.failCtl {L : FirstOrder.Language} (dt : Data L) {A R P : Type} [Fintype dt.SlotIx] [LinearOrder A] [LinearOrder R] [LinearOrder P] [FirstOrder.Language.wide.Structure (Univ A R P dt.KIx dt.dd)] [Finite A] {PR : Prog A R P dt.CtlIx dt.SlotIx dt.KIx dt.dd} (RF : RegFile (Univ A R P dt.KIx dt.dd)) [Nonempty A] [L.IsRelational] [L.Structure A] (vi : dt.VarIx) (st : TapeStD dt A R P) {v : Univ A R P dt.KIx dt.dd → Prop} (tOf : Fin (dt.arOf vi) → dt.X.Tag) (ℓ₀ : Fin (dt.arOf vi)) (f₀ : dt.CtlIx → A) : dt.CtlIx → A

The control after a failing gate sequence: the fail store at the failing block's entry, the flag clear.

Equations

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

theorem DescriptiveComplexity.Draw.Data.varGatesFail_run {L : FirstOrder.Language} (dt : Data L) {A R P : Type} [Fintype dt.SlotIx] [LinearOrder A] [LinearOrder R] [LinearOrder P] [FirstOrder.Language.wide.Structure (Univ A R P dt.KIx dt.dd)] [Finite A] [Finite R] [Finite P] {PR : Prog A R P dt.CtlIx dt.SlotIx dt.KIx dt.dd} (RF : RegFile (Univ A R P dt.KIx dt.dd)) (hord : ∀ (x y : Univ A R P dt.KIx dt.dd), WMLe x y ↔ tagTupleLe x y) [Nonempty A] [L.IsRelational] [L.Structure A] (vi : dt.VarIx) (st : TapeStD dt A R P) {v : Univ A R P dt.KIx dt.dd → Prop} {emb : dt.VarPhF vi → P} {exitPh : P} {rEmb : (i : dt.VarSiteF vi) → dt.VarShF vi i → R} [Finite dt.KIx] (hrules : ∀ (i : dt.VarSiteF vi) (ρ : dt.VarShF vi i), PR.rules (rEmb i ρ) = dt.varRuleF PR.zero PR.one vi (dt.varArgsOf PR.zero PR.one vi) emb exitPh i ρ) (hR : PR.table.Reads) (hlin : IsLinOrd WMLe) {gtop gbot : Univ A R P dt.KIx dt.dd} (htop : ∀ (y : Univ A R P dt.KIx dt.dd), WMLe y gtop) (hbot : ∀ (y : Univ A R P dt.KIx dt.dd), WMLe gbot y) {v' : Univ A R P dt.KIx dt.dd → Prop} (hv : WMSetLt WMLe v (RF.cell gbot)) (hvi : WMIncr WMLe v v') (hwkSt : st.wk = fun (r : Univ A R P dt.KIx dt.dd → Prop) => r = v) (TestOf : Fin (dt.arOf vi) → Univ A R P dt.KIx dt.dd → Prop) (hcompatOf : ∀ (ℓ : Fin (dt.arOf vi)) (u : Univ A R P dt.KIx dt.dd), dt.wellShapedG PR.zero PR.one (Sum.inl (Fin.castLE ⋯ ℓ)) (PR.passTracksAt RF.cell Slot.mir (dt.back RF.cell PR.zero PR.one ⋯ st) st.mir (RF.cell u)) ↔ TestOf ℓ u) (tOf : Fin (dt.arOf vi) → dt.X.Tag) (htagOf : ∀ (ℓ : Fin (dt.arOf vi)), dt.dspTagOf PR.zero PR.one (wmBlk st.mir (Tag.arg (toLex (Sum.inl (Fin.castLE ⋯ ℓ))))) = tOf ℓ) (ℓ₀ : Fin (dt.arOf vi)) (hTestLt : ∀ (ℓ : Fin (dt.arOf vi)), ↑ℓ < ↑ℓ₀ → ∀ (u : Univ A R P dt.KIx dt.dd), TestOf ℓ u) {u₀ : Univ A R P dt.KIx dt.dd} (hfail : ¬TestOf ℓ₀ u₀) (f₀ : dt.CtlIx → A) : Relation.ReflTransGen (wideData (Univ A R P dt.KIx dt.dd)).Step { state := Sum.inr (PR.stElt (emb (VarPh.gatesP (SeqPh.chk 0))) f₀), head := Sum.inl v', tape := wideTape (PR.trackTapeAt RF.cell Slot.val (dt.back RF.cell PR.zero PR.one ⋯ st) st.val) (PR.syElt PR.blank) } { state := Sum.inr (PR.stElt (emb VarPh.vchk1) (dt.failCtl RF vi st tOf ℓ₀ f₀)), head := Sum.inl v, tape := wideTape (PR.trackTapeAt RF.cell Slot.val (dt.back RF.cell PR.zero PR.one ⋯ st) st.val) (PR.syElt PR.blank) }

The gates' leg at a junk address: the walk-back, the passing prefix, the failing block, and the walk-back at the verdict checkpoint – the fail store applied, the flag clear.

theorem DescriptiveComplexity.Draw.Data.varBg_back {L : FirstOrder.Language} (dt : Data L) {A R P : Type} [Fintype dt.SlotIx] [LinearOrder A] [LinearOrder R] [LinearOrder P] [FirstOrder.Language.wide.Structure (Univ A R P dt.KIx dt.dd)] {PR : Prog A R P dt.CtlIx dt.SlotIx dt.KIx dt.dd} (RF : RegFile (Univ A R P dt.KIx dt.dd)) (hord : ∀ (x y : Univ A R P dt.KIx dt.dd), WMLe x y ↔ tagTupleLe x y) {v : Univ A R P dt.KIx dt.dd → Prop} (hlin : IsLinOrd WMLe) {gtop : Univ A R P dt.KIx dt.dd} (htop : ∀ (y : Univ A R P dt.KIx dt.dd), WMLe y gtop) (stV : TapeStD dt A R P) (hwkV : stV.wk = fun (r : Univ A R P dt.KIx dt.dd → Prop) => r = v) : dt.VarBg (laidFile RF hord) PR.zero PR.one v gtop (dt.back RF.cell PR.zero PR.one ⋯ stV) stV.val

The background bundle, discharged at a boundary state: the five slot equations DescriptiveComplexity.Draw.Data.var_run's kits read are definitional in DescriptiveComplexity.Draw.Data.back, given the marker and the order facts.

theorem DescriptiveComplexity.Draw.Data.varMachineFail_run {L : FirstOrder.Language} (dt : Data L) {A R P : Type} [Fintype dt.SlotIx] [LinearOrder A] [LinearOrder R] [LinearOrder P] [FirstOrder.Language.wide.Structure (Univ A R P dt.KIx dt.dd)] [Finite A] [Finite R] [Finite P] {PR : Prog A R P dt.CtlIx dt.SlotIx dt.KIx dt.dd} (RF : RegFile (Univ A R P dt.KIx dt.dd)) (hord : ∀ (x y : Univ A R P dt.KIx dt.dd), WMLe x y ↔ tagTupleLe x y) [Nonempty A] [L.IsRelational] [L.Structure A] (vi : dt.VarIx) (st : TapeStD dt A R P) {v : Univ A R P dt.KIx dt.dd → Prop} {emb : dt.VarPhF vi → P} {exitPh : P} {rEmb : (i : dt.VarSiteF vi) → dt.VarShF vi i → R} [Finite dt.KIx] (hrules : ∀ (i : dt.VarSiteF vi) (ρ : dt.VarShF vi i), PR.rules (rEmb i ρ) = dt.varRuleF PR.zero PR.one vi (dt.varArgsOf PR.zero PR.one vi) emb exitPh i ρ) (hR : PR.table.Reads) (hlin : IsLinOrd WMLe) {gtop gbot : Univ A R P dt.KIx dt.dd} (htop : ∀ (y : Univ A R P dt.KIx dt.dd), WMLe y gtop) (hbot : ∀ (y : Univ A R P dt.KIx dt.dd), WMLe gbot y) {v' : Univ A R P dt.KIx dt.dd → Prop} (hv : WMSetLt WMLe v (RF.cell gbot)) (hvi : WMIncr WMLe v v') (hwkSt : st.wk = fun (r : Univ A R P dt.KIx dt.dd → Prop) => r = v) (TestOf : Fin (dt.arOf vi) → Univ A R P dt.KIx dt.dd → Prop) (hcompatOf : ∀ (ℓ : Fin (dt.arOf vi)) (u : Univ A R P dt.KIx dt.dd), dt.wellShapedG PR.zero PR.one (Sum.inl (Fin.castLE ⋯ ℓ)) (PR.passTracksAt RF.cell Slot.mir (dt.back RF.cell PR.zero PR.one ⋯ st) st.mir (RF.cell u)) ↔ TestOf ℓ u) (tOf : Fin (dt.arOf vi) → dt.X.Tag) (htagOf : ∀ (ℓ : Fin (dt.arOf vi)), dt.dspTagOf PR.zero PR.one (wmBlk st.mir (Tag.arg (toLex (Sum.inl (Fin.castLE ⋯ ℓ))))) = tOf ℓ) (ℓ₀ : Fin (dt.arOf vi)) (hTestLt : ∀ (ℓ : Fin (dt.arOf vi)), ↑ℓ < ↑ℓ₀ → ∀ (u : Univ A R P dt.KIx dt.dd), TestOf ℓ u) {u₀ : Univ A R P dt.KIx dt.dd} (hfail : ¬TestOf ℓ₀ u₀) (f₀ : dt.CtlIx → A) {rest' : (Univ A R P dt.KIx dt.dd → Prop) → dt.SlotIx → A} (hoff : ∀ (r : Univ A R P dt.KIx dt.dd → Prop), r ≠ v → rest' r = dt.back RF.cell PR.zero PR.one ⋯ st r) (hupd : rest' v = Function.update (dt.back RF.cell PR.zero PR.one ⋯ st v) (dt.varArgsOf PR.zero PR.one vi).newSlot PR.zero) : Relation.ReflTransGen (wideData (Univ A R P dt.KIx dt.dd)).Step { state := Sum.inr (PR.stElt (emb VarPh.vchk0) f₀), head := Sum.inl v, tape := wideTape (PR.trackTapeAt RF.cell Slot.val (dt.back RF.cell PR.zero PR.one ⋯ st) st.val) (PR.syElt PR.blank) } { state := Sum.inr (PR.stElt exitPh (dt.failCtl RF vi st tOf ℓ₀ ((dt.varArgsOf PR.zero PR.one vi).enterSt f₀ (dt.back RF.cell PR.zero PR.one ⋯ st v)))), head := Sum.inl v', tape := wideTape (PR.trackTapeAt RF.cell Slot.val rest' st.val) (PR.syElt PR.blank) }

The whole machinery at a junk address: entry, the failing gates, and the verdict checkpoint's clear flag routing straight to the exit with the stage slot erased – the VAL loop never entered.

noncomputable def DescriptiveComplexity.Draw.Data.ungatedCtl {L : FirstOrder.Language} (dt : Data L) {A R P : Type} [Fintype dt.SlotIx] [LinearOrder A] [LinearOrder R] [LinearOrder P] [FirstOrder.Language.wide.Structure (Univ A R P dt.KIx dt.dd)] [Finite A] {PR : Prog A R P dt.CtlIx dt.SlotIx dt.KIx dt.dd} (RF : RegFile (Univ A R P dt.KIx dt.dd)) [Nonempty A] [L.IsRelational] [L.Structure A] (vi : dt.VarIx) (st : TapeStD dt A R P) {v : Univ A R P dt.KIx dt.dd → Prop} (tOf : Fin (dt.arOf vi) → dt.X.Tag) (f₀ : dt.CtlIx → A) : dt.CtlIx → A

The control after a completed but failing gate sequence: the whole gates' thread – every block's file test passed and every block's machinery ran – with the flag clear because some block encoded no point.

Equations

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

theorem DescriptiveComplexity.Draw.Data.varMachineUngated_run {L : FirstOrder.Language} (dt : Data L) {A R P : Type} [Fintype dt.SlotIx] [LinearOrder A] [LinearOrder R] [LinearOrder P] [FirstOrder.Language.wide.Structure (Univ A R P dt.KIx dt.dd)] [Finite A] [Finite R] [Finite P] {PR : Prog A R P dt.CtlIx dt.SlotIx dt.KIx dt.dd} (RF : RegFile (Univ A R P dt.KIx dt.dd)) (hord : ∀ (x y : Univ A R P dt.KIx dt.dd), WMLe x y ↔ tagTupleLe x y) [Nonempty A] [L.IsRelational] [L.Structure A] (vi : dt.VarIx) (st : TapeStD dt A R P) {v : Univ A R P dt.KIx dt.dd → Prop} {emb : dt.VarPhF vi → P} {exitPh : P} {rEmb : (i : dt.VarSiteF vi) → dt.VarShF vi i → R} [Finite dt.KIx] (hrules : ∀ (i : dt.VarSiteF vi) (ρ : dt.VarShF vi i), PR.rules (rEmb i ρ) = dt.varRuleF PR.zero PR.one vi (dt.varArgsOf PR.zero PR.one vi) emb exitPh i ρ) (hR : PR.table.Reads) (hlin : IsLinOrd WMLe) {gtop gbot : Univ A R P dt.KIx dt.dd} (htop : ∀ (y : Univ A R P dt.KIx dt.dd), WMLe y gtop) (hbot : ∀ (y : Univ A R P dt.KIx dt.dd), WMLe gbot y) {v' : Univ A R P dt.KIx dt.dd → Prop} (hv : WMSetLt WMLe v (RF.cell gbot)) (hvi : WMIncr WMLe v v') (hwkSt : st.wk = fun (r : Univ A R P dt.KIx dt.dd → Prop) => r = v) (TestOf : Fin (dt.arOf vi) → Univ A R P dt.KIx dt.dd → Prop) (hcompatOf : ∀ (ℓ : Fin (dt.arOf vi)) (u : Univ A R P dt.KIx dt.dd), dt.wellShapedG PR.zero PR.one (Sum.inl (Fin.castLE ⋯ ℓ)) (PR.passTracksAt RF.cell Slot.mir (dt.back RF.cell PR.zero PR.one ⋯ st) st.mir (RF.cell u)) ↔ TestOf ℓ u) (tOf : Fin (dt.arOf vi) → dt.X.Tag) (htagOf : ∀ (ℓ : Fin (dt.arOf vi)), dt.dspTagOf PR.zero PR.one (wmBlk st.mir (Tag.arg (toLex (Sum.inl (Fin.castLE ⋯ ℓ))))) = tOf ℓ) (hTestOf : ∀ (ℓ : Fin (dt.arOf vi)) (u : Univ A R P dt.KIx dt.dd), TestOf ℓ u) (ℓ₀ : Fin (dt.arOf vi)) (hbad : ¬((∀ (t' : dt.X.Tag), wmBlk st.mir (Tag.arg (toLex (Sum.inl (Fin.castLE ⋯ ℓ₀)))) (encTagTup dt.ly PR.zero PR.one t') ↔ t' = tOf ℓ₀) ∧ ExpExpansion.DomHolds (tOf ℓ₀, decRho dt.ly PR.zero PR.one (wmBlk st.mir (Tag.arg (toLex (Sum.inl (Fin.castLE ⋯ ℓ₀)))))))) (f₀ : dt.CtlIx → A) {rest' : (Univ A R P dt.KIx dt.dd → Prop) → dt.SlotIx → A} (hoff : ∀ (r : Univ A R P dt.KIx dt.dd → Prop), r ≠ v → rest' r = dt.back RF.cell PR.zero PR.one ⋯ st r) (hupd : rest' v = Function.update (dt.back RF.cell PR.zero PR.one ⋯ st v) (dt.varArgsOf PR.zero PR.one vi).newSlot PR.zero) : Relation.ReflTransGen (wideData (Univ A R P dt.KIx dt.dd)).Step { state := Sum.inr (PR.stElt (emb VarPh.vchk0) f₀), head := Sum.inl v, tape := wideTape (PR.trackTapeAt RF.cell Slot.val (dt.back RF.cell PR.zero PR.one ⋯ st) st.val) (PR.syElt PR.blank) } { state := Sum.inr (PR.stElt exitPh (dt.ungatedCtl RF vi st tOf ((dt.varArgsOf PR.zero PR.one vi).enterSt f₀ (dt.back RF.cell PR.zero PR.one ⋯ st v)))), head := Sum.inl v', tape := wideTape (PR.trackTapeAt RF.cell Slot.val rest' st.val) (PR.syElt PR.blank) }

The whole machinery at a shaped but ungated address: every block passes its file test – the total dispatch carries each block's machinery through – but some block encodes no point, its witness not one-hot at the dispatched tag or its domain sentence failing. The gates complete with the flag clear, and the verdict checkpoint routes straight to the exit with the stage slot erased – the VAL loop never entered. The third landing an arbitrary address makes, beside the gated and the shape-failing ones.

The whole variable machinery, run

noncomputable def DescriptiveComplexity.Draw.Data.roundSt {L : FirstOrder.Language} (dt : Data L) {A R P : Type} (st : TapeStD dt A R P) (m : Univ A R P dt.KIx dt.dd → Prop) : TapeStD dt A R P

The state of one VAL-loop round: the entry state with the round's VAL content.

Equations

• dt.roundSt st m = { mir := st.mir, tgt := st.tgt, sav := st.sav, val := m, old := st.old, new := st.new, wk := st.wk, bot := st.bot, ltp := st.ltp }

theorem DescriptiveComplexity.Draw.Data.igPassP_roundSt {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] (RF : RegFile (Univ A R P dt.KIx dt.dd)) [Nonempty A] [L.Structure A] (zero one : A) (vi : dt.VarIx) (st st' : TapeStD dt A R P) (m : Univ A R P dt.KIx dt.dd → Prop) (ℓ : Fin (dt.nIn vi)) : dt.igPassP RF zero one vi (dt.roundSt st m) ℓ ↔ dt.igPassP RF zero one vi (dt.roundSt st' m) ℓ

Two round states at the same register ask the same pass.

theorem DescriptiveComplexity.Draw.Data.roundSt_val {L : FirstOrder.Language} {dt : Data L} {A R P : Type} (stV : TapeStD dt A R P) : dt.roundSt stV stV.val = stV

A state written with the register it already holds is itself.

theorem DescriptiveComplexity.Draw.Data.back_roundSt_off {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)] (RF : RegFile (Univ A R P dt.KIx dt.dd)) (st : TapeStD dt A R P) {zero one : A} (m₁ m₂ r : Univ A R P dt.KIx dt.dd → Prop) (s : dt.SlotIx) (hs : s ≠ Slot.val) : dt.back RF.cell zero one ⋯ (dt.roundSt st m₁) r s = dt.back RF.cell zero one ⋯ (dt.roundSt st m₂) r s

Two round states' backgrounds agree off the VAL slot.

noncomputable def DescriptiveComplexity.Draw.Data.valCarry {L : FirstOrder.Language} (dt : Data L) {A R P : Type} [FirstOrder.Language.wide.Structure (Univ A R P dt.KIx dt.dd)] [Nonempty A] (s : Univ A R P dt.KIx dt.dd → Prop) : Univ A R P dt.KIx dt.dd

The carry of a VAL round: the greatest element the register is clear at, everything above it set – what the increment's landing phase names.

Equations

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

theorem DescriptiveComplexity.Draw.Data.valCarry_eq {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)] [Nonempty A] (hlin : IsLinOrd WMLe) {s : Univ A R P dt.KIx dt.dd → Prop} {u₀ : Univ A R P dt.KIx dt.dd} (h1 : ¬s u₀) (h2 : ∀ (w : Univ A R P dt.KIx dt.dd), WMLt WMLe u₀ w → s w) : dt.valCarry s = u₀

The carry is unique, so the chosen one is the hypothesis's.

noncomputable def DescriptiveComplexity.Draw.Data.roundFX {L : FirstOrder.Language} {dt : Data L} {A R P : Type} [Fintype dt.SlotIx] [LinearOrder A] [LinearOrder R] [LinearOrder P] [FirstOrder.Language.wide.Structure (Univ A R P dt.KIx dt.dd)] [Finite A] {PR : Prog A R P dt.CtlIx dt.SlotIx dt.KIx dt.dd} (RF : RegFile (Univ A R P dt.KIx dt.dd)) (hord : ∀ (x y : Univ A R P dt.KIx dt.dd), WMLe x y ↔ tagTupleLe x y) [Nonempty A] [L.IsRelational] [L.Structure A] (vi : dt.VarIx) (st : TapeStD dt A R P) (v : Univ A R P dt.KIx dt.dd → Prop) {ιV : Type} (mV : ιV → Univ A R P dt.KIx dt.dd → Prop) (semOf : (a : ιV) → (∀ (ℓ : Fin (dt.nIn vi)), dt.igPassP RF PR.zero PR.one vi (dt.roundSt st (mV a)) ℓ) → (b : Fin (dt.natOf vi)) → dt.KindSem PR.zero PR.one vi (dt.roundSt st (mV a)) (dt.kindOf vi b)) (q : dt.CtlIx → A) (a : ιV) : dt.CtlIx → A

The exit control of one VAL round, at an entry control: the inner gates' thread over the round's register, then – at a passing round only, both flags set – the matrix thread on its output.

Equations

• DescriptiveComplexity.Draw.Data.roundFX RF hord vi st v mV semOf q a = dt.roundCtl RF hord ⋯ vi (dt.roundSt st (mV a)) v (semOf a) q

noncomputable def DescriptiveComplexity.Draw.Data.varFM {L : FirstOrder.Language} {dt : Data L} {A R P : Type} [Fintype dt.SlotIx] [LinearOrder A] [LinearOrder R] [LinearOrder P] [FirstOrder.Language.wide.Structure (Univ A R P dt.KIx dt.dd)] [Finite A] {PR : Prog A R P dt.CtlIx dt.SlotIx dt.KIx dt.dd} (RF : RegFile (Univ A R P dt.KIx dt.dd)) (hord : ∀ (x y : Univ A R P dt.KIx dt.dd), WMLe x y ↔ tagTupleLe x y) [Nonempty A] [L.IsRelational] [L.Structure A] (vi : dt.VarIx) (st : TapeStD dt A R P) (v : Univ A R P dt.KIx dt.dd → Prop) {ιV : Type} [LinearOrder ιV] (mV : ιV → Univ A R P dt.KIx dt.dd → Prop) (semOf : (a : ιV) → (∀ (ℓ : Fin (dt.nIn vi)), dt.igPassP RF PR.zero PR.one vi (dt.roundSt st (mV a)) ℓ) → (b : Fin (dt.natOf vi)) → dt.KindSem PR.zero PR.one vi (dt.roundSt st (mV a)) (dt.kindOf vi b)) (fG : dt.CtlIx → A) : ιV → dt.CtlIx → A

The VAL loop's entry-control thread: the fold's start at the cleared register, each round the matrix pass folded and stored at the carry's block.

Equations

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

noncomputable def DescriptiveComplexity.Draw.Data.roundLeaf {L : FirstOrder.Language} {dt : Data L} {A R P : Type} [Fintype dt.SlotIx] {PR : Prog A R P dt.CtlIx dt.SlotIx dt.KIx dt.dd} (vi : dt.VarIx) (q : dt.CtlIx → A) : Prop

The leaf a round stores: the two gate flags' combination – False if an ∃-level's block is not an encoding, the matrix's value only if every ∀-level's is.

Equations

• DescriptiveComplexity.Draw.Data.roundLeaf vi q = (dt.ctlBit PR.one q dt.existGateC ∧ (dt.ctlBit PR.one q dt.allGateC → dt.postLeaf PR.one vi q))

The fold invariant of the VAL loop

theorem DescriptiveComplexity.Draw.Data.readAcc_varFM {L : FirstOrder.Language} {dt : Data L} {A R P : Type} [Fintype dt.SlotIx] [LinearOrder A] [LinearOrder R] [LinearOrder P] [FirstOrder.Language.wide.Structure (Univ A R P dt.KIx dt.dd)] [Finite A] {PR : Prog A R P dt.CtlIx dt.SlotIx dt.KIx dt.dd} (RF : RegFile (Univ A R P dt.KIx dt.dd)) (hord : ∀ (x y : Univ A R P dt.KIx dt.dd), WMLe x y ↔ tagTupleLe x y) [Nonempty A] [L.IsRelational] [L.Structure A] (vi : dt.VarIx) (st : TapeStD dt A R P) {v : Univ A R P dt.KIx dt.dd → Prop} (hlin : IsLinOrd WMLe) {ιV : Type} [LinearOrder ιV] [Finite ιV] (mV : ιV → Univ A R P dt.KIx dt.dd → Prop) (semOf : (a : ιV) → (∀ (ℓ : Fin (dt.nIn vi)), dt.igPassP RF PR.zero PR.one vi (dt.roundSt st (mV a)) ℓ) → (b : Fin (dt.natOf vi)) → dt.KindSem PR.zero PR.one vi (dt.roundSt st (mV a)) (dt.kindOf vi b)) {a₀ : ιV} (hbotV : ∀ (a : ιV), a₀ ≤ a) (hmV0 : mV a₀ = fun (x : Univ A R P dt.KIx dt.dd) => False) (hIncr : ∀ (a a' : ιV), a < a' → (∀ (b : ιV), ¬(a < b ∧ b < a')) → WMIncr WMLe (mV a) (mV a')) (hKin : ∀ (a : ιV) (t : Tag R P dt.KIx) (w : Fin dt.dd → A), mV a (t, w) → ∃ (j : Fin dt.ki), t = argIn dt.ko j) (fG : dt.CtlIx → A) {Ps : (Fin dt.ki → (Fin dt.dd → A) → Prop) → Prop} (hleaf : ∀ (a : ιV), roundLeaf vi (roundFX RF hord vi st v mV semOf (varFM RF hord vi st v mV semOf fG a) a) ↔ Ps (ixBlk (argIn dt.ko) (mV a))) (a : ιV) (j : ℕ) (hj : j < dt.ki) : dt.readAcc PR.one (varFM RF hord vi st v mV semOf fG a) j ↔ accCVal (dt.polOf vi) Ps (WMSetLe tupLeLex) j (ixBlk (argIn dt.ko) (mV a))

The VAL loop maintains the fold's contributions: at every round of the enumeration, the accumulator vector of the control thread reads the accCVal contributions of the inner quantifier prefix at the register's inner blocks – the invariant that turns the machinery's exit verdict into the prefix's value.

theorem DescriptiveComplexity.Draw.Data.accVerdict_varFM {L : FirstOrder.Language} {dt : Data L} {A R P : Type} [Fintype dt.SlotIx] [LinearOrder A] [LinearOrder R] [LinearOrder P] [FirstOrder.Language.wide.Structure (Univ A R P dt.KIx dt.dd)] [Finite A] {PR : Prog A R P dt.CtlIx dt.SlotIx dt.KIx dt.dd} (RF : RegFile (Univ A R P dt.KIx dt.dd)) (hord : ∀ (x y : Univ A R P dt.KIx dt.dd), WMLe x y ↔ tagTupleLe x y) [Nonempty A] [L.IsRelational] [L.Structure A] (vi : dt.VarIx) (st : TapeStD dt A R P) {v : Univ A R P dt.KIx dt.dd → Prop} (hlin : IsLinOrd WMLe) {ιV : Type} [LinearOrder ιV] [Finite ιV] (mV : ιV → Univ A R P dt.KIx dt.dd → Prop) (semOf : (a : ιV) → (∀ (ℓ : Fin (dt.nIn vi)), dt.igPassP RF PR.zero PR.one vi (dt.roundSt st (mV a)) ℓ) → (b : Fin (dt.natOf vi)) → dt.KindSem PR.zero PR.one vi (dt.roundSt st (mV a)) (dt.kindOf vi b)) {a₀ aT : ιV} (hbotV : ∀ (a : ιV), a₀ ≤ a) (hmV0 : mV a₀ = fun (x : Univ A R P dt.KIx dt.dd) => False) (hIncr : ∀ (a a' : ιV), a < a' → (∀ (b : ιV), ¬(a < b ∧ b < a')) → WMIncr WMLe (mV a) (mV a')) (hKin : ∀ (a : ιV) (t : Tag R P dt.KIx) (w : Fin dt.dd → A), mV a (t, w) → ∃ (j : Fin dt.ki), t = argIn dt.ko j) (hTop : ∀ (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 aT) u) (fG : dt.CtlIx → A) {Ps : (Fin dt.ki → (Fin dt.dd → A) → Prop) → Prop} (hleaf : ∀ (a : ιV), roundLeaf vi (roundFX RF hord vi st v mV semOf (varFM RF hord vi st v mV semOf fG a) a) ↔ Ps (ixBlk (argIn dt.ko) (mV a))) : dt.accVerdict PR.one (dt.polOf vi) ((dt.varArgsOf PR.zero PR.one vi).postFold (roundFX RF hord vi st v mV semOf (varFM RF hord vi st v mV semOf fG aT) aT) (dt.back RF.cell PR.zero PR.one ⋯ (dt.roundSt st (mV aT)) v)) ↔ altQuantFrom (dt.polOf vi) Ps 0 (ixBlk (argIn dt.ko) (mV aT))

The machinery's verdict is the inner prefix's value: at the exhausted register – every inner block full – the exit fold's bit is the alternating quantifier prefix over the inner blocks, applied to the matrix's value.

The leaf, discharged

theorem DescriptiveComplexity.Draw.Data.postLeaf_roundFX {L : FirstOrder.Language} {dt : Data L} {A R P : Type} [Fintype dt.SlotIx] [LinearOrder A] [LinearOrder R] [LinearOrder P] [FirstOrder.Language.wide.Structure (Univ A R P dt.KIx dt.dd)] [Finite A] [Finite R] [Finite P] {PR : Prog A R P dt.CtlIx dt.SlotIx dt.KIx dt.dd} (RF : RegFile (Univ A R P dt.KIx dt.dd)) (hord : ∀ (x y : Univ A R P dt.KIx dt.dd), WMLe x y ↔ tagTupleLe x y) [Nonempty A] [L.IsRelational] [L.Structure A] (vi : dt.VarIx) (st : TapeStD dt A R P) {v : Univ A R P dt.KIx dt.dd → Prop} (hlin : IsLinOrd WMLe) {ιV : Type} (mV : ιV → Univ A R P dt.KIx dt.dd → Prop) [LinearOrder (dt.X.Map A)] (σ : dt.d.B.Assignment (dt.X.Map A)) (a : ιV) (wa : Fin (dt.nOf vi) → dt.X.Map A) (hENCa : ∀ (j : Fin (dt.nOf vi)), wmBlk (dt.lvSet (dt.roundSt st (mV a)) vi j) (Tag.arg (toLex (dt.lvBlk vi j))) = encMap dt.ly PR.zero PR.one (wa j)) (hOlda : ∀ (i : dt.d.B.ι) (ts : Fin (dt.d.B.arity i) → Fin (dt.nOf vi)), (dt.roundSt st (mV a)).old i (dt.stageTgtD PR.zero vi i ts (dt.roundSt st (mV a)) v (dt.d.B.arity i)) ↔ σ i fun (k : Fin (dt.d.B.arity i)) => wa (ts k)) (hordP : ∀ (p q : dt.X.Map A), p ≤ q ↔ p ≤ q) (q : dt.CtlIx → A) : dt.postLeaf PR.one vi (dt.matFs RF hord PR.zero PR.one vi (dt.roundSt st (mV a)) v (dt.varArgsOf PR.zero PR.one vi).enterAtomSt (fun (b : Fin (dt.natOf vi)) => dt.mkKindSem PR.zero PR.one vi (dt.roundSt st (mV a)) wa hENCa (dt.kindOf vi b)) q (dt.natOf vi)) ↔ qfValue (dt.matOf vi) fun (atm : ((dt.X.E.sum FirstOrder.Language.order).sum dt.d.B.lang).BoundedFormula Empty (dt.nOf vi)) => (matAtom? atm).elim False (MatAtom.holds σ wa)

A round's leaf is the matrix's realization: with the round's semantic pack built by mkKindSem from the encoded valuation, the fold's leaf after the matrix pass is the quantifier-free matrix's value at that valuation – the concrete form of the invariant's hleaf hypothesis.

theorem DescriptiveComplexity.Draw.Data.accVerdict_varFM_qfValue {L : FirstOrder.Language} {dt : Data L} {A R P : Type} [Fintype dt.SlotIx] [LinearOrder A] [LinearOrder R] [LinearOrder P] [FirstOrder.Language.wide.Structure (Univ A R P dt.KIx dt.dd)] [Finite A] [Finite R] [Finite P] {PR : Prog A R P dt.CtlIx dt.SlotIx dt.KIx dt.dd} (RF : RegFile (Univ A R P dt.KIx dt.dd)) (hord : ∀ (x y : Univ A R P dt.KIx dt.dd), WMLe x y ↔ tagTupleLe x y) [Nonempty A] [L.IsRelational] [L.Structure A] (vi : dt.VarIx) (st : TapeStD dt A R P) {v : Univ A R P dt.KIx dt.dd → Prop} (hlin : IsLinOrd WMLe) {ιV : Type} [LinearOrder ιV] [Finite ιV] (mV : ιV → Univ A R P dt.KIx dt.dd → Prop) (semOf : (a : ιV) → (∀ (ℓ : Fin (dt.nIn vi)), dt.igPassP RF PR.zero PR.one vi (dt.roundSt st (mV a)) ℓ) → (b : Fin (dt.natOf vi)) → dt.KindSem PR.zero PR.one vi (dt.roundSt st (mV a)) (dt.kindOf vi b)) [LinearOrder (dt.X.Map A)] {a₀ aT : ιV} (hbotV : ∀ (a : ιV), a₀ ≤ a) (hmV0 : mV a₀ = fun (x : Univ A R P dt.KIx dt.dd) => False) (hIncr : ∀ (a a' : ιV), a < a' → (∀ (b : ιV), ¬(a < b ∧ b < a')) → WMIncr WMLe (mV a) (mV a')) (hKin : ∀ (a : ιV) (t : Tag R P dt.KIx) (w : Fin dt.dd → A), mV a (t, w) → ∃ (j : Fin dt.ki), t = argIn dt.ko j) (hTop : ∀ (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 aT) u) (σ : dt.d.B.Assignment (dt.X.Map A)) (wOf : (a : ιV) → (∀ (ℓ : Fin (dt.nIn vi)), dt.igPassP RF PR.zero PR.one vi (dt.roundSt st (mV a)) ℓ) → Fin (dt.nOf vi) → dt.X.Map A) (hENC : ∀ (a : ιV) (hp : ∀ (ℓ : Fin (dt.nIn vi)), dt.igPassP RF PR.zero PR.one vi (dt.roundSt st (mV a)) ℓ) (j : Fin (dt.nOf vi)), wmBlk (dt.lvSet (dt.roundSt st (mV a)) vi j) (Tag.arg (toLex (dt.lvBlk vi j))) = encMap dt.ly PR.zero PR.one (wOf a hp j)) (hOld : ∀ (a : ιV) (hp : ∀ (ℓ : Fin (dt.nIn vi)), dt.igPassP RF PR.zero PR.one vi (dt.roundSt st (mV a)) ℓ) (i : dt.d.B.ι) (ts : Fin (dt.d.B.arity i) → Fin (dt.nOf vi)), (dt.roundSt st (mV a)).old i (dt.stageTgtD PR.zero vi i ts (dt.roundSt st (mV a)) v (dt.d.B.arity i)) ↔ σ i fun (k : Fin (dt.d.B.arity i)) => wOf a hp (ts k)) (hordP : ∀ (p q : dt.X.Map A), p ≤ q ↔ p ≤ q) {Ps : (Fin dt.ki → (Fin dt.dd → A) → Prop) → Prop} (hsem : ∀ (a : ιV) (hp : ∀ (ℓ : Fin (dt.nIn vi)), dt.igPassP RF PR.zero PR.one vi (dt.roundSt st (mV a)) ℓ) (b : Fin (dt.natOf vi)), semOf a hp b = dt.mkKindSem PR.zero PR.one vi (dt.roundSt st (mV a)) (wOf a hp) ⋯ (dt.kindOf vi b)) (fG : dt.CtlIx → A) {Ex Al : ιV → Prop} (hEx : ∀ (a : ιV), dt.ctlBit PR.one (roundFX RF hord vi st v mV semOf (varFM RF hord vi st v mV semOf fG a) a) dt.existGateC ↔ Ex a) (hAll : ∀ (a : ιV), dt.ctlBit PR.one (roundFX RF hord vi st v mV semOf (varFM RF hord vi st v mV semOf fG a) a) dt.allGateC ↔ Al a) (hPass : ∀ (a : ιV), Ex a → Al a → ∀ (ℓ : Fin (dt.nIn vi)), dt.igPassP RF PR.zero PR.one vi (dt.roundSt st (mV a)) ℓ) (hPsPass : ∀ (a : ιV) (hp : ∀ (ℓ : Fin (dt.nIn vi)), dt.igPassP RF PR.zero PR.one vi (dt.roundSt st (mV a)) ℓ), Ex a ∧ (Al a → qfValue (dt.matOf vi) fun (atm : ((dt.X.E.sum FirstOrder.Language.order).sum dt.d.B.lang).BoundedFormula Empty (dt.nOf vi)) => (matAtom? atm).elim False (MatAtom.holds σ (wOf a hp))) ↔ Ps (ixBlk (argIn dt.ko) (mV a))) (hPsFail : ∀ (a : ιV), ¬(Ex a ∧ Al a) → (Ex a ↔ Ps (ixBlk (argIn dt.ko) (mV a)))) : dt.accVerdict PR.one (dt.polOf vi) ((dt.varArgsOf PR.zero PR.one vi).postFold (roundFX RF hord vi st v mV semOf (varFM RF hord vi st v mV semOf fG aT) aT) (dt.back RF.cell PR.zero PR.one ⋯ (dt.roundSt st (mV aT)) v)) ↔ altQuantFrom (dt.polOf vi) Ps 0 (ixBlk (argIn dt.ko) (mV aT))

One variable's verdict, semantically: with each round's pack built by mkKindSem from an encoded valuation, the machinery's exit bit at the exhausted register is the alternating quantifier prefix over the inner blocks, applied to the quantifier-free matrix's realization. The remaining interface (hPs) is the well-definedness of the matrix's value as a function of the blocks alone – the encoding layer's obligation.

The threaded twins of the VAL loop's two threads

A round's exit state is its entry state unless the round's matrix ran a stage atom, which normalizes SAV and TARGET (DescriptiveComplexity.Draw.Data.roundEndSt). Whether it ran at all is the gates' verdict, read off the control entering the round – so the two have to be iterated together, one pair per round, exactly as the spine's nodes are one scale up.

What is threaded is not the state but the two scratch registers (DescriptiveComplexity.Draw.Data.roundEndSt_eq): every other register is the machinery's entry state's, definitionally. That is what keeps the semantic packs available – a pack reads the tape state through the levels' register sets, i.e., through the mirror and VAL alone, so one family indexed by the two registers serves every round, and it can actually be built, which a family over arbitrary states could not be.

@[reducible, inline]

abbrev DescriptiveComplexity.Draw.Data.Scratch {L : FirstOrder.Language} (dt : Data L) (A R P : Type) : Type

The two registers one round of the VAL loop can change.

Equations

• dt.Scratch A R P = ((DescriptiveComplexity.Draw.Univ A R P dt.KIx dt.dd → Prop) × (DescriptiveComplexity.Draw.Univ A R P dt.KIx dt.dd → Prop))

noncomputable def DescriptiveComplexity.Draw.Data.varRdSt {L : FirstOrder.Language} {dt : Data L} {A R P : Type} (st : TapeStD dt A R P) (p : dt.Scratch A R P) (m : Univ A R P dt.KIx dt.dd → Prop) : TapeStD dt A R P

The state a round is entered in: the machinery's entry state with the round's two scratch registers and the register it enumerates.

Equations

• DescriptiveComplexity.Draw.Data.varRdSt st p m = { mir := st.mir, tgt := p.2, sav := p.1, val := m, old := st.old, new := st.new, wk := st.wk, bot := st.bot, ltp := st.ltp }

noncomputable def DescriptiveComplexity.Draw.Data.varPairT {L : FirstOrder.Language} {dt : Data L} {A R P : Type} [Fintype dt.SlotIx] [LinearOrder A] [LinearOrder R] [LinearOrder P] [FirstOrder.Language.wide.Structure (Univ A R P dt.KIx dt.dd)] [Finite A] {PR : Prog A R P dt.CtlIx dt.SlotIx dt.KIx dt.dd} (RF : RegFile (Univ A R P dt.KIx dt.dd)) (hord : ∀ (x y : Univ A R P dt.KIx dt.dd), WMLe x y ↔ tagTupleLe x y) [Nonempty A] [L.IsRelational] [L.Structure A] (vi : dt.VarIx) (st : TapeStD dt A R P) (v : Univ A R P dt.KIx dt.dd → Prop) {ιV : Type} [LinearOrder ιV] (mV : ιV → Univ A R P dt.KIx dt.dd → Prop) (semT : (p : dt.Scratch A R P) → (a : ιV) → (∀ (ℓ : Fin (dt.nIn vi)), dt.igPassP RF PR.zero PR.one vi (varRdSt st p (mV a)) ℓ) → (b : Fin (dt.natOf vi)) → dt.KindSem PR.zero PR.one vi (dt.matSt vi (varRdSt st p (mV a)) v ↑b) (dt.kindOf vi b)) (fG : dt.CtlIx → A) : ιV → dt.Scratch A R P × (dt.CtlIx → A)

The VAL loop's thread: the two scratch registers beside the control, the fold's start at the cleared register, and at each cover the round's exit – the store taken against the background the round ends in.

Equations

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

noncomputable def DescriptiveComplexity.Draw.Data.varSTT {L : FirstOrder.Language} {dt : Data L} {A R P : Type} [Fintype dt.SlotIx] [LinearOrder A] [LinearOrder R] [LinearOrder P] [FirstOrder.Language.wide.Structure (Univ A R P dt.KIx dt.dd)] [Finite A] {PR : Prog A R P dt.CtlIx dt.SlotIx dt.KIx dt.dd} (RF : RegFile (Univ A R P dt.KIx dt.dd)) (hord : ∀ (x y : Univ A R P dt.KIx dt.dd), WMLe x y ↔ tagTupleLe x y) [Nonempty A] [L.IsRelational] [L.Structure A] (vi : dt.VarIx) (st : TapeStD dt A R P) (v : Univ A R P dt.KIx dt.dd → Prop) {ιV : Type} [LinearOrder ιV] (mV : ιV → Univ A R P dt.KIx dt.dd → Prop) (semT : (p : dt.Scratch A R P) → (a : ιV) → (∀ (ℓ : Fin (dt.nIn vi)), dt.igPassP RF PR.zero PR.one vi (varRdSt st p (mV a)) ℓ) → (b : Fin (dt.natOf vi)) → dt.KindSem PR.zero PR.one vi (dt.matSt vi (varRdSt st p (mV a)) v ↑b) (dt.kindOf vi b)) (fG : dt.CtlIx → A) (a : ιV) : dt.Scratch A R P

The scratch family of the VAL loop.

Equations

• DescriptiveComplexity.Draw.Data.varSTT RF hord vi st v mV semT fG a = (DescriptiveComplexity.Draw.Data.varPairT RF hord vi st v mV semT fG a).1

noncomputable def DescriptiveComplexity.Draw.Data.varStT {L : FirstOrder.Language} {dt : Data L} {A R P : Type} [Fintype dt.SlotIx] [LinearOrder A] [LinearOrder R] [LinearOrder P] [FirstOrder.Language.wide.Structure (Univ A R P dt.KIx dt.dd)] [Finite A] {PR : Prog A R P dt.CtlIx dt.SlotIx dt.KIx dt.dd} (RF : RegFile (Univ A R P dt.KIx dt.dd)) (hord : ∀ (x y : Univ A R P dt.KIx dt.dd), WMLe x y ↔ tagTupleLe x y) [Nonempty A] [L.IsRelational] [L.Structure A] (vi : dt.VarIx) (st : TapeStD dt A R P) (v : Univ A R P dt.KIx dt.dd → Prop) {ιV : Type} [LinearOrder ιV] (mV : ιV → Univ A R P dt.KIx dt.dd → Prop) (semT : (p : dt.Scratch A R P) → (a : ιV) → (∀ (ℓ : Fin (dt.nIn vi)), dt.igPassP RF PR.zero PR.one vi (varRdSt st p (mV a)) ℓ) → (b : Fin (dt.natOf vi)) → dt.KindSem PR.zero PR.one vi (dt.matSt vi (varRdSt st p (mV a)) v ↑b) (dt.kindOf vi b)) (fG : dt.CtlIx → A) (a : ιV) : TapeStD dt A R P

The tape family of the VAL loop – the state each round is entered in.

Equations

• DescriptiveComplexity.Draw.Data.varStT RF hord vi st v mV semT fG a = DescriptiveComplexity.Draw.Data.varRdSt st (DescriptiveComplexity.Draw.Data.varSTT RF hord vi st v mV semT fG a) (mV a)

noncomputable def DescriptiveComplexity.Draw.Data.varFMT {L : FirstOrder.Language} {dt : Data L} {A R P : Type} [Fintype dt.SlotIx] [LinearOrder A] [LinearOrder R] [LinearOrder P] [FirstOrder.Language.wide.Structure (Univ A R P dt.KIx dt.dd)] [Finite A] {PR : Prog A R P dt.CtlIx dt.SlotIx dt.KIx dt.dd} (RF : RegFile (Univ A R P dt.KIx dt.dd)) (hord : ∀ (x y : Univ A R P dt.KIx dt.dd), WMLe x y ↔ tagTupleLe x y) [Nonempty A] [L.IsRelational] [L.Structure A] (vi : dt.VarIx) (st : TapeStD dt A R P) (v : Univ A R P dt.KIx dt.dd → Prop) {ιV : Type} [LinearOrder ιV] (mV : ιV → Univ A R P dt.KIx dt.dd → Prop) (semT : (p : dt.Scratch A R P) → (a : ιV) → (∀ (ℓ : Fin (dt.nIn vi)), dt.igPassP RF PR.zero PR.one vi (varRdSt st p (mV a)) ℓ) → (b : Fin (dt.natOf vi)) → dt.KindSem PR.zero PR.one vi (dt.matSt vi (varRdSt st p (mV a)) v ↑b) (dt.kindOf vi b)) (fG : dt.CtlIx → A) (a : ιV) : dt.CtlIx → A

The control family of the VAL loop, threaded – the twin of DescriptiveComplexity.Draw.Data.varFM.

Equations

• DescriptiveComplexity.Draw.Data.varFMT RF hord vi st v mV semT fG a = (DescriptiveComplexity.Draw.Data.varPairT RF hord vi st v mV semT fG a).2

noncomputable def DescriptiveComplexity.Draw.Data.varStE {L : FirstOrder.Language} {dt : Data L} {A R P : Type} [Fintype dt.SlotIx] [LinearOrder A] [LinearOrder R] [LinearOrder P] [FirstOrder.Language.wide.Structure (Univ A R P dt.KIx dt.dd)] [Finite A] {PR : Prog A R P dt.CtlIx dt.SlotIx dt.KIx dt.dd} (RF : RegFile (Univ A R P dt.KIx dt.dd)) (hord : ∀ (x y : Univ A R P dt.KIx dt.dd), WMLe x y ↔ tagTupleLe x y) [Nonempty A] [L.IsRelational] [L.Structure A] (vi : dt.VarIx) (st : TapeStD dt A R P) (v : Univ A R P dt.KIx dt.dd → Prop) {ιV : Type} [LinearOrder ιV] (mV : ιV → Univ A R P dt.KIx dt.dd → Prop) (semT : (p : dt.Scratch A R P) → (a : ιV) → (∀ (ℓ : Fin (dt.nIn vi)), dt.igPassP RF PR.zero PR.one vi (varRdSt st p (mV a)) ℓ) → (b : Fin (dt.natOf vi)) → dt.KindSem PR.zero PR.one vi (dt.matSt vi (varRdSt st p (mV a)) v ↑b) (dt.kindOf vi b)) (fG : dt.CtlIx → A) (a : ιV) : TapeStD dt A R P

The state one round ends in – the next round's entry state at a cover, and the loop's exit state at the top.

Equations

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

noncomputable def DescriptiveComplexity.Draw.Data.varFXT {L : FirstOrder.Language} {dt : Data L} {A R P : Type} [Fintype dt.SlotIx] [LinearOrder A] [LinearOrder R] [LinearOrder P] [FirstOrder.Language.wide.Structure (Univ A R P dt.KIx dt.dd)] [Finite A] {PR : Prog A R P dt.CtlIx dt.SlotIx dt.KIx dt.dd} (RF : RegFile (Univ A R P dt.KIx dt.dd)) (hord : ∀ (x y : Univ A R P dt.KIx dt.dd), WMLe x y ↔ tagTupleLe x y) [Nonempty A] [L.IsRelational] [L.Structure A] (vi : dt.VarIx) (st : TapeStD dt A R P) (v : Univ A R P dt.KIx dt.dd → Prop) {ιV : Type} [LinearOrder ιV] (mV : ιV → Univ A R P dt.KIx dt.dd → Prop) (semT : (p : dt.Scratch A R P) → (a : ιV) → (∀ (ℓ : Fin (dt.nIn vi)), dt.igPassP RF PR.zero PR.one vi (varRdSt st p (mV a)) ℓ) → (b : Fin (dt.natOf vi)) → dt.KindSem PR.zero PR.one vi (dt.matSt vi (varRdSt st p (mV a)) v ↑b) (dt.kindOf vi b)) (fG : dt.CtlIx → A) (a : ιV) : dt.CtlIx → A

The exit control of one VAL round, threaded – the twin of DescriptiveComplexity.Draw.Data.roundFX, at the state the round's atoms actually run at.

Equations

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

theorem DescriptiveComplexity.Draw.Data.varStT_fields {L : FirstOrder.Language} {dt : Data L} {A R P : Type} [Fintype dt.SlotIx] [LinearOrder A] [LinearOrder R] [LinearOrder P] [FirstOrder.Language.wide.Structure (Univ A R P dt.KIx dt.dd)] [Finite A] {PR : Prog A R P dt.CtlIx dt.SlotIx dt.KIx dt.dd} (RF : RegFile (Univ A R P dt.KIx dt.dd)) (hord : ∀ (x y : Univ A R P dt.KIx dt.dd), WMLe x y ↔ tagTupleLe x y) [Nonempty A] [L.IsRelational] [L.Structure A] (vi : dt.VarIx) (st : TapeStD dt A R P) {v : Univ A R P dt.KIx dt.dd → Prop} {ιV : Type} [LinearOrder ιV] (mV : ιV → Univ A R P dt.KIx dt.dd → Prop) (semT : (p : dt.Scratch A R P) → (a : ιV) → (∀ (ℓ : Fin (dt.nIn vi)), dt.igPassP RF PR.zero PR.one vi (varRdSt st p (mV a)) ℓ) → (b : Fin (dt.natOf vi)) → dt.KindSem PR.zero PR.one vi (dt.matSt vi (varRdSt st p (mV a)) v ↑b) (dt.kindOf vi b)) (fG : dt.CtlIx → A) (a : ιV) : (varStT RF hord vi st v mV semT fG a).wk = st.wk ∧ (varStT RF hord vi st v mV semT fG a).mir = st.mir ∧ (varStT RF hord vi st v mV semT fG a).bot = st.bot ∧ (varStT RF hord vi st v mV semT fG a).old = st.old ∧ (varStT RF hord vi st v mV semT fG a).val = mV a

The registers a round leaves alone ride the whole loop – by construction now, since only the two scratch ones are threaded.

theorem DescriptiveComplexity.Draw.Data.varStE_val {L : FirstOrder.Language} {dt : Data L} {A R P : Type} [Fintype dt.SlotIx] [LinearOrder A] [LinearOrder R] [LinearOrder P] [FirstOrder.Language.wide.Structure (Univ A R P dt.KIx dt.dd)] [Finite A] {PR : Prog A R P dt.CtlIx dt.SlotIx dt.KIx dt.dd} (RF : RegFile (Univ A R P dt.KIx dt.dd)) (hord : ∀ (x y : Univ A R P dt.KIx dt.dd), WMLe x y ↔ tagTupleLe x y) [Nonempty A] [L.IsRelational] [L.Structure A] (vi : dt.VarIx) (st : TapeStD dt A R P) {v : Univ A R P dt.KIx dt.dd → Prop} {ιV : Type} [LinearOrder ιV] (mV : ιV → Univ A R P dt.KIx dt.dd → Prop) (semT : (p : dt.Scratch A R P) → (a : ιV) → (∀ (ℓ : Fin (dt.nIn vi)), dt.igPassP RF PR.zero PR.one vi (varRdSt st p (mV a)) ℓ) → (b : Fin (dt.natOf vi)) → dt.KindSem PR.zero PR.one vi (dt.matSt vi (varRdSt st p (mV a)) v ↑b) (dt.kindOf vi b)) (fG : dt.CtlIx → A) (a : ιV) : (varStE RF hord vi st v mV semT fG a).val = mV a

A round leaves the register it was entered with.

theorem DescriptiveComplexity.Draw.Data.varStE_new {L : FirstOrder.Language} {dt : Data L} {A R P : Type} [Fintype dt.SlotIx] [LinearOrder A] [LinearOrder R] [LinearOrder P] [FirstOrder.Language.wide.Structure (Univ A R P dt.KIx dt.dd)] [Finite A] {PR : Prog A R P dt.CtlIx dt.SlotIx dt.KIx dt.dd} (RF : RegFile (Univ A R P dt.KIx dt.dd)) (hord : ∀ (x y : Univ A R P dt.KIx dt.dd), WMLe x y ↔ tagTupleLe x y) [Nonempty A] [L.IsRelational] [L.Structure A] (vi : dt.VarIx) (st : TapeStD dt A R P) {v : Univ A R P dt.KIx dt.dd → Prop} {ιV : Type} [LinearOrder ιV] (mV : ιV → Univ A R P dt.KIx dt.dd → Prop) (semT : (p : dt.Scratch A R P) → (a : ιV) → (∀ (ℓ : Fin (dt.nIn vi)), dt.igPassP RF PR.zero PR.one vi (varRdSt st p (mV a)) ℓ) → (b : Fin (dt.natOf vi)) → dt.KindSem PR.zero PR.one vi (dt.matSt vi (varRdSt st p (mV a)) v ↑b) (dt.kindOf vi b)) (fG : dt.CtlIx → A) (a : ιV) : (varStE RF hord vi st v mV semT fG a).new = st.new

The VAL loop never touches a stage track: only the two scratch registers are threaded, so the new tracks the spine writes ride the whole loop.

theorem DescriptiveComplexity.Draw.Data.varRdSt_varStE {L : FirstOrder.Language} {dt : Data L} {A R P : Type} [Fintype dt.SlotIx] [LinearOrder A] [LinearOrder R] [LinearOrder P] [FirstOrder.Language.wide.Structure (Univ A R P dt.KIx dt.dd)] [Finite A] {PR : Prog A R P dt.CtlIx dt.SlotIx dt.KIx dt.dd} (RF : RegFile (Univ A R P dt.KIx dt.dd)) (hord : ∀ (x y : Univ A R P dt.KIx dt.dd), WMLe x y ↔ tagTupleLe x y) [Nonempty A] [L.IsRelational] [L.Structure A] (vi : dt.VarIx) (st : TapeStD dt A R P) {v : Univ A R P dt.KIx dt.dd → Prop} {ιV : Type} [LinearOrder ιV] (mV : ιV → Univ A R P dt.KIx dt.dd → Prop) (semT : (p : dt.Scratch A R P) → (a : ιV) → (∀ (ℓ : Fin (dt.nIn vi)), dt.igPassP RF PR.zero PR.one vi (varRdSt st p (mV a)) ℓ) → (b : Fin (dt.natOf vi)) → dt.KindSem PR.zero PR.one vi (dt.matSt vi (varRdSt st p (mV a)) v ↑b) (dt.kindOf vi b)) (fG : dt.CtlIx → A) (a : ιV) (m : Univ A R P dt.KIx dt.dd → Prop) : varRdSt st ((varStE RF hord vi st v mV semT fG a).sav, (varStE RF hord vi st v mV semT fG a).tgt) m = dt.roundSt (varStE RF hord vi st v mV semT fG a) m

A round's exit state is the next round's entry state, once the next round's register is written over it.

theorem DescriptiveComplexity.Draw.Data.varSTT_bot {L : FirstOrder.Language} {dt : Data L} {A R P : Type} [Fintype dt.SlotIx] [LinearOrder A] [LinearOrder R] [LinearOrder P] [FirstOrder.Language.wide.Structure (Univ A R P dt.KIx dt.dd)] [Finite A] {PR : Prog A R P dt.CtlIx dt.SlotIx dt.KIx dt.dd} (RF : RegFile (Univ A R P dt.KIx dt.dd)) (hord : ∀ (x y : Univ A R P dt.KIx dt.dd), WMLe x y ↔ tagTupleLe x y) [Nonempty A] [L.IsRelational] [L.Structure A] (vi : dt.VarIx) (st : TapeStD dt A R P) {v : Univ A R P dt.KIx dt.dd → Prop} {ιV : Type} [LinearOrder ιV] (mV : ιV → Univ A R P dt.KIx dt.dd → Prop) (semT : (p : dt.Scratch A R P) → (a : ιV) → (∀ (ℓ : Fin (dt.nIn vi)), dt.igPassP RF PR.zero PR.one vi (varRdSt st p (mV a)) ℓ) → (b : Fin (dt.natOf vi)) → dt.KindSem PR.zero PR.one vi (dt.matSt vi (varRdSt st p (mV a)) v ↑b) (dt.kindOf vi b)) {a₀ : ιV} (hbotV : ∀ (a : ιV), a₀ ≤ a) (fG : dt.CtlIx → A) : varSTT RF hord vi st v mV semT fG a₀ = (st.sav, st.tgt)

The thread starts at the entry state.

theorem DescriptiveComplexity.Draw.Data.varStT_bot {L : FirstOrder.Language} {dt : Data L} {A R P : Type} [Fintype dt.SlotIx] [LinearOrder A] [LinearOrder R] [LinearOrder P] [FirstOrder.Language.wide.Structure (Univ A R P dt.KIx dt.dd)] [Finite A] {PR : Prog A R P dt.CtlIx dt.SlotIx dt.KIx dt.dd} (RF : RegFile (Univ A R P dt.KIx dt.dd)) (hord : ∀ (x y : Univ A R P dt.KIx dt.dd), WMLe x y ↔ tagTupleLe x y) [Nonempty A] [L.IsRelational] [L.Structure A] (vi : dt.VarIx) (st : TapeStD dt A R P) {v : Univ A R P dt.KIx dt.dd → Prop} {ιV : Type} [LinearOrder ιV] (mV : ιV → Univ A R P dt.KIx dt.dd → Prop) (semT : (p : dt.Scratch A R P) → (a : ιV) → (∀ (ℓ : Fin (dt.nIn vi)), dt.igPassP RF PR.zero PR.one vi (varRdSt st p (mV a)) ℓ) → (b : Fin (dt.natOf vi)) → dt.KindSem PR.zero PR.one vi (dt.matSt vi (varRdSt st p (mV a)) v ↑b) (dt.kindOf vi b)) {a₀ : ιV} (hbotV : ∀ (a : ιV), a₀ ≤ a) (fG : dt.CtlIx → A) : varStT RF hord vi st v mV semT fG a₀ = dt.roundSt st (mV a₀)

The thread starts at the entry state.

theorem DescriptiveComplexity.Draw.Data.varFMT_bot {L : FirstOrder.Language} {dt : Data L} {A R P : Type} [Fintype dt.SlotIx] [LinearOrder A] [LinearOrder R] [LinearOrder P] [FirstOrder.Language.wide.Structure (Univ A R P dt.KIx dt.dd)] [Finite A] {PR : Prog A R P dt.CtlIx dt.SlotIx dt.KIx dt.dd} (RF : RegFile (Univ A R P dt.KIx dt.dd)) (hord : ∀ (x y : Univ A R P dt.KIx dt.dd), WMLe x y ↔ tagTupleLe x y) [Nonempty A] [L.IsRelational] [L.Structure A] (vi : dt.VarIx) (st : TapeStD dt A R P) {v : Univ A R P dt.KIx dt.dd → Prop} {ιV : Type} [LinearOrder ιV] (mV : ιV → Univ A R P dt.KIx dt.dd → Prop) (semT : (p : dt.Scratch A R P) → (a : ιV) → (∀ (ℓ : Fin (dt.nIn vi)), dt.igPassP RF PR.zero PR.one vi (varRdSt st p (mV a)) ℓ) → (b : Fin (dt.natOf vi)) → dt.KindSem PR.zero PR.one vi (dt.matSt vi (varRdSt st p (mV a)) v ↑b) (dt.kindOf vi b)) {a₀ : ιV} (hbotV : ∀ (a : ιV), a₀ ≤ a) (fG : dt.CtlIx → A) : varFMT RF hord vi st v mV semT fG a₀ = (dt.varArgsOf PR.zero PR.one vi).initSt fG (dt.back RF.cell PR.zero PR.one ⋯ (dt.roundSt st fun (x : Univ A R P dt.KIx dt.dd) => False) v)

The control thread starts at the fold's start.

theorem DescriptiveComplexity.Draw.Data.varStT_covers {L : FirstOrder.Language} {dt : Data L} {A R P : Type} [Fintype dt.SlotIx] [LinearOrder A] [LinearOrder R] [LinearOrder P] [FirstOrder.Language.wide.Structure (Univ A R P dt.KIx dt.dd)] [Finite A] {PR : Prog A R P dt.CtlIx dt.SlotIx dt.KIx dt.dd} (RF : RegFile (Univ A R P dt.KIx dt.dd)) (hord : ∀ (x y : Univ A R P dt.KIx dt.dd), WMLe x y ↔ tagTupleLe x y) [Nonempty A] [L.IsRelational] [L.Structure A] (vi : dt.VarIx) (st : TapeStD dt A R P) {v : Univ A R P dt.KIx dt.dd → Prop} {ιV : Type} [LinearOrder ιV] [Finite ιV] (mV : ιV → Univ A R P dt.KIx dt.dd → Prop) (semT : (p : dt.Scratch A R P) → (a : ιV) → (∀ (ℓ : Fin (dt.nIn vi)), dt.igPassP RF PR.zero PR.one vi (varRdSt st p (mV a)) ℓ) → (b : Fin (dt.natOf vi)) → dt.KindSem PR.zero PR.one vi (dt.matSt vi (varRdSt st p (mV a)) v ↑b) (dt.kindOf vi b)) {a a' : ιV} (hlt : a < a') (hnb : ∀ (b : ιV), ¬(a < b ∧ b < a')) (fG : dt.CtlIx → A) : varStT RF hord vi st v mV semT fG a' = dt.roundSt (varStE RF hord vi st v mV semT fG a) (mV a')

The tape's cover equation: the next round is entered in this round's exit state, its own register written over it.

theorem DescriptiveComplexity.Draw.Data.varFMT_covers {L : FirstOrder.Language} {dt : Data L} {A R P : Type} [Fintype dt.SlotIx] [LinearOrder A] [LinearOrder R] [LinearOrder P] [FirstOrder.Language.wide.Structure (Univ A R P dt.KIx dt.dd)] [Finite A] {PR : Prog A R P dt.CtlIx dt.SlotIx dt.KIx dt.dd} (RF : RegFile (Univ A R P dt.KIx dt.dd)) (hord : ∀ (x y : Univ A R P dt.KIx dt.dd), WMLe x y ↔ tagTupleLe x y) [Nonempty A] [L.IsRelational] [L.Structure A] (vi : dt.VarIx) (st : TapeStD dt A R P) {v : Univ A R P dt.KIx dt.dd → Prop} {ιV : Type} [LinearOrder ιV] [Finite ιV] (mV : ιV → Univ A R P dt.KIx dt.dd → Prop) (semT : (p : dt.Scratch A R P) → (a : ιV) → (∀ (ℓ : Fin (dt.nIn vi)), dt.igPassP RF PR.zero PR.one vi (varRdSt st p (mV a)) ℓ) → (b : Fin (dt.natOf vi)) → dt.KindSem PR.zero PR.one vi (dt.matSt vi (varRdSt st p (mV a)) v ↑b) (dt.kindOf vi b)) {a a' : ιV} (hlt : a < a') (hnb : ∀ (b : ιV), ¬(a < b ∧ b < a')) (fG : dt.CtlIx → A) : varFMT RF hord vi st v mV semT fG a' = (dt.varArgsOf PR.zero PR.one vi).storeCarry (tagBlk (dt.valCarry (mV a)).1) ((dt.varArgsOf PR.zero PR.one vi).postFold (varFXT RF hord vi st v mV semT fG a) (dt.back RF.cell PR.zero PR.one ⋯ (varStE RF hord vi st v mV semT fG a) v)) (dt.back RF.cell PR.zero PR.one ⋯ (varStE RF hord vi st v mV semT fG a) v)

The control's cover equation: the round's exit control, folded and stored at the block its increment carried.

The threaded loop is the unthreaded one

The VAL loop's rounds run at states that differ from the machinery's entry state in SAV and TARGET alone, and every control they compute is blind to that difference (DescriptiveComplexity.Draw.Data.roundCtlT_eq_roundCtl, DescriptiveComplexity.Draw.Data.roundCtl_congr_scratch). What the threading can change is the semantic pack, since a family indexed by the scratch registers may pick different points at different registers; so the bridge is stated at a pack that is one unthreaded pack transported (semCastT), which is what a reduction supplies (DescriptiveComplexity.Draw.Data.gatedSem, whose points are the address's blocks and nothing else).

theorem DescriptiveComplexity.Draw.Data.scratchEq_varRdSt {L : FirstOrder.Language} {dt : Data L} {A R P : Type} (st : TapeStD dt A R P) (p : dt.Scratch A R P) (m : Univ A R P dt.KIx dt.dd → Prop) : dt.ScratchEq (varRdSt st p m) (dt.roundSt st m)

A round's entry state is the round state up to the two scratch registers.

noncomputable def DescriptiveComplexity.Draw.Data.semCastT {L : FirstOrder.Language} {dt : Data L} {A R P : Type} [Fintype dt.SlotIx] [LinearOrder A] [LinearOrder R] [LinearOrder P] [FirstOrder.Language.wide.Structure (Univ A R P dt.KIx dt.dd)] [Finite A] {PR : Prog A R P dt.CtlIx dt.SlotIx dt.KIx dt.dd} (RF : RegFile (Univ A R P dt.KIx dt.dd)) [Nonempty A] [L.Structure A] (vi : dt.VarIx) (st : TapeStD dt A R P) (v : Univ A R P dt.KIx dt.dd → Prop) {ιV : Type} (mV : ιV → Univ A R P dt.KIx dt.dd → Prop) (sem₀ : (a : ιV) → (∀ (ℓ : Fin (dt.nIn vi)), dt.igPassP RF PR.zero PR.one vi (dt.roundSt st (mV a)) ℓ) → (b : Fin (dt.natOf vi)) → dt.KindSem PR.zero PR.one vi (dt.roundSt st (mV a)) (dt.kindOf vi b)) (p : dt.Scratch A R P) (a : ιV) (hp : ∀ (ℓ : Fin (dt.nIn vi)), dt.igPassP RF PR.zero PR.one vi (varRdSt st p (mV a)) ℓ) (b : Fin (dt.natOf vi)) : dt.KindSem PR.zero PR.one vi (dt.matSt vi (varRdSt st p (mV a)) v ↑b) (dt.kindOf vi b)

One unthreaded pack, at every state a round reaches: the round's own state and the states its matrix threads all share the mirror and VAL of the round state, so kindSemCast carries the pack to each of them.

Equations

• DescriptiveComplexity.Draw.Data.semCastT RF vi st v mV sem₀ p a hp b = dt.kindSemCast PR.zero PR.one vi ⋯ ⋯ (dt.kindOf vi b) (sem₀ a ⋯ b)

theorem DescriptiveComplexity.Draw.Data.roundCtlT_semCastT {L : FirstOrder.Language} {dt : Data L} {A R P : Type} [Fintype dt.SlotIx] [LinearOrder A] [LinearOrder R] [LinearOrder P] [FirstOrder.Language.wide.Structure (Univ A R P dt.KIx dt.dd)] [Finite A] {PR : Prog A R P dt.CtlIx dt.SlotIx dt.KIx dt.dd} (RF : RegFile (Univ A R P dt.KIx dt.dd)) (hord : ∀ (x y : Univ A R P dt.KIx dt.dd), WMLe x y ↔ tagTupleLe x y) [Nonempty A] [L.IsRelational] [L.Structure A] (vi : dt.VarIx) (st : TapeStD dt A R P) {v : Univ A R P dt.KIx dt.dd → Prop} {ιV : Type} (mV : ιV → Univ A R P dt.KIx dt.dd → Prop) (sem₀ : (a : ιV) → (∀ (ℓ : Fin (dt.nIn vi)), dt.igPassP RF PR.zero PR.one vi (dt.roundSt st (mV a)) ℓ) → (b : Fin (dt.natOf vi)) → dt.KindSem PR.zero PR.one vi (dt.roundSt st (mV a)) (dt.kindOf vi b)) (hreg : ¬∃ (u : Univ A R P dt.KIx dt.dd), v = RF.cell u) (p : dt.Scratch A R P) (a : ιV) (q : dt.CtlIx → A) : dt.roundCtlT RF hord ⋯ vi (varRdSt st p (mV a)) v (semCastT RF vi st v mV sem₀ p a) q = roundFX RF hord vi st v mV sem₀ q a

One threaded round is the unthreaded round: a round's own state is the round state up to SAV and TARGET, its matrix threads those two further, and the pack rides along – three transports that compose to none.

theorem DescriptiveComplexity.Draw.Data.varFXT_eq_roundFX {L : FirstOrder.Language} {dt : Data L} {A R P : Type} [Fintype dt.SlotIx] [LinearOrder A] [LinearOrder R] [LinearOrder P] [FirstOrder.Language.wide.Structure (Univ A R P dt.KIx dt.dd)] [Finite A] {PR : Prog A R P dt.CtlIx dt.SlotIx dt.KIx dt.dd} (RF : RegFile (Univ A R P dt.KIx dt.dd)) (hord : ∀ (x y : Univ A R P dt.KIx dt.dd), WMLe x y ↔ tagTupleLe x y) [Nonempty A] [L.IsRelational] [L.Structure A] (vi : dt.VarIx) (st : TapeStD dt A R P) {v : Univ A R P dt.KIx dt.dd → Prop} {ιV : Type} [LinearOrder ιV] (mV : ιV → Univ A R P dt.KIx dt.dd → Prop) (sem₀ : (a : ιV) → (∀ (ℓ : Fin (dt.nIn vi)), dt.igPassP RF PR.zero PR.one vi (dt.roundSt st (mV a)) ℓ) → (b : Fin (dt.natOf vi)) → dt.KindSem PR.zero PR.one vi (dt.roundSt st (mV a)) (dt.kindOf vi b)) (hreg : ¬∃ (u : Univ A R P dt.KIx dt.dd), v = RF.cell u) (fG : dt.CtlIx → A) (a : ιV) : varFXT RF hord vi st v mV (semCastT RF vi st v mV sem₀) fG a = roundFX RF hord vi st v mV sem₀ (varFMT RF hord vi st v mV (semCastT RF vi st v mV sem₀) fG a) a

The threaded round of the VAL loop is the unthreaded one, at the state the loop's own thread produced.

theorem DescriptiveComplexity.Draw.Data.varFMT_eq_varFM {L : FirstOrder.Language} {dt : Data L} {A R P : Type} [Fintype dt.SlotIx] [LinearOrder A] [LinearOrder R] [LinearOrder P] [FirstOrder.Language.wide.Structure (Univ A R P dt.KIx dt.dd)] [Finite A] {PR : Prog A R P dt.CtlIx dt.SlotIx dt.KIx dt.dd} (RF : RegFile (Univ A R P dt.KIx dt.dd)) (hord : ∀ (x y : Univ A R P dt.KIx dt.dd), WMLe x y ↔ tagTupleLe x y) [Nonempty A] [L.IsRelational] [L.Structure A] (vi : dt.VarIx) (st : TapeStD dt A R P) {v : Univ A R P dt.KIx dt.dd → Prop} {ιV : Type} [LinearOrder ιV] [Finite ιV] (mV : ιV → Univ A R P dt.KIx dt.dd → Prop) (sem₀ : (a : ιV) → (∀ (ℓ : Fin (dt.nIn vi)), dt.igPassP RF PR.zero PR.one vi (dt.roundSt st (mV a)) ℓ) → (b : Fin (dt.natOf vi)) → dt.KindSem PR.zero PR.one vi (dt.roundSt st (mV a)) (dt.kindOf vi b)) (hreg : ¬∃ (u : Univ A R P dt.KIx dt.dd), v = RF.cell u) (fG : dt.CtlIx → A) (a : ιV) : varFMT RF hord vi st v mV (semCastT RF vi st v mV sem₀) fG a = varFM RF hord vi st v mV sem₀ fG a

The VAL loop's threaded control is its unthreaded control: round by round, varFXT_eq_roundFX, the backgrounds agreeing because a round's exit state is the round state up to SAV and TARGET. This is the bridge between the control the machine's run produces and the control DescriptiveComplexity.Draw.Data.accVerdict_leafP reads.

noncomputable def DescriptiveComplexity.Draw.Data.varFG {L : FirstOrder.Language} {dt : Data L} {A R P : Type} [Fintype dt.SlotIx] [LinearOrder A] [LinearOrder R] [LinearOrder P] [FirstOrder.Language.wide.Structure (Univ A R P dt.KIx dt.dd)] [Finite A] {PR : Prog A R P dt.CtlIx dt.SlotIx dt.KIx dt.dd} (RF : RegFile (Univ A R P dt.KIx dt.dd)) [Nonempty A] [L.IsRelational] [L.Structure A] (vi : dt.VarIx) (st : TapeStD dt A R P) (v : Univ A R P dt.KIx dt.dd → Prop) (tOf : Fin (dt.arOf vi) → dt.X.Tag) (f₀ : dt.CtlIx → A) : dt.CtlIx → A

The control the gates leave, at the reduction's own budgets – what both forms of the machinery's run start their VAL loop from.

Equations

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

theorem DescriptiveComplexity.Draw.Data.varMachine_run {L : FirstOrder.Language} {dt : Data L} {A R P : Type} [Fintype dt.SlotIx] [LinearOrder A] [LinearOrder R] [LinearOrder P] [FirstOrder.Language.wide.Structure (Univ A R P dt.KIx dt.dd)] [Finite A] [Finite R] [Finite P] {PR : Prog A R P dt.CtlIx dt.SlotIx dt.KIx dt.dd} (RF : RegFile (Univ A R P dt.KIx dt.dd)) (hord : ∀ (x y : Univ A R P dt.KIx dt.dd), WMLe x y ↔ tagTupleLe x y) [Nonempty A] [L.IsRelational] [L.Structure A] (vi : dt.VarIx) (st : TapeStD dt A R P) {v : Univ A R P dt.KIx dt.dd → Prop} {emb : dt.VarPhF vi → P} {exitPh : P} {rEmb : (i : dt.VarSiteF vi) → dt.VarShF vi i → R} [Finite dt.KIx] (hrules : ∀ (i : dt.VarSiteF vi) (ρ : dt.VarShF vi i), PR.rules (rEmb i ρ) = dt.varRuleF PR.zero PR.one vi (dt.varArgsOf PR.zero PR.one vi) emb exitPh i ρ) (hR : PR.table.Reads) (hlin : IsLinOrd WMLe) {gtop gbot : Univ A R P dt.KIx dt.dd} (htop : ∀ (y : Univ A R P dt.KIx dt.dd), WMLe y gtop) (hbot : ∀ (y : Univ A R P dt.KIx dt.dd), WMLe gbot y) (hwork : ∀ {r : Univ A R P dt.KIx dt.dd → Prop}, ¬r gbot → ∀ (u : Univ A R P dt.KIx dt.dd), WMSetLt WMLe r (RF.cell u)) {v' : Univ A R P dt.KIx dt.dd → Prop} (hv : WMSetLt WMLe v (RF.cell gbot)) (hvi : WMIncr WMLe v v') (hwkSt : st.wk = fun (r : Univ A R P dt.KIx dt.dd → Prop) => r = v) (TestOf : Fin (dt.arOf vi) → Univ A R P dt.KIx dt.dd → Prop) (hcompatOf : ∀ (ℓ : Fin (dt.arOf vi)) (u : Univ A R P dt.KIx dt.dd), dt.wellShapedG PR.zero PR.one (Sum.inl (Fin.castLE ⋯ ℓ)) (PR.passTracksAt RF.cell Slot.mir (dt.back RF.cell PR.zero PR.one ⋯ st) st.mir (RF.cell u)) ↔ TestOf ℓ u) (tOf : Fin (dt.arOf vi) → dt.X.Tag) {ιV : Type} [LinearOrder ιV] [Finite ιV] {a₀ aT : ιV} (hbotV : ∀ (a : ιV), a₀ ≤ a) (htopV : ∀ (a : ιV), a ≤ aT) (mV : ιV → Univ A R P dt.KIx dt.dd → Prop) (hmV0 : mV a₀ = fun (x : Univ A R P dt.KIx dt.dd) => False) (hIncr : ∀ (a a' : ιV), a < a' → (∀ (b : ιV), ¬(a < b ∧ b < a')) → WMIncr WMLe (mV a) (mV a')) (hTestT : ∀ (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 aT) u) (hTestF : ∀ a < aT, ∃ (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) (hmir : st.mir = v) (hbotSt : st.bot = fun (r : Univ A R P dt.KIx dt.dd → Prop) => r = fun (x : Univ A R P dt.KIx dt.dd) => False) (hsav : st.sav = v) (htgt : st.tgt = v) (semOf : (a : ιV) → (∀ (ℓ : Fin (dt.nIn vi)), dt.igPassP RF PR.zero PR.one vi (dt.roundSt st (mV a)) ℓ) → (b : Fin (dt.natOf vi)) → dt.KindSem PR.zero PR.one vi (dt.roundSt st (mV a)) (dt.kindOf vi b)) (hDom : ∀ (ℓ : Fin (dt.arOf vi)), ExpExpansion.DomHolds (tOf ℓ, decRho dt.ly PR.zero PR.one (wmBlk st.mir (Tag.arg (toLex (Sum.inl (Fin.castLE ⋯ ℓ))))))) (hwitOf : ∀ (ℓ : Fin (dt.arOf vi)) (t' : dt.X.Tag), wmBlk st.mir (Tag.arg (toLex (Sum.inl (Fin.castLE ⋯ ℓ)))) (encTagTup dt.ly PR.zero PR.one t') ↔ t' = tOf ℓ) (hTestOf : ∀ (ℓ : Fin (dt.arOf vi)) (u : Univ A R P dt.KIx dt.dd), TestOf ℓ u) (f₀ : dt.CtlIx → A) : Relation.ReflTransGen (wideData (Univ A R P dt.KIx dt.dd)).Step { state := Sum.inr (PR.stElt (emb VarPh.vchk0) f₀), head := Sum.inl v, tape := wideTape (PR.trackTapeAt RF.cell Slot.val (dt.back RF.cell PR.zero PR.one ⋯ st) st.val) (PR.syElt PR.blank) } { state := Sum.inr (PR.stElt (emb VarPh.vchk2) ((dt.varArgsOf PR.zero PR.one vi).postFold (roundFX RF hord vi st v mV semOf (varFM RF hord vi st v mV semOf (dt.gatesFs RF PR.zero PR.one vi st v (fun (ℓ : Fin (dt.arOf vi)) => Sum.inl (Fin.castLE ⋯ ℓ)) ⋯ ⋯ ⋯ tOf (dt.varArgsOf PR.zero PR.one vi).enterBlockSt ((dt.varArgsOf PR.zero PR.one vi).enterSt f₀ (dt.back RF.cell PR.zero PR.one ⋯ st v)) (dt.arOf vi)) aT) aT) (dt.back RF.cell PR.zero PR.one ⋯ (dt.roundSt st (mV aT)) v))), head := Sum.inl v, tape := wideTape (PR.trackTapeAt RF.cell Slot.val (dt.back RF.cell PR.zero PR.one ⋯ (dt.roundSt st (mV aT))) (mV aT)) (PR.syElt PR.blank) }

One variable's machinery, fully instantiated: from the entry checkpoint at the marker, through the gates at a gated address, the VAL clear and the rounds of matrix pass, exhaustion test and block-indexed increment, to the exit checkpoint – the fold spelled by the concrete threads, every leg the assembled runs of the layers below.

theorem DescriptiveComplexity.Draw.Data.varMachine_run_thread {L : FirstOrder.Language} {dt : Data L} {A R P : Type} [Fintype dt.SlotIx] [LinearOrder A] [LinearOrder R] [LinearOrder P] [FirstOrder.Language.wide.Structure (Univ A R P dt.KIx dt.dd)] [Finite A] [Finite R] [Finite P] {PR : Prog A R P dt.CtlIx dt.SlotIx dt.KIx dt.dd} (RF : RegFile (Univ A R P dt.KIx dt.dd)) (hord : ∀ (x y : Univ A R P dt.KIx dt.dd), WMLe x y ↔ tagTupleLe x y) [Nonempty A] [L.IsRelational] [L.Structure A] (vi : dt.VarIx) (st : TapeStD dt A R P) {v : Univ A R P dt.KIx dt.dd → Prop} {emb : dt.VarPhF vi → P} {exitPh : P} {rEmb : (i : dt.VarSiteF vi) → dt.VarShF vi i → R} [Finite dt.KIx] (hrules : ∀ (i : dt.VarSiteF vi) (ρ : dt.VarShF vi i), PR.rules (rEmb i ρ) = dt.varRuleF PR.zero PR.one vi (dt.varArgsOf PR.zero PR.one vi) emb exitPh i ρ) (hR : PR.table.Reads) (hlin : IsLinOrd WMLe) {gtop gbot : Univ A R P dt.KIx dt.dd} (htop : ∀ (y : Univ A R P dt.KIx dt.dd), WMLe y gtop) (hbot : ∀ (y : Univ A R P dt.KIx dt.dd), WMLe gbot y) (hwork : ∀ {r : Univ A R P dt.KIx dt.dd → Prop}, ¬r gbot → ∀ (u : Univ A R P dt.KIx dt.dd), WMSetLt WMLe r (RF.cell u)) {v' : Univ A R P dt.KIx dt.dd → Prop} (hv : WMSetLt WMLe v (RF.cell gbot)) (hvi : WMIncr WMLe v v') (hwkSt : st.wk = fun (r : Univ A R P dt.KIx dt.dd → Prop) => r = v) (TestOf : Fin (dt.arOf vi) → Univ A R P dt.KIx dt.dd → Prop) (hcompatOf : ∀ (ℓ : Fin (dt.arOf vi)) (u : Univ A R P dt.KIx dt.dd), dt.wellShapedG PR.zero PR.one (Sum.inl (Fin.castLE ⋯ ℓ)) (PR.passTracksAt RF.cell Slot.mir (dt.back RF.cell PR.zero PR.one ⋯ st) st.mir (RF.cell u)) ↔ TestOf ℓ u) (tOf : Fin (dt.arOf vi) → dt.X.Tag) {ιV : Type} [LinearOrder ιV] [Finite ιV] {a₀ aT : ιV} (hbotV : ∀ (a : ιV), a₀ ≤ a) (htopV : ∀ (a : ιV), a ≤ aT) (mV : ιV → Univ A R P dt.KIx dt.dd → Prop) (hmV0 : mV a₀ = fun (x : Univ A R P dt.KIx dt.dd) => False) (hIncr : ∀ (a a' : ιV), a < a' → (∀ (b : ιV), ¬(a < b ∧ b < a')) → WMIncr WMLe (mV a) (mV a')) (hTestT : ∀ (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 aT) u) (hTestF : ∀ a < aT, ∃ (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) (hmir : st.mir = v) (hbotSt : st.bot = fun (r : Univ A R P dt.KIx dt.dd → Prop) => r = fun (x : Univ A R P dt.KIx dt.dd) => False) (semT : (p : dt.Scratch A R P) → (a : ιV) → (∀ (ℓ : Fin (dt.nIn vi)), dt.igPassP RF PR.zero PR.one vi (varRdSt st p (mV a)) ℓ) → (b : Fin (dt.natOf vi)) → dt.KindSem PR.zero PR.one vi (dt.matSt vi (varRdSt st p (mV a)) v ↑b) (dt.kindOf vi b)) (hDom : ∀ (ℓ : Fin (dt.arOf vi)), ExpExpansion.DomHolds (tOf ℓ, decRho dt.ly PR.zero PR.one (wmBlk st.mir (Tag.arg (toLex (Sum.inl (Fin.castLE ⋯ ℓ))))))) (hwitOf : ∀ (ℓ : Fin (dt.arOf vi)) (t' : dt.X.Tag), wmBlk st.mir (Tag.arg (toLex (Sum.inl (Fin.castLE ⋯ ℓ)))) (encTagTup dt.ly PR.zero PR.one t') ↔ t' = tOf ℓ) (hTestOf : ∀ (ℓ : Fin (dt.arOf vi)) (u : Univ A R P dt.KIx dt.dd), TestOf ℓ u) (f₀ : dt.CtlIx → A) : Relation.ReflTransGen (wideData (Univ A R P dt.KIx dt.dd)).Step { state := Sum.inr (PR.stElt (emb VarPh.vchk0) f₀), head := Sum.inl v, tape := wideTape (PR.trackTapeAt RF.cell Slot.val (dt.back RF.cell PR.zero PR.one ⋯ st) st.val) (PR.syElt PR.blank) } { state := Sum.inr (PR.stElt (emb VarPh.vchk2) ((dt.varArgsOf PR.zero PR.one vi).postFold (varFXT RF hord vi st v mV semT (varFG RF vi st v tOf f₀) aT) (dt.back RF.cell PR.zero PR.one ⋯ (varStE RF hord vi st v mV semT (varFG RF vi st v tOf f₀) aT) v))), head := Sum.inl v, tape := wideTape (PR.trackTapeAt RF.cell Slot.val (dt.back RF.cell PR.zero PR.one ⋯ (varStE RF hord vi st v mV semT (varFG RF vi st v tOf f₀) aT)) (mV aT)) (PR.syElt PR.blank) }

One variable's machinery, fully instantiated – threaded: as DescriptiveComplexity.Draw.Data.varMachine_run with no boundary discipline assumed, so it applies at every address of a sweep and not only at the one whose SAV and TARGET the advance happens to have left behind. The rounds run at the states the thread produces, and the loop ends in DescriptiveComplexity.Draw.Data.varStE at the top, which differs from the entry state in SAV and TARGET alone.