The atom kinds, dispatched: one stage interface for the matrix

The matrix's sequencer treats every classified atom alike; this file makes that literal. DescriptiveComplexity.Draw.Data.KindSem carries the one piece of semantic data a kind's run needs (the encoded points, for an expansion atom – the others need none), DescriptiveComplexity.Draw.Data.kindExitCtl is the control each kind's machinery leaves behind, and DescriptiveComplexity.Draw.Data.kind_hStage is the uniform stage discharge: whatever the kind, from the machinery's entry phase one cell right of the marker to the exit phase back there, at the Slot.val-walked presentation – the shape DescriptiveComplexity.Draw.seq_run consumes.

Generic slot-preservation through the generated families

theorem DescriptiveComplexity.Draw.chainSt_apply_of {A Q : Type} (q : Q) {nr : ℕ} (bit : Fin nr → Prop) (upd : Fin nr → Bool → (Q → A) → Q → A) (hupd : ∀ (i : Fin nr) (bb : Bool) (f : Q → A), upd i bb f q = f q) (base : Q → A) (n : ℕ) : chainSt bit upd base n q = base q

A within-round chain preserving a control value preserves it end to end.

theorem DescriptiveComplexity.Draw.elemFam_apply_of {A R P Q W K : Type} {dd : ℕ} {ι : Type} [LinearOrder ι] [Finite ι] (q : Q) {nr : ℕ} {setFlag : Fin nr → Bool → (Q → A) → (W → A) → Q → A} {initEl advEl : (Q → A) → (W → A) → Q → A} {I : Type} {rest : (Univ A R P K dd → Prop) → W → A} {v : Univ A R P K dd → Prop} {m : Fin nr → I → Prop} (hSet : ∀ (k : Fin nr) (bb : Bool) (f : Q → A) (g : W → A), setFlag k bb f g q = f q) (hInit : ∀ (f : Q → A) (g : W → A), initEl f g q = f q) (hAdv : ∀ (f : Q → A) (g : W → A), advEl f g q = f q) (xOf : ι → Fin nr → I) (f₀ : Q → A) (a : ι) (j : Fin (nr + 1)) : elemFam setFlag initEl advEl rest v m xOf f₀ a j q = f₀ q

A control value the loop's operations never write survives the whole generated element family.

theorem DescriptiveComplexity.Draw.tupleIter1_apply_of {A R P Q W K : Type} {dd : ℕ} {ι : Type} [LinearOrder ι] [Finite ι] (q : Q) {setBit : Bool → (Q → A) → (W → A) → Q → A} {initLv advLv : (Q → A) → (W → A) → Q → A} {I : Type} {mSrc : I → Prop} {v : Univ A R P K dd → Prop} {restF : (I → Prop) → (Univ A R P K dd → Prop) → W → A} (hSet : ∀ (bb : Bool) (f : Q → A) (g : W → A), setBit bb f g q = f q) (hInit : ∀ (f : Q → A) (g : W → A), initLv f g q = f q) (hAdv : ∀ (f : Q → A) (g : W → A), advLv f g q = f q) (xS xD : ι → I) (mD₀ : I → Prop) (f₀ : Q → A) (a : ι) : tupleIter1 setBit initLv advLv mSrc v restF xS xD mD₀ f₀ a q = f₀ q

A control value the copy loop's operations never write survives the generated tuple family.

noncomputable def DescriptiveComplexity.Draw.Data.KindSem {L : FirstOrder.Language} (dt : Data L) {A R P : Type} [LinearOrder A] [L.Structure A] (zero one : A) (vi : dt.VarIx) (st : TapeStD dt A R P) : MatAtom dt.X dt.d.B (dt.nOf vi) → Type

The semantic data of one atom's run: an expansion atom needs the points its levels' registers encode; the other kinds need nothing.

Equations

• One or more equations did not get rendered due to their size.
• dt.KindSem zero one vi st (DescriptiveComplexity.Draw.MatAtom.eq a a_1) = PUnit.{1}
• dt.KindSem zero one vi st (DescriptiveComplexity.Draw.MatAtom.ord a a_1) = PUnit.{1}
• dt.KindSem zero one vi st (DescriptiveComplexity.Draw.MatAtom.stage i a) = PUnit.{1}

noncomputable def DescriptiveComplexity.Draw.Data.kindSemCast {L : FirstOrder.Language} (dt : Data L) {A R P : Type} [LinearOrder A] [L.Structure A] (zero one : A) (vi : dt.VarIx) {st st' : TapeStD dt A R P} (hmir : st.mir = st'.mir) (hval : st.val = st'.val) (κ : MatAtom dt.X dt.d.B (dt.nOf vi)) (s : dt.KindSem zero one vi st κ) : dt.KindSem zero one vi st' κ

A semantic pack transports along the registers it reads. DescriptiveComplexity.Draw.Data.KindSem sees the tape state only through the levels' register sets, so a pack at one state is a pack at every state with the same mirror and VAL. This is what lets one pack – built at an address's entry state – serve every position of the spine and every round of the VAL loop, whose states differ from it in the tracks they have written and in the two scratch registers.

Equations

• dt.kindSemCast zero one vi hmir hval (DescriptiveComplexity.Draw.MatAtom.eq a a_1) s_2 = s_2
• dt.kindSemCast zero one vi hmir hval (DescriptiveComplexity.Draw.MatAtom.ord a a_1) s_2 = s_2
• dt.kindSemCast zero one vi hmir hval (DescriptiveComplexity.Draw.MatAtom.stage i a) s_2 = s_2
• dt.kindSemCast zero one vi hmir hval (DescriptiveComplexity.Draw.MatAtom.exp a ts) s_2 = ⟨↑s_2, ⋯⟩

theorem DescriptiveComplexity.Draw.Data.kindSemCast_triple {L : FirstOrder.Language} (dt : Data L) {A R P : Type} [LinearOrder A] [L.Structure A] (zero one : A) (vi : dt.VarIx) {st₁ st₂ st₃ : TapeStD dt A R P} (h1 : st₁.mir = st₂.mir) (h2 : st₁.val = st₂.val) (h3 : st₂.mir = st₃.mir) (h4 : st₂.val = st₃.val) (h5 : st₃.mir = st₁.mir) (h6 : st₃.val = st₁.val) (κ : MatAtom dt.X dt.d.B (dt.nOf vi)) (s : dt.KindSem zero one vi st₁ κ) : dt.kindSemCast zero one vi h5 h6 κ (dt.kindSemCast zero one vi h3 h4 κ (dt.kindSemCast zero one vi h1 h2 κ s)) = s

A round trip of transports is the identity – the shape the VAL loop's bridge closes with: the pack leaves the round state, travels to the round's own state and to the state its matrix threads, and comes back.

noncomputable def DescriptiveComplexity.Draw.Data.kindExitCtl {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)) (hord : ∀ (x y : Univ A R P dt.KIx dt.dd), WMLe x y ↔ tagTupleLe x y) [Nonempty A] [L.IsRelational] [L.Structure A] (zero one : A) (vi : dt.VarIx) (av : Fin dt.natMax) (st : TapeStD dt A R P) (v : Univ A R P dt.KIx dt.dd → Prop) (κ : MatAtom dt.X dt.d.B (dt.nOf vi)) : dt.KindSem zero one vi st κ → dt.kindArgs κ * Fintype.card dt.X.Tag ≤ dt.ntgDim → dt.kindDepth κ ≤ dt.eDim → dt.kindReads κ ≤ dt.nfDim → (dt.CtlIx → A) → dt.CtlIx → A

