What the spine does to the tape, at an arbitrary file

DescriptiveComplexity.Problems.Wide.DrawSpineSem read at a coarse file: what a whole spine leaves on the tape at one address, the sweep's fold over the addresses, and the semantic packs the positions are run with.

One position's write

The spine's writes

@[reducible, inline]

abbrev DescriptiveComplexity.Draw.Data.IxWritesNew {L : FirstOrder.Language} (dt : Data L) {A R P I : Type} {v : Univ A R P dt.KIx dt.dd → Prop} (stOf : Fin (dt.nv + 1) → TapeSt dt A R P I) (bOf : Fin dt.nv → Prop) : Prop

The only thing the new tracks need of a position: its own cell at the marker holds its verdict and every other cell rides. Weaker than the cover equation hst, and weaker on purpose – a branched position's leg is not literally a DescriptiveComplexity.Draw.Data.ixPostVarSt of the position's entry state (its VAL loop may normalize the two scratch registers first), while this projection of it is (DescriptiveComplexity.Draw.Data.ixLegStB_new).

Equations

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

theorem DescriptiveComplexity.Draw.Data.ixSpineRide {L : FirstOrder.Language} (dt : Data L) {A R P I : Type} {v : Univ A R P dt.KIx dt.dd → Prop} {mOf : Fin dt.nv → I → Prop} {stOf : Fin (dt.nv + 1) → TapeSt dt A R P I} {bOf : Fin dt.nv → Prop} (hst : ∀ (j : Fin dt.nv), stOf j.succ = dt.ixPostVarSt v (stOf j.castSucc) (mOf j) (dt.varList.get j) (bOf j)) {β : Sort u_1} (G : TapeSt dt A R P I → β) (hF : ∀ (st : TapeSt dt A R P I) (m : I → Prop) (i : dt.d.B.ι) (b : Prop), G (dt.ixPostVarSt v st m i b) = G st) (k : Fin (dt.nv + 1)) : G (stOf k) = G (stOf 0)

Anything a position's write leaves alone rides the whole spine: the induction along the positions, once, for every field but val and new.

theorem DescriptiveComplexity.Draw.Data.ixSpine_mir {L : FirstOrder.Language} (dt : Data L) {A R P I : Type} {v : Univ A R P dt.KIx dt.dd → Prop} {mOf : Fin dt.nv → I → Prop} {stOf : Fin (dt.nv + 1) → TapeSt dt A R P I} {bOf : Fin dt.nv → Prop} (hst : ∀ (j : Fin dt.nv), stOf j.succ = dt.ixPostVarSt v (stOf j.castSucc) (mOf j) (dt.varList.get j) (bOf j)) (k : Fin (dt.nv + 1)) : (stOf k).mir = (stOf 0).mir

The working address rides the spine.

theorem DescriptiveComplexity.Draw.Data.ixSpine_new_off {L : FirstOrder.Language} (dt : Data L) {A R P I : Type} {v : Univ A R P dt.KIx dt.dd → Prop} {stOf : Fin (dt.nv + 1) → TapeSt dt A R P I} {bOf : Fin dt.nv → Prop} (hstN : dt.IxWritesNew stOf bOf) (k : Fin (dt.nv + 1)) (i : dt.d.B.ι) {r : Univ A R P dt.KIx dt.dd → Prop} (hr : r ≠ v) : (stOf k).new i r ↔ (stOf 0).new i r

Off the marker, the new tracks ride the spine: a position writes its own cell only.

theorem DescriptiveComplexity.Draw.Data.ixNew_last_get {L : FirstOrder.Language} (dt : Data L) {A R P I : Type} {v : Univ A R P dt.KIx dt.dd → Prop} {stOf : Fin (dt.nv + 1) → TapeSt dt A R P I} {bOf : Fin dt.nv → Prop} (hstN : dt.IxWritesNew stOf bOf) (j : Fin dt.nv) : (stOf (Fin.last dt.nv)).new (dt.varList.get j) v ↔ bOf j

At the marker, a variable's new cell is the verdict of its own position: it is written there, and no later position writes it, the enumeration being duplicate-free.

theorem DescriptiveComplexity.Draw.Data.ixNew_last_of_false {L : FirstOrder.Language} (dt : Data L) {A R P I : Type} {v : Univ A R P dt.KIx dt.dd → Prop} {stOf : Fin (dt.nv + 1) → TapeSt dt A R P I} {bOf : Fin dt.nv → Prop} (hstN : dt.IxWritesNew stOf bOf) (hbOf : ∀ (j : Fin dt.nv), ¬bOf j) (i : dt.d.B.ι) : ¬(stOf (Fin.last dt.nv)).new i v

At an address every position rejects, the marker's new cells are all clear – the junk legs (DescriptiveComplexity.Draw.Data.ixVarLegFail_reachesIn, DescriptiveComplexity.Draw.Data.ixVarLegUngated_reachesIn) store False, which is what the stage dictionary holds at an address that encodes no tuple.

The spine's semantic reading

