The spine's legs at an arbitrary file

DescriptiveComplexity.Problems.Wide.DrawInstEval read at a coarse file: one variable's machinery per spine position, the legs' controls and states, and the legs' runs with their costs.

The legs are generic in the outer phase: what they read of it is the evaluation's own phases, embedded by ep, and the machineries' rules – never the spine's, whose rule shape the space-bounded and the clocked programs do not share. The fold of these legs is DescriptiveComplexity.Problems.Wide.NexSpine.

noncomputable def DescriptiveComplexity.Draw.Data.ixPostVarSt {L : FirstOrder.Language} (dt : Data L) {A R P I : Type} (v : Univ A R P dt.KIx dt.dd → Prop) (st : TapeSt dt A R P I) (m : I → Prop) (i : dt.d.B.ι) (b : Prop) : TapeSt dt A R P I

The tape state after one spine position: the round state at the final VAL content, the variable's new track set at the marker to the machinery's verdict.

Equations

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

One position's leg

noncomputable def DescriptiveComplexity.Draw.Data.ixLegCtlT {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] {v : Univ A R P dt.KIx dt.dd → Prop} {ιV : Type} [LinearOrder ιV] {aT : ιV} (mV : ιV → I → Prop) (j : Fin dt.nv) (st : TapeSt dt A R P I) (tOf : Fin (dt.arOf (dt.varAt j)) → dt.X.Tag) (semT : (p : dt.IxScratch A R P I) → (a : ιV) → (∀ (ℓ : Fin (dt.nIn (dt.varAt j))), dt.ixIGPassP F PR.zero PR.one (dt.varAt j) (ixVarRdSt st p (mV a)) ℓ) → (b : Fin (dt.natOf (dt.varAt j))) → dt.IxKindSem PR.zero PR.one (dt.varAt j) (dt.ixMatSt (dt.varAt j) (ixVarRdSt st p (mV a)) v ↑b) elt (dt.kindOf (dt.varAt j) b)) (f₀ : dt.CtlIx → A) : dt.CtlIx → A

The control after one position's leg, threaded – the twin of DescriptiveComplexity.Draw.Data.ixLegCtl, with the VAL loop's rounds run at the states the thread produces for them.

Equations

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

noncomputable def DescriptiveComplexity.Draw.Data.ixLegStT {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] {v : Univ A R P dt.KIx dt.dd → Prop} {ιV : Type} [LinearOrder ιV] {aT : ιV} (mV : ιV → I → Prop) (j : Fin dt.nv) (st : TapeSt dt A R P I) (tOf : Fin (dt.arOf (dt.varAt j)) → dt.X.Tag) (semT : (p : dt.IxScratch A R P I) → (a : ιV) → (∀ (ℓ : Fin (dt.nIn (dt.varAt j))), dt.ixIGPassP F PR.zero PR.one (dt.varAt j) (ixVarRdSt st p (mV a)) ℓ) → (b : Fin (dt.natOf (dt.varAt j))) → dt.IxKindSem PR.zero PR.one (dt.varAt j) (dt.ixMatSt (dt.varAt j) (ixVarRdSt st p (mV a)) v ↑b) elt (dt.kindOf (dt.varAt j) b)) (f₀ : dt.CtlIx → A) : TapeSt dt A R P I

The tape state after one position's leg, threaded: the VAL loop's exit state – the entry state's SAV and TARGET normalized if any of its rounds ran a stage atom – with the variable's new track written at the marker.

Equations

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

noncomputable def DescriptiveComplexity.Draw.Data.ixLegCost {L : FirstOrder.Language} (dt : Data L) (A : Type) (w wP wR wK n : ℕ) : ℕ

What one leg of the evaluation's spine is charged: the walk-back, the whole machinery of the position's variable, and the written exit. Uniform over the positions – the largest of the variables' costs – so the spine's fold is a single width.

Equations

• dt.ixLegCost A w wP wR wK n = (1 + Finset.univ.sup fun (j : Fin dt.nv) => dt.ixVarCost A (dt.varAt j) w wP wR wK n) + 1