The control one atom's machinery leaves behind, by kind: the fold's exit at the comparison's or the expansion atom's family, the verdict store at the stage atom's read bit.

Equations

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

theorem DescriptiveComplexity.Draw.Data.kindExitCtl_congr_scratch {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)) (hord : ∀ (x y : Univ A R P dt.KIx dt.dd), WMLe x y ↔ tagTupleLe x y) [Nonempty A] [L.IsRelational] [L.Structure A] {zero one : A} {vi : dt.VarIx} {av : Fin dt.natMax} {st : TapeStD dt A R P} {v : Univ A R P dt.KIx dt.dd → Prop} {st' : TapeStD dt A R P} (h : dt.ScratchEq st st') (hreg : ¬∃ (u : Univ A R P dt.KIx dt.dd), v = RF.cell u) (κ : MatAtom dt.X dt.d.B (dt.nOf vi)) (sem : dt.KindSem zero one vi st κ) (hk : dt.kindArgs κ * Fintype.card dt.X.Tag ≤ dt.ntgDim) (hn : dt.kindDepth κ ≤ dt.eDim) (hrd : dt.kindReads κ ≤ dt.nfDim) (f : dt.CtlIx → A) : dt.kindExitCtl RF hord zero one vi av st v κ sem hk hn hrd f = dt.kindExitCtl RF hord zero one vi av st' v κ (dt.kindSemCast zero one vi ⋯ ⋯ κ sem) hk hn hrd f

An atom's machinery is blind to the two scratch registers: each kind's loop reads the levels' register sets and its background at the working cell, and each kind's exit reads the control alone (DescriptiveComplexity.Draw.Data.cmpArgs_exitSt_congr and its two siblings). The pack travels by DescriptiveComplexity.Draw.Data.kindSemCast, which keeps its points. This is the brick the whole threaded-versus-unthreaded bridge is built from.

noncomputable def DescriptiveComplexity.Draw.Data.kindEndSt {L : FirstOrder.Language} (dt : Data L) {A R P : Type} (vi : dt.VarIx) (v : Univ A R P dt.KIx dt.dd → Prop) (κ : MatAtom dt.X dt.d.B (dt.nOf vi)) (st : TapeStD dt A R P) : TapeStD dt A R P

The state an atom leaves: a stage atom normalizes SAV and TARGET to the home address (its random access writes them whatever they held), every other kind leaves the state alone.

Equations

• dt.kindEndSt vi v (DescriptiveComplexity.Draw.MatAtom.stage i a) st = DescriptiveComplexity.Draw.Data.stageEndSt st v
• dt.kindEndSt vi v κ st = st

theorem DescriptiveComplexity.Draw.Data.kind_hStage_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} {av : Fin dt.natMax} {st : TapeStD dt A R P} {v : Univ A R P dt.KIx dt.dd → Prop} [Finite dt.KIx] (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) (hmirSt : 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) (κ : MatAtom dt.X dt.d.B (dt.nOf vi)) (hk : dt.kindArgs κ * Fintype.card dt.X.Tag ≤ dt.ntgDim) (hnd : dt.kindDepth κ ≤ dt.eDim) (hrd : dt.kindReads κ ≤ dt.nfDim) (sem : dt.KindSem PR.zero PR.one vi st κ) {emb : dt.KindPh κ → P} {exitPh : P} {rEmb : (s : dt.KindSite κ) → dt.KindSh κ s → R} (hrules : ∀ (s : dt.KindSite κ) (ρ : dt.KindSh κ s), PR.rules (rEmb s ρ) = dt.kindRule PR.zero PR.one κ (dt.kindArgsOf PR.zero PR.one vi av κ hk hnd hrd) emb exitPh s ρ) (f : dt.CtlIx → A) : Relation.ReflTransGen (wideData (Univ A R P dt.KIx dt.dd)).Step { state := Sum.inr (PR.stElt (emb (dt.kindEntry κ)) 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.kindExitCtl RF hord PR.zero PR.one vi av st v κ sem hk hnd hrd f)), head := Sum.inl v', tape := wideTape (PR.trackTapeAt RF.cell Slot.val (dt.back RF.cell PR.zero PR.one ⋯ (dt.kindEndSt vi v κ st)) (dt.kindEndSt vi v κ st).val) (PR.syElt PR.blank) }

The uniform stage discharge, threaded: as DescriptiveComplexity.Draw.Data.kind_hStage but with no boundary discipline assumed – the atom's exit state is DescriptiveComplexity.Draw.Data.kindEndSt, which normalizes SAV and TARGET exactly when the atom is a stage atom.