theorem DescriptiveComplexity.Draw.Data.ixNew_last_next_at {L : FirstOrder.Language} (dt : Data L) {A R : Type} [Fintype dt.SlotIx] [LinearOrder A] [LinearOrder R] {P : Type} [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} (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)) (hix : IsLinOrd F.le) (hblkP : ∀ (u : I), F.blk u = tagBlk (elt u).1) {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) [Nonempty A] [L.IsRelational] [L.Structure A] (hpassEnc : ∀ (vi : dt.VarIx) (stV : TapeSt dt A R P I) (ℓ : Fin (dt.nIn vi)), dt.ixIGPassP F PR.zero PR.one vi stV ℓ ↔ IsEnc dt.ly PR.zero PR.one (wmBlk (ixAddr elt stV.val) (Tag.arg (toLex (dt.igBlk vi ℓ))))) [LinearOrder (dt.X.Map A)] {v : Univ A R P dt.KIx dt.dd → Prop} {ιV : Type} [LinearOrder ιV] [Finite ιV] (mV : ιV → I → Prop) (hUse : ∀ (a : ιV) (u : I), mV a u → Use u) (hlin : IsLinOrd WMLe) (hord : ∀ (x y : Univ A R P dt.KIx dt.dd), WMLe x y ↔ tagTupleLe x y) {a₀ aT : ιV} (hbotV : ∀ (a : ιV), a₀ ≤ a) (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')) (hKin : ∀ (a : ιV) (t : Tag R P dt.KIx) (w : Fin dt.dd → A), ixAddr elt (mV a) (t, w) → ∃ (j : Fin dt.ki), t = argIn dt.ko j) (hTop : ∀ (u : Univ A R P dt.KIx dt.dd), dt.InnerFull (fun (u : Univ A R P dt.KIx dt.dd) => tagBlk u.1) (ixAddr elt (mV aT)) u) (σ : dt.d.B.Assignment (dt.X.Map A)) {stOf : Fin (dt.nv + 1) → TapeSt dt A R P I} {bOf : Fin dt.nv → Prop} (j : Fin dt.nv) (semOfJ : (a : ιV) → (∀ (ℓ : Fin (dt.nIn (dt.varAt j))), dt.ixIGPassP F PR.zero PR.one (dt.varAt j) (dt.ixRoundSt (stOf j.castSucc) (mV a)) ℓ) → (b : Fin (dt.natOf (dt.varAt j))) → dt.IxKindSem PR.zero PR.one (dt.varAt j) (dt.ixRoundSt (stOf j.castSucc) (mV a)) elt (dt.kindOf (dt.varAt j) b)) (fG : dt.CtlIx → A) (hstN : dt.IxWritesNew stOf bOf) (hmirOf : (stOf j.castSucc).mir = (stOf 0).mir) (holdOf : (stOf j.castSucc).old = (stOf 0).old) (hbj : bOf j ↔ dt.accVerdict PR.one (dt.polOf (dt.varAt j)) ((dt.varArgsOf PR.zero PR.one (dt.varAt j)).postFold (ixRoundFX F hinj hhasP heltP (dt.varAt j) (stOf j.castSucc) v mV semOfJ (ixVarFM F hinj hhasP heltP (dt.varAt j) (stOf j.castSucc) v mV semOfJ fG aT) aT) (dt.ixBack F.toLayout PR.zero PR.one ⋯ (dt.ixRoundSt (stOf j.castSucc) (mV aT)) v))) (mbW : Fin (dt.arOf (dt.varAt j)) → dt.X.Map A) (hmb : ∀ (ℓ : Fin (dt.arOf (dt.varAt j))), dt.ixMirBlk (stOf 0) (Fin.castLE ⋯ ℓ) = encMap dt.ly PR.zero PR.one (mbW ℓ)) {Below : (Univ A R P dt.KIx dt.dd → Prop) → Prop} (hdict : ∀ (iv : dt.d.B.ι) (x : Fin (dt.d.B.arity iv) → dt.X.Map A), Below (tupAddr dt.ly PR.zero PR.one ⋯ x) → ((stOf 0).old iv (tupAddr dt.ly PR.zero PR.one ⋯ x) ↔ σ iv x)) (hbelow : ∀ (a : ιV) (iv : dt.d.B.ι) (ts : Fin (dt.d.B.arity iv) → Fin (dt.nOf (dt.varAt j))), Below (ixAddr elt (dt.ixStageTgt F hhasP (dt.varAt j) ts (have __src := dt.ixRoundSt (stOf j.castSucc) (mV a); { mir := __src.mir, tgt := __src.tgt, sav := ixMark elt v, val := __src.val, old := __src.old, new := __src.new, wk := __src.wk, bot := __src.bot, ltp := __src.ltp }) (dt.d.B.arity iv)))) (hordP : ∀ (p q : dt.X.Map A), p ≤ q ↔ p ≤ q) (hsem : ∀ (a : ιV) (hp : ∀ (ℓ : Fin (dt.nIn (dt.varAt j))), dt.ixIGPassP F PR.zero PR.one (dt.varAt j) (dt.ixRoundSt (stOf j.castSucc) (mV a)) ℓ) (b : Fin (dt.natOf (dt.varAt j))) (hmb' : ∀ (ℓ : Fin (dt.arOf (dt.varAt j))), wmBlk (ixAddr elt (dt.ixRoundSt (stOf j.castSucc) (mV a)).mir) (Tag.arg (toLex (Sum.inl (Fin.castLE ⋯ ℓ)))) = encMap dt.ly PR.zero PR.one (mbW ℓ)), semOfJ a hp b = dt.ixPassSem F hpassEnc (dt.varAt j) (dt.ixRoundSt (stOf j.castSucc) (mV a)) hp mbW hmb' b) : (stOf (Fin.last dt.nv)).new (dt.varList.get j) v ↔ dt.d.next σ (dt.varList.get j) mbW

After the spine, one variable's new cell holds its own step of the iteration – the per-position form: only the position of that variable, its pack and its verdict are named, so an address where other positions are junk is covered too (which is what a sweep needs, the gates being per variable).