noncomputable def DescriptiveComplexity.Draw.Data.ixOutLegCost {L : FirstOrder.Language} (dt : Data L) (A : Type) (w wP wR wK n : ℕ) : ℕ

What the output's leg is charged: the same shape at the output's own machinery, which is the none variable's.

Equations

• dt.ixOutLegCost A w wP wR wK n = 1 + dt.ixVarCost A none w wP wR wK n + 1

The costs, factored

The clock compares a product: a width and a number of rounds, each bounded on its own (nexTotal_lt_two_pow). So each cost above, which is «once plus a round's cost per VAL content», is rewritten here as «a width times the rounds and one more» – the width is the sum of the two parts, and nothing about the program is used but the shape of the definitions.

noncomputable def DescriptiveComplexity.Draw.Data.ixVarCD {L : FirstOrder.Language} (dt : Data L) (A : Type) (vi : dt.VarIx) (w wP wR wK : ℕ) : ℕ

A variable's machinery, as one width: what it pays once and what it pays per VAL round, added.

Equations

• dt.ixVarCD A vi w wP wR wK = dt.ixVarGatesCost A vi w wP + dt.ixRoundCost A vi w wP wR wK + 3 * wP + 6 + (2 * wP + dt.ixRoundCost A vi w wP wR wK + 3)

noncomputable def DescriptiveComplexity.Draw.Data.ixLegWidth {L : FirstOrder.Language} (dt : Data L) (A : Type) (w wP wR wK : ℕ) : ℕ

The width of a leg of the spine: the largest variable's, and the leg's own two steps.

Equations

• dt.ixLegWidth A w wP wR wK = 4 + Finset.univ.sup fun (j : Fin dt.nv) => dt.ixVarCD A (dt.varAt j) w wP wR wK

noncomputable def DescriptiveComplexity.Draw.Data.ixEvalWidth {L : FirstOrder.Language} (dt : Data L) (A : Type) (w wP wR wK : ℕ) : ℕ

The width of the whole clocked evaluation: the spine's width times its positions, the output machinery's own, and the four steps that join them – the dispatch into the spine, the dispatch into the output's leg and the two the legs themselves pay. This is the first factor the clock compares.

Equations

• dt.ixEvalWidth A w wP wR wK = dt.ixLegWidth A w wP wR wK * dt.nv + dt.ixVarCD A none w wP wR wK + 4