theorem DescriptiveComplexity.Draw.Data.kind_hStage {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} {av : Fin dt.natMax} {st : TapeStD dt A R P} {v : Univ A R P dt.KIx dt.dd → Prop} [Finite dt.KIx] (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) (hmirSt : 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) (κ : MatAtom dt.X dt.d.B (dt.nOf vi)) (hk : dt.kindArgs κ * Fintype.card dt.X.Tag ≤ dt.ntgDim) (hnd : dt.kindDepth κ ≤ dt.eDim) (hrd : dt.kindReads κ ≤ dt.nfDim) (sem : dt.KindSem PR.zero PR.one vi st κ) {emb : dt.KindPh κ → P} {exitPh : P} {rEmb : (s : dt.KindSite κ) → dt.KindSh κ s → R} (hrules : ∀ (s : dt.KindSite κ) (ρ : dt.KindSh κ s), PR.rules (rEmb s ρ) = dt.kindRule PR.zero PR.one κ (dt.kindArgsOf PR.zero PR.one vi av κ hk hnd hrd) emb exitPh s ρ) (f : dt.CtlIx → A) : Relation.ReflTransGen (wideData (Univ A R P dt.KIx dt.dd)).Step { state := Sum.inr (PR.stElt (emb (dt.kindEntry κ)) 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.kindExitCtl RF hord PR.zero PR.one vi av st v κ sem hk hnd hrd 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 uniform stage discharge: whatever the kind, the atom's machinery runs from its entry phase one cell right of the marker to the exit phase back there, leaving DescriptiveComplexity.Draw.Data.kindExitCtl in the control and the tape untouched.

The matrix, assembled

noncomputable def DescriptiveComplexity.Draw.Data.matFs {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)) (hord : ∀ (x y : Univ A R P dt.KIx dt.dd), WMLe x y ↔ tagTupleLe x y) [Nonempty A] [L.IsRelational] [L.Structure A] (zero one : A) (vi : dt.VarIx) (st : TapeStD dt A R P) (v : Univ A R P dt.KIx dt.dd → Prop) (enterSt : Fin (dt.natOf vi) → (dt.CtlIx → A) → (dt.SlotIx → A) → dt.CtlIx → A) (sem : (a : Fin (dt.natOf vi)) → dt.KindSem zero one vi st (dt.kindOf vi a)) (f₀ : dt.CtlIx → A) : ℕ → dt.CtlIx → A

The control thread across the matrix's atoms: each atom's machinery entered through the dispatch's enterSt, its exit control the next atom's input.

Equations

• One or more equations did not get rendered due to their size.
• dt.matFs RF hord zero one vi st v enterSt sem f₀ 0 = f₀

The threaded states of the matrix

theorem DescriptiveComplexity.Draw.Data.kindEndSt_fields {L : FirstOrder.Language} {dt : Data L} {A R P : Type} {vi : dt.VarIx} {v : Univ A R P dt.KIx dt.dd → Prop} (κ : MatAtom dt.X dt.d.B (dt.nOf vi)) (st : TapeStD dt A R P) : (dt.kindEndSt vi v κ st).wk = st.wk ∧ (dt.kindEndSt vi v κ st).mir = st.mir ∧ (dt.kindEndSt vi v κ st).bot = st.bot ∧ (dt.kindEndSt vi v κ st).val = st.val ∧ (dt.kindEndSt vi v κ st).old = st.old

An atom's exit state keeps the marker, the mirror, the bottom mark and the VAL register: only SAV and TARGET can move.

noncomputable def DescriptiveComplexity.Draw.Data.matSt {L : FirstOrder.Language} (dt : Data L) {A R P : Type} (vi : dt.VarIx) (st : TapeStD dt A R P) (v : Univ A R P dt.KIx dt.dd → Prop) : ℕ → TapeStD dt A R P

The state after the matrix's first n atoms: each stage atom normalizes SAV and TARGET, the other kinds change nothing.

Equations

• dt.matSt vi st v 0 = st
• dt.matSt vi st v n.succ = if h : n < dt.natOf vi then dt.kindEndSt vi v (dt.kindOf vi ⟨n, h⟩) (dt.matSt vi st v n) else dt.matSt vi st v n

theorem DescriptiveComplexity.Draw.Data.matSt_fields {L : FirstOrder.Language} {dt : Data L} {A R P : Type} {vi : dt.VarIx} {st : TapeStD dt A R P} {v : Univ A R P dt.KIx dt.dd → Prop} (n : ℕ) : (dt.matSt vi st v n).wk = st.wk ∧ (dt.matSt vi st v n).mir = st.mir ∧ (dt.matSt vi st v n).bot = st.bot ∧ (dt.matSt vi st v n).val = st.val ∧ (dt.matSt vi st v n).old = st.old

The threaded states differ from the entry state in SAV and TARGET alone – so every hypothesis the atoms need at them is the entry state's.

theorem DescriptiveComplexity.Draw.Data.tapeSt_eq_savTgt {L : FirstOrder.Language} {dt : Data L} {A R P : Type} {X Y : TapeStD dt A R P} (hmir : X.mir = Y.mir) (hval : X.val = Y.val) (hold : X.old = Y.old) (hnew : X.new = Y.new) (hwk : X.wk = Y.wk) (hbot : X.bot = Y.bot) (hltp : X.ltp = Y.ltp) : X = { mir := Y.mir, tgt := X.tgt, sav := X.sav, val := Y.val, old := Y.old, new := Y.new, wk := Y.wk, bot := Y.bot, ltp := Y.ltp }

A tape state is determined by its two scratch registers, given the other seven – the shape every threaded state of the machinery has against the state it started from.

theorem DescriptiveComplexity.Draw.Data.kindEndSt_fields' {L : FirstOrder.Language} {dt : Data L} {A R P : Type} {vi : dt.VarIx} {v : Univ A R P dt.KIx dt.dd → Prop} (κ : MatAtom dt.X dt.d.B (dt.nOf vi)) (st : TapeStD dt A R P) : (dt.kindEndSt vi v κ st).new = st.new ∧ (dt.kindEndSt vi v κ st).ltp = st.ltp

The remaining registers an atom leaves alone – the three DescriptiveComplexity.Draw.Data.kindEndSt_fields does not list, so that the seven together pin the state down to its SAV and TARGET.

theorem DescriptiveComplexity.Draw.Data.matSt_fields' {L : FirstOrder.Language} {dt : Data L} {A R P : Type} {vi : dt.VarIx} {st : TapeStD dt A R P} {v : Univ A R P dt.KIx dt.dd → Prop} (n : ℕ) : (dt.matSt vi st v n).new = st.new ∧ (dt.matSt vi st v n).ltp = st.ltp

The same two, along the matrix's whole chain of atoms.

theorem DescriptiveComplexity.Draw.Data.matSt_eq {L : FirstOrder.Language} {dt : Data L} {A R P : Type} {vi : dt.VarIx} {st : TapeStD dt A R P} {v : Univ A R P dt.KIx dt.dd → Prop} (n : ℕ) : dt.matSt vi st v n = { mir := st.mir, tgt := (dt.matSt vi st v n).tgt, sav := (dt.matSt vi st v n).sav, val := st.val, old := st.old, new := st.new, wk := st.wk, bot := st.bot, ltp := st.ltp }

The matrix's threaded state is its entry state with the two scratch registers rewritten – the sharpening of DescriptiveComplexity.Draw.Data.matSt_fields that lets the loop above thread the two registers instead of the whole state, and with them keep every semantic pack at the state it was built for.

theorem DescriptiveComplexity.Draw.Data.kindExitCtl_apply_avC {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)) (hord : ∀ (x y : Univ A R P dt.KIx dt.dd), WMLe x y ↔ tagTupleLe x y) [Nonempty A] [L.IsRelational] [L.Structure A] {zero one : A} {vi : dt.VarIx} {av : Fin dt.natMax} {st : TapeStD dt A R P} {v : Univ A R P dt.KIx dt.dd → Prop} (κ : MatAtom dt.X dt.d.B (dt.nOf vi)) (sem : dt.KindSem zero one vi st κ) (hk : dt.kindArgs κ * Fintype.card dt.X.Tag ≤ dt.ntgDim) (hnd : dt.kindDepth κ ≤ dt.eDim) (hrd : dt.kindReads κ ≤ dt.nfDim) (f : dt.CtlIx → A) {a' : Fin dt.natMax} (hne : dt.avC a' ≠ dt.avC av) : dt.kindExitCtl RF hord zero one vi av st v κ sem hk hnd hrd f (dt.avC a') = f (dt.avC a')