theorem DescriptiveComplexity.Draw.Data.ixNew_last_next {L : FirstOrder.Language} (dt : Data L) {A R : Type} [Fintype dt.SlotIx] [LinearOrder A] [LinearOrder R] {P : Type} [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} (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)) (hix : IsLinOrd F.le) (hblkP : ∀ (u : I), F.blk u = tagBlk (elt u).1) {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) [Nonempty A] [L.IsRelational] [L.Structure A] (hpassEnc : ∀ (vi : dt.VarIx) (stV : TapeSt dt A R P I) (ℓ : Fin (dt.nIn vi)), dt.ixIGPassP F PR.zero PR.one vi stV ℓ ↔ IsEnc dt.ly PR.zero PR.one (wmBlk (ixAddr elt stV.val) (Tag.arg (toLex (dt.igBlk vi ℓ))))) [LinearOrder (dt.X.Map A)] {v : Univ A R P dt.KIx dt.dd → Prop} {ιV : Type} [LinearOrder ιV] [Finite ιV] (mV : ιV → I → Prop) (hUse : ∀ (a : ιV) (u : I), mV a u → Use u) (hlin : IsLinOrd WMLe) (hord : ∀ (x y : Univ A R P dt.KIx dt.dd), WMLe x y ↔ tagTupleLe x y) {a₀ aT : ιV} (hbotV : ∀ (a : ιV), a₀ ≤ a) (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')) (hKin : ∀ (a : ιV) (t : Tag R P dt.KIx) (w : Fin dt.dd → A), ixAddr elt (mV a) (t, w) → ∃ (j : Fin dt.ki), t = argIn dt.ko j) (hTop : ∀ (u : Univ A R P dt.KIx dt.dd), dt.InnerFull (fun (u : Univ A R P dt.KIx dt.dd) => tagBlk u.1) (ixAddr elt (mV aT)) u) (σ : dt.d.B.Assignment (dt.X.Map A)) {stOf : Fin (dt.nv + 1) → TapeSt dt A R P I} {bOf : Fin dt.nv → Prop} (semOfJ : (j : Fin dt.nv) → (a : ιV) → (∀ (ℓ : Fin (dt.nIn (dt.varAt j))), dt.ixIGPassP F PR.zero PR.one (dt.varAt j) (dt.ixRoundSt (stOf j.castSucc) (mV a)) ℓ) → (b : Fin (dt.natOf (dt.varAt j))) → dt.IxKindSem PR.zero PR.one (dt.varAt j) (dt.ixRoundSt (stOf j.castSucc) (mV a)) elt (dt.kindOf (dt.varAt j) b)) (fGOf : Fin dt.nv → dt.CtlIx → A) (hstN : dt.IxWritesNew stOf bOf) (hmirOf : ∀ (k : Fin (dt.nv + 1)), (stOf k).mir = (stOf 0).mir) (holdOf : ∀ (k : Fin (dt.nv + 1)), (stOf k).old = (stOf 0).old) (hbOf : ∀ (j : Fin dt.nv), bOf j ↔ dt.accVerdict PR.one (dt.polOf (dt.varAt j)) ((dt.varArgsOf PR.zero PR.one (dt.varAt j)).postFold (ixRoundFX F hinj hhasP heltP (dt.varAt j) (stOf j.castSucc) v mV (semOfJ j) (ixVarFM F hinj hhasP heltP (dt.varAt j) (stOf j.castSucc) v mV (semOfJ j) (fGOf j) aT) aT) (dt.ixBack F.toLayout PR.zero PR.one ⋯ (dt.ixRoundSt (stOf j.castSucc) (mV aT)) v))) (pt : Fin dt.ko → dt.X.Map A) (hpt : ∀ (k : Fin dt.ko), dt.ixMirBlk (stOf 0) k = encMap dt.ly PR.zero PR.one (pt k)) {Below : (Univ A R P dt.KIx dt.dd → Prop) → Prop} (hdict : ∀ (iv : dt.d.B.ι) (x : Fin (dt.d.B.arity iv) → dt.X.Map A), Below (tupAddr dt.ly PR.zero PR.one ⋯ x) → ((stOf 0).old iv (tupAddr dt.ly PR.zero PR.one ⋯ x) ↔ σ iv x)) (hbelow : ∀ (j : Fin dt.nv) (a : ιV) (iv : dt.d.B.ι) (ts : Fin (dt.d.B.arity iv) → Fin (dt.nOf (dt.varAt j))), Below (ixAddr elt (dt.ixStageTgt F hhasP (dt.varAt j) ts (have __src := dt.ixRoundSt (stOf j.castSucc) (mV a); { mir := __src.mir, tgt := __src.tgt, sav := ixMark elt v, val := __src.val, old := __src.old, new := __src.new, wk := __src.wk, bot := __src.bot, ltp := __src.ltp }) (dt.d.B.arity iv)))) (hordP : ∀ (p q : dt.X.Map A), p ≤ q ↔ p ≤ q) (hsem : ∀ (j : Fin dt.nv) (a : ιV) (hp : ∀ (ℓ : Fin (dt.nIn (dt.varAt j))), dt.ixIGPassP F PR.zero PR.one (dt.varAt j) (dt.ixRoundSt (stOf j.castSucc) (mV a)) ℓ) (b : Fin (dt.natOf (dt.varAt j))) (hmb' : ∀ (ℓ : Fin (dt.arOf (dt.varAt j))), wmBlk (ixAddr elt (dt.ixRoundSt (stOf j.castSucc) (mV a)).mir) (Tag.arg (toLex (Sum.inl (Fin.castLE ⋯ ℓ)))) = encMap dt.ly PR.zero PR.one (pt (Fin.castLE ⋯ ℓ))), semOfJ j a hp b = dt.ixPassSem F hpassEnc (dt.varAt j) (dt.ixRoundSt (stOf j.castSucc) (mV a)) hp (fun (ℓ : Fin (dt.arOf (dt.varAt j))) => pt (Fin.castLE ⋯ ℓ)) hmb' b) (i : dt.d.B.ι) : (stOf (Fin.last dt.nv)).new i v ↔ dt.d.next σ i fun (ℓ : Fin (dt.d.B.arity i)) => pt (Fin.castLE ⋯ ℓ)

After the spine, every new track holds the next stage at the address's points. The position of a variable writes its verdict, which DescriptiveComplexity.Draw.Data.ixAccVerdict_next reads as DescriptiveComplexity.StepDef.next; the mirror and the dictionary ride the spine, so the semantic hypotheses need only be given at the entry state.

What a whole sweep leaves behind

The address's cell, in dictionary form

The semantic pack, transported along the spine

The per-position families, built