theorem DescriptiveComplexity.Draw.Data.ixVarLeg_run_thread_reachesIn {L : FirstOrder.Language} (dt : Data L) {A R P : Type} [Fintype dt.SlotIx] [LinearOrder A] [LinearOrder R] [LinearOrder P] (ep : EvalPh dt.nv dt.PMF → 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] [Finite dt.KIx] {v v' : Univ A R P dt.KIx dt.dd → Prop} {rEmbM : (j : Fin dt.nv) → (i : dt.VarSiteF (dt.varAt j)) → dt.VarShF (dt.varAt j) i → R} (hrulesM : ∀ (j : Fin dt.nv) (i : dt.VarSiteF (dt.varAt j)) (ρ : dt.VarShF (dt.varAt j) i), PR.rules (rEmbM j i ρ) = dt.varRuleF PR.zero PR.one (dt.varAt j) (dt.varArgsOf PR.zero PR.one (dt.varAt j)) (fun (p : dt.VarPhF (dt.varAt j)) => ep (EvalPh.sub (Sum.inl ⟨j, p⟩))) (ep (EvalPh.chk j.succ)) 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) (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)) (hv : WMSetLt WMLe v (F.cell gbot)) (hvi : WMIncr WMLe v 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) {ιV : Type} [LinearOrder ιV] [Finite ιV] {a₀ aT : ιV} (hbotV : ∀ (a : ιV), a₀ ≤ a) (htopV : ∀ (a : ιV), a ≤ aT) (mV : ιV → I → Prop) (hmV0 : mV a₀ = fun (x : I) => False) (hIncr : ∀ (a a' : ιV), a < a' → (∀ (b : ιV), ¬(a < b ∧ b < a')) → WMIncr F.le (mV a) (mV a')) (hTestT : ∀ (u : I), dt.InnerFull F.blk (mV aT) u) (hTestF : ∀ a < aT, ∃ (u : I), ¬dt.InnerFull F.blk (mV a) u) (j : Fin dt.nv) (st : TapeSt dt A R P I) (hwkSt : st.wk = fun (r : Univ A R P dt.KIx dt.dd → Prop) => r = v) (TestOf : Fin (dt.arOf (dt.varAt j)) → I → Prop) (hcompatOf : ∀ (ℓ : Fin (dt.arOf (dt.varAt j))) (u : I), dt.wellShapedG PR.zero PR.one (Sum.inl (Fin.castLE ⋯ ℓ)) (PR.passTracksAt F.cell Slot.mir (dt.ixBack F.toLayout PR.zero PR.one ⋯ st) st.mir (F.cell u)) ↔ TestOf ℓ u) (tOf : Fin (dt.arOf (dt.varAt j)) → dt.X.Tag) (hwitOf : ∀ (ℓ : Fin (dt.arOf (dt.varAt j))) (t' : dt.X.Tag), wmBlk (ixAddr elt st.mir) (Tag.arg (toLex (Sum.inl (Fin.castLE ⋯ ℓ)))) (encTagTup dt.ly PR.zero PR.one t') ↔ t' = tOf ℓ) (hmir : 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) (semT : (p : dt.IxScratch A R P I) → (a : ιV) → (∀ (ℓ : Fin (dt.nIn (dt.varAt j))), dt.ixIGPassP F PR.zero PR.one (dt.varAt j) (ixVarRdSt st p (mV a)) ℓ) → (b : Fin (dt.natOf (dt.varAt j))) → dt.IxKindSem PR.zero PR.one (dt.varAt j) (dt.ixMatSt (dt.varAt j) (ixVarRdSt st p (mV a)) v ↑b) elt (dt.kindOf (dt.varAt j) b)) (hDom : ∀ (ℓ : Fin (dt.arOf (dt.varAt j))), ExpExpansion.DomHolds (tOf ℓ, decRho dt.ly PR.zero PR.one (wmBlk (ixAddr elt st.mir) (Tag.arg (toLex (Sum.inl (Fin.castLE ⋯ ℓ))))))) (hTestOf : ∀ (ℓ : Fin (dt.arOf (dt.varAt j))) (u : I), TestOf ℓ u) (f₀ : dt.CtlIx → A) : (wideData (Univ A R P dt.KIx dt.dd)).ReachesIn (dt.ixLegCost A w wP wR wK (Nat.card ιV)) { state := Sum.inr (PR.stElt (ep (EvalPh.sub (dt.smEntry j))) 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 (ep (EvalPh.chk j.succ)) (dt.ixLegCtlT F hinj hhasP heltP mV j st tOf semT f₀)), head := Sum.inl v', tape := wideTape (PR.trackTapeAt F.cell Slot.val (dt.ixBack F.toLayout PR.zero PR.one ⋯ (dt.ixLegStT F hinj hhasP heltP mV j st tOf semT f₀)) (mV aT)) (PR.syElt PR.blank) }

One spine position's leg – threaded: the leg without the boundary hypotheses hsav/htgt, which the sweep cannot supply at more than one address. The leg ends in DescriptiveComplexity.Draw.Data.ixLegStT, the machinery's own exit state with the stage bit written at the marker.

theorem DescriptiveComplexity.Draw.Data.ixVarLegFail_reachesIn {L : FirstOrder.Language} (dt : Data L) {A R P : Type} [Fintype dt.SlotIx] [LinearOrder A] [LinearOrder R] [LinearOrder P] (ep : EvalPh dt.nv dt.PMF → 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] [Finite dt.KIx] {v v' : Univ A R P dt.KIx dt.dd → Prop} {rEmbM : (j : Fin dt.nv) → (i : dt.VarSiteF (dt.varAt j)) → dt.VarShF (dt.varAt j) i → R} (hrulesM : ∀ (j : Fin dt.nv) (i : dt.VarSiteF (dt.varAt j)) (ρ : dt.VarShF (dt.varAt j) i), PR.rules (rEmbM j i ρ) = dt.varRuleF PR.zero PR.one (dt.varAt j) (dt.varArgsOf PR.zero PR.one (dt.varAt j)) (fun (p : dt.VarPhF (dt.varAt j)) => ep (EvalPh.sub (Sum.inl ⟨j, p⟩))) (ep (EvalPh.chk j.succ)) 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) (hv : WMSetLt WMLe v (F.cell gbot)) (hvi : WMIncr WMLe v v') (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) (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) {ιV : Type} (j : Fin dt.nv) (st : TapeSt dt A R P I) (hwkSt : st.wk = fun (r : Univ A R P dt.KIx dt.dd → Prop) => r = v) (TestOf : Fin (dt.arOf (dt.varAt j)) → I → Prop) (hcompatOf : ∀ (ℓ : Fin (dt.arOf (dt.varAt j))) (u : I), dt.wellShapedG PR.zero PR.one (Sum.inl (Fin.castLE ⋯ ℓ)) (PR.passTracksAt F.cell Slot.mir (dt.ixBack F.toLayout PR.zero PR.one ⋯ st) st.mir (F.cell u)) ↔ TestOf ℓ u) (tOf : Fin (dt.arOf (dt.varAt j)) → dt.X.Tag) (htagOf : ∀ (ℓ : Fin (dt.arOf (dt.varAt j))), dt.dspTagOf PR.zero PR.one (wmBlk (ixAddr elt st.mir) (Tag.arg (toLex (Sum.inl (Fin.castLE ⋯ ℓ))))) = tOf ℓ) (ℓ₀ : Fin (dt.arOf (dt.varAt j))) (hTestLt : ∀ (ℓ : Fin (dt.arOf (dt.varAt j))), ↑ℓ < ↑ℓ₀ → ∀ (u : I), TestOf ℓ u) {u₀ : I} (hfail : ¬TestOf ℓ₀ u₀) (f₀ : dt.CtlIx → A) : (wideData (Univ A R P dt.KIx dt.dd)).ReachesIn (dt.ixLegCost A w wP wR wK (Nat.card ιV)) { state := Sum.inr (PR.stElt (ep (EvalPh.sub (dt.smEntry j))) 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 (ep (EvalPh.chk j.succ)) (dt.ixFailCtl F hhasP (dt.varAt j) st tOf ℓ₀ ((dt.varArgsOf PR.zero PR.one (dt.varAt j)).enterSt f₀ (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 ⋯ (dt.ixPostVarSt v st st.val (dt.varList.get j) False)) st.val) (PR.syElt PR.blank) }

One spine position's leg at a junk address: the walk-back, the machinery's failing gates, and the erased stage slot at the marker – the verdict False, the VAL register untouched.

theorem DescriptiveComplexity.Draw.Data.ixVarLegUngated_reachesIn {L : FirstOrder.Language} (dt : Data L) {A R P : Type} [Fintype dt.SlotIx] [LinearOrder A] [LinearOrder R] [LinearOrder P] (ep : EvalPh dt.nv dt.PMF → 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] [Finite dt.KIx] {v v' : Univ A R P dt.KIx dt.dd → Prop} {rEmbM : (j : Fin dt.nv) → (i : dt.VarSiteF (dt.varAt j)) → dt.VarShF (dt.varAt j) i → R} (hrulesM : ∀ (j : Fin dt.nv) (i : dt.VarSiteF (dt.varAt j)) (ρ : dt.VarShF (dt.varAt j) i), PR.rules (rEmbM j i ρ) = dt.varRuleF PR.zero PR.one (dt.varAt j) (dt.varArgsOf PR.zero PR.one (dt.varAt j)) (fun (p : dt.VarPhF (dt.varAt j)) => ep (EvalPh.sub (Sum.inl ⟨j, p⟩))) (ep (EvalPh.chk j.succ)) 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) (hv : WMSetLt WMLe v (F.cell gbot)) (hvi : WMIncr WMLe v v') (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) (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) {ιV : Type} (j : Fin dt.nv) (st : TapeSt dt A R P I) (hwkSt : st.wk = fun (r : Univ A R P dt.KIx dt.dd → Prop) => r = v) (TestOf : Fin (dt.arOf (dt.varAt j)) → I → Prop) (hcompatOf : ∀ (ℓ : Fin (dt.arOf (dt.varAt j))) (u : I), dt.wellShapedG PR.zero PR.one (Sum.inl (Fin.castLE ⋯ ℓ)) (PR.passTracksAt F.cell Slot.mir (dt.ixBack F.toLayout PR.zero PR.one ⋯ st) st.mir (F.cell u)) ↔ TestOf ℓ u) (tOf : Fin (dt.arOf (dt.varAt j)) → dt.X.Tag) (htagOf : ∀ (ℓ : Fin (dt.arOf (dt.varAt j))), dt.dspTagOf PR.zero PR.one (wmBlk (ixAddr elt st.mir) (Tag.arg (toLex (Sum.inl (Fin.castLE ⋯ ℓ))))) = tOf ℓ) (hTestOf : ∀ (ℓ : Fin (dt.arOf (dt.varAt j))) (u : I), TestOf ℓ u) (ℓ₀ : Fin (dt.arOf (dt.varAt j))) (hbad : ¬((∀ (t' : dt.X.Tag), wmBlk (ixAddr elt st.mir) (Tag.arg (toLex (Sum.inl (Fin.castLE ⋯ ℓ₀)))) (encTagTup dt.ly PR.zero PR.one t') ↔ t' = tOf ℓ₀) ∧ ExpExpansion.DomHolds (tOf ℓ₀, decRho dt.ly PR.zero PR.one (wmBlk (ixAddr elt st.mir) (Tag.arg (toLex (Sum.inl (Fin.castLE ⋯ ℓ₀)))))))) (f₀ : dt.CtlIx → A) : (wideData (Univ A R P dt.KIx dt.dd)).ReachesIn (dt.ixLegCost A w wP wR wK (Nat.card ιV)) { state := Sum.inr (PR.stElt (ep (EvalPh.sub (dt.smEntry j))) 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 (ep (EvalPh.chk j.succ)) (dt.ixUngatedCtl F hhasP (dt.varAt j) st tOf ((dt.varArgsOf PR.zero PR.one (dt.varAt j)).enterSt f₀ (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 ⋯ (dt.ixPostVarSt v st st.val (dt.varList.get j) False)) st.val) (PR.syElt PR.blank) }

One spine position's leg at a shaped but ungated address: the walk-back, the whole gate sequence – every file test passing, the total dispatch carrying every block through – the clear flag at the verdict checkpoint, and the erased stage slot at the marker: the verdict False, the VAL register untouched. With DescriptiveComplexity.Draw.Data.ixVarLeg_run_thread_reachesIn and DescriptiveComplexity.Draw.Data.ixVarLegFail_reachesIn this covers every address the sweep visits.

The output's leg

The out machinery is the same shape at vi := none, entered by the walk home after a passed convergence sweep, its exit the accepting phase. Its stage slot is the working-cell marker itself, so an accepting verdict's write is idempotent – the tape after the leg is the machinery's own end tape.

noncomputable def DescriptiveComplexity.Draw.Data.ixOutCtl {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] {v : Univ A R P dt.KIx dt.dd → Prop} {ιV : Type} [LinearOrder ιV] {aT : ιV} (mV : ιV → I → Prop) (st : TapeSt dt A R P I) (tOf : Fin (dt.arOf none) → dt.X.Tag) (semOf : (a : ιV) → (∀ (ℓ : Fin (dt.nIn none)), dt.ixIGPassP F PR.zero PR.one none (dt.ixRoundSt st (mV a)) ℓ) → (b : Fin (dt.natOf none)) → dt.IxKindSem PR.zero PR.one none (dt.ixRoundSt st (mV a)) elt (dt.kindOf none b)) (f₀ : dt.CtlIx → A) : dt.CtlIx → A

The control after the output's leg: the out machinery's exit fold.

Equations

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

Which leg a position takes

A position's machinery has three runs, by what its gates do: DescriptiveComplexity.Draw.Data.ixVarLeg_run_thread_reachesIn when every block is well shaped and the tags and the domain sentence agree, DescriptiveComplexity.Draw.Data.ixVarLegUngated_reachesIn when the blocks are well shaped but the verdict flag is cleared, and DescriptiveComplexity.Draw.Data.ixVarLegFail_reachesIn when a block fails the shape test – which is the one that needs a witness, and a least one, so that the blocks before it have run.

def DescriptiveComplexity.Draw.Data.ixShapeAt {L : FirstOrder.Language} (dt : Data L) {A R P : Type} [Fintype dt.SlotIx] [LinearOrder A] [LinearOrder R] [LinearOrder P] [FirstOrder.Language.wide.Structure (Univ A R P dt.KIx dt.dd)] {PR : Prog A R P dt.CtlIx dt.SlotIx dt.KIx dt.dd} {I : Type} (F : LaidFile dt A R P I) (j : Fin dt.nv) (st : TapeSt dt A R P I) (ℓ : Fin (dt.arOf (dt.varAt j))) (u : I) : Prop

The shape test the gates run, at a position and a state: the per-cell question a block's TestKit asks, which is what tells the third leg from the other two.

Equations

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

noncomputable def DescriptiveComplexity.Draw.Data.ixTagAt {L : FirstOrder.Language} (dt : Data L) {A R P : Type} [Fintype dt.SlotIx] [LinearOrder A] [Finite A] {PR : Prog A R P dt.CtlIx dt.SlotIx dt.KIx dt.dd} {I : Type} {elt : I → Univ A R P dt.KIx dt.dd} [Nonempty A] [L.Structure A] (j : Fin dt.nv) (st : TapeSt dt A R P I) (ℓ : Fin (dt.arOf (dt.varAt j))) : dt.X.Tag

The tag a block's witness cells name, as the machine reads it – so htagOf is rfl at this choice.

Equations

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

def DescriptiveComplexity.Draw.Data.ixTagDomAt {L : FirstOrder.Language} (dt : Data L) {A R P : Type} [Fintype dt.SlotIx] [LinearOrder A] [Finite A] {PR : Prog A R P dt.CtlIx dt.SlotIx dt.KIx dt.dd} {I : Type} {elt : I → Univ A R P dt.KIx dt.dd} [Nonempty A] [L.Structure A] (j : Fin dt.nv) (st : TapeSt dt A R P I) (ℓ : Fin (dt.arOf (dt.varAt j))) : Prop

The other half of a block's gate: its tag witnesses are one-hot at the tag they name, and the expansion's domain sentence holds of the point the block decodes. Together with DescriptiveComplexity.Draw.Data.ixShapeAt this is the gates' verdict.

Equations

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

def DescriptiveComplexity.Draw.Data.ixGatedAt {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} [Nonempty A] [L.Structure A] (j : Fin dt.nv) (st : TapeSt dt A R P I) : Prop

A position is gated when every block passes both halves.

Equations

• dt.ixGatedAt F j st = ((∀ (ℓ : Fin (dt.arOf (dt.varAt j))) (u : I), dt.ixShapeAt F j st ℓ u) ∧ ∀ (ℓ : Fin (dt.arOf (dt.varAt j))), dt.ixTagDomAt j st ℓ)

noncomputable def DescriptiveComplexity.Draw.Data.ixLegStB {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] {v : Univ A R P dt.KIx dt.dd → Prop} {ιV : Type} [LinearOrder ιV] {aT : ιV} (mV : ιV → I → Prop) (j : Fin dt.nv) (st : TapeSt dt A R P I) (semT : dt.ixGatedAt F j st → (p : dt.IxScratch A R P I) → (a : ιV) → (∀ (ℓ : Fin (dt.nIn (dt.varAt j))), dt.ixIGPassP F PR.zero PR.one (dt.varAt j) (ixVarRdSt st p (mV a)) ℓ) → (b : Fin (dt.natOf (dt.varAt j))) → dt.IxKindSem PR.zero PR.one (dt.varAt j) (dt.ixMatSt (dt.varAt j) (ixVarRdSt st p (mV a)) v ↑b) elt (dt.kindOf (dt.varAt j) b)) (f₀ : dt.CtlIx → A) : TapeSt dt A R P I

The state one position's leg leaves, whichever leg it takes: the machinery's own exit at a gated position, and the entry state with the stage bit erased at the two ungated ones – which agree on the tape and differ only in their control.

Equations

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

noncomputable def DescriptiveComplexity.Draw.Data.ixLegCtlB {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] {v : Univ A R P dt.KIx dt.dd → Prop} {ιV : Type} [LinearOrder ιV] {aT : ιV} (mV : ιV → I → Prop) (j : Fin dt.nv) (st : TapeSt dt A R P I) (semT : dt.ixGatedAt F j st → (p : dt.IxScratch A R P I) → (a : ιV) → (∀ (ℓ : Fin (dt.nIn (dt.varAt j))), dt.ixIGPassP F PR.zero PR.one (dt.varAt j) (ixVarRdSt st p (mV a)) ℓ) → (b : Fin (dt.natOf (dt.varAt j))) → dt.IxKindSem PR.zero PR.one (dt.varAt j) (dt.ixMatSt (dt.varAt j) (ixVarRdSt st p (mV a)) v ↑b) elt (dt.kindOf (dt.varAt j) b)) (f₀ : dt.CtlIx → A) : dt.CtlIx → A

The control one position's leg leaves: the machinery's fold at a gated position, the ungated exit when the blocks are well shaped but a tag or the domain fails, and the failing gates' exit – at the least badly shaped block – otherwise.

Equations

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

theorem DescriptiveComplexity.Draw.Data.ixLegStB_fields {L : FirstOrder.Language} (dt : Data L) {A R P : Type} [Fintype dt.SlotIx] [LinearOrder A] [LinearOrder R] [LinearOrder P] [FirstOrder.Language.wide.Structure (Univ A R P dt.KIx dt.dd)] [Finite A] {PR : Prog A R P dt.CtlIx dt.SlotIx dt.KIx dt.dd} {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] {v : Univ A R P dt.KIx dt.dd → Prop} {ιV : Type} [LinearOrder ιV] {aT : ιV} (mV : ιV → I → Prop) (j : Fin dt.nv) (st : TapeSt dt A R P I) (semT : dt.ixGatedAt F j st → (p : dt.IxScratch A R P I) → (a : ιV) → (∀ (ℓ : Fin (dt.nIn (dt.varAt j))), dt.ixIGPassP F PR.zero PR.one (dt.varAt j) (ixVarRdSt st p (mV a)) ℓ) → (b : Fin (dt.natOf (dt.varAt j))) → dt.IxKindSem PR.zero PR.one (dt.varAt j) (dt.ixMatSt (dt.varAt j) (ixVarRdSt st p (mV a)) v ↑b) elt (dt.kindOf (dt.varAt j) b)) (f₀ : dt.CtlIx → A) : (dt.ixLegStB F hinj hhasP heltP mV j st semT f₀).mir = st.mir ∧ (dt.ixLegStB F hinj hhasP heltP mV j st semT f₀).wk = st.wk ∧ (dt.ixLegStB F hinj hhasP heltP mV j st semT f₀).bot = st.bot ∧ (dt.ixLegStB F hinj hhasP heltP mV j st semT f₀).old = st.old ∧ (dt.ixLegStB F hinj hhasP heltP mV j st semT f₀).ltp = st.ltp

What a leg leaves alone, whichever leg it takes: the ungated legs never enter the VAL loop, so they touch nothing but the stage bit, and the gated one is DescriptiveComplexity.Draw.Data.ixLegStT_fields. The val register is left out on purpose – it is the loop's top at a gated position and the entry state's at the other two.