The matrix's sequencer at an arbitrary file

DescriptiveComplexity.Problems.Wide.DrawInstSeq read at a coarse file: the uniform stage discharge (ixKind_hStage), the control the sequencer folds (ixKindExitCtl, ixMatFs), the matrix's run and the gates' run, all at the registers of an arbitrary file rather than the elements of the universe.

The runs here are Relation.ReflTransGen: the atoms below them carry their budgets, and the counting of the layers above the matrix is one pass, to be made once the conversion reaches the evaluation.

noncomputable def DescriptiveComplexity.Draw.Data.IxKindSem {L : FirstOrder.Language} (dt : Data L) {A R P : Type} [LinearOrder A] {I : Type} [L.Structure A] (zero one : A) (vi : dt.VarIx) (st : TapeSt dt A R P I) (elt : I → Univ A R P dt.KIx dt.dd) : 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.IxKindSem zero one vi st elt (DescriptiveComplexity.Draw.MatAtom.eq a a_1) = PUnit.{1}
• dt.IxKindSem zero one vi st elt (DescriptiveComplexity.Draw.MatAtom.ord a a_1) = PUnit.{1}
• dt.IxKindSem zero one vi st elt (DescriptiveComplexity.Draw.MatAtom.stage i a) = PUnit.{1}

noncomputable def DescriptiveComplexity.Draw.Data.ixKindSemCast {L : FirstOrder.Language} (dt : Data L) {A R P : Type} [LinearOrder A] {I : Type} {elt : I → Univ A R P dt.KIx dt.dd} [L.Structure A] (zero one : A) (vi : dt.VarIx) {st st' : TapeSt dt A R P I} (hmir : st.mir = st'.mir) (hval : st.val = st'.val) (κ : MatAtom dt.X dt.d.B (dt.nOf vi)) (s : dt.IxKindSem zero one vi st elt κ) : dt.IxKindSem zero one vi st' elt κ

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.ixKindSemCast zero one vi hmir hval (DescriptiveComplexity.Draw.MatAtom.eq a a_1) s_2 = s_2
• dt.ixKindSemCast zero one vi hmir hval (DescriptiveComplexity.Draw.MatAtom.ord a a_1) s_2 = s_2
• dt.ixKindSemCast zero one vi hmir hval (DescriptiveComplexity.Draw.MatAtom.stage i a) s_2 = s_2
• dt.ixKindSemCast zero one vi hmir hval (DescriptiveComplexity.Draw.MatAtom.exp a ts) s_2 = ⟨↑s_2, ⋯⟩

theorem DescriptiveComplexity.Draw.Data.ixKindSemCast_triple {L : FirstOrder.Language} (dt : Data L) {A R P : Type} [LinearOrder A] {I : Type} {elt : I → Univ A R P dt.KIx dt.dd} [L.Structure A] (zero one : A) (vi : dt.VarIx) {st₁ st₂ st₃ : TapeSt dt A R P I} (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.IxKindSem zero one vi st₁ elt κ) : dt.ixKindSemCast zero one vi h5 h6 κ (dt.ixKindSemCast zero one vi h3 h4 κ (dt.ixKindSemCast 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.ixKindExitCtl {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] {I : Type} (F : LaidFile dt A R P I) {elt : I → Univ A R P dt.KIx dt.dd} [Nonempty A] [L.IsRelational] [L.Structure A] (zero one : A) (hhas : F.toLayout.HasName zero) (vi : dt.VarIx) (av : Fin dt.natMax) (st : TapeSt dt A R P I) (v : Univ A R P dt.KIx dt.dd → Prop) (κ : MatAtom dt.X dt.d.B (dt.nOf vi)) : dt.IxKindSem zero one vi st elt κ → 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.ixKindExitCtl_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] {I : Type} (F : LaidFile dt A R P I) {elt : I → Univ A R P dt.KIx dt.dd} [Nonempty A] [L.IsRelational] [L.Structure A] {zero one : A} (hhas : F.toLayout.HasName zero) {vi : dt.VarIx} {av : Fin dt.natMax} {st : TapeSt dt A R P I} {v : Univ A R P dt.KIx dt.dd → Prop} {st' : TapeSt dt A R P I} (h : dt.ScratchEq st st') (hreg : ¬∃ (u : I), v = F.cell u) (κ : MatAtom dt.X dt.d.B (dt.nOf vi)) (sem : dt.IxKindSem zero one vi st elt κ) (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.ixKindExitCtl F zero one hhas vi av st v κ sem hk hn hrd f = dt.ixKindExitCtl F zero one hhas vi av st' v κ (dt.ixKindSemCast 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.ixKindEndSt {L : FirstOrder.Language} (dt : Data L) {A R P I : Type} {elt : I → Univ A R P dt.KIx dt.dd} (vi : dt.VarIx) (v : Univ A R P dt.KIx dt.dd → Prop) (κ : MatAtom dt.X dt.d.B (dt.nOf vi)) (st : TapeSt dt A R P I) : TapeSt dt A R P I

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.ixKindEndSt vi v (DescriptiveComplexity.Draw.MatAtom.stage i a) st = dt.ixStageEndSt st elt v
• dt.ixKindEndSt vi v κ st = st

noncomputable def DescriptiveComplexity.Draw.Data.ixKindCost {L : FirstOrder.Language} (dt : Data L) (A : Type) (vi : dt.VarIx) (w wP wR wK : ℕ) : MatAtom dt.X dt.d.B (dt.nOf vi) → ℕ

What one atom's machinery is charged, by kind. A comparison walks its two coordinate loops once per tuple, an expansion its tag flags and then its leaf reads once per point of the evaluation order, both at the width w a walk to a named register costs; a stage atom pays its nine trips and thirteen dispatches over one copy loop per argument, at the widths the caller supplies. The bound is uniform in the atom's data – the expansion's are bounded by ntgDim and nfDim – which is what makes the sequencer's fold a single width.

Equations

• dt.ixKindCost A vi w wP wR wK (DescriptiveComplexity.Draw.MatAtom.eq a a_1) = 1 + ((2 + (w + 2) * 2) * (Nat.card (Lex (Fin dt.dd0 → A)) + 1) + 1)
• dt.ixKindCost A vi w wP wR wK (DescriptiveComplexity.Draw.MatAtom.ord a a_1) = 1 + ((2 + (w + 2) * 2) * (Nat.card (Lex (Fin dt.dd0 → A)) + 1) + 1)
• dt.ixKindCost A vi w wP wR wK (DescriptiveComplexity.Draw.MatAtom.exp a a_1) = 1 + ((w + 2) * dt.ntgDim + 2 + ((2 + (w + 2) * dt.nfDim) * (Nat.card (Lex (Fin dt.eDim → A)) + 1) + 1))
• dt.ixKindCost A vi w wP wR wK (DescriptiveComplexity.Draw.MatAtom.stage iv a) = 5 * wP + 2 * wR + 2 * wK + ((2 * w + 8) * (Nat.card (Lex (Fin dt.dd0 → A)) + 1) + 1 + 1) * dt.d.B.arity iv + 13

theorem DescriptiveComplexity.Draw.Data.ixKind_hStage_thread_reachesIn {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} {I : Type} [Finite I] (F : LaidFile dt A R P I) {elt : I → Univ A R P dt.KIx dt.dd} (hinj : Function.Injective elt) (hhasP : F.toLayout.HasName PR.zero) (heltP : ∀ (b : Fin dt.ko ⊕ Fin dt.ki) (c : Fin dt.dd0 → A), elt (F.toLayout.reg hhasP b c) = dt.blkElt b (pad PR.zero c)) (hsepP : F.toLayout.NameSep PR.zero ⋯) (hix : IsLinOrd F.le) {e₀ : Univ A R P dt.KIx dt.dd} (he₀ : ∀ (y : Univ A R P dt.KIx dt.dd), WMLe e₀ y) (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 : TapeSt dt A R P I} {v : Univ A R P dt.KIx dt.dd → Prop} [Finite dt.KIx] (hR : PR.table.Reads) (hlin : IsLinOrd WMLe) {gtop gbot : I} (htop : ∀ (y : I), F.le y gtop) (hbot : ∀ (y : I), F.le gbot y) (hwork : ∀ {r : Univ A R P dt.KIx dt.dd → Prop}, (∀ (x : Univ A R P dt.KIx dt.dd), r x → ∃ (i : dt.KIx), x.1 = Tag.arg i) → ∀ (u : I), WMSetLt WMLe r (F.cell u)) {v' : Univ A R P dt.KIx dt.dd → Prop} (hv : WMSetLt WMLe v (F.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 = ixMark elt 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) {Use : I → Prop} (hmono : ∀ (u u' : I), WMLt F.le u u' ↔ WMLt WMLe (elt u) (elt u')) (hup : ∀ (u : I) (x : Univ A R P dt.KIx dt.dd), Use u → WMLt WMLe (elt u) x → ∃ (u' : I), Use u' ∧ elt u' = x) (hvh : IxHolds elt Use v) (hxdUse : ∀ {iv : dt.d.B.ι} (ℓ : Fin (dt.d.B.arity iv)) (b : Lex (Fin dt.dd0 → A)), Use (dt.ixStageXD F hhasP ℓ b)) (w wG wP wR wK : ℕ) (hgap : ∀ (u u' : I), IxSucc F.le u u' → wideRank (F.cell u') - wideRank (F.cell u) ≤ wG) (hwP : wideRank (F.cell gtop) + 2 + ((ixRank F.le gtop - ixRank F.le gbot) * wG + 1) + wideRank (F.cell gbot) ≤ wP) (hwR : ∀ (s : Univ A R P dt.KIx dt.dd → Prop), WMSetLt WMLe s (F.cell gbot) → wideRank s + 4 ≤ wR) (hwK : ∀ (T : Univ A R P dt.KIx dt.dd → Prop), WMSetLt WMLe T (F.cell gbot) → wideRank T * (1 + (wideRank (F.cell gtop) + 3 + (ixRank F.le gtop - ixRank F.le gbot) * wG + wideRank (F.cell gbot)) + (wideRank (F.cell gtop) + ((ixRank F.le gtop - ixRank F.le gbot) * wG + 1) + wideRank (F.cell gbot) + 4)) + 1 + (wideRank (F.cell gtop) + 3 + (ixRank F.le gtop - ixRank F.le gbot) * wG + wideRank (F.cell gbot)) ≤ wK) (hcostR : ∀ (b : Fin dt.ko ⊕ Fin dt.ki) (c : Fin dt.dd0 → A), 2 * (wideRank (F.cell (F.toLayout.reg hhasP b c)) - wideRank v) + 2 ≤ w) (κ : 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.IxKindSem PR.zero PR.one vi st elt κ) {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) : (wideData (Univ A R P dt.KIx dt.dd)).ReachesIn (dt.ixKindCost A vi w wP wR wK κ) { state := Sum.inr (PR.stElt (emb (dt.kindEntry κ)) f), head := Sum.inl v', tape := wideTape (PR.trackTapeAt F.cell Slot.val (dt.ixBack F.toLayout PR.zero PR.one ⋯ st) st.val) (PR.syElt PR.blank) } { state := Sum.inr (PR.stElt exitPh (dt.ixKindExitCtl F PR.zero PR.one hhasP vi av st v κ sem hk hnd hrd f)), head := Sum.inl v', tape := wideTape (PR.trackTapeAt F.cell Slot.val (dt.ixBack F.toLayout PR.zero PR.one ⋯ (dt.ixKindEndSt vi v κ st)) (dt.ixKindEndSt vi v κ st).val) (PR.syElt PR.blank) }