noncomputable def DescriptiveComplexity.Draw.Data.ixSpineNode {L : FirstOrder.Language} (dt : Data L) {A R : Type} [Fintype dt.SlotIx] [LinearOrder A] [LinearOrder R] {P : Type} [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) (f₀ : dt.CtlIx → A) (sem₀ : (j : Fin dt.nv) → (a : ιV) → (∀ (ℓ : Fin (dt.nIn (dt.varAt j))), dt.ixIGPassP F PR.zero PR.one (dt.varAt j) (dt.ixRoundSt st₀ (mV a)) ℓ) → (b : Fin (dt.natOf (dt.varAt j))) → dt.IxKindSem PR.zero PR.one (dt.varAt j) (dt.ixRoundSt st₀ (mV a)) elt (dt.kindOf (dt.varAt j) b)) (tOf : (j : Fin dt.nv) → Fin (dt.arOf (dt.varAt j)) → dt.X.Tag) : ℕ → (st : TapeSt dt A R P I) ×' st.mir = st₀.mir ×' (dt.CtlIx → A)

One node of the spine: the tape state, the proof that its mirror is still the address's – which is what lets the next node build its pack – and the control. The three have to be produced together: the pack a position's leg needs is typed at that position's state, and is available only because the mirror rode (ixSpineSem).

Equations

• One or more equations did not get rendered due to their size.
• dt.ixSpineNode F hinj hhasP heltP mV st₀ f₀ sem₀ tOf 0 = ⟨st₀, ⟨⋯, f₀⟩⟩

noncomputable def DescriptiveComplexity.Draw.Data.ixSpineStOf {L : FirstOrder.Language} (dt : Data L) {A R : Type} [Fintype dt.SlotIx] [LinearOrder A] [LinearOrder R] {P : Type} [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) (f₀ : dt.CtlIx → A) (sem₀ : (j : Fin dt.nv) → (a : ιV) → (∀ (ℓ : Fin (dt.nIn (dt.varAt j))), dt.ixIGPassP F PR.zero PR.one (dt.varAt j) (dt.ixRoundSt st₀ (mV a)) ℓ) → (b : Fin (dt.natOf (dt.varAt j))) → dt.IxKindSem PR.zero PR.one (dt.varAt j) (dt.ixRoundSt st₀ (mV a)) elt (dt.kindOf (dt.varAt j) b)) (tOf : (j : Fin dt.nv) → Fin (dt.arOf (dt.varAt j)) → dt.X.Tag) (k : Fin (dt.nv + 1)) : TapeSt dt A R P I

The tape family of the spine.

Equations

• dt.ixSpineStOf F hinj hhasP heltP mV st₀ f₀ sem₀ tOf k = (dt.ixSpineNode F hinj hhasP heltP mV st₀ f₀ sem₀ tOf ↑k).fst

The per-position families, threaded

noncomputable def DescriptiveComplexity.Draw.Data.ixSpineNodeT {L : FirstOrder.Language} (dt : Data L) {A R : Type} [Fintype dt.SlotIx] [LinearOrder A] [LinearOrder R] {P : Type} [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) (f₀ : dt.CtlIx → A) (sem₀ : (j : Fin dt.nv) → (a : ιV) → (∀ (ℓ : Fin (dt.nIn (dt.varAt j))), dt.ixIGPassP F PR.zero PR.one (dt.varAt j) (dt.ixRoundSt st₀ (mV a)) ℓ) → (b : Fin (dt.natOf (dt.varAt j))) → dt.IxKindSem PR.zero PR.one (dt.varAt j) (dt.ixRoundSt st₀ (mV a)) elt (dt.kindOf (dt.varAt j) b)) (tOf : (j : Fin dt.nv) → Fin (dt.arOf (dt.varAt j)) → dt.X.Tag) : ℕ → (st : TapeSt dt A R P I) ×' st.mir = st₀.mir ×' (dt.CtlIx → A)

One node of the spine, threaded: as DescriptiveComplexity.Draw.Data.ixSpineNode, with the leg's own exit state – SAV and TARGET as its VAL loop left them – instead of the normalized one. The mirror still rides, which is what makes the next position's pack exist.

Equations

• One or more equations did not get rendered due to their size.
• dt.ixSpineNodeT F hinj hhasP heltP mV st₀ f₀ sem₀ tOf 0 = ⟨st₀, ⟨⋯, f₀⟩⟩

noncomputable def DescriptiveComplexity.Draw.Data.ixSpineStOfT {L : FirstOrder.Language} (dt : Data L) {A R : Type} [Fintype dt.SlotIx] [LinearOrder A] [LinearOrder R] {P : Type} [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) (f₀ : dt.CtlIx → A) (sem₀ : (j : Fin dt.nv) → (a : ιV) → (∀ (ℓ : Fin (dt.nIn (dt.varAt j))), dt.ixIGPassP F PR.zero PR.one (dt.varAt j) (dt.ixRoundSt st₀ (mV a)) ℓ) → (b : Fin (dt.natOf (dt.varAt j))) → dt.IxKindSem PR.zero PR.one (dt.varAt j) (dt.ixRoundSt st₀ (mV a)) elt (dt.kindOf (dt.varAt j) b)) (tOf : (j : Fin dt.nv) → Fin (dt.arOf (dt.varAt j)) → dt.X.Tag) (k : Fin (dt.nv + 1)) : TapeSt dt A R P I

The threaded tape family of the spine.

Equations

• dt.ixSpineStOfT F hinj hhasP heltP mV st₀ f₀ sem₀ tOf k = (dt.ixSpineNodeT F hinj hhasP heltP mV st₀ f₀ sem₀ tOf ↑k).fst