A foreign verdict slot survives one atom's machinery: whatever the kind, its exit control writes its own verdict slot and scratch, never another atom's.

theorem DescriptiveComplexity.Draw.Data.kindExitCtl_apply_accC {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)) (hord : ∀ (x y : Univ A R P dt.KIx dt.dd), WMLe x y ↔ tagTupleLe x y) [Nonempty A] [L.IsRelational] [L.Structure A] {zero one : A} {vi : dt.VarIx} {av : Fin dt.natMax} {st : TapeStD dt A R P} {v : Univ A R P dt.KIx dt.dd → Prop} (κ : MatAtom dt.X dt.d.B (dt.nOf vi)) (sem : dt.KindSem zero one vi st κ) (hk : dt.kindArgs κ * Fintype.card dt.X.Tag ≤ dt.ntgDim) (hnd : dt.kindDepth κ ≤ dt.eDim) (hrd : dt.kindReads κ ≤ dt.nfDim) (f : dt.CtlIx → A) (jj : Fin dt.naDim) : dt.kindExitCtl RF hord zero one vi av st v κ sem hk hnd hrd f (dt.accC jj) = f (dt.accC jj)

An accumulator slot survives one atom's machinery: no atom's exit control ever writes the inner fold's vector.

theorem DescriptiveComplexity.Draw.Data.matFs_apply_accC {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)) (hord : ∀ (x y : Univ A R P dt.KIx dt.dd), WMLe x y ↔ tagTupleLe x y) [Nonempty A] [L.IsRelational] [L.Structure A] {zero one : A} {vi : dt.VarIx} {st : TapeStD dt A R P} {v : Univ A R P dt.KIx dt.dd → Prop} (enterSt : Fin (dt.natOf vi) → (dt.CtlIx → A) → (dt.SlotIx → A) → dt.CtlIx → A) (hEnterAcc : ∀ (b : Fin (dt.natOf vi)) (f : dt.CtlIx → A) (g : dt.SlotIx → A) (jj : Fin dt.naDim), enterSt b f g (dt.accC jj) = f (dt.accC jj)) (sem : (b : Fin (dt.natOf vi)) → dt.KindSem zero one vi st (dt.kindOf vi b)) (f₀ : dt.CtlIx → A) (jj : Fin dt.naDim) (n : ℕ) : dt.matFs RF hord zero one vi st v enterSt sem f₀ n (dt.accC jj) = f₀ (dt.accC jj)

The inner fold's vector survives the whole matrix: no atom writes it, so the thread's accumulators after all atoms are the entry's.