The uniform stage discharge, threaded, on a clock: as DescriptiveComplexity.Draw.Data.ixKind_hStage_thread with the atom's cost counted – DescriptiveComplexity.Draw.Data.ixKindCost, whatever the kind.

theorem DescriptiveComplexity.Draw.Data.ixKind_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} {I : Type} [Finite I] (F : LaidFile dt A R P I) {elt : I → Univ A R P dt.KIx dt.dd} (hinj : Function.Injective elt) (hhasP : F.toLayout.HasName PR.zero) (heltP : ∀ (b : Fin dt.ko ⊕ Fin dt.ki) (c : Fin dt.dd0 → A), elt (F.toLayout.reg hhasP b c) = dt.blkElt b (pad PR.zero c)) (hsepP : F.toLayout.NameSep PR.zero ⋯) (hix : IsLinOrd F.le) {e₀ : Univ A R P dt.KIx dt.dd} (he₀ : ∀ (y : Univ A R P dt.KIx dt.dd), WMLe e₀ y) (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 : TapeSt dt A R P I} {v : Univ A R P dt.KIx dt.dd → Prop} [Finite dt.KIx] (hR : PR.table.Reads) (hlin : IsLinOrd WMLe) {gtop gbot : I} (htop : ∀ (y : I), F.le y gtop) (hbot : ∀ (y : I), F.le gbot y) (hwork : ∀ {r : Univ A R P dt.KIx dt.dd → Prop}, (∀ (x : Univ A R P dt.KIx dt.dd), r x → ∃ (i : dt.KIx), x.1 = Tag.arg i) → ∀ (u : I), WMSetLt WMLe r (F.cell u)) {v' : Univ A R P dt.KIx dt.dd → Prop} (hv : WMSetLt WMLe v (F.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 = ixMark elt 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) {Use : I → Prop} (hmono : ∀ (u u' : I), WMLt F.le u u' ↔ WMLt WMLe (elt u) (elt u')) (hup : ∀ (u : I) (x : Univ A R P dt.KIx dt.dd), Use u → WMLt WMLe (elt u) x → ∃ (u' : I), Use u' ∧ elt u' = x) (hvh : IxHolds elt Use v) (hxdUse : ∀ {iv : dt.d.B.ι} (ℓ : Fin (dt.d.B.arity iv)) (b : Lex (Fin dt.dd0 → A)), Use (dt.ixStageXD F hhasP ℓ b)) (w wG wP wR wK : ℕ) (hgap : ∀ (u u' : I), IxSucc F.le u u' → wideRank (F.cell u') - wideRank (F.cell u) ≤ wG) (hwP : wideRank (F.cell gtop) + 2 + ((ixRank F.le gtop - ixRank F.le gbot) * wG + 1) + wideRank (F.cell gbot) ≤ wP) (hwR : ∀ (s : Univ A R P dt.KIx dt.dd → Prop), WMSetLt WMLe s (F.cell gbot) → wideRank s + 4 ≤ wR) (hwK : ∀ (T : Univ A R P dt.KIx dt.dd → Prop), WMSetLt WMLe T (F.cell gbot) → wideRank T * (1 + (wideRank (F.cell gtop) + 3 + (ixRank F.le gtop - ixRank F.le gbot) * wG + wideRank (F.cell gbot)) + (wideRank (F.cell gtop) + ((ixRank F.le gtop - ixRank F.le gbot) * wG + 1) + wideRank (F.cell gbot) + 4)) + 1 + (wideRank (F.cell gtop) + 3 + (ixRank F.le gtop - ixRank F.le gbot) * wG + wideRank (F.cell gbot)) ≤ wK) (hcostR : ∀ (b : Fin dt.ko ⊕ Fin dt.ki) (c : Fin dt.dd0 → A), 2 * (wideRank (F.cell (F.toLayout.reg hhasP b c)) - wideRank v) + 2 ≤ w) (κ : 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.IxKindSem PR.zero PR.one vi st elt κ) {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 F.cell Slot.val (dt.ixBack F.toLayout PR.zero PR.one ⋯ st) st.val) (PR.syElt PR.blank) } { state := Sum.inr (PR.stElt exitPh (dt.ixKindExitCtl F PR.zero PR.one hhasP vi av st v κ sem hk hnd hrd f)), head := Sum.inl v', tape := wideTape (PR.trackTapeAt F.cell Slot.val (dt.ixBack F.toLayout PR.zero PR.one ⋯ (dt.ixKindEndSt vi v κ st)) (dt.ixKindEndSt 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.ixKind_hStage_reachesIn {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} {I : Type} [Finite I] (F : LaidFile dt A R P I) {elt : I → Univ A R P dt.KIx dt.dd} (hinj : Function.Injective elt) (hhasP : F.toLayout.HasName PR.zero) (heltP : ∀ (b : Fin dt.ko ⊕ Fin dt.ki) (c : Fin dt.dd0 → A), elt (F.toLayout.reg hhasP b c) = dt.blkElt b (pad PR.zero c)) (hsepP : F.toLayout.NameSep PR.zero ⋯) (hix : IsLinOrd F.le) {e₀ : Univ A R P dt.KIx dt.dd} (he₀ : ∀ (y : Univ A R P dt.KIx dt.dd), WMLe e₀ y) (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 : TapeSt dt A R P I} {v : Univ A R P dt.KIx dt.dd → Prop} [Finite dt.KIx] (hR : PR.table.Reads) (hlin : IsLinOrd WMLe) {gtop gbot : I} (htop : ∀ (y : I), F.le y gtop) (hbot : ∀ (y : I), F.le gbot y) (hwork : ∀ {r : Univ A R P dt.KIx dt.dd → Prop}, (∀ (x : Univ A R P dt.KIx dt.dd), r x → ∃ (i : dt.KIx), x.1 = Tag.arg i) → ∀ (u : I), WMSetLt WMLe r (F.cell u)) {v' : Univ A R P dt.KIx dt.dd → Prop} (hv : WMSetLt WMLe v (F.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 = ixMark elt 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 = ixMark elt v) (htgt : st.tgt = ixMark elt v) {Use : I → Prop} (hmono : ∀ (u u' : I), WMLt F.le u u' ↔ WMLt WMLe (elt u) (elt u')) (hup : ∀ (u : I) (x : Univ A R P dt.KIx dt.dd), Use u → WMLt WMLe (elt u) x → ∃ (u' : I), Use u' ∧ elt u' = x) (hvh : IxHolds elt Use v) (hxdUse : ∀ {iv : dt.d.B.ι} (ℓ : Fin (dt.d.B.arity iv)) (b : Lex (Fin dt.dd0 → A)), Use (dt.ixStageXD F hhasP ℓ b)) (w wG wP wR wK : ℕ) (hgap : ∀ (u u' : I), IxSucc F.le u u' → wideRank (F.cell u') - wideRank (F.cell u) ≤ wG) (hwP : wideRank (F.cell gtop) + 2 + ((ixRank F.le gtop - ixRank F.le gbot) * wG + 1) + wideRank (F.cell gbot) ≤ wP) (hwR : ∀ (s : Univ A R P dt.KIx dt.dd → Prop), WMSetLt WMLe s (F.cell gbot) → wideRank s + 4 ≤ wR) (hwK : ∀ (T : Univ A R P dt.KIx dt.dd → Prop), WMSetLt WMLe T (F.cell gbot) → wideRank T * (1 + (wideRank (F.cell gtop) + 3 + (ixRank F.le gtop - ixRank F.le gbot) * wG + wideRank (F.cell gbot)) + (wideRank (F.cell gtop) + ((ixRank F.le gtop - ixRank F.le gbot) * wG + 1) + wideRank (F.cell gbot) + 4)) + 1 + (wideRank (F.cell gtop) + 3 + (ixRank F.le gtop - ixRank F.le gbot) * wG + wideRank (F.cell gbot)) ≤ wK) (hcostR : ∀ (b : Fin dt.ko ⊕ Fin dt.ki) (c : Fin dt.dd0 → A), 2 * (wideRank (F.cell (F.toLayout.reg hhasP b c)) - wideRank v) + 2 ≤ w) (κ : 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.IxKindSem PR.zero PR.one vi st elt κ) {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) : (wideData (Univ A R P dt.KIx dt.dd)).ReachesIn (dt.ixKindCost A vi w wP wR wK κ) { state := Sum.inr (PR.stElt (emb (dt.kindEntry κ)) f), head := Sum.inl v', tape := wideTape (PR.trackTapeAt F.cell Slot.val (dt.ixBack F.toLayout PR.zero PR.one ⋯ st) st.val) (PR.syElt PR.blank) } { state := Sum.inr (PR.stElt exitPh (dt.ixKindExitCtl F PR.zero PR.one hhasP vi av st v κ sem hk hnd hrd f)), head := Sum.inl v', tape := wideTape (PR.trackTapeAt F.cell Slot.val (dt.ixBack F.toLayout PR.zero PR.one ⋯ st) st.val) (PR.syElt PR.blank) }

The uniform stage discharge, on a clock: as DescriptiveComplexity.Draw.Data.ixKind_hStage with the atom's cost counted – DescriptiveComplexity.Draw.Data.ixKindCost, whatever the kind.

theorem DescriptiveComplexity.Draw.Data.ixKind_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} {I : Type} [Finite I] (F : LaidFile dt A R P I) {elt : I → Univ A R P dt.KIx dt.dd} (hinj : Function.Injective elt) (hhasP : F.toLayout.HasName PR.zero) (heltP : ∀ (b : Fin dt.ko ⊕ Fin dt.ki) (c : Fin dt.dd0 → A), elt (F.toLayout.reg hhasP b c) = dt.blkElt b (pad PR.zero c)) (hsepP : F.toLayout.NameSep PR.zero ⋯) (hix : IsLinOrd F.le) {e₀ : Univ A R P dt.KIx dt.dd} (he₀ : ∀ (y : Univ A R P dt.KIx dt.dd), WMLe e₀ y) (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 : TapeSt dt A R P I} {v : Univ A R P dt.KIx dt.dd → Prop} [Finite dt.KIx] (hR : PR.table.Reads) (hlin : IsLinOrd WMLe) {gtop gbot : I} (htop : ∀ (y : I), F.le y gtop) (hbot : ∀ (y : I), F.le gbot y) (hwork : ∀ {r : Univ A R P dt.KIx dt.dd → Prop}, (∀ (x : Univ A R P dt.KIx dt.dd), r x → ∃ (i : dt.KIx), x.1 = Tag.arg i) → ∀ (u : I), WMSetLt WMLe r (F.cell u)) {v' : Univ A R P dt.KIx dt.dd → Prop} (hv : WMSetLt WMLe v (F.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 = ixMark elt 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 = ixMark elt v) (htgt : st.tgt = ixMark elt v) {Use : I → Prop} (hmono : ∀ (u u' : I), WMLt F.le u u' ↔ WMLt WMLe (elt u) (elt u')) (hup : ∀ (u : I) (x : Univ A R P dt.KIx dt.dd), Use u → WMLt WMLe (elt u) x → ∃ (u' : I), Use u' ∧ elt u' = x) (hvh : IxHolds elt Use v) (hxdUse : ∀ {iv : dt.d.B.ι} (ℓ : Fin (dt.d.B.arity iv)) (b : Lex (Fin dt.dd0 → A)), Use (dt.ixStageXD F hhasP ℓ b)) (w wG wP wR wK : ℕ) (hgap : ∀ (u u' : I), IxSucc F.le u u' → wideRank (F.cell u') - wideRank (F.cell u) ≤ wG) (hwP : wideRank (F.cell gtop) + 2 + ((ixRank F.le gtop - ixRank F.le gbot) * wG + 1) + wideRank (F.cell gbot) ≤ wP) (hwR : ∀ (s : Univ A R P dt.KIx dt.dd → Prop), WMSetLt WMLe s (F.cell gbot) → wideRank s + 4 ≤ wR) (hwK : ∀ (T : Univ A R P dt.KIx dt.dd → Prop), WMSetLt WMLe T (F.cell gbot) → wideRank T * (1 + (wideRank (F.cell gtop) + 3 + (ixRank F.le gtop - ixRank F.le gbot) * wG + wideRank (F.cell gbot)) + (wideRank (F.cell gtop) + ((ixRank F.le gtop - ixRank F.le gbot) * wG + 1) + wideRank (F.cell gbot) + 4)) + 1 + (wideRank (F.cell gtop) + 3 + (ixRank F.le gtop - ixRank F.le gbot) * wG + wideRank (F.cell gbot)) ≤ wK) (hcostR : ∀ (b : Fin dt.ko ⊕ Fin dt.ki) (c : Fin dt.dd0 → A), 2 * (wideRank (F.cell (F.toLayout.reg hhasP b c)) - wideRank v) + 2 ≤ w) (κ : 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.IxKindSem PR.zero PR.one vi st elt κ) {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 F.cell Slot.val (dt.ixBack F.toLayout PR.zero PR.one ⋯ st) st.val) (PR.syElt PR.blank) } { state := Sum.inr (PR.stElt exitPh (dt.ixKindExitCtl F PR.zero PR.one hhasP vi av st v κ sem hk hnd hrd f)), head := Sum.inl v', tape := wideTape (PR.trackTapeAt F.cell Slot.val (dt.ixBack F.toLayout 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.ixMatCost {L : FirstOrder.Language} (dt : Data L) (A : Type) (vi : dt.VarIx) (w wP wR wK : ℕ) : ℕ

What the matrix charges one atom: the largest of its atoms' costs. A clocked caller that has no reason to prefer a coarser width takes this one, and the fold's (w + 2) * natOf vi + 1 is then a closed expression in the file's widths.

Equations

• dt.ixMatCost A vi w wP wR wK = Finset.univ.sup fun (a : Fin (dt.natOf vi)) => dt.ixKindCost A vi w wP wR wK (dt.kindOf vi a)

noncomputable def DescriptiveComplexity.Draw.Data.ixMatFs {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] {I : Type} (F : LaidFile dt A R P I) {elt : I → Univ A R P dt.KIx dt.dd} [Nonempty A] [L.IsRelational] [L.Structure A] (zero one : A) (hhas : F.toLayout.HasName zero) (vi : dt.VarIx) (st : TapeSt dt A R P I) (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.IxKindSem zero one vi st elt (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.ixMatFs F zero one hhas vi st v enterSt sem f₀ 0 = f₀

The threaded states of the matrix

theorem DescriptiveComplexity.Draw.Data.ixKindEndSt_fields {L : FirstOrder.Language} {dt : Data L} {A R P I : Type} {elt : I → Univ A R P dt.KIx dt.dd} {vi : dt.VarIx} {v : Univ A R P dt.KIx dt.dd → Prop} (κ : MatAtom dt.X dt.d.B (dt.nOf vi)) (st : TapeSt dt A R P I) : (dt.ixKindEndSt vi v κ st).wk = st.wk ∧ (dt.ixKindEndSt vi v κ st).mir = st.mir ∧ (dt.ixKindEndSt vi v κ st).bot = st.bot ∧ (dt.ixKindEndSt vi v κ st).val = st.val ∧ (dt.ixKindEndSt 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.ixMatSt {L : FirstOrder.Language} (dt : Data L) {A R P I : Type} {elt : I → Univ A R P dt.KIx dt.dd} (vi : dt.VarIx) (st : TapeSt dt A R P I) (v : Univ A R P dt.KIx dt.dd → Prop) : ℕ → TapeSt dt A R P I

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

Equations

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

theorem DescriptiveComplexity.Draw.Data.ixMatSt_fields {L : FirstOrder.Language} {dt : Data L} {A R P I : Type} {elt : I → Univ A R P dt.KIx dt.dd} {vi : dt.VarIx} {st : TapeSt dt A R P I} {v : Univ A R P dt.KIx dt.dd → Prop} (n : ℕ) : (dt.ixMatSt vi st v n).wk = st.wk ∧ (dt.ixMatSt vi st v n).mir = st.mir ∧ (dt.ixMatSt vi st v n).bot = st.bot ∧ (dt.ixMatSt vi st v n).val = st.val ∧ (dt.ixMatSt 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.ixTapeSt_eq_savTgt {L : FirstOrder.Language} {dt : Data L} {A R P I : Type} {X Y : TapeSt dt A R P I} (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.ixKindEndSt_fields' {L : FirstOrder.Language} {dt : Data L} {A R P I : Type} {elt : I → Univ A R P dt.KIx dt.dd} {vi : dt.VarIx} {v : Univ A R P dt.KIx dt.dd → Prop} (κ : MatAtom dt.X dt.d.B (dt.nOf vi)) (st : TapeSt dt A R P I) : (dt.ixKindEndSt vi v κ st).new = st.new ∧ (dt.ixKindEndSt 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.ixMatSt_fields' {L : FirstOrder.Language} {dt : Data L} {A R P I : Type} {elt : I → Univ A R P dt.KIx dt.dd} {vi : dt.VarIx} {st : TapeSt dt A R P I} {v : Univ A R P dt.KIx dt.dd → Prop} (n : ℕ) : (dt.ixMatSt vi st v n).new = st.new ∧ (dt.ixMatSt vi st v n).ltp = st.ltp

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

theorem DescriptiveComplexity.Draw.Data.ixMatSt_eq {L : FirstOrder.Language} {dt : Data L} {A R P I : Type} {elt : I → Univ A R P dt.KIx dt.dd} {vi : dt.VarIx} {st : TapeSt dt A R P I} {v : Univ A R P dt.KIx dt.dd → Prop} (n : ℕ) : dt.ixMatSt vi st v n = { mir := st.mir, tgt := (dt.ixMatSt vi st v n).tgt, sav := (dt.ixMatSt 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.ixKindExitCtl_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] {I : Type} (F : LaidFile dt A R P I) {elt : I → Univ A R P dt.KIx dt.dd} [Nonempty A] [L.IsRelational] [L.Structure A] {zero one : A} (hhas : F.toLayout.HasName zero) {vi : dt.VarIx} {av : Fin dt.natMax} {st : TapeSt dt A R P I} {v : Univ A R P dt.KIx dt.dd → Prop} (κ : MatAtom dt.X dt.d.B (dt.nOf vi)) (sem : dt.IxKindSem zero one vi st elt κ) (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.ixKindExitCtl F zero one hhas 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.ixKindExitCtl_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] {I : Type} (F : LaidFile dt A R P I) {elt : I → Univ A R P dt.KIx dt.dd} [Nonempty A] [L.IsRelational] [L.Structure A] {zero one : A} (hhas : F.toLayout.HasName zero) {vi : dt.VarIx} {av : Fin dt.natMax} {st : TapeSt dt A R P I} {v : Univ A R P dt.KIx dt.dd → Prop} (κ : MatAtom dt.X dt.d.B (dt.nOf vi)) (sem : dt.IxKindSem zero one vi st elt κ) (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.ixKindExitCtl F zero one hhas 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.ixMatFs_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] {I : Type} (F : LaidFile dt A R P I) {elt : I → Univ A R P dt.KIx dt.dd} [Nonempty A] [L.IsRelational] [L.Structure A] {zero one : A} (hhas : F.toLayout.HasName zero) {vi : dt.VarIx} {st : TapeSt dt A R P I} {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.IxKindSem zero one vi st elt (dt.kindOf vi b)) (f₀ : dt.CtlIx → A) (jj : Fin dt.naDim) (n : ℕ) : dt.ixMatFs F zero one hhas 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.ixMatFs_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] {I : Type} (F : LaidFile dt A R P I) {elt : I → Univ A R P dt.KIx dt.dd} [Nonempty A] [L.IsRelational] [L.Structure A] {zero one : A} (hhas : F.toLayout.HasName zero) {vi : dt.VarIx} {st : TapeSt dt A R P I} {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.IxKindSem zero one vi st elt (dt.kindOf vi b)) (f₀ : dt.CtlIx → A) (a : Fin (dt.natOf vi)) : dt.ixMatFs F zero one hhas vi st v enterSt sem f₀ (dt.natOf vi) (dt.avC (Fin.castLE ⋯ a)) = dt.ixKindExitCtl F zero one hhas vi (Fin.castLE ⋯ a) st v (dt.kindOf vi a) (sem a) ⋯ ⋯ ⋯ (enterSt a (dt.ixMatFs F zero one hhas vi st v enterSt sem f₀ ↑a) (dt.ixBack F.toLayout 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.ixMkKindSem {L : FirstOrder.Language} (dt : Data L) {A R P : Type} [LinearOrder A] {I : Type} [L.Structure A] (zero one : A) (vi : dt.VarIx) (st : TapeSt dt A R P I) {elt : I → Univ A R P dt.KIx dt.dd} (w : Fin (dt.nOf vi) → dt.X.Map A) (hENC : ∀ (j : Fin (dt.nOf vi)), wmBlk (ixAddr elt (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.IxKindSem zero one vi st elt κ

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

Equations

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

theorem DescriptiveComplexity.Draw.Data.ixKindSemCast_ixMkKindSem {L : FirstOrder.Language} {dt : Data L} {A R P : Type} [LinearOrder A] {I : Type} {elt : I → Univ A R P dt.KIx dt.dd} [L.Structure A] (zero one : A) (vi : dt.VarIx) {st st' : TapeSt dt A R P I} (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 (ixAddr elt (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 (ixAddr elt (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.ixKindSemCast zero one vi hmir hval κ (dt.ixMkKindSem zero one vi st w hENC κ) = dt.ixMkKindSem 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.ixCmpAgr_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)] {I : Type} (F : LaidFile dt A R P I) {elt : I → Univ A R P dt.KIx dt.dd} (hinj : Function.Injective elt) [L.Structure A] {zero one : A} (hhas : F.toLayout.HasName zero) (helt : ∀ (b : Fin dt.ko ⊕ Fin dt.ki) (c : Fin dt.dd0 → A), elt (F.toLayout.reg hhas b c) = dt.blkElt b (pad zero c)) {vi : dt.VarIx} {st : TapeSt dt A R P I} {j₁ j₂ : Fin (dt.nOf vi)} {p q : dt.X.Map A} (h1 : wmBlk (ixAddr elt (dt.lvSet st vi j₁)) (Tag.arg (toLex (dt.lvBlk vi j₁))) = encMap dt.ly zero one p) (h2 : wmBlk (ixAddr elt (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 F zero hhas 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.ixCmpAgr_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)] {I : Type} (F : LaidFile dt A R P I) {elt : I → Univ A R P dt.KIx dt.dd} (hinj : Function.Injective elt) [L.Structure A] {zero one : A} (hhas : F.toLayout.HasName zero) (helt : ∀ (b : Fin dt.ko ⊕ Fin dt.ki) (c : Fin dt.dd0 → A), elt (F.toLayout.reg hhas b c) = dt.blkElt b (pad zero c)) {vi : dt.VarIx} {st : TapeSt dt A R P I} (hzo : zero ≠ one) {j₁ j₂ : Fin (dt.nOf vi)} {p q : dt.X.Map A} (h1 : wmBlk (ixAddr elt (dt.lvSet st vi j₁)) (Tag.arg (toLex (dt.lvBlk vi j₁))) = encMap dt.ly zero one p) (h2 : wmBlk (ixAddr elt (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 F zero hhas 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.ixCmp_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] {I : Type} (F : LaidFile dt A R P I) {elt : I → Univ A R P dt.KIx dt.dd} (hinj : Function.Injective elt) [L.Structure A] {zero one : A} (hhas : F.toLayout.HasName zero) (helt : ∀ (b : Fin dt.ko ⊕ Fin dt.ki) (c : Fin dt.dd0 → A), elt (F.toLayout.reg hhas b c) = dt.blkElt b (pad zero c)) {vi : dt.VarIx} {st : TapeSt dt A R P I} (hzo : zero ≠ one) {j₁ j₂ : Fin (dt.nOf vi)} {p q : dt.X.Map A} (h1 : wmBlk (ixAddr elt (dt.lvSet st vi j₁)) (Tag.arg (toLex (dt.lvBlk vi j₁))) = encMap dt.ly zero one p) (h2 : wmBlk (ixAddr elt (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 F zero hhas vi j₁ j₂ st u) ∨ ∃ (u : Lex (Fin dt.dd0 → A)), CmpFst F zero hhas 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_ixKindExitCtl_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] {I : Type} (F : LaidFile dt A R P I) {elt : I → Univ A R P dt.KIx dt.dd} (hinj : Function.Injective elt) [Nonempty A] [L.IsRelational] [L.Structure A] {zero one : A} (hhas : F.toLayout.HasName zero) (helt : ∀ (b : Fin dt.ko ⊕ Fin dt.ki) (c : Fin dt.dd0 → A), elt (F.toLayout.reg hhas b c) = dt.blkElt b (pad zero c)) {vi : dt.VarIx} {av : Fin dt.natMax} {st : TapeSt dt A R P I} {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 (ixAddr elt (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 (ixAddr elt (dt.ixStageTgt F hhas vi ts { mir := st.mir, tgt := st.tgt, sav := ixMark elt v, val := st.val, old := st.old, new := st.new, wk := st.wk, bot := st.bot, ltp := st.ltp } (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.ixKindExitCtl F zero one hhas vi av st v κ (dt.ixMkKindSem 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_ixMatFs_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] {I : Type} (F : LaidFile dt A R P I) {elt : I → Univ A R P dt.KIx dt.dd} (hinj : Function.Injective elt) [Nonempty A] [L.IsRelational] [L.Structure A] {zero one : A} (hhas : F.toLayout.HasName zero) (helt : ∀ (b : Fin dt.ko ⊕ Fin dt.ki) (c : Fin dt.dd0 → A), elt (F.toLayout.reg hhas b c) = dt.blkElt b (pad zero c)) {vi : dt.VarIx} {st : TapeSt dt A R P I} {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 (ixAddr elt (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 (ixAddr elt (dt.ixStageTgt F hhas vi ts { mir := st.mir, tgt := st.tgt, sav := ixMark elt v, val := st.val, old := st.old, new := st.new, wk := st.wk, bot := st.bot, ltp := st.ltp } (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.ixMatFs F zero one hhas vi st v enterSt (fun (b : Fin (dt.natOf vi)) => dt.ixMkKindSem 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.ixMatFsT {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] {I : Type} (F : LaidFile dt A R P I) {elt : I → Univ A R P dt.KIx dt.dd} [Nonempty A] [L.IsRelational] [L.Structure A] (zero one : A) (hhas : F.toLayout.HasName zero) (vi : dt.VarIx) (st : TapeSt dt A R P I) (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.IxKindSem zero one vi (dt.ixMatSt vi st v ↑a) elt (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.ixMatFsT F zero one hhas vi st v enterSt sem f₀ 0 = f₀

theorem DescriptiveComplexity.Draw.Data.ixScratchEq_matSt {L : FirstOrder.Language} {dt : Data L} {A R P I : Type} {elt : I → Univ A R P dt.KIx dt.dd} {vi : dt.VarIx} {st : TapeSt dt A R P I} {v : Univ A R P dt.KIx dt.dd → Prop} (n : ℕ) : dt.ScratchEq (dt.ixMatSt 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.ixMatFs_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] {I : Type} (F : LaidFile dt A R P I) {elt : I → Univ A R P dt.KIx dt.dd} [Nonempty A] [L.IsRelational] [L.Structure A] {zero one : A} (hhas : F.toLayout.HasName zero) {vi : dt.VarIx} {st : TapeSt dt A R P I} {v : Univ A R P dt.KIx dt.dd → Prop} {st' : TapeSt dt A R P I} (h : dt.ScratchEq st st') (hreg : ¬∃ (u : I), v = F.cell u) (enterSt : Fin (dt.natOf vi) → (dt.CtlIx → A) → (dt.SlotIx → A) → dt.CtlIx → A) (sem : (a : Fin (dt.natOf vi)) → dt.IxKindSem zero one vi st elt (dt.kindOf vi a)) (f₀ : dt.CtlIx → A) (n : ℕ) : dt.ixMatFs F zero one hhas vi st v enterSt sem f₀ n = dt.ixMatFs F zero one hhas vi st' v enterSt (fun (a : Fin (dt.natOf vi)) => dt.ixKindSemCast 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.ixMatFsT_eq_ixMatFs {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] {I : Type} (F : LaidFile dt A R P I) {elt : I → Univ A R P dt.KIx dt.dd} [Nonempty A] [L.IsRelational] [L.Structure A] {zero one : A} (hhas : F.toLayout.HasName zero) {vi : dt.VarIx} {st : TapeSt dt A R P I} {v : Univ A R P dt.KIx dt.dd → Prop} (hreg : ¬∃ (u : I), v = F.cell u) (enterSt : Fin (dt.natOf vi) → (dt.CtlIx → A) → (dt.SlotIx → A) → dt.CtlIx → A) (semT : (a : Fin (dt.natOf vi)) → dt.IxKindSem zero one vi (dt.ixMatSt vi st v ↑a) elt (dt.kindOf vi a)) (f₀ : dt.CtlIx → A) (n : ℕ) : dt.ixMatFsT F zero one hhas vi st v enterSt semT f₀ n = dt.ixMatFs F zero one hhas vi st v enterSt (fun (a : Fin (dt.natOf vi)) => dt.ixKindSemCast 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.ixMatrix_run_thread_reachesIn {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} {I : Type} [Finite I] (F : LaidFile dt A R P I) {elt : I → Univ A R P dt.KIx dt.dd} (hinj : Function.Injective elt) (hhasP : F.toLayout.HasName PR.zero) (heltP : ∀ (b : Fin dt.ko ⊕ Fin dt.ki) (c : Fin dt.dd0 → A), elt (F.toLayout.reg hhasP b c) = dt.blkElt b (pad PR.zero c)) (hsepP : F.toLayout.NameSep PR.zero ⋯) (hix : IsLinOrd F.le) {e₀ : Univ A R P dt.KIx dt.dd} (he₀ : ∀ (y : Univ A R P dt.KIx dt.dd), WMLe e₀ y) (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 : TapeSt dt A R P I} {v : Univ A R P dt.KIx dt.dd → Prop} [Finite dt.KIx] (hR : PR.table.Reads) (hlin : IsLinOrd WMLe) {gtop gbot : I} (htop : ∀ (y : I), F.le y gtop) (hbot : ∀ (y : I), F.le gbot y) (hwork : ∀ {r : Univ A R P dt.KIx dt.dd → Prop}, (∀ (x : Univ A R P dt.KIx dt.dd), r x → ∃ (i : dt.KIx), x.1 = Tag.arg i) → ∀ (u : I), WMSetLt WMLe r (F.cell u)) {v' : Univ A R P dt.KIx dt.dd → Prop} (hv : WMSetLt WMLe v (F.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 = ixMark elt 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) {Use : I → Prop} (hmono : ∀ (u u' : I), WMLt F.le u u' ↔ WMLt WMLe (elt u) (elt u')) (hup : ∀ (u : I) (x : Univ A R P dt.KIx dt.dd), Use u → WMLt WMLe (elt u) x → ∃ (u' : I), Use u' ∧ elt u' = x) (hvh : IxHolds elt Use v) (hxdUse : ∀ {iv : dt.d.B.ι} (ℓ : Fin (dt.d.B.arity iv)) (b : Lex (Fin dt.dd0 → A)), Use (dt.ixStageXD F hhasP ℓ b)) (w wG wP wR wK : ℕ) (hgap : ∀ (u u' : I), IxSucc F.le u u' → wideRank (F.cell u') - wideRank (F.cell u) ≤ wG) (hwP : wideRank (F.cell gtop) + 2 + ((ixRank F.le gtop - ixRank F.le gbot) * wG + 1) + wideRank (F.cell gbot) ≤ wP) (hwR : ∀ (s : Univ A R P dt.KIx dt.dd → Prop), WMSetLt WMLe s (F.cell gbot) → wideRank s + 4 ≤ wR) (hwK : ∀ (T : Univ A R P dt.KIx dt.dd → Prop), WMSetLt WMLe T (F.cell gbot) → wideRank T * (1 + (wideRank (F.cell gtop) + 3 + (ixRank F.le gtop - ixRank F.le gbot) * wG + wideRank (F.cell gbot)) + (wideRank (F.cell gtop) + ((ixRank F.le gtop - ixRank F.le gbot) * wG + 1) + wideRank (F.cell gbot) + 4)) + 1 + (wideRank (F.cell gtop) + 3 + (ixRank F.le gtop - ixRank F.le gbot) * wG + wideRank (F.cell gbot)) ≤ wK) (hcostR : ∀ (b : Fin dt.ko ⊕ Fin dt.ki) (c : Fin dt.dd0 → A), 2 * (wideRank (F.cell (F.toLayout.reg hhasP b c)) - wideRank v) + 2 ≤ w) {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 ρ) (wA : ℕ) (hwA : ∀ (a : Fin (dt.natOf vi)), dt.ixKindCost A vi w wP wR wK (dt.kindOf vi a) ≤ wA) (semT : (a : Fin (dt.natOf vi)) → dt.IxKindSem PR.zero PR.one vi (dt.ixMatSt vi st v ↑a) elt (dt.kindOf vi a)) (f₀ : dt.CtlIx → A) : (wideData (Univ A R P dt.KIx dt.dd)).ReachesIn ((wA + 2) * dt.natOf vi + 1) { state := Sum.inr (PR.stElt (emb (SeqPh.chk 0)) f₀), head := Sum.inl v, tape := wideTape (PR.trackTapeAt F.cell Slot.val (dt.ixBack F.toLayout PR.zero PR.one ⋯ st) st.val) (PR.syElt PR.blank) } { state := Sum.inr (PR.stElt exitPh (dt.ixMatFsT F PR.zero PR.one hhasP vi st v enterSt semT f₀ (dt.natOf vi))), head := Sum.inl v', tape := wideTape (PR.trackTapeAt F.cell Slot.val (dt.ixBack F.toLayout PR.zero PR.one ⋯ (dt.ixMatSt vi st v (dt.natOf vi))) (dt.ixMatSt vi st v (dt.natOf vi)).val) (PR.syElt PR.blank) }

The matrix's run, threaded, on a clock: as DescriptiveComplexity.Draw.Data.ixMatrix_run_thread with the atoms counted – one atom's width, one dispatch and one step back per atom, and one step to leave.

theorem DescriptiveComplexity.Draw.Data.ixMatrix_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} {I : Type} [Finite I] (F : LaidFile dt A R P I) {elt : I → Univ A R P dt.KIx dt.dd} (hinj : Function.Injective elt) (hhasP : F.toLayout.HasName PR.zero) (heltP : ∀ (b : Fin dt.ko ⊕ Fin dt.ki) (c : Fin dt.dd0 → A), elt (F.toLayout.reg hhasP b c) = dt.blkElt b (pad PR.zero c)) (hsepP : F.toLayout.NameSep PR.zero ⋯) (hix : IsLinOrd F.le) {e₀ : Univ A R P dt.KIx dt.dd} (he₀ : ∀ (y : Univ A R P dt.KIx dt.dd), WMLe e₀ y) (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 : TapeSt dt A R P I} {v : Univ A R P dt.KIx dt.dd → Prop} [Finite dt.KIx] (hR : PR.table.Reads) (hlin : IsLinOrd WMLe) {gtop gbot : I} (htop : ∀ (y : I), F.le y gtop) (hbot : ∀ (y : I), F.le gbot y) (hwork : ∀ {r : Univ A R P dt.KIx dt.dd → Prop}, (∀ (x : Univ A R P dt.KIx dt.dd), r x → ∃ (i : dt.KIx), x.1 = Tag.arg i) → ∀ (u : I), WMSetLt WMLe r (F.cell u)) {v' : Univ A R P dt.KIx dt.dd → Prop} (hv : WMSetLt WMLe v (F.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 = ixMark elt 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) {Use : I → Prop} (hmono : ∀ (u u' : I), WMLt F.le u u' ↔ WMLt WMLe (elt u) (elt u')) (hup : ∀ (u : I) (x : Univ A R P dt.KIx dt.dd), Use u → WMLt WMLe (elt u) x → ∃ (u' : I), Use u' ∧ elt u' = x) (hvh : IxHolds elt Use v) (hxdUse : ∀ {iv : dt.d.B.ι} (ℓ : Fin (dt.d.B.arity iv)) (b : Lex (Fin dt.dd0 → A)), Use (dt.ixStageXD F hhasP ℓ b)) (w wG wP wR wK : ℕ) (hgap : ∀ (u u' : I), IxSucc F.le u u' → wideRank (F.cell u') - wideRank (F.cell u) ≤ wG) (hwP : wideRank (F.cell gtop) + 2 + ((ixRank F.le gtop - ixRank F.le gbot) * wG + 1) + wideRank (F.cell gbot) ≤ wP) (hwR : ∀ (s : Univ A R P dt.KIx dt.dd → Prop), WMSetLt WMLe s (F.cell gbot) → wideRank s + 4 ≤ wR) (hwK : ∀ (T : Univ A R P dt.KIx dt.dd → Prop), WMSetLt WMLe T (F.cell gbot) → wideRank T * (1 + (wideRank (F.cell gtop) + 3 + (ixRank F.le gtop - ixRank F.le gbot) * wG + wideRank (F.cell gbot)) + (wideRank (F.cell gtop) + ((ixRank F.le gtop - ixRank F.le gbot) * wG + 1) + wideRank (F.cell gbot) + 4)) + 1 + (wideRank (F.cell gtop) + 3 + (ixRank F.le gtop - ixRank F.le gbot) * wG + wideRank (F.cell gbot)) ≤ wK) (hcostR : ∀ (b : Fin dt.ko ⊕ Fin dt.ki) (c : Fin dt.dd0 → A), 2 * (wideRank (F.cell (F.toLayout.reg hhasP b c)) - wideRank v) + 2 ≤ w) {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.IxKindSem PR.zero PR.one vi (dt.ixMatSt vi st v ↑a) elt (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 F.cell Slot.val (dt.ixBack F.toLayout PR.zero PR.one ⋯ st) st.val) (PR.syElt PR.blank) } { state := Sum.inr (PR.stElt exitPh (dt.ixMatFsT F PR.zero PR.one hhasP vi st v enterSt semT f₀ (dt.natOf vi))), head := Sum.inl v', tape := wideTape (PR.trackTapeAt F.cell Slot.val (dt.ixBack F.toLayout PR.zero PR.one ⋯ (dt.ixMatSt vi st v (dt.natOf vi))) (dt.ixMatSt vi st v (dt.natOf vi)).val) (PR.syElt PR.blank) }

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

theorem DescriptiveComplexity.Draw.Data.ixMatrix_reachesIn {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} {I : Type} [Finite I] (F : LaidFile dt A R P I) {elt : I → Univ A R P dt.KIx dt.dd} (hinj : Function.Injective elt) (hhasP : F.toLayout.HasName PR.zero) (heltP : ∀ (b : Fin dt.ko ⊕ Fin dt.ki) (c : Fin dt.dd0 → A), elt (F.toLayout.reg hhasP b c) = dt.blkElt b (pad PR.zero c)) (hsepP : F.toLayout.NameSep PR.zero ⋯) (hix : IsLinOrd F.le) {e₀ : Univ A R P dt.KIx dt.dd} (he₀ : ∀ (y : Univ A R P dt.KIx dt.dd), WMLe e₀ y) (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 : TapeSt dt A R P I} {v : Univ A R P dt.KIx dt.dd → Prop} [Finite dt.KIx] (hR : PR.table.Reads) (hlin : IsLinOrd WMLe) {gtop gbot : I} (htop : ∀ (y : I), F.le y gtop) (hbot : ∀ (y : I), F.le gbot y) (hwork : ∀ {r : Univ A R P dt.KIx dt.dd → Prop}, (∀ (x : Univ A R P dt.KIx dt.dd), r x → ∃ (i : dt.KIx), x.1 = Tag.arg i) → ∀ (u : I), WMSetLt WMLe r (F.cell u)) {v' : Univ A R P dt.KIx dt.dd → Prop} (hv : WMSetLt WMLe v (F.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 = ixMark elt 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 = ixMark elt v) (htgt : st.tgt = ixMark elt v) {Use : I → Prop} (hmono : ∀ (u u' : I), WMLt F.le u u' ↔ WMLt WMLe (elt u) (elt u')) (hup : ∀ (u : I) (x : Univ A R P dt.KIx dt.dd), Use u → WMLt WMLe (elt u) x → ∃ (u' : I), Use u' ∧ elt u' = x) (hvh : IxHolds elt Use v) (hxdUse : ∀ {iv : dt.d.B.ι} (ℓ : Fin (dt.d.B.arity iv)) (b : Lex (Fin dt.dd0 → A)), Use (dt.ixStageXD F hhasP ℓ b)) (w wG wP wR wK : ℕ) (hgap : ∀ (u u' : I), IxSucc F.le u u' → wideRank (F.cell u') - wideRank (F.cell u) ≤ wG) (hwP : wideRank (F.cell gtop) + 2 + ((ixRank F.le gtop - ixRank F.le gbot) * wG + 1) + wideRank (F.cell gbot) ≤ wP) (hwR : ∀ (s : Univ A R P dt.KIx dt.dd → Prop), WMSetLt WMLe s (F.cell gbot) → wideRank s + 4 ≤ wR) (hwK : ∀ (T : Univ A R P dt.KIx dt.dd → Prop), WMSetLt WMLe T (F.cell gbot) → wideRank T * (1 + (wideRank (F.cell gtop) + 3 + (ixRank F.le gtop - ixRank F.le gbot) * wG + wideRank (F.cell gbot)) + (wideRank (F.cell gtop) + ((ixRank F.le gtop - ixRank F.le gbot) * wG + 1) + wideRank (F.cell gbot) + 4)) + 1 + (wideRank (F.cell gtop) + 3 + (ixRank F.le gtop - ixRank F.le gbot) * wG + wideRank (F.cell gbot)) ≤ wK) (hcostR : ∀ (b : Fin dt.ko ⊕ Fin dt.ki) (c : Fin dt.dd0 → A), 2 * (wideRank (F.cell (F.toLayout.reg hhasP b c)) - wideRank v) + 2 ≤ w) {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.IxKindSem PR.zero PR.one vi st elt (dt.kindOf vi a)) (wA : ℕ) (hwA : ∀ (a : Fin (dt.natOf vi)), dt.ixKindCost A vi w wP wR wK (dt.kindOf vi a) ≤ wA) (f₀ : dt.CtlIx → A) : (wideData (Univ A R P dt.KIx dt.dd)).ReachesIn ((wA + 2) * dt.natOf vi + 1) { state := Sum.inr (PR.stElt (emb (SeqPh.chk 0)) f₀), head := Sum.inl v, tape := wideTape (PR.trackTapeAt F.cell Slot.val (dt.ixBack F.toLayout PR.zero PR.one ⋯ st) st.val) (PR.syElt PR.blank) } { state := Sum.inr (PR.stElt exitPh (dt.ixMatFs F PR.zero PR.one hhasP vi st v enterSt sem f₀ (dt.natOf vi))), head := Sum.inl v', tape := wideTape (PR.trackTapeAt F.cell Slot.val (dt.ixBack F.toLayout PR.zero PR.one ⋯ st) st.val) (PR.syElt PR.blank) }

The matrix's run, on a clock: as DescriptiveComplexity.Draw.Data.ixMatrix_run with the atoms counted – one atom's width, one dispatch and one step back per atom, and one step to leave.

theorem DescriptiveComplexity.Draw.Data.ixMatrix_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} {I : Type} [Finite I] (F : LaidFile dt A R P I) {elt : I → Univ A R P dt.KIx dt.dd} (hinj : Function.Injective elt) (hhasP : F.toLayout.HasName PR.zero) (heltP : ∀ (b : Fin dt.ko ⊕ Fin dt.ki) (c : Fin dt.dd0 → A), elt (F.toLayout.reg hhasP b c) = dt.blkElt b (pad PR.zero c)) (hsepP : F.toLayout.NameSep PR.zero ⋯) (hix : IsLinOrd F.le) {e₀ : Univ A R P dt.KIx dt.dd} (he₀ : ∀ (y : Univ A R P dt.KIx dt.dd), WMLe e₀ y) (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 : TapeSt dt A R P I} {v : Univ A R P dt.KIx dt.dd → Prop} [Finite dt.KIx] (hR : PR.table.Reads) (hlin : IsLinOrd WMLe) {gtop gbot : I} (htop : ∀ (y : I), F.le y gtop) (hbot : ∀ (y : I), F.le gbot y) (hwork : ∀ {r : Univ A R P dt.KIx dt.dd → Prop}, (∀ (x : Univ A R P dt.KIx dt.dd), r x → ∃ (i : dt.KIx), x.1 = Tag.arg i) → ∀ (u : I), WMSetLt WMLe r (F.cell u)) {v' : Univ A R P dt.KIx dt.dd → Prop} (hv : WMSetLt WMLe v (F.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 = ixMark elt 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 = ixMark elt v) (htgt : st.tgt = ixMark elt v) {Use : I → Prop} (hmono : ∀ (u u' : I), WMLt F.le u u' ↔ WMLt WMLe (elt u) (elt u')) (hup : ∀ (u : I) (x : Univ A R P dt.KIx dt.dd), Use u → WMLt WMLe (elt u) x → ∃ (u' : I), Use u' ∧ elt u' = x) (hvh : IxHolds elt Use v) (hxdUse : ∀ {iv : dt.d.B.ι} (ℓ : Fin (dt.d.B.arity iv)) (b : Lex (Fin dt.dd0 → A)), Use (dt.ixStageXD F hhasP ℓ b)) (w wG wP wR wK : ℕ) (hgap : ∀ (u u' : I), IxSucc F.le u u' → wideRank (F.cell u') - wideRank (F.cell u) ≤ wG) (hwP : wideRank (F.cell gtop) + 2 + ((ixRank F.le gtop - ixRank F.le gbot) * wG + 1) + wideRank (F.cell gbot) ≤ wP) (hwR : ∀ (s : Univ A R P dt.KIx dt.dd → Prop), WMSetLt WMLe s (F.cell gbot) → wideRank s + 4 ≤ wR) (hwK : ∀ (T : Univ A R P dt.KIx dt.dd → Prop), WMSetLt WMLe T (F.cell gbot) → wideRank T * (1 + (wideRank (F.cell gtop) + 3 + (ixRank F.le gtop - ixRank F.le gbot) * wG + wideRank (F.cell gbot)) + (wideRank (F.cell gtop) + ((ixRank F.le gtop - ixRank F.le gbot) * wG + 1) + wideRank (F.cell gbot) + 4)) + 1 + (wideRank (F.cell gtop) + 3 + (ixRank F.le gtop - ixRank F.le gbot) * wG + wideRank (F.cell gbot)) ≤ wK) (hcostR : ∀ (b : Fin dt.ko ⊕ Fin dt.ki) (c : Fin dt.dd0 → A), 2 * (wideRank (F.cell (F.toLayout.reg hhasP b c)) - wideRank v) + 2 ≤ w) {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.IxKindSem PR.zero PR.one vi st elt (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 F.cell Slot.val (dt.ixBack F.toLayout PR.zero PR.one ⋯ st) st.val) (PR.syElt PR.blank) } { state := Sum.inr (PR.stElt exitPh (dt.ixMatFs F PR.zero PR.one hhasP vi st v enterSt sem f₀ (dt.natOf vi))), head := Sum.inl v', tape := wideTape (PR.trackTapeAt F.cell Slot.val (dt.ixBack F.toLayout 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.ixGateCost {L : FirstOrder.Language} (dt : Data L) (A : Type) (w wP : ℕ) : ℕ

What one gate block's machinery is charged: the file test's sweep of the registers, the passing dispatch, the walk back and the tag flags, then the domain evaluation's leaf reads once per point of the evaluation order. Uniform in the block – the tag count and the read count are bounded by ntgDim and nfDim – so the gate sequence's fold is a single width.

Equations

• dt.ixGateCost A w wP = wP + (1 + (1 + ((w + 2) * dt.ntgDim + 2 + ((2 + (w + 2) * dt.nfDim) * (Nat.card (Lex (Fin dt.eDim → A)) + 1) + 1))))

noncomputable def DescriptiveComplexity.Draw.Data.ixGatesFs {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] {I : Type} (F : LaidFile dt A R P I) [Nonempty A] [L.IsRelational] [L.Structure A] (zero one : A) (hhas : F.toLayout.HasName zero) (vi : dt.VarIx) (st : TapeSt dt A R P I) (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.ixGatesFs F zero one hhas vi st v bOf hc hnG hrdG tOf enterSt f₀ 0 = f₀

theorem DescriptiveComplexity.Draw.Data.ixGates_reachesIn {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} {I : Type} [Finite I] (F : LaidFile dt A R P I) {elt : I → Univ A R P dt.KIx dt.dd} (hinj : Function.Injective elt) (hhasP : F.toLayout.HasName PR.zero) (heltP : ∀ (b : Fin dt.ko ⊕ Fin dt.ki) (c : Fin dt.dd0 → A), elt (F.toLayout.reg hhasP b c) = dt.blkElt b (pad PR.zero c)) (hsepP : F.toLayout.NameSep PR.zero ⋯) (hix : IsLinOrd F.le) [Nonempty A] [L.IsRelational] [L.Structure A] {vi : dt.VarIx} {st : TapeSt dt A R P I} {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 : I} (htop : ∀ (y : I), F.le y gtop) (hbot : ∀ (y : I), F.le gbot y) {v' : Univ A R P dt.KIx dt.dd → Prop} (hv : WMSetLt WMLe v (F.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) → I → Prop) (hcompatOf : ∀ (ℓ : Fin (dt.arOf vi)) (u : I), wellGOf ℓ (PR.passTracksAt F.cell Slot.mir (dt.ixBack F.toLayout PR.zero PR.one ⋯ st) st.mir (F.cell u)) ↔ TestOf ℓ u) {wG : ℕ} (hgap : ∀ (u u' : I), IxSucc F.le u u' → wideRank (F.cell u') - wideRank (F.cell u) ≤ wG) (w wP : ℕ) (hwP : wideRank (F.cell gtop) + 2 + ((ixRank F.le gtop - ixRank F.le gbot) * wG + 1) + wideRank (F.cell gbot) ≤ wP) (hcostR : ∀ (b : Fin dt.ko ⊕ Fin dt.ki) (c : Fin dt.dd0 → A), 2 * (wideRank (F.cell (F.toLayout.reg hhasP b c)) - wideRank v) + 2 ≤ w) (tOf : Fin (dt.arOf vi) → dt.X.Tag) (htagOf : ∀ (ℓ : Fin (dt.arOf vi)), dt.dspTagOf PR.zero PR.one (wmBlk (ixAddr elt st.mir) (Tag.arg (toLex (bOf ℓ)))) = tOf ℓ) (hTestOf : ∀ (ℓ : Fin (dt.arOf vi)) (u : I), TestOf ℓ u) (f₀ : dt.CtlIx → A) : (wideData (Univ A R P dt.KIx dt.dd)).ReachesIn ((dt.ixGateCost A w wP + 2) * dt.arOf vi + 1) { state := Sum.inr (PR.stElt (emb (SeqPh.chk 0)) f₀), head := Sum.inl v, tape := wideTape (PR.trackTapeAt F.cell Slot.val (dt.ixBack F.toLayout PR.zero PR.one ⋯ st) st.val) (PR.syElt PR.blank) } { state := Sum.inr (PR.stElt exitPh (dt.ixGatesFs F PR.zero PR.one hhasP vi st v bOf hc hnG hrdG tOf enterSt f₀ (dt.arOf vi))), head := Sum.inl v', tape := wideTape (PR.trackTapeAt F.cell Slot.val (dt.ixBack F.toLayout PR.zero PR.one ⋯ st) st.val) (PR.syElt PR.blank) }

The gates' run at a gated address, on a clock: as DescriptiveComplexity.Draw.Data.ixGates_run with the blocks counted – one block's width, its dispatch and the step back per block, and one step to leave.

theorem DescriptiveComplexity.Draw.Data.ixGates_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} {I : Type} [Finite I] (F : LaidFile dt A R P I) {elt : I → Univ A R P dt.KIx dt.dd} (hinj : Function.Injective elt) (hhasP : F.toLayout.HasName PR.zero) (heltP : ∀ (b : Fin dt.ko ⊕ Fin dt.ki) (c : Fin dt.dd0 → A), elt (F.toLayout.reg hhasP b c) = dt.blkElt b (pad PR.zero c)) (hsepP : F.toLayout.NameSep PR.zero ⋯) (hix : IsLinOrd F.le) [Nonempty A] [L.IsRelational] [L.Structure A] {vi : dt.VarIx} {st : TapeSt dt A R P I} {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 : I} (htop : ∀ (y : I), F.le y gtop) (hbot : ∀ (y : I), F.le gbot y) {v' : Univ A R P dt.KIx dt.dd → Prop} (hv : WMSetLt WMLe v (F.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) → I → Prop) (hcompatOf : ∀ (ℓ : Fin (dt.arOf vi)) (u : I), wellGOf ℓ (PR.passTracksAt F.cell Slot.mir (dt.ixBack F.toLayout PR.zero PR.one ⋯ st) st.mir (F.cell u)) ↔ TestOf ℓ u) {wG : ℕ} (hgap : ∀ (u u' : I), IxSucc F.le u u' → wideRank (F.cell u') - wideRank (F.cell u) ≤ wG) (w wP : ℕ) (hwP : wideRank (F.cell gtop) + 2 + ((ixRank F.le gtop - ixRank F.le gbot) * wG + 1) + wideRank (F.cell gbot) ≤ wP) (hcostR : ∀ (b : Fin dt.ko ⊕ Fin dt.ki) (c : Fin dt.dd0 → A), 2 * (wideRank (F.cell (F.toLayout.reg hhasP b c)) - wideRank v) + 2 ≤ w) (tOf : Fin (dt.arOf vi) → dt.X.Tag) (htagOf : ∀ (ℓ : Fin (dt.arOf vi)), dt.dspTagOf PR.zero PR.one (wmBlk (ixAddr elt st.mir) (Tag.arg (toLex (bOf ℓ)))) = tOf ℓ) (hTestOf : ∀ (ℓ : Fin (dt.arOf vi)) (u : I), 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 F.cell Slot.val (dt.ixBack F.toLayout PR.zero PR.one ⋯ st) st.val) (PR.syElt PR.blank) } { state := Sum.inr (PR.stElt exitPh (dt.ixGatesFs F PR.zero PR.one hhasP vi st v bOf hc hnG hrdG tOf enterSt f₀ (dt.arOf vi))), head := Sum.inl v', tape := wideTape (PR.trackTapeAt F.cell Slot.val (dt.ixBack F.toLayout 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.ixGates_reachesIn_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} {I : Type} [Finite I] (F : LaidFile dt A R P I) {elt : I → Univ A R P dt.KIx dt.dd} (hinj : Function.Injective elt) (hhasP : F.toLayout.HasName PR.zero) (heltP : ∀ (b : Fin dt.ko ⊕ Fin dt.ki) (c : Fin dt.dd0 → A), elt (F.toLayout.reg hhasP b c) = dt.blkElt b (pad PR.zero c)) (hsepP : F.toLayout.NameSep PR.zero ⋯) (hix : IsLinOrd F.le) [Nonempty A] [L.IsRelational] [L.Structure A] {vi : dt.VarIx} {st : TapeSt dt A R P I} {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 : I} (htop : ∀ (y : I), F.le y gtop) (hbot : ∀ (y : I), F.le gbot y) {v' : Univ A R P dt.KIx dt.dd → Prop} (hv : WMSetLt WMLe v (F.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) → I → Prop) (hcompatOf : ∀ (ℓ : Fin (dt.arOf vi)) (u : I), wellGOf ℓ (PR.passTracksAt F.cell Slot.mir (dt.ixBack F.toLayout PR.zero PR.one ⋯ st) st.mir (F.cell u)) ↔ TestOf ℓ u) {wG : ℕ} (hgap : ∀ (u u' : I), IxSucc F.le u u' → wideRank (F.cell u') - wideRank (F.cell u) ≤ wG) (w wP : ℕ) (hwP : wideRank (F.cell gtop) + 2 + ((ixRank F.le gtop - ixRank F.le gbot) * wG + 1) + wideRank (F.cell gbot) ≤ wP) (hcostR : ∀ (b : Fin dt.ko ⊕ Fin dt.ki) (c : Fin dt.dd0 → A), 2 * (wideRank (F.cell (F.toLayout.reg hhasP b c)) - wideRank v) + 2 ≤ w) (tOf : Fin (dt.arOf vi) → dt.X.Tag) (htagOf : ∀ (ℓ : Fin (dt.arOf vi)), dt.dspTagOf PR.zero PR.one (wmBlk (ixAddr elt st.mir) (Tag.arg (toLex (bOf ℓ)))) = tOf ℓ) (ℓ₀ : Fin (dt.arOf vi)) (hTestLt : ∀ (ℓ : Fin (dt.arOf vi)), ↑ℓ < ↑ℓ₀ → ∀ (u : I), TestOf ℓ u) {u₀ : I} (hfail : ¬TestOf ℓ₀ u₀) (f₀ : dt.CtlIx → A) : (wideData (Univ A R P dt.KIx dt.dd)).ReachesIn ((dt.ixGateCost A w wP + 2) * ↑ℓ₀ + (1 + (wP + 1))) { state := Sum.inr (PR.stElt (emb (SeqPh.chk 0)) f₀), head := Sum.inl v, tape := wideTape (PR.trackTapeAt F.cell Slot.val (dt.ixBack F.toLayout PR.zero PR.one ⋯ st) st.val) (PR.syElt PR.blank) } { state := Sum.inr (PR.stElt failPh (setFail (enterSt ℓ₀ (dt.ixGatesFs F PR.zero PR.one hhasP vi st v bOf hc hnG hrdG tOf enterSt f₀ ↑ℓ₀) (dt.ixBack F.toLayout PR.zero PR.one ⋯ st v)) (dt.ixBack F.toLayout PR.zero PR.one ⋯ st v))), head := Sum.inl v', tape := wideTape (PR.trackTapeAt F.cell Slot.val (dt.ixBack F.toLayout PR.zero PR.one ⋯ st) st.val) (PR.syElt PR.blank) }

The gates' run at a junk address, on a clock: as DescriptiveComplexity.Draw.Data.ixGates_run_fail with the passing prefix counted, the failing dispatch and the failing block's sweep on top.

theorem DescriptiveComplexity.Draw.Data.ixGates_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} {I : Type} [Finite I] (F : LaidFile dt A R P I) {elt : I → Univ A R P dt.KIx dt.dd} (hinj : Function.Injective elt) (hhasP : F.toLayout.HasName PR.zero) (heltP : ∀ (b : Fin dt.ko ⊕ Fin dt.ki) (c : Fin dt.dd0 → A), elt (F.toLayout.reg hhasP b c) = dt.blkElt b (pad PR.zero c)) (hsepP : F.toLayout.NameSep PR.zero ⋯) (hix : IsLinOrd F.le) [Nonempty A] [L.IsRelational] [L.Structure A] {vi : dt.VarIx} {st : TapeSt dt A R P I} {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 : I} (htop : ∀ (y : I), F.le y gtop) (hbot : ∀ (y : I), F.le gbot y) {v' : Univ A R P dt.KIx dt.dd → Prop} (hv : WMSetLt WMLe v (F.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) → I → Prop) (hcompatOf : ∀ (ℓ : Fin (dt.arOf vi)) (u : I), wellGOf ℓ (PR.passTracksAt F.cell Slot.mir (dt.ixBack F.toLayout PR.zero PR.one ⋯ st) st.mir (F.cell u)) ↔ TestOf ℓ u) {wG : ℕ} (hgap : ∀ (u u' : I), IxSucc F.le u u' → wideRank (F.cell u') - wideRank (F.cell u) ≤ wG) (w wP : ℕ) (hwP : wideRank (F.cell gtop) + 2 + ((ixRank F.le gtop - ixRank F.le gbot) * wG + 1) + wideRank (F.cell gbot) ≤ wP) (hcostR : ∀ (b : Fin dt.ko ⊕ Fin dt.ki) (c : Fin dt.dd0 → A), 2 * (wideRank (F.cell (F.toLayout.reg hhasP b c)) - wideRank v) + 2 ≤ w) (tOf : Fin (dt.arOf vi) → dt.X.Tag) (htagOf : ∀ (ℓ : Fin (dt.arOf vi)), dt.dspTagOf PR.zero PR.one (wmBlk (ixAddr elt st.mir) (Tag.arg (toLex (bOf ℓ)))) = tOf ℓ) (ℓ₀ : Fin (dt.arOf vi)) (hTestLt : ∀ (ℓ : Fin (dt.arOf vi)), ↑ℓ < ↑ℓ₀ → ∀ (u : I), TestOf ℓ u) {u₀ : I} (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 F.cell Slot.val (dt.ixBack F.toLayout PR.zero PR.one ⋯ st) st.val) (PR.syElt PR.blank) } { state := Sum.inr (PR.stElt failPh (setFail (enterSt ℓ₀ (dt.ixGatesFs F PR.zero PR.one hhasP vi st v bOf hc hnG hrdG tOf enterSt f₀ ↑ℓ₀) (dt.ixBack F.toLayout PR.zero PR.one ⋯ st v)) (dt.ixBack F.toLayout PR.zero PR.one ⋯ st v))), head := Sum.inl v', tape := wideTape (PR.trackTapeAt F.cell Slot.val (dt.ixBack F.toLayout 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_ixGatesFs {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} {I : Type} (F : LaidFile dt A R P I) {elt : I → Univ A R P dt.KIx dt.dd} (hinj : Function.Injective elt) (hhasP : F.toLayout.HasName PR.zero) (heltP : ∀ (b : Fin dt.ko ⊕ Fin dt.ki) (c : Fin dt.dd0 → A), elt (F.toLayout.reg hhasP b c) = dt.blkElt b (pad PR.zero c)) [Nonempty A] [L.IsRelational] [L.Structure A] {vi : dt.VarIx} {st : TapeSt dt A R P I} {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.ixGatesFs F PR.zero PR.one hhasP 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 (ixAddr elt 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 (ixAddr elt 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.