theorem DescriptiveComplexity.Draw.Data.ixSpineStOfT_mir {L : FirstOrder.Language} (dt : Data L) {A R : Type} [Fintype dt.SlotIx] [LinearOrder A] [LinearOrder R] {P : Type} [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) (f₀ : dt.CtlIx → A) (sem₀ : (j : Fin dt.nv) → (a : ιV) → (∀ (ℓ : Fin (dt.nIn (dt.varAt j))), dt.ixIGPassP F PR.zero PR.one (dt.varAt j) (dt.ixRoundSt st₀ (mV a)) ℓ) → (b : Fin (dt.natOf (dt.varAt j))) → dt.IxKindSem PR.zero PR.one (dt.varAt j) (dt.ixRoundSt st₀ (mV a)) elt (dt.kindOf (dt.varAt j) b)) (tOf : (j : Fin dt.nv) → Fin (dt.arOf (dt.varAt j)) → dt.X.Tag) (k : Fin (dt.nv + 1)) : (dt.ixSpineStOfT F hinj hhasP heltP mV st₀ f₀ sem₀ tOf k).mir = st₀.mir

The mirror rides the threaded family too – by construction.

The per-position families, branched

The threaded family above runs the gated leg at every position, which a sweep cannot afford: it visits junk addresses too. The branched family takes whichever of the three legs each position's own gates call for (DescriptiveComplexity.Draw.Data.ixLegStB), and is otherwise the same recursion – the mirror still rides, because no leg writes it.

Its semantic parameter is not the entry state's pack transported: it is the conditioned family DescriptiveComplexity.Draw.Data.ixGatedSem inhabits – a pack at every gated position of every state, at every address. Conditioned, because at a junk position no pack exists (the argument blocks encode nothing there); quantified over the address as well, because the sweep runs this spine at v := w for an address w its own binders are fixed before. With that type the parameter is supplied outright at the top – fun w => dt.ixGatedSem hzo hlin mV – and no semantic assumption about a position survives in the run layer.

noncomputable def DescriptiveComplexity.Draw.Data.ixSpineNodeB {L : FirstOrder.Language} (dt : Data L) {A R : Type} [Fintype dt.SlotIx] [LinearOrder A] [LinearOrder R] {P : Type} [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) (f₀ : dt.CtlIx → A) (semB : (w : Univ A R P dt.KIx dt.dd → Prop) → (j : Fin dt.nv) → (st : TapeSt dt A R P I) → 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)) w ↑b) elt (dt.kindOf (dt.varAt j) b)) : ℕ → (st : TapeSt dt A R P I) ×' st.mir = st₀.mir ×' (dt.CtlIx → A)

One node of the spine, branched.

Equations

• One or more equations did not get rendered due to their size.
• dt.ixSpineNodeB F hinj hhasP heltP mV st₀ f₀ semB 0 = ⟨st₀, ⟨⋯, f₀⟩⟩

noncomputable def DescriptiveComplexity.Draw.Data.ixSpineStOfB {L : FirstOrder.Language} (dt : Data L) {A R : Type} [Fintype dt.SlotIx] [LinearOrder A] [LinearOrder R] {P : Type} [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) (f₀ : dt.CtlIx → A) (semB : (w : Univ A R P dt.KIx dt.dd → Prop) → (j : Fin dt.nv) → (st : TapeSt dt A R P I) → 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)) w ↑b) elt (dt.kindOf (dt.varAt j) b)) (k : Fin (dt.nv + 1)) : TapeSt dt A R P I

The branched tape family of the spine.

Equations

• dt.ixSpineStOfB F hinj hhasP heltP mV st₀ f₀ semB k = (dt.ixSpineNodeB F hinj hhasP heltP mV st₀ f₀ semB ↑k).fst

noncomputable def DescriptiveComplexity.Draw.Data.ixSpineFsOfB {L : FirstOrder.Language} (dt : Data L) {A R : Type} [Fintype dt.SlotIx] [LinearOrder A] [LinearOrder R] {P : Type} [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) (f₀ : dt.CtlIx → A) (semB : (w : Univ A R P dt.KIx dt.dd → Prop) → (j : Fin dt.nv) → (st : TapeSt dt A R P I) → 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)) w ↑b) elt (dt.kindOf (dt.varAt j) b)) (k : Fin (dt.nv + 1)) : dt.CtlIx → A

The branched control family of the spine.

Equations

• dt.ixSpineFsOfB F hinj hhasP heltP mV st₀ f₀ semB k = (dt.ixSpineNodeB F hinj hhasP heltP mV st₀ f₀ semB ↑k).snd.snd

theorem DescriptiveComplexity.Draw.Data.ixSpineStOfB_mir {L : FirstOrder.Language} (dt : Data L) {A R : Type} [Fintype dt.SlotIx] [LinearOrder A] [LinearOrder R] {P : Type} [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) (f₀ : dt.CtlIx → A) (semB : (w : Univ A R P dt.KIx dt.dd → Prop) → (j : Fin dt.nv) → (st : TapeSt dt A R P I) → 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)) w ↑b) elt (dt.kindOf (dt.varAt j) b)) (k : Fin (dt.nv + 1)) : (dt.ixSpineStOfB F hinj hhasP heltP mV st₀ f₀ semB k).mir = st₀.mir

The mirror rides the branched family – by construction.

theorem DescriptiveComplexity.Draw.Data.ixSpineStOfB_wk {L : FirstOrder.Language} (dt : Data L) {A R : Type} [Fintype dt.SlotIx] [LinearOrder A] [LinearOrder R] {P : Type} [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) (f₀ : dt.CtlIx → A) (semB : (w : Univ A R P dt.KIx dt.dd → Prop) → (j : Fin dt.nv) → (st : TapeSt dt A R P I) → 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)) w ↑b) elt (dt.kindOf (dt.varAt j) b)) (k : Fin (dt.nv + 1)) : (dt.ixSpineStOfB F hinj hhasP heltP mV st₀ f₀ semB k).wk = st₀.wk

The marker rides the branched family: no leg writes the working register, so the hwkOf a spine asks for is the entry state's.

theorem DescriptiveComplexity.Draw.Data.ixSpineStOfB_bot {L : FirstOrder.Language} (dt : Data L) {A R : Type} [Fintype dt.SlotIx] [LinearOrder A] [LinearOrder R] {P : Type} [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) (f₀ : dt.CtlIx → A) (semB : (w : Univ A R P dt.KIx dt.dd → Prop) → (j : Fin dt.nv) → (st : TapeSt dt A R P I) → 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)) w ↑b) elt (dt.kindOf (dt.varAt j) b)) (k : Fin (dt.nv + 1)) : (dt.ixSpineStOfB F hinj hhasP heltP mV st₀ f₀ semB k).bot = st₀.bot

The bottom mark rides the branched family – the hbotOf a spine asks for.

theorem DescriptiveComplexity.Draw.Data.ixSpineStOfB_old {L : FirstOrder.Language} (dt : Data L) {A R : Type} [Fintype dt.SlotIx] [LinearOrder A] [LinearOrder R] {P : Type} [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) (f₀ : dt.CtlIx → A) (semB : (w : Univ A R P dt.KIx dt.dd → Prop) → (j : Fin dt.nv) → (st : TapeSt dt A R P I) → 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)) w ↑b) elt (dt.kindOf (dt.varAt j) b)) (k : Fin (dt.nv + 1)) : (dt.ixSpineStOfB F hinj hhasP heltP mV st₀ f₀ semB k).old = st₀.old

The dictionary rides the branched family: no leg of the evaluation writes the old tracks, so the stage the spine reads at its last checkpoint is the stage it was entered with. This is what lets a guessing program discharge the output's hdict: what its guess wrote is what the verdict is read against.

noncomputable def DescriptiveComplexity.Draw.Data.ixSpineSemOfB {L : FirstOrder.Language} (dt : Data L) {A R : Type} [Fintype dt.SlotIx] [LinearOrder A] [LinearOrder R] {P : Type} [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) (f₀ : dt.CtlIx → A) (semB : (w : Univ A R P dt.KIx dt.dd → Prop) → (j : Fin dt.nv) → (st : TapeSt dt A R P I) → 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)) w ↑b) elt (dt.kindOf (dt.varAt j) b)) (j : Fin dt.nv) (hg : dt.ixGatedAt F j (dt.ixSpineStOfB F hinj hhasP heltP mV st₀ f₀ semB j.castSucc)) (p : dt.IxScratch A R P I) (a : ιV) (hp : ∀ (ℓ : Fin (dt.nIn (dt.varAt j))), dt.ixIGPassP F PR.zero PR.one (dt.varAt j) (ixVarRdSt (dt.ixSpineStOfB F hinj hhasP heltP mV st₀ f₀ semB j.castSucc) 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 (dt.ixSpineStOfB F hinj hhasP heltP mV st₀ f₀ semB j.castSucc) p (mV a)) v ↑b) elt (dt.kindOf (dt.varAt j) b)

The packs of the branched family: the parameter's own, at the position's state – the gate being what makes them exist.

Equations

• dt.ixSpineSemOfB F hinj hhasP heltP mV st₀ f₀ semB j hg p a hp b = semB v j (dt.ixSpineStOfB F hinj hhasP heltP mV st₀ f₀ semB j.castSucc) hg p a hp b

theorem DescriptiveComplexity.Draw.Data.ixSpineFsOfB_succ {L : FirstOrder.Language} (dt : Data L) {A R : Type} [Fintype dt.SlotIx] [LinearOrder A] [LinearOrder R] {P : Type} [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) (f₀ : dt.CtlIx → A) (semB : (w : Univ A R P dt.KIx dt.dd → Prop) → (j : Fin dt.nv) → (st : TapeSt dt A R P I) → 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)) w ↑b) elt (dt.kindOf (dt.varAt j) b)) (j : Fin dt.nv) : dt.ixSpineFsOfB F hinj hhasP heltP mV st₀ f₀ semB j.succ = dt.ixLegCtlB F hinj hhasP heltP mV j (dt.ixSpineStOfB F hinj hhasP heltP mV st₀ f₀ semB j.castSucc) (dt.ixSpineSemOfB F hinj hhasP heltP mV st₀ f₀ semB j) (dt.ixSpineFsOfB F hinj hhasP heltP mV st₀ f₀ semB j.castSucc)

The branched control's cover equation – DescriptiveComplexity.Draw.Data.nexIxSpineB_reachesIn's hfs.

theorem DescriptiveComplexity.Draw.Data.ixSpineStOfB_succ {L : FirstOrder.Language} (dt : Data L) {A R : Type} [Fintype dt.SlotIx] [LinearOrder A] [LinearOrder R] {P : Type} [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) (f₀ : dt.CtlIx → A) (semB : (w : Univ A R P dt.KIx dt.dd → Prop) → (j : Fin dt.nv) → (st : TapeSt dt A R P I) → 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)) w ↑b) elt (dt.kindOf (dt.varAt j) b)) (j : Fin dt.nv) : dt.ixSpineStOfB F hinj hhasP heltP mV st₀ f₀ semB j.succ = dt.ixLegStB F hinj hhasP heltP mV j (dt.ixSpineStOfB F hinj hhasP heltP mV st₀ f₀ semB j.castSucc) (dt.ixSpineSemOfB F hinj hhasP heltP mV st₀ f₀ semB j) (dt.ixSpineFsOfB F hinj hhasP heltP mV st₀ f₀ semB j.castSucc)

The branched tape's cover equation – DescriptiveComplexity.Draw.Data.nexIxSpineB_reachesIn's hst.

The branched spine's dictionary at one address

Gating is per variable, and so is the reading: at an address whose blocks below a variable's arity all encode points, that variable's cell holds one step of the iteration there; where one of them does not, the position takes an ungated leg, writes False, and the dictionary is False too. Nothing is assumed of the other variables' blocks – which is what a sweep needs, since it passes every address.

theorem DescriptiveComplexity.Draw.Data.ixOutAcc_iff_out {L : FirstOrder.Language} (dt : Data L) {A R : Type} [Fintype dt.SlotIx] [LinearOrder A] [LinearOrder R] {P : Type} [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} (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)) (hix : IsLinOrd F.le) (hblkP : ∀ (u : I), F.blk u = tagBlk (elt u).1) {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) [Nonempty A] [L.IsRelational] [L.Structure A] (hpassEnc : ∀ (vi : dt.VarIx) (stV : TapeSt dt A R P I) (ℓ : Fin (dt.nIn vi)), dt.ixIGPassP F PR.zero PR.one vi stV ℓ ↔ IsEnc dt.ly PR.zero PR.one (wmBlk (ixAddr elt stV.val) (Tag.arg (toLex (dt.igBlk vi ℓ))))) [LinearOrder (dt.X.Map A)] {v : Univ A R P dt.KIx dt.dd → Prop} {ιV : Type} [LinearOrder ιV] [Finite ιV] (mV : ιV → I → Prop) (hUse : ∀ (a : ιV) (u : I), mV a u → Use u) (hlin : IsLinOrd WMLe) (hord : ∀ (x y : Univ A R P dt.KIx dt.dd), WMLe x y ↔ tagTupleLe x y) {a₀ aT : ιV} (hbotV : ∀ (a : ιV), a₀ ≤ a) (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')) (hKin : ∀ (a : ιV) (t : Tag R P dt.KIx) (w : Fin dt.dd → A), ixAddr elt (mV a) (t, w) → ∃ (jj : Fin dt.ki), t = argIn dt.ko jj) (hTop : ∀ (u : Univ A R P dt.KIx dt.dd), dt.InnerFull (fun (u : Univ A R P dt.KIx dt.dd) => tagBlk u.1) (ixAddr elt (mV aT)) u) (σ : dt.d.B.Assignment (dt.X.Map A)) (st : TapeSt dt A R P I) {Below : (Univ A R P dt.KIx dt.dd → Prop) → Prop} (hdict : ∀ (iv : dt.d.B.ι) (x : Fin (dt.d.B.arity iv) → dt.X.Map A), Below (tupAddr dt.ly PR.zero PR.one ⋯ x) → (st.old iv (tupAddr dt.ly PR.zero PR.one ⋯ x) ↔ σ iv x)) (hbelow : ∀ (a : ιV) (iv : dt.d.B.ι) (ts : Fin (dt.d.B.arity iv) → Fin (dt.nOf none)), Below (ixAddr elt (dt.ixStageTgt F hhasP none ts (have __src := dt.ixRoundSt st (mV a); { mir := __src.mir, tgt := __src.tgt, sav := ixMark elt v, val := __src.val, old := __src.old, new := __src.new, wk := __src.wk, bot := __src.bot, ltp := __src.ltp }) (dt.d.B.arity iv)))) (hordP : ∀ (p q : dt.X.Map A), p ≤ q ↔ p ≤ q) (tOf : Fin (dt.arOf none) → dt.X.Tag) (f₀ : dt.CtlIx → A) : (dt.varArgsOf PR.zero PR.one none).accBit (dt.ixOutCtl F hinj hhasP heltP mV st tOf (fun (a : ιV) (hp : ∀ (ℓ : Fin (dt.nIn none)), dt.ixIGPassP F PR.zero PR.one none (dt.ixRoundSt st (mV a)) ℓ) (b : Fin (dt.natOf none)) => dt.ixPassSem F hpassEnc none (dt.ixRoundSt st (mV a)) hp (fun (ℓ : Fin (dt.arOf none)) => ℓ.elim0) ⋯ b) f₀) ↔ dt.X.Map A ⊨ dt.d.out

The verdict the output's leg leaves is the output sentence, at the stage the tracks hold. The output variable is nullary, so its blocks encode the empty tuple and there is nothing to ask of them – which is why this is the one verdict a program can take at the address its head starts on. This is the hacc a run through the output's machinery (DescriptiveComplexity.Draw.Data.nexIxEvalOutB_reachesIn) asks for, and the reason the accepting bit says anything at all.

The sweep's families, over an arbitrary per-address leg

Everything the sweep's families need of an address's evaluation is what state and control it ends in. Taking those two as parameters makes the whole layer – the iteration, its two cover equations, and the ride lemmas that discharge reaches_sweep's hwkE/hmirE/hltpE – serve any evaluation: the spine as first built, its threaded twin, and the branched form a junk address will need.

noncomputable def DescriptiveComplexity.Draw.Data.ixSweepPairG {L : FirstOrder.Language} (dt : Data L) {A R P : Type} [FirstOrder.Language.wide.Structure (Univ A R P dt.KIx dt.dd)] [Finite A] [Finite R] [Finite P] {I : Type} {elt : I → Univ A R P dt.KIx dt.dd} [Finite dt.KIx] (stE : (Univ A R P dt.KIx dt.dd → Prop) → TapeSt dt A R P I → (dt.CtlIx → A) → TapeSt dt A R P I) (fsE : (Univ A R P dt.KIx dt.dd → Prop) → TapeSt dt A R P I → (dt.CtlIx → A) → dt.CtlIx → A) (hlin : IsLinOrd WMLe) (st₀ : TapeSt dt A R P I) (f₀ : dt.CtlIx → A) (w : Univ A R P dt.KIx dt.dd → Prop) : TapeSt dt A R P I × (dt.CtlIx → A)

The pair the sweep arrives at each address with: the base at the empty address, and at every increment the previous address's evaluation exit – its marker moved on and its mirror set to the new address, exactly the shape DescriptiveComplexity.Draw.Data.reaches_sweep demands.

Equations

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

noncomputable def DescriptiveComplexity.Draw.Data.ixSweepSWG {L : FirstOrder.Language} (dt : Data L) {A R P : Type} [FirstOrder.Language.wide.Structure (Univ A R P dt.KIx dt.dd)] [Finite A] [Finite R] [Finite P] {I : Type} {elt : I → Univ A R P dt.KIx dt.dd} [Finite dt.KIx] (stE : (Univ A R P dt.KIx dt.dd → Prop) → TapeSt dt A R P I → (dt.CtlIx → A) → TapeSt dt A R P I) (fsE : (Univ A R P dt.KIx dt.dd → Prop) → TapeSt dt A R P I → (dt.CtlIx → A) → dt.CtlIx → A) (hlin : IsLinOrd WMLe) (st₀ : TapeSt dt A R P I) (f₀ : dt.CtlIx → A) (w : Univ A R P dt.KIx dt.dd → Prop) : TapeSt dt A R P I

The sweep's tape family – reaches_sweep's SW.

Equations

• dt.ixSweepSWG stE fsE hlin st₀ f₀ w = (dt.ixSweepPairG stE fsE hlin st₀ f₀ w).1

noncomputable def DescriptiveComplexity.Draw.Data.ixSweepFSG {L : FirstOrder.Language} (dt : Data L) {A R P : Type} [FirstOrder.Language.wide.Structure (Univ A R P dt.KIx dt.dd)] [Finite A] [Finite R] [Finite P] {I : Type} {elt : I → Univ A R P dt.KIx dt.dd} [Finite dt.KIx] (stE : (Univ A R P dt.KIx dt.dd → Prop) → TapeSt dt A R P I → (dt.CtlIx → A) → TapeSt dt A R P I) (fsE : (Univ A R P dt.KIx dt.dd → Prop) → TapeSt dt A R P I → (dt.CtlIx → A) → dt.CtlIx → A) (hlin : IsLinOrd WMLe) (st₀ : TapeSt dt A R P I) (f₀ : dt.CtlIx → A) (w : Univ A R P dt.KIx dt.dd → Prop) : dt.CtlIx → A

The sweep's control family – reaches_sweep's FS.

Equations

• dt.ixSweepFSG stE fsE hlin st₀ f₀ w = (dt.ixSweepPairG stE fsE hlin st₀ f₀ w).2

noncomputable def DescriptiveComplexity.Draw.Data.ixSweepStEG {L : FirstOrder.Language} (dt : Data L) {A R P : Type} [FirstOrder.Language.wide.Structure (Univ A R P dt.KIx dt.dd)] [Finite A] [Finite R] [Finite P] {I : Type} {elt : I → Univ A R P dt.KIx dt.dd} [Finite dt.KIx] (stE : (Univ A R P dt.KIx dt.dd → Prop) → TapeSt dt A R P I → (dt.CtlIx → A) → TapeSt dt A R P I) (fsE : (Univ A R P dt.KIx dt.dd → Prop) → TapeSt dt A R P I → (dt.CtlIx → A) → dt.CtlIx → A) (hlin : IsLinOrd WMLe) (st₀ : TapeSt dt A R P I) (f₀ : dt.CtlIx → A) (w : Univ A R P dt.KIx dt.dd → Prop) : TapeSt dt A R P I

The state the sweep leaves each address in – reaches_sweep's stE.

Equations

• dt.ixSweepStEG stE fsE hlin st₀ f₀ w = stE w (dt.ixSweepSWG stE fsE hlin st₀ f₀ w) (dt.ixSweepFSG stE fsE hlin st₀ f₀ w)

theorem DescriptiveComplexity.Draw.Data.ixSweepSWG_bot {L : FirstOrder.Language} (dt : Data L) {A R P : Type} [FirstOrder.Language.wide.Structure (Univ A R P dt.KIx dt.dd)] [Finite A] [Finite R] [Finite P] {I : Type} {elt : I → Univ A R P dt.KIx dt.dd} [Finite dt.KIx] (stE : (Univ A R P dt.KIx dt.dd → Prop) → TapeSt dt A R P I → (dt.CtlIx → A) → TapeSt dt A R P I) (fsE : (Univ A R P dt.KIx dt.dd → Prop) → TapeSt dt A R P I → (dt.CtlIx → A) → dt.CtlIx → A) (hlin : IsLinOrd WMLe) (st₀ : TapeSt dt A R P I) (f₀ : dt.CtlIx → A) : (dt.ixSweepSWG stE fsE hlin st₀ f₀ fun (x : Univ A R P dt.KIx dt.dd) => False) = st₀

theorem DescriptiveComplexity.Draw.Data.ixSweepSWG_incr {L : FirstOrder.Language} (dt : Data L) {A R P : Type} [FirstOrder.Language.wide.Structure (Univ A R P dt.KIx dt.dd)] [Finite A] [Finite R] [Finite P] {I : Type} {elt : I → Univ A R P dt.KIx dt.dd} [Finite dt.KIx] (stE : (Univ A R P dt.KIx dt.dd → Prop) → TapeSt dt A R P I → (dt.CtlIx → A) → TapeSt dt A R P I) (fsE : (Univ A R P dt.KIx dt.dd → Prop) → TapeSt dt A R P I → (dt.CtlIx → A) → dt.CtlIx → A) (hlin : IsLinOrd WMLe) (st₀ : TapeSt dt A R P I) (f₀ : dt.CtlIx → A) {w w' : Univ A R P dt.KIx dt.dd → Prop} (hi : WMIncr WMLe w w') : dt.ixSweepSWG stE fsE hlin st₀ f₀ w' = have __src := dt.atSt (dt.ixSweepStEG stE fsE hlin st₀ f₀ w) w'; { mir := ixMark elt w', tgt := __src.tgt, sav := __src.sav, val := __src.val, old := __src.old, new := __src.new, wk := __src.wk, bot := __src.bot, ltp := __src.ltp }

The tape's cover equation – reaches_sweep's hSW, verbatim.

The sweep's families

The stage atom's restore, as an algebra

DescriptiveComplexity.Draw.Data.stageEndSt st v = { st with sav := v, tgt := v }: the random access writes the home address into SAV and TARGET whatever they held, so a stage atom is transparent exactly when they held it already – which is what ixStageEndSt_eq's two hypotheses say, and why they are not a proof artifact.

Closing the sweep's gap by “reading the mirror” therefore means threading that normalization rather than assuming it away: an atom's exit state is ixStageEndSt st v, and the layers above carry it. These are the equations that threading needs; they are all definitional, which is what makes the propagation mechanical.