theorem DescriptiveComplexity.Draw.Data.matFs_apply_avC {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)) (hord : ∀ (x y : Univ A R P dt.KIx dt.dd), WMLe x y ↔ tagTupleLe x y) [Nonempty A] [L.IsRelational] [L.Structure A] {zero one : A} {vi : dt.VarIx} {st : TapeStD dt A R P} {v : Univ A R P dt.KIx dt.dd → Prop} (enterSt : Fin (dt.natOf vi) → (dt.CtlIx → A) → (dt.SlotIx → A) → dt.CtlIx → A) (hEnterAv : ∀ (b : Fin (dt.natOf vi)) (f : dt.CtlIx → A) (g : dt.SlotIx → A) (a' : Fin dt.natMax), enterSt b f g (dt.avC a') = f (dt.avC a')) (sem : (b : Fin (dt.natOf vi)) → dt.KindSem zero one vi st (dt.kindOf vi b)) (f₀ : dt.CtlIx → A) (a : Fin (dt.natOf vi)) : dt.matFs RF hord zero one vi st v enterSt sem f₀ (dt.natOf vi) (dt.avC (Fin.castLE ⋯ a)) = dt.kindExitCtl RF hord zero one vi (Fin.castLE ⋯ a) st v (dt.kindOf vi a) (sem a) ⋯ ⋯ ⋯ (enterSt a (dt.matFs RF hord zero one vi st v enterSt sem f₀ ↑a) (dt.back RF.cell zero one ⋯ st v)) (dt.avC (Fin.castLE ⋯ a))

An atom's verdict bit survives the rest of the matrix: the thread's value at atom a's slot after all atoms is what atom a's own machinery wrote.

noncomputable def DescriptiveComplexity.Draw.Data.mkKindSem {L : FirstOrder.Language} (dt : Data L) {A R P : Type} [LinearOrder A] [L.Structure A] (zero one : A) (vi : dt.VarIx) (st : TapeStD dt A R P) (w : Fin (dt.nOf vi) → dt.X.Map A) (hENC : ∀ (j : Fin (dt.nOf vi)), wmBlk (dt.lvSet st vi j) (Tag.arg (toLex (dt.lvBlk vi j))) = encMap dt.ly zero one (w j)) (κ : MatAtom dt.X dt.d.B (dt.nOf vi)) : dt.KindSem zero one vi st κ

The semantic data of every atom, from one encoded valuation: the expansion atoms' points are the valuation's, everything else needs nothing.

Equations

• dt.mkKindSem zero one vi st w hENC (DescriptiveComplexity.Draw.MatAtom.eq a a_1) = PUnit.unit
• dt.mkKindSem zero one vi st w hENC (DescriptiveComplexity.Draw.MatAtom.ord a a_1) = PUnit.unit
• dt.mkKindSem zero one vi st w hENC (DescriptiveComplexity.Draw.MatAtom.stage i a) = PUnit.unit
• dt.mkKindSem zero one vi st w hENC (DescriptiveComplexity.Draw.MatAtom.exp a ts) = ⟨fun (ℓ : Fin k) => w (ts ℓ), ⋯⟩

theorem DescriptiveComplexity.Draw.Data.kindSemCast_mkKindSem {L : FirstOrder.Language} {dt : Data L} {A R P : Type} [LinearOrder A] [L.Structure A] (zero one : A) (vi : dt.VarIx) {st st' : TapeStD dt A R P} (hmir : st.mir = st'.mir) (hval : st.val = st'.val) {w w' : Fin (dt.nOf vi) → dt.X.Map A} (hww : w = w') (hENC : ∀ (j : Fin (dt.nOf vi)), wmBlk (dt.lvSet st vi j) (Tag.arg (toLex (dt.lvBlk vi j))) = encMap dt.ly zero one (w j)) (hENC' : ∀ (j : Fin (dt.nOf vi)), wmBlk (dt.lvSet st' vi j) (Tag.arg (toLex (dt.lvBlk vi j))) = encMap dt.ly zero one (w' j)) (κ : MatAtom dt.X dt.d.B (dt.nOf vi)) : dt.kindSemCast zero one vi hmir hval κ (dt.mkKindSem zero one vi st w hENC κ) = dt.mkKindSem zero one vi st' w' hENC' κ

The transport of a built pack is the built pack: mkKindSem puts the valuation's points in and nothing else, and the proof components are irrelevant.

theorem DescriptiveComplexity.Draw.Data.cmpAgr_iff_padBits {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)) (hord : ∀ (x y : Univ A R P dt.KIx dt.dd), WMLe x y ↔ tagTupleLe x y) [L.Structure A] {zero one : A} {vi : dt.VarIx} {st : TapeStD dt A R P} {j₁ j₂ : Fin (dt.nOf vi)} {p q : dt.X.Map A} (h1 : wmBlk (dt.lvSet st vi j₁) (Tag.arg (toLex (dt.lvBlk vi j₁))) = encMap dt.ly zero one p) (h2 : wmBlk (dt.lvSet st vi j₂) (Tag.arg (toLex (dt.lvBlk vi j₂))) = encMap dt.ly zero one q) (u : Lex (Fin dt.dd0 → A)) : CmpAgr (laidFile RF hord) zero ⋯ vi j₁ j₂ st u ↔ (dt.padBits zero (encMap dt.ly zero one p) (ofLex u) ↔ dt.padBits zero (encMap dt.ly zero one q) (ofLex u))

One round's agreement is the padded bits': given the two registers hold encodings, the machine's per-tuple question is the encodings'.

theorem DescriptiveComplexity.Draw.Data.cmpAgr_all_iff {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)) (hord : ∀ (x y : Univ A R P dt.KIx dt.dd), WMLe x y ↔ tagTupleLe x y) [L.Structure A] {zero one : A} {vi : dt.VarIx} {st : TapeStD dt A R P} (hzo : zero ≠ one) {j₁ j₂ : Fin (dt.nOf vi)} {p q : dt.X.Map A} (h1 : wmBlk (dt.lvSet st vi j₁) (Tag.arg (toLex (dt.lvBlk vi j₁))) = encMap dt.ly zero one p) (h2 : wmBlk (dt.lvSet st vi j₂) (Tag.arg (toLex (dt.lvBlk vi j₂))) = encMap dt.ly zero one q) : (∀ (u : Lex (Fin dt.dd0 → A)), CmpAgr (laidFile RF hord) zero ⋯ vi j₁ j₂ st u) ↔ p = q

The equality atom's verdict is point equality: agreement at every tuple decides the two encoded points.

theorem DescriptiveComplexity.Draw.Data.cmp_ord_iff {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)) (hord : ∀ (x y : Univ A R P dt.KIx dt.dd), WMLe x y ↔ tagTupleLe x y) [L.Structure A] {zero one : A} {vi : dt.VarIx} {st : TapeStD dt A R P} (hzo : zero ≠ one) {j₁ j₂ : Fin (dt.nOf vi)} {p q : dt.X.Map A} (h1 : wmBlk (dt.lvSet st vi j₁) (Tag.arg (toLex (dt.lvBlk vi j₁))) = encMap dt.ly zero one p) (h2 : wmBlk (dt.lvSet st vi j₂) (Tag.arg (toLex (dt.lvBlk vi j₂))) = encMap dt.ly zero one q) : ((∀ (u : Lex (Fin dt.dd0 → A)), CmpAgr (laidFile RF hord) zero ⋯ vi j₁ j₂ st u) ∨ ∃ (u : Lex (Fin dt.dd0 → A)), CmpFst (laidFile RF hord) zero ⋯ vi j₁ j₂ st u) ↔ p ≤ q

