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.

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.

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.

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.

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.

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.

The fold invariant of the VAL loop

The leaf, discharged

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.

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).

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.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.