The order atom's verdict is the chosen order: agreement everywhere, or a first difference with the second block holding the cell, is exactly the binary order of the two encodings – the order the reduction puts on the points.

theorem DescriptiveComplexity.Draw.Data.ctlBit_kindExitCtl_self {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] (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] {zero one : A} {vi : dt.VarIx} {av : Fin dt.natMax} {st : TapeStD dt A R P} {v : Univ A R P dt.KIx dt.dd → Prop} [LinearOrder (dt.X.Map A)] (hzo : zero ≠ one) (hlin : IsLinOrd WMLe) (σ : dt.d.B.Assignment (dt.X.Map A)) (w : Fin (dt.nOf vi) → dt.X.Map A) (hENC : ∀ (j : Fin (dt.nOf vi)), wmBlk (dt.lvSet st vi j) (Tag.arg (toLex (dt.lvBlk vi j))) = encMap dt.ly zero one (w j)) (hOld : ∀ (i : dt.d.B.ι) (ts : Fin (dt.d.B.arity i) → Fin (dt.nOf vi)), st.old i (dt.stageTgtD zero vi i ts st v (dt.d.B.arity i)) ↔ σ i fun (q : Fin (dt.d.B.arity i)) => w (ts q)) (hordP : ∀ (p q : dt.X.Map A), p ≤ q ↔ p ≤ q) (κ : MatAtom dt.X dt.d.B (dt.nOf vi)) (hk : dt.kindArgs κ * Fintype.card dt.X.Tag ≤ dt.ntgDim) (hnd : dt.kindDepth κ ≤ dt.eDim) (hrd : dt.kindReads κ ≤ dt.nfDim) (f : dt.CtlIx → A) : dt.ctlBit one (dt.kindExitCtl RF hord zero one vi av st v κ (dt.mkKindSem zero one vi st w hENC κ) hk hnd hrd f) (dt.avC av) ↔ MatAtom.holds σ w κ

One atom's own verdict bit is its truth: whatever the kind, the bit the exit control writes in the atom's slot is MatAtom.holds at the encoded valuation.

theorem DescriptiveComplexity.Draw.Data.ctlBit_avC_matFs_holds {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] (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] {zero one : A} {vi : dt.VarIx} {st : TapeStD dt A R P} {v : Univ A R P dt.KIx dt.dd → Prop} [LinearOrder (dt.X.Map A)] (hzo : zero ≠ one) (hlin : IsLinOrd WMLe) (σ : dt.d.B.Assignment (dt.X.Map A)) (w : Fin (dt.nOf vi) → dt.X.Map A) (hENC : ∀ (j : Fin (dt.nOf vi)), wmBlk (dt.lvSet st vi j) (Tag.arg (toLex (dt.lvBlk vi j))) = encMap dt.ly zero one (w j)) (hOld : ∀ (i : dt.d.B.ι) (ts : Fin (dt.d.B.arity i) → Fin (dt.nOf vi)), st.old i (dt.stageTgtD zero vi i ts st v (dt.d.B.arity i)) ↔ σ i fun (q : Fin (dt.d.B.arity i)) => w (ts q)) (hordP : ∀ (p q : dt.X.Map A), p ≤ q ↔ p ≤ q) (enterSt : Fin (dt.natOf vi) → (dt.CtlIx → A) → (dt.SlotIx → A) → dt.CtlIx → A) (hEnterAv : ∀ (b : Fin (dt.natOf vi)) (f : dt.CtlIx → A) (g : dt.SlotIx → A) (a' : Fin dt.natMax), enterSt b f g (dt.avC a') = f (dt.avC a')) (f₀ : dt.CtlIx → A) (a : Fin (dt.natOf vi)) : dt.ctlBit one (dt.matFs RF hord zero one vi st v enterSt (fun (b : Fin (dt.natOf vi)) => dt.mkKindSem zero one vi st w hENC (dt.kindOf vi b)) f₀ (dt.natOf vi)) (dt.avC (Fin.castLE ⋯ a)) ↔ MatAtom.holds σ w (dt.kindOf vi a)

The matrix's verdicts, at the points: after the whole matrix, atom a's slot holds MatAtom.holds of its kind at the encoded valuation – the hav input of DescriptiveComplexity.Draw.Data.postLeaf_iff_qfValue, verbatim.

noncomputable def DescriptiveComplexity.Draw.Data.matFsT {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)) (hord : ∀ (x y : Univ A R P dt.KIx dt.dd), WMLe x y ↔ tagTupleLe x y) [Nonempty A] [L.IsRelational] [L.Structure A] (zero one : A) (vi : dt.VarIx) (st : TapeStD dt A R P) (v : Univ A R P dt.KIx dt.dd → Prop) (enterSt : Fin (dt.natOf vi) → (dt.CtlIx → A) → (dt.SlotIx → A) → dt.CtlIx → A) (sem : (a : Fin (dt.natOf vi)) → dt.KindSem zero one vi (dt.matSt vi st v ↑a) (dt.kindOf vi a)) (f₀ : dt.CtlIx → A) : ℕ → dt.CtlIx → A

The control thread across the matrix's atoms, threaded: as DescriptiveComplexity.Draw.Data.matFs, with each atom's exit control computed at the state that atom actually runs at.

Equations

• One or more equations did not get rendered due to their size.
• dt.matFsT RF hord zero one vi st v enterSt sem f₀ 0 = f₀

theorem DescriptiveComplexity.Draw.Data.scratchEq_matSt {L : FirstOrder.Language} {dt : Data L} {A R P : Type} {vi : dt.VarIx} {st : TapeStD dt A R P} {v : Univ A R P dt.KIx dt.dd → Prop} (n : ℕ) : dt.ScratchEq (dt.matSt vi st v n) st

A threaded state of the matrix is the entry state up to the two scratch registers – matSt_eq in the form the congruences take.

theorem DescriptiveComplexity.Draw.Data.matFs_congr_scratch {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)) (hord : ∀ (x y : Univ A R P dt.KIx dt.dd), WMLe x y ↔ tagTupleLe x y) [Nonempty A] [L.IsRelational] [L.Structure A] {zero one : A} {vi : dt.VarIx} {st : TapeStD dt A R P} {v : Univ A R P dt.KIx dt.dd → Prop} {st' : TapeStD dt A R P} (h : dt.ScratchEq st st') (hreg : ¬∃ (u : Univ A R P dt.KIx dt.dd), v = RF.cell u) (enterSt : Fin (dt.natOf vi) → (dt.CtlIx → A) → (dt.SlotIx → A) → dt.CtlIx → A) (sem : (a : Fin (dt.natOf vi)) → dt.KindSem zero one vi st (dt.kindOf vi a)) (f₀ : dt.CtlIx → A) (n : ℕ) : dt.matFs RF hord zero one vi st v enterSt sem f₀ n = dt.matFs RF hord zero one vi st' v enterSt (fun (a : Fin (dt.natOf vi)) => dt.kindSemCast zero one vi ⋯ ⋯ (dt.kindOf vi a) (sem a)) f₀ n

The matrix is blind to the two scratch registers: atom by atom, kindExitCtl_congr_scratch.

theorem DescriptiveComplexity.Draw.Data.matFsT_eq_matFs {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)) (hord : ∀ (x y : Univ A R P dt.KIx dt.dd), WMLe x y ↔ tagTupleLe x y) [Nonempty A] [L.IsRelational] [L.Structure A] {zero one : A} {vi : dt.VarIx} {st : TapeStD dt A R P} {v : Univ A R P dt.KIx dt.dd → Prop} (hreg : ¬∃ (u : Univ A R P dt.KIx dt.dd), v = RF.cell u) (enterSt : Fin (dt.natOf vi) → (dt.CtlIx → A) → (dt.SlotIx → A) → dt.CtlIx → A) (semT : (a : Fin (dt.natOf vi)) → dt.KindSem zero one vi (dt.matSt vi st v ↑a) (dt.kindOf vi a)) (f₀ : dt.CtlIx → A) (n : ℕ) : dt.matFsT RF hord zero one vi st v enterSt semT f₀ n = dt.matFs RF hord zero one vi st v enterSt (fun (a : Fin (dt.natOf vi)) => dt.kindSemCast zero one vi ⋯ ⋯ (dt.kindOf vi a) (semT a)) f₀ n

The threaded matrix is the unthreaded one: an atom's machinery reads the levels' registers and its background at the working cell (kindExitCtl_congr_scratch), and the threading rewrites SAV and TARGET alone. This is the bridge between the control the run produces and the control the semantics is stated at.

theorem DescriptiveComplexity.Draw.Data.matrix_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} [Finite dt.KIx] (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) (hmirSt : 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) {emb : dt.MatrixPh vi → P} {exitPh : P} {rEmb : (i : dt.MatrixSite vi) → dt.MatrixSh vi i → R} (enterSt : Fin (dt.natOf vi) → (dt.CtlIx → A) → (dt.SlotIx → A) → dt.CtlIx → A) (hrules : ∀ (i : dt.MatrixSite vi) (ρ : dt.MatrixSh vi i), PR.rules (rEmb i ρ) = dt.matrixRule PR.zero PR.one vi emb (fun (a : Fin (dt.natOf vi)) => dt.atomArgs PR.zero PR.one vi a) enterSt exitPh i ρ) (semT : (a : Fin (dt.natOf vi)) → dt.KindSem PR.zero PR.one vi (dt.matSt vi st v ↑a) (dt.kindOf vi a)) (f₀ : dt.CtlIx → A) : Relation.ReflTransGen (wideData (Univ A R P dt.KIx dt.dd)).Step { state := Sum.inr (PR.stElt (emb (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 exitPh (dt.matFsT RF hord PR.zero PR.one vi st v enterSt semT f₀ (dt.natOf vi))), head := Sum.inl v', tape := wideTape (PR.trackTapeAt RF.cell Slot.val (dt.back RF.cell PR.zero PR.one ⋯ (dt.matSt vi st v (dt.natOf vi))) (dt.matSt vi st v (dt.natOf vi)).val) (PR.syElt PR.blank) }

The matrix's run, threaded: as DescriptiveComplexity.Draw.Data.matrix_run with no boundary discipline assumed – the tape ends in the threaded state DescriptiveComplexity.Draw.Data.matSt, which differs from the entry state in SAV and TARGET alone, and only if the matrix has a stage atom.

theorem DescriptiveComplexity.Draw.Data.matrix_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} [Finite dt.KIx] (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) (hmirSt : 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) {emb : dt.MatrixPh vi → P} {exitPh : P} {rEmb : (i : dt.MatrixSite vi) → dt.MatrixSh vi i → R} (enterSt : Fin (dt.natOf vi) → (dt.CtlIx → A) → (dt.SlotIx → A) → dt.CtlIx → A) (hrules : ∀ (i : dt.MatrixSite vi) (ρ : dt.MatrixSh vi i), PR.rules (rEmb i ρ) = dt.matrixRule PR.zero PR.one vi emb (fun (a : Fin (dt.natOf vi)) => dt.atomArgs PR.zero PR.one vi a) enterSt exitPh i ρ) (sem : (a : Fin (dt.natOf vi)) → dt.KindSem PR.zero PR.one vi st (dt.kindOf vi a)) (f₀ : dt.CtlIx → A) : Relation.ReflTransGen (wideData (Univ A R P dt.KIx dt.dd)).Step { state := Sum.inr (PR.stElt (emb (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 exitPh (dt.matFs RF hord PR.zero PR.one vi st v enterSt sem f₀ (dt.natOf 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 matrix's run: from the checkpoint before the first atom at the marker to the exit phase one cell to its right after the last, the verdict slots holding each atom's fold, the tape untouched.

The gates, assembled

noncomputable def DescriptiveComplexity.Draw.Data.gatesFs {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.IsRelational] [L.Structure A] (zero one : A) (vi : dt.VarIx) (st : TapeStD dt A R P) (v : Univ A R P dt.KIx dt.dd → Prop) (bOf : Fin (dt.arOf vi) → Fin dt.ko ⊕ Fin dt.ki) (hc : Fintype.card dt.X.Tag ≤ dt.ntgDim) (hnG : ∀ (t' : dt.X.Tag), (dt.domPk t').n ≤ dt.eDim) (hrdG : ∀ (t' : dt.X.Tag), dt.domNr t' ≤ dt.nfDim) (tOf : Fin (dt.arOf vi) → dt.X.Tag) (enterSt : Fin (dt.arOf vi) → (dt.CtlIx → A) → (dt.SlotIx → A) → dt.CtlIx → A) (f₀ : dt.CtlIx → A) : ℕ → dt.CtlIx → A

The control thread across the gates' blocks (the all-pass path): each block's machinery entered through the dispatch's enterSt, its conjoining exit the next block's input.

Equations

• One or more equations did not get rendered due to their size.
• dt.gatesFs RF zero one vi st v bOf hc hnG hrdG tOf enterSt f₀ 0 = f₀

theorem DescriptiveComplexity.Draw.Data.gates_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} [Finite dt.KIx] (bOf : Fin (dt.arOf vi) → Fin dt.ko ⊕ Fin dt.ki) (hc : Fintype.card dt.X.Tag ≤ dt.ntgDim) (hnG : ∀ (t' : dt.X.Tag), (dt.domPk t').n ≤ dt.eDim) (hrdG : ∀ (t' : dt.X.Tag), dt.domNr t' ≤ dt.nfDim) (wellGOf : Fin (dt.arOf vi) → (dt.SlotIx → A) → Prop) (setFail : (dt.CtlIx → A) → (dt.SlotIx → A) → dt.CtlIx → A) {emb : dt.GatesPh vi → P} {failPh exitPh : P} {rEmb : (i : dt.GatesSite vi) → dt.GatesSh vi i → R} (enterSt : Fin (dt.arOf vi) → (dt.CtlIx → A) → (dt.SlotIx → A) → dt.CtlIx → A) (hrules : ∀ (i : dt.GatesSite vi) (ρ : dt.GatesSh vi i), PR.rules (rEmb i ρ) = dt.gatesRule PR.one vi emb (fun (ℓ : Fin (dt.arOf vi)) => dt.gateArgs PR.zero PR.one (bOf ℓ) hc hnG hrdG) wellGOf setFail enterSt failPh 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), wellGOf ℓ (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 (bOf ℓ)))) = 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 (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 exitPh (dt.gatesFs RF PR.zero PR.one vi st v bOf hc hnG hrdG tOf enterSt 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' run at a gated address: every block passes its shape test, every domain evaluation runs on its block's decoded tag, and the sequence exits with the conjoined verdict in the flag.

theorem DescriptiveComplexity.Draw.Data.gates_run_fail {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} [Finite dt.KIx] (bOf : Fin (dt.arOf vi) → Fin dt.ko ⊕ Fin dt.ki) (hc : Fintype.card dt.X.Tag ≤ dt.ntgDim) (hnG : ∀ (t' : dt.X.Tag), (dt.domPk t').n ≤ dt.eDim) (hrdG : ∀ (t' : dt.X.Tag), dt.domNr t' ≤ dt.nfDim) (wellGOf : Fin (dt.arOf vi) → (dt.SlotIx → A) → Prop) (setFail : (dt.CtlIx → A) → (dt.SlotIx → A) → dt.CtlIx → A) {emb : dt.GatesPh vi → P} {failPh exitPh : P} {rEmb : (i : dt.GatesSite vi) → dt.GatesSh vi i → R} (enterSt : Fin (dt.arOf vi) → (dt.CtlIx → A) → (dt.SlotIx → A) → dt.CtlIx → A) (hrules : ∀ (i : dt.GatesSite vi) (ρ : dt.GatesSh vi i), PR.rules (rEmb i ρ) = dt.gatesRule PR.one vi emb (fun (ℓ : Fin (dt.arOf vi)) => dt.gateArgs PR.zero PR.one (bOf ℓ) hc hnG hrdG) wellGOf setFail enterSt failPh 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), wellGOf ℓ (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 (bOf ℓ)))) = 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 (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 failPh (setFail (enterSt ℓ₀ (dt.gatesFs RF PR.zero PR.one vi st v bOf hc hnG hrdG tOf enterSt f₀ ↑ℓ₀) (dt.back RF.cell PR.zero PR.one ⋯ st v)) (dt.back RF.cell PR.zero PR.one ⋯ st v))), 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' run at a junk address: the blocks below ℓ₀ pass, block ℓ₀'s shape test fails, and the run leaves the whole gate sequence through the failing exit with the fail store applied.

theorem DescriptiveComplexity.Draw.Data.ctlBit_gateFlagC_gatesFs {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} (bOf : Fin (dt.arOf vi) → Fin dt.ko ⊕ Fin dt.ki) (hc : Fintype.card dt.X.Tag ≤ dt.ntgDim) (hnG : ∀ (t' : dt.X.Tag), (dt.domPk t').n ≤ dt.eDim) (hrdG : ∀ (t' : dt.X.Tag), dt.domNr t' ≤ dt.nfDim) (enterSt : Fin (dt.arOf vi) → (dt.CtlIx → A) → (dt.SlotIx → A) → dt.CtlIx → A) (tOf : Fin (dt.arOf vi) → dt.X.Tag) (hzo : PR.zero ≠ PR.one) (hEnter : ∀ (ℓ : Fin (dt.arOf vi)) (f : dt.CtlIx → A) (g : dt.SlotIx → A), dt.ctlBit PR.one (enterSt ℓ f g) dt.gateFlagC ↔ dt.ctlBit PR.one f dt.gateFlagC) (f₀ : dt.CtlIx → A) (n : ℕ) : dt.ctlBit PR.one (dt.gatesFs RF PR.zero PR.one vi st v bOf hc hnG hrdG tOf enterSt f₀ n) dt.gateFlagC ↔ dt.ctlBit PR.one f₀ dt.gateFlagC ∧ ∀ (ℓ : Fin (dt.arOf vi)), ↑ℓ < n → (∀ (t' : dt.X.Tag), wmBlk st.mir (Tag.arg (toLex (bOf ℓ))) (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 (bOf ℓ)))))

The gates' verdict, characterized: after the first n blocks of the all-pass path, the flag holds exactly when it held at entry and every gated block's decoded assignment satisfies its tag's domain sentence.