What the spine does to the tape at one address

DescriptiveComplexity.Draw.Data.evalSpine_run takes the per-position tape family stOf as a parameter, tied together by one cover equation per position (stOf j.succ = postVarSt …). This file reads that family: what the whole spine leaves on the tape at the address it was run at.

Two halves, both by the same induction along the positions:

• everything but val and the marker's new cells rides – the stage dictionary, the mirror and the three markers are the same at every position (spineRide, and the named corollaries): the spine writes only the cell it stands on, which is why the next address's leg may assume the same dictionary;
• the marker's new cell of a variable is that variable's verdict (new_last_get): the write happens at the position the variable sits at, and no later position touches it – the enumeration DescriptiveComplexity.Draw.Data.varList being Finset.univ.toList, hence duplicate-free and complete (exists_varList_get).

Joined with DescriptiveComplexity.Draw.Data.accVerdict_next, that is new_last_next: after the spine, the new track of every variable holds, at the address, one step of the iteration at the address's points – the per-address obligation the sweep's induction carries.

One obstacle sits between this and the instantiation, and the last section removes it: a position's semantic pack is typed at that position's tape state, so a family of packs looks like it has to be built position by position – while the pack can only be built once the mirror invariant is known, which is what the family's own defining equations give. KindSem in fact reads the state only through the levels' register sets (lvSet_congr) and the pass condition through the VAL register alone (igPassP_congr, igPassP_roundSt – a file test reads the block mark, the VAL digit, the padding mark and the names, all of which either ride or are the tape's permanent geometry). So one pack transports along the whole spine (kindSemCast, packaged as spineSem), and its content survives the transport (kindSemCast_mkKindSem, passW_congr, kindSemCast_passSem, packaged as spineSem_passSem) – which is what discharges each position's hsem.

With that, the families themselves are built, not assumed: spineNode recurses along the positions producing the tape state, the proof that its mirror is still the address's, and the control – the three together, because the pack a position's leg needs is typed at that position's state and is available only because the mirror rode. Its projections spineStOf/spineFsOf/spineSemOf satisfy spineStOf_succ and spineFsOf_succ, which are the hst and hfs DescriptiveComplexity.Draw.Data.evalSpine_run asks for.

One scale up, the same is done for the sweep: sweepSW/sweepFS are the pair the sweep arrives at each address with – with sweepStE_wk, sweepStE_mir and sweepStE_ltp discharging three of the four remaining obligations of DescriptiveComplexity.Draw.Data.reaches_sweep, and eq_of_sweepSW_sav recording why the fourth (hspine) cannot be met until the program refreshes SAV and TARGET at each address – an iteration along the addresses (addrIter), because the control accumulates even though the tape's writes are local – and sweepSW_incr/sweepFS_incr are exactly DescriptiveComplexity.Draw.Data.reaches_sweep's hSW and hFS.

On top of it, the same statement in the form the next sweep reads its input in – new_last_trackOf at an address whose blocks encode a tuple, new_last_trackOf_of_junk where they do not, both sides being empty there – and the sweep itself: sweep_new, the address-by-address induction (DescriptiveComplexity.holds_of_wideRounds) saying a sweep rewrites the new tracks of exactly the addresses it has passed, everything else still carrying what it started with.

Iterating along the addresses

The sweep's families cannot both be written in closed form: the tape's new tracks are local to the address a leg stands on – sweep_new is their closed form – but the control threads, a leg's exit control being its entry control transformed. So the pair is defined by an iteration along the address order, which is DescriptiveComplexity.Draw.iterOrd at the linear order the addresses already carry (DescriptiveComplexity.isLinOrd_wmSetLe, turned into an instance locally – the order must never be an ambient instance on α → Prop, which carries Pi's own).

The successor is named rather than quantified (wmNext): a step of iterOrd is indexed by the address it leaves, while the state it produces mentions the one it arrives at.

noncomputable def DescriptiveComplexity.Draw.wmNext {α : Type} [Finite α] {Le : α → α → Prop} (h : IsLinOrd Le) (w : α → Prop) : α → Prop

The next address, chosen: the increment where one exists, the address itself at the full set (where the sweep has ended).

Equations

• DescriptiveComplexity.Draw.wmNext h w = if hx : ∃ (x : α), ¬w x then ⋯.choose else w

theorem DescriptiveComplexity.Draw.wmNext_eq {α : Type} [Finite α] {Le : α → α → Prop} (h : IsLinOrd Le) {w w' : α → Prop} (hi : WMIncr Le w w') : wmNext h w = w'

At an address with an increment, wmNext is it – the increment being unique.

noncomputable def DescriptiveComplexity.Draw.addrIter {α : Type} {Le : α → α → Prop} {Q' : Type u_1} (h : IsLinOrd (WMSetLe Le)) (init : Q') (step : (α → Prop) → Q' → Q') (w : α → Prop) : Q'

A value iterated along the addresses: the base at the empty address, one step per increment.

Equations

• DescriptiveComplexity.Draw.addrIter h init step w = DescriptiveComplexity.Draw.iterOrd init step w

theorem DescriptiveComplexity.Draw.addrIter_bot {α : Type} [Finite α] {Le : α → α → Prop} {Q' : Type u_1} (hL : IsLinOrd Le) (h : IsLinOrd (WMSetLe Le)) (init : Q') (step : (α → Prop) → Q' → Q') : (addrIter h init step fun (x : α) => False) = init

At the empty address the iteration is the base.

theorem DescriptiveComplexity.Draw.addrIter_incr {α : Type} [Finite α] {Le : α → α → Prop} {Q' : Type u_1} (hL : IsLinOrd Le) (h : IsLinOrd (WMSetLe Le)) {w w' : α → Prop} (hi : WMIncr Le w w') (init : Q') (step : (α → Prop) → Q' → Q') : addrIter h init step w' = step w (addrIter h init step w)

Across an increment the iteration steps once, at the address it leaves.

The enumeration of the variables

theorem DescriptiveComplexity.Draw.Data.exists_varList_get {L : FirstOrder.Language} (dt : Data L) (i : dt.d.B.ι) : ∃ (j : Fin dt.nv), dt.varList.get j = i

The enumeration lists every variable.

theorem DescriptiveComplexity.Draw.Data.varList_nodup {L : FirstOrder.Language} (dt : Data L) : dt.varList.Nodup

The enumeration lists each variable once.

theorem DescriptiveComplexity.Draw.Data.varList_get_inj {L : FirstOrder.Language} {dt : Data L} {j j' : Fin dt.nv} (h : dt.varList.get j = dt.varList.get j') : j = j'

Two positions carrying the same variable are the same position.

One position's write

theorem DescriptiveComplexity.Draw.Data.new_postVarSt {L : FirstOrder.Language} (dt : Data L) {A R : Type} {v : Univ A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd → Prop} (st : TapeStD dt A R (OuterPh (EvalPh dt.nv dt.PMF))) (m : Univ A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd → Prop) (i' i : dt.d.B.ι) (b : Prop) (r : Univ A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd → Prop) : (dt.postVarSt v st m i b).new i' r = if i' = i ∧ r = v then b else st.new i' r

What a position writes: the variable's cell at the marker, nothing else.

The spine's writes

@[reducible, inline]

abbrev DescriptiveComplexity.Draw.Data.WritesNew {L : FirstOrder.Language} (dt : Data L) {A R : Type} {v : Univ A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd → Prop} (stOf : Fin (dt.nv + 1) → TapeStD dt A R (OuterPh (EvalPh dt.nv dt.PMF))) (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.postVarSt 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.legStB_new).

Equations

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

theorem DescriptiveComplexity.Draw.Data.spineRide {L : FirstOrder.Language} (dt : Data L) {A R : Type} {v : Univ A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd → Prop} {mOf : Fin dt.nv → Univ A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd → Prop} {stOf : Fin (dt.nv + 1) → TapeStD dt A R (OuterPh (EvalPh dt.nv dt.PMF))} {bOf : Fin dt.nv → Prop} (hst : ∀ (j : Fin dt.nv), stOf j.succ = dt.postVarSt v (stOf j.castSucc) (mOf j) (dt.varList.get j) (bOf j)) {β : Sort u_1} (F : TapeStD dt A R (OuterPh (EvalPh dt.nv dt.PMF)) → β) (hF : ∀ (st : TapeStD dt A R (OuterPh (EvalPh dt.nv dt.PMF))) (m : Univ A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd → Prop) (i : dt.d.B.ι) (b : Prop), F (dt.postVarSt v st m i b) = F st) (k : Fin (dt.nv + 1)) : F (stOf k) = F (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.spine_mir {L : FirstOrder.Language} (dt : Data L) {A R : Type} {v : Univ A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd → Prop} {mOf : Fin dt.nv → Univ A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd → Prop} {stOf : Fin (dt.nv + 1) → TapeStD dt A R (OuterPh (EvalPh dt.nv dt.PMF))} {bOf : Fin dt.nv → Prop} (hst : ∀ (j : Fin dt.nv), stOf j.succ = dt.postVarSt 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.spine_new_off {L : FirstOrder.Language} (dt : Data L) {A R : Type} {v : Univ A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd → Prop} {stOf : Fin (dt.nv + 1) → TapeStD dt A R (OuterPh (EvalPh dt.nv dt.PMF))} {bOf : Fin dt.nv → Prop} (hstN : dt.WritesNew stOf bOf) (k : Fin (dt.nv + 1)) (i : dt.d.B.ι) {r : Univ A R (OuterPh (EvalPh dt.nv dt.PMF)) 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.new_last_get {L : FirstOrder.Language} (dt : Data L) {A R : Type} {v : Univ A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd → Prop} {stOf : Fin (dt.nv + 1) → TapeStD dt A R (OuterPh (EvalPh dt.nv dt.PMF))} {bOf : Fin dt.nv → Prop} (hstN : dt.WritesNew 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.new_last_of_false {L : FirstOrder.Language} (dt : Data L) {A R : Type} {v : Univ A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd → Prop} {stOf : Fin (dt.nv + 1) → TapeStD dt A R (OuterPh (EvalPh dt.nv dt.PMF))} {bOf : Fin dt.nv → Prop} (hstN : dt.WritesNew 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.varLegFail_run, DescriptiveComplexity.Draw.Data.varLegUngated_run) 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.new_last_next_at {L : FirstOrder.Language} (dt : Data L) {A R : Type} [Fintype dt.SlotIx] [LinearOrder A] [LinearOrder R] [LinearOrder (OuterPh (EvalPh dt.nv dt.PMF))] [FirstOrder.Language.wide.Structure (Univ A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd)] [Finite A] [Finite R] [Finite (OuterPh (EvalPh dt.nv dt.PMF))] {PR : Prog A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.CtlIx dt.SlotIx dt.KIx dt.dd} (RF : RegFile (Univ A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd)) [Nonempty A] [L.IsRelational] [L.Structure A] [LinearOrder (dt.X.Map A)] {v : Univ A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd → Prop} {ιV : Type} [LinearOrder ιV] [Finite ιV] (mV : ιV → Univ A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd → Prop) (hlin : IsLinOrd WMLe) (hord : ∀ (x y : Univ A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd), WMLe x y ↔ tagTupleLe x y) {a₀ aT : ιV} (hbotV : ∀ (a : ιV), a₀ ≤ a) (hmV0 : mV a₀ = fun (x : Univ A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd) => False) (hIncr : ∀ (a a' : ιV), a < a' → (∀ (b : ιV), ¬(a < b ∧ b < a')) → WMIncr WMLe (mV a) (mV a')) (hKin : ∀ (a : ιV) (t : Tag R (OuterPh (EvalPh dt.nv dt.PMF)) dt.KIx) (w : Fin dt.dd → A), mV a (t, w) → ∃ (j : Fin dt.ki), t = argIn dt.ko j) (hTop : ∀ (u : Univ A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd), dt.InnerFull (fun (u : Univ A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd) => tagBlk u.1) (mV aT) u) (σ : dt.d.B.Assignment (dt.X.Map A)) {stOf : Fin (dt.nv + 1) → TapeStD dt A R (OuterPh (EvalPh dt.nv dt.PMF))} {bOf : Fin dt.nv → Prop} (j : Fin dt.nv) (semOfJ : (a : ιV) → (∀ (ℓ : Fin (dt.nIn (dt.varAt j))), dt.igPassP RF PR.zero PR.one (dt.varAt j) (dt.roundSt (stOf j.castSucc) (mV a)) ℓ) → (b : Fin (dt.natOf (dt.varAt j))) → dt.KindSem PR.zero PR.one (dt.varAt j) (dt.roundSt (stOf j.castSucc) (mV a)) (dt.kindOf (dt.varAt j) b)) (fG : dt.CtlIx → A) (hstN : dt.WritesNew 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 (roundFX RF hord (dt.varAt j) (stOf j.castSucc) v mV semOfJ (varFM RF hord (dt.varAt j) (stOf j.castSucc) v mV semOfJ fG aT) aT) (dt.back RF.cell PR.zero PR.one ⋯ (dt.roundSt (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.mirBlk (stOf 0) (Fin.castLE ⋯ ℓ) = encMap dt.ly PR.zero PR.one (mbW ℓ)) {Below : (Univ A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd → Prop) → Prop} (hdict : ∀ (iv : dt.d.B.ι) (s : Univ A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd → Prop), Below s → ((stOf 0).old iv s ↔ trackOf dt.ly PR.zero PR.one ⋯ σ s)) (hbelow : ∀ (a : ιV) (iv : dt.d.B.ι) (ts : Fin (dt.d.B.arity iv) → Fin (dt.nOf (dt.varAt j))), Below (dt.stageTgtD PR.zero (dt.varAt j) iv ts (dt.roundSt (stOf j.castSucc) (mV a)) v (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.igPassP RF PR.zero PR.one (dt.varAt j) (dt.roundSt (stOf j.castSucc) (mV a)) ℓ) (b : Fin (dt.natOf (dt.varAt j))) (hmb' : ∀ (ℓ : Fin (dt.arOf (dt.varAt j))), wmBlk (dt.roundSt (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.passSem RF ⋯ hlin (dt.varAt j) (dt.roundSt (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.new_last_next {L : FirstOrder.Language} (dt : Data L) {A R : Type} [Fintype dt.SlotIx] [LinearOrder A] [LinearOrder R] [LinearOrder (OuterPh (EvalPh dt.nv dt.PMF))] [FirstOrder.Language.wide.Structure (Univ A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd)] [Finite A] [Finite R] [Finite (OuterPh (EvalPh dt.nv dt.PMF))] {PR : Prog A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.CtlIx dt.SlotIx dt.KIx dt.dd} (RF : RegFile (Univ A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd)) [Nonempty A] [L.IsRelational] [L.Structure A] [LinearOrder (dt.X.Map A)] {v : Univ A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd → Prop} {ιV : Type} [LinearOrder ιV] [Finite ιV] (mV : ιV → Univ A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd → Prop) (hlin : IsLinOrd WMLe) (hord : ∀ (x y : Univ A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd), WMLe x y ↔ tagTupleLe x y) {a₀ aT : ιV} (hbotV : ∀ (a : ιV), a₀ ≤ a) (hmV0 : mV a₀ = fun (x : Univ A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd) => False) (hIncr : ∀ (a a' : ιV), a < a' → (∀ (b : ιV), ¬(a < b ∧ b < a')) → WMIncr WMLe (mV a) (mV a')) (hKin : ∀ (a : ιV) (t : Tag R (OuterPh (EvalPh dt.nv dt.PMF)) dt.KIx) (w : Fin dt.dd → A), mV a (t, w) → ∃ (j : Fin dt.ki), t = argIn dt.ko j) (hTop : ∀ (u : Univ A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd), dt.InnerFull (fun (u : Univ A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd) => tagBlk u.1) (mV aT) u) (σ : dt.d.B.Assignment (dt.X.Map A)) {stOf : Fin (dt.nv + 1) → TapeStD dt A R (OuterPh (EvalPh dt.nv dt.PMF))} {bOf : Fin dt.nv → Prop} (semOfJ : (j : Fin dt.nv) → (a : ιV) → (∀ (ℓ : Fin (dt.nIn (dt.varAt j))), dt.igPassP RF PR.zero PR.one (dt.varAt j) (dt.roundSt (stOf j.castSucc) (mV a)) ℓ) → (b : Fin (dt.natOf (dt.varAt j))) → dt.KindSem PR.zero PR.one (dt.varAt j) (dt.roundSt (stOf j.castSucc) (mV a)) (dt.kindOf (dt.varAt j) b)) (fGOf : Fin dt.nv → dt.CtlIx → A) (hstN : dt.WritesNew 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 (roundFX RF hord (dt.varAt j) (stOf j.castSucc) v mV (semOfJ j) (varFM RF hord (dt.varAt j) (stOf j.castSucc) v mV (semOfJ j) (fGOf j) aT) aT) (dt.back RF.cell PR.zero PR.one ⋯ (dt.roundSt (stOf j.castSucc) (mV aT)) v))) (pt : Fin dt.ko → dt.X.Map A) (hpt : ∀ (k : Fin dt.ko), dt.mirBlk (stOf 0) k = encMap dt.ly PR.zero PR.one (pt k)) {Below : (Univ A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd → Prop) → Prop} (hdict : ∀ (iv : dt.d.B.ι) (s : Univ A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd → Prop), Below s → ((stOf 0).old iv s ↔ trackOf dt.ly PR.zero PR.one ⋯ σ s)) (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 (dt.stageTgtD PR.zero (dt.varAt j) iv ts (dt.roundSt (stOf j.castSucc) (mV a)) v (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.igPassP RF PR.zero PR.one (dt.varAt j) (dt.roundSt (stOf j.castSucc) (mV a)) ℓ) (b : Fin (dt.natOf (dt.varAt j))) (hmb' : ∀ (ℓ : Fin (dt.arOf (dt.varAt j))), wmBlk (dt.roundSt (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.passSem RF ⋯ hlin (dt.varAt j) (dt.roundSt (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.accVerdict_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

theorem DescriptiveComplexity.Draw.Data.sweep_new {L : FirstOrder.Language} (dt : Data L) {A R : Type} [FirstOrder.Language.wide.Structure (Univ A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd)] [Finite A] [Finite R] [Finite (OuterPh (EvalPh dt.nv dt.PMF))] [Finite dt.KIx] (hlin : IsLinOrd WMLe) {s₀ s₁ : Univ A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd → Prop} {SW stE : (Univ A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd → Prop) → TapeStD dt A R (OuterPh (EvalPh dt.nv dt.PMF))} {N : dt.d.B.ι → (Univ A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd → Prop) → Prop} (hat : ∀ (w : Univ A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd → Prop), WMSetLe WMLe s₀ w → WMSetLt WMLe w s₁ → ∀ (i : dt.d.B.ι), (stE w).new i w ↔ N i w) (hoff : ∀ (w : Univ A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd → Prop), WMSetLe WMLe s₀ w → WMSetLt WMLe w s₁ → ∀ (i : dt.d.B.ι) (r : Univ A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd → Prop), r ≠ w → ((stE w).new i r ↔ (SW w).new i r)) (hSW : ∀ (w w' : Univ A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd → Prop), WMIncr WMLe w w' → WMSetLe WMLe s₀ w → WMSetLe WMLe w' s₁ → SW w' = have __src := dt.atSt (stE w) w'; { mir := 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 }) (w : Univ A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd → Prop) : WMSetLe WMLe s₀ w → WMSetLe WMLe w s₁ → (∀ (i : dt.d.B.ι) (r : Univ A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd → Prop), WMSetLe WMLe s₀ r → WMSetLt WMLe r w → ((SW w).new i r ↔ N i r)) ∧ ∀ (i : dt.d.B.ι) (r : Univ A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd → Prop), ¬(WMSetLe WMLe s₀ r ∧ WMSetLt WMLe r w) → ((SW w).new i r ↔ (SW s₀).new i r)

A sweep rewrites the new tracks of exactly the addresses it has passed. The address-by-address induction (DescriptiveComplexity.holds_of_wideRounds) over the two facts one address contributes – its own cell now holds the target (hat, which new_last_next and new_last_of_false supply), every other cell is untouched (hoff, which spine_new_off supplies) – with the entry state of the next address read off the sweep's own tape family (hSW, the hSW of DescriptiveComplexity.Draw.Data.reaches_sweep).

Below the address reached, the tracks are the target; elsewhere they are still the sweep's initial ones. Stated for an arbitrary target family N, so the same lemma serves the stage sweep (N the dictionary of d.next σ) and any other.

The address's cell, in dictionary form

theorem DescriptiveComplexity.Draw.Data.new_last_trackOf_of_junk {L : FirstOrder.Language} (dt : Data L) {A R : Type} [Fintype dt.SlotIx] [LinearOrder A] {PR : Prog A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.CtlIx dt.SlotIx dt.KIx dt.dd} [L.Structure A] [LinearOrder (dt.X.Map A)] {v : Univ A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd → Prop} {stOf : Fin (dt.nv + 1) → TapeStD dt A R (OuterPh (EvalPh dt.nv dt.PMF))} {bOf : Fin dt.nv → Prop} (hstN : dt.WritesNew stOf bOf) (hbOf : ∀ (j : Fin dt.nv), ¬bOf j) (σ : dt.d.B.Assignment (dt.X.Map A)) (i : dt.d.B.ι) {ℓ₀ : Fin (dt.d.B.arity i)} (hℓ : ∀ (p : dt.X.Map A), wmBlk v (argOut dt.ki (Fin.castLE ⋯ ℓ₀)) ≠ encMap dt.ly PR.zero PR.one p) : (stOf (Fin.last dt.nv)).new i v ↔ trackOf dt.ly PR.zero PR.one ⋯ (dt.d.next σ) v

At a junk address the cell and the dictionary are both empty: the legs store False (new_last_of_false) and a track holds nothing where a block below the variable's arity encodes no point (DescriptiveComplexity.Draw.not_trackOf_of_notEnc), so the two readings agree there too.

theorem DescriptiveComplexity.Draw.Data.new_last_trackOf {L : FirstOrder.Language} (dt : Data L) {A R : Type} [Fintype dt.SlotIx] [LinearOrder A] [LinearOrder R] [LinearOrder (OuterPh (EvalPh dt.nv dt.PMF))] [FirstOrder.Language.wide.Structure (Univ A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd)] [Finite A] [Finite R] [Finite (OuterPh (EvalPh dt.nv dt.PMF))] {PR : Prog A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.CtlIx dt.SlotIx dt.KIx dt.dd} (RF : RegFile (Univ A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd)) [Nonempty A] [L.IsRelational] [L.Structure A] [LinearOrder (dt.X.Map A)] {v : Univ A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd → Prop} {ιV : Type} [LinearOrder ιV] [Finite ιV] (mV : ιV → Univ A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd → Prop) (hlin : IsLinOrd WMLe) (hord : ∀ (x y : Univ A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd), WMLe x y ↔ tagTupleLe x y) {a₀ aT : ιV} (hbotV : ∀ (a : ιV), a₀ ≤ a) (hmV0 : mV a₀ = fun (x : Univ A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd) => False) (hIncr : ∀ (a a' : ιV), a < a' → (∀ (b : ιV), ¬(a < b ∧ b < a')) → WMIncr WMLe (mV a) (mV a')) (hKin : ∀ (a : ιV) (t : Tag R (OuterPh (EvalPh dt.nv dt.PMF)) dt.KIx) (w : Fin dt.dd → A), mV a (t, w) → ∃ (j : Fin dt.ki), t = argIn dt.ko j) (hTop : ∀ (u : Univ A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd), dt.InnerFull (fun (u : Univ A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd) => tagBlk u.1) (mV aT) u) (σ : dt.d.B.Assignment (dt.X.Map A)) {stOf : Fin (dt.nv + 1) → TapeStD dt A R (OuterPh (EvalPh dt.nv dt.PMF))} {bOf : Fin dt.nv → Prop} (semOfJ : (j : Fin dt.nv) → (a : ιV) → (∀ (ℓ : Fin (dt.nIn (dt.varAt j))), dt.igPassP RF PR.zero PR.one (dt.varAt j) (dt.roundSt (stOf j.castSucc) (mV a)) ℓ) → (b : Fin (dt.natOf (dt.varAt j))) → dt.KindSem PR.zero PR.one (dt.varAt j) (dt.roundSt (stOf j.castSucc) (mV a)) (dt.kindOf (dt.varAt j) b)) (fGOf : Fin dt.nv → dt.CtlIx → A) (hstN : dt.WritesNew 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 (roundFX RF hord (dt.varAt j) (stOf j.castSucc) v mV (semOfJ j) (varFM RF hord (dt.varAt j) (stOf j.castSucc) v mV (semOfJ j) (fGOf j) aT) aT) (dt.back RF.cell PR.zero PR.one ⋯ (dt.roundSt (stOf j.castSucc) (mV aT)) v))) (pt : Fin dt.ko → dt.X.Map A) (hmir : (stOf 0).mir = v) (hpt : ∀ (k : Fin dt.ko), wmBlk v (argOut dt.ki k) = encMap dt.ly PR.zero PR.one (pt k)) {Below : (Univ A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd → Prop) → Prop} (hdict : ∀ (iv : dt.d.B.ι) (s : Univ A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd → Prop), Below s → ((stOf 0).old iv s ↔ trackOf dt.ly PR.zero PR.one ⋯ σ s)) (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 (dt.stageTgtD PR.zero (dt.varAt j) iv ts (dt.roundSt (stOf j.castSucc) (mV a)) v (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.igPassP RF PR.zero PR.one (dt.varAt j) (dt.roundSt (stOf j.castSucc) (mV a)) ℓ) (b : Fin (dt.natOf (dt.varAt j))) (hmb' : ∀ (ℓ : Fin (dt.arOf (dt.varAt j))), wmBlk (dt.roundSt (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.passSem RF ⋯ hlin (dt.varAt j) (dt.roundSt (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 ↔ trackOf dt.ly PR.zero PR.one ⋯ (dt.d.next σ) v

At an encoded address the cell holds the dictionary of the next stage: new_last_next read through DescriptiveComplexity.Draw.trackOf_of_blocks, the sweep's mirror invariant (hmir) turning the address's blocks into the ones the machinery read. This is the form the sweep's induction (sweep_new) consumes, and the form the next sweep's hdict is in.

The semantic pack, transported along the spine

theorem DescriptiveComplexity.Draw.Data.passW_congr {L : FirstOrder.Language} (dt : Data L) {A R : Type} [LinearOrder A] [LinearOrder R] [LinearOrder (OuterPh (EvalPh dt.nv dt.PMF))] [FirstOrder.Language.wide.Structure (Univ A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd)] [Finite A] (RF : RegFile (Univ A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd)) [Nonempty A] [L.Structure A] {zero one : A} (hzo : zero ≠ one) (hlin : IsLinOrd WMLe) (vi : dt.VarIx) {st st' : TapeStD dt A R (OuterPh (EvalPh dt.nv dt.PMF))} (hmir : st.mir = st'.mir) (hval : st.val = st'.val) (hp : ∀ (ℓ : Fin (dt.nIn vi)), dt.igPassP RF zero one vi st ℓ) (hp' : ∀ (ℓ : Fin (dt.nIn vi)), dt.igPassP RF zero one vi st' ℓ) (mbW : Fin (dt.arOf vi) → dt.X.Map A) (hmb : ∀ (ℓ : Fin (dt.arOf vi)), wmBlk st.mir (Tag.arg (toLex (Sum.inl (Fin.castLE ⋯ ℓ)))) = encMap dt.ly zero one (mbW ℓ)) (hmb' : ∀ (ℓ : Fin (dt.arOf vi)), wmBlk st'.mir (Tag.arg (toLex (Sum.inl (Fin.castLE ⋯ ℓ)))) = encMap dt.ly zero one (mbW ℓ)) : dt.passW RF zero one hzo hlin vi st hp mbW = dt.passW RF zero one hzo hlin vi st' hp' mbW

A passing round's valuation depends on the registers alone: both states' choices encode the same block value, and the encoding is injective.

theorem DescriptiveComplexity.Draw.Data.kindSemCast_passSem {L : FirstOrder.Language} (dt : Data L) {A R : Type} [LinearOrder A] [LinearOrder R] [LinearOrder (OuterPh (EvalPh dt.nv dt.PMF))] [FirstOrder.Language.wide.Structure (Univ A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd)] [Finite A] (RF : RegFile (Univ A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd)) [Nonempty A] [L.Structure A] {zero one : A} (hzo : zero ≠ one) (hlin : IsLinOrd WMLe) (vi : dt.VarIx) {st st' : TapeStD dt A R (OuterPh (EvalPh dt.nv dt.PMF))} (hmir : st.mir = st'.mir) (hval : st.val = st'.val) (hp : ∀ (ℓ : Fin (dt.nIn vi)), dt.igPassP RF zero one vi st ℓ) (hp' : ∀ (ℓ : Fin (dt.nIn vi)), dt.igPassP RF zero one vi st' ℓ) (mbW : Fin (dt.arOf vi) → dt.X.Map A) (hmb : ∀ (ℓ : Fin (dt.arOf vi)), wmBlk st.mir (Tag.arg (toLex (Sum.inl (Fin.castLE ⋯ ℓ)))) = encMap dt.ly zero one (mbW ℓ)) (hmb' : ∀ (ℓ : Fin (dt.arOf vi)), wmBlk st'.mir (Tag.arg (toLex (Sum.inl (Fin.castLE ⋯ ℓ)))) = encMap dt.ly zero one (mbW ℓ)) (b : Fin (dt.natOf vi)) : dt.kindSemCast zero one vi hmir hval (dt.kindOf vi b) (dt.passSem RF hzo hlin vi st hp mbW hmb b) = dt.passSem RF hzo hlin vi st' hp' mbW hmb' b

The pass's pack transports to the pass's pack: what a spine position's hsem is discharged by, when its pack is the entry state's carried forward by kindSemCast.

noncomputable def DescriptiveComplexity.Draw.Data.spineSem {L : FirstOrder.Language} (dt : Data L) {A R : Type} [LinearOrder A] [LinearOrder R] [LinearOrder (OuterPh (EvalPh dt.nv dt.PMF))] [FirstOrder.Language.wide.Structure (Univ A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd)] [Finite A] (RF : RegFile (Univ A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd)) [Nonempty A] [L.Structure A] {ιV : Type} (zero one : A) (vi : dt.VarIx) {st₀ st : TapeStD dt A R (OuterPh (EvalPh dt.nv dt.PMF))} (mV : ιV → Univ A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd → Prop) (sem₀ : (a : ιV) → (∀ (ℓ : Fin (dt.nIn vi)), dt.igPassP RF zero one vi (dt.roundSt st₀ (mV a)) ℓ) → (b : Fin (dt.natOf vi)) → dt.KindSem zero one vi (dt.roundSt st₀ (mV a)) (dt.kindOf vi b)) (hmir : st.mir = st₀.mir) (a : ιV) (hp : ∀ (ℓ : Fin (dt.nIn vi)), dt.igPassP RF zero one vi (dt.roundSt st (mV a)) ℓ) (b : Fin (dt.natOf vi)) : dt.KindSem zero one vi (dt.roundSt st (mV a)) (dt.kindOf vi b)

One pack, carried to every position of the spine: the packs of the positions are the entry state's, transported. This is what makes the per-position family definable – the recursion that builds the tape family needs a pack at each of its own states, and here it has one as soon as the mirror rides.

Equations

• dt.spineSem RF zero one vi mV sem₀ hmir a hp b = dt.kindSemCast zero one vi ⋯ ⋯ (dt.kindOf vi b) (sem₀ a ⋯ b)

noncomputable def DescriptiveComplexity.Draw.Data.spineSemT {L : FirstOrder.Language} (dt : Data L) {A R : Type} [LinearOrder A] [LinearOrder R] [LinearOrder (OuterPh (EvalPh dt.nv dt.PMF))] [FirstOrder.Language.wide.Structure (Univ A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd)] [Finite A] (RF : RegFile (Univ A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd)) [Nonempty A] [L.Structure A] {ιV : Type} (zero one : A) (vi : dt.VarIx) {st₀ st : TapeStD dt A R (OuterPh (EvalPh dt.nv dt.PMF))} {v : Univ A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd → Prop} (mV : ιV → Univ A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd → Prop) (sem₀ : (a : ιV) → (∀ (ℓ : Fin (dt.nIn vi)), dt.igPassP RF zero one vi (dt.roundSt st₀ (mV a)) ℓ) → (b : Fin (dt.natOf vi)) → dt.KindSem zero one vi (dt.roundSt st₀ (mV a)) (dt.kindOf vi b)) (hmir : st.mir = st₀.mir) (p : dt.Scratch A R (OuterPh (EvalPh dt.nv dt.PMF))) (a : ιV) (hp : ∀ (ℓ : Fin (dt.nIn vi)), dt.igPassP RF zero one vi (varRdSt st p (mV a)) ℓ) (b : Fin (dt.natOf vi)) : dt.KindSem zero one vi (dt.matSt vi (varRdSt st p (mV a)) v ↑b) (dt.kindOf vi b)

One pack, carried to every round of every position – threaded: as DescriptiveComplexity.Draw.Data.spineSem, at the states the VAL loop's own thread produces. Those differ from the position's entry state in the two scratch registers and the register they enumerate, and a pack reads the state through the mirror and VAL alone, so the entry state's pack transports to all of them.

Equations

• dt.spineSemT RF zero one vi mV sem₀ hmir p a hp b = dt.kindSemCast zero one vi ⋯ ⋯ (dt.kindOf vi b) (dt.kindSemCast zero one vi ⋯ ⋯ (dt.kindOf vi b) (sem₀ a ⋯ b))

theorem DescriptiveComplexity.Draw.Data.spineSem_passSem {L : FirstOrder.Language} (dt : Data L) {A R : Type} [LinearOrder A] [LinearOrder R] [LinearOrder (OuterPh (EvalPh dt.nv dt.PMF))] [FirstOrder.Language.wide.Structure (Univ A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd)] [Finite A] (RF : RegFile (Univ A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd)) [Nonempty A] [L.Structure A] {ιV : Type} {zero one : A} (hzo : zero ≠ one) (hlin : IsLinOrd WMLe) (vi : dt.VarIx) {st₀ st : TapeStD dt A R (OuterPh (EvalPh dt.nv dt.PMF))} (mV : ιV → Univ A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd → Prop) (sem₀ : (a : ιV) → (∀ (ℓ : Fin (dt.nIn vi)), dt.igPassP RF zero one vi (dt.roundSt st₀ (mV a)) ℓ) → (b : Fin (dt.natOf vi)) → dt.KindSem zero one vi (dt.roundSt st₀ (mV a)) (dt.kindOf vi b)) (hmir : st.mir = st₀.mir) (mbW : Fin (dt.arOf vi) → dt.X.Map A) (hsem₀ : ∀ (a : ιV) (hp₀ : ∀ (ℓ : Fin (dt.nIn vi)), dt.igPassP RF zero one vi (dt.roundSt st₀ (mV a)) ℓ) (b : Fin (dt.natOf vi)) (hm₀ : ∀ (ℓ : Fin (dt.arOf vi)), wmBlk (dt.roundSt st₀ (mV a)).mir (Tag.arg (toLex (Sum.inl (Fin.castLE ⋯ ℓ)))) = encMap dt.ly zero one (mbW ℓ)), sem₀ a hp₀ b = dt.passSem RF hzo hlin vi (dt.roundSt st₀ (mV a)) hp₀ mbW hm₀ b) (a : ιV) (hp : ∀ (ℓ : Fin (dt.nIn vi)), dt.igPassP RF zero one vi (dt.roundSt st (mV a)) ℓ) (b : Fin (dt.natOf vi)) (hm : ∀ (ℓ : Fin (dt.arOf vi)), wmBlk (dt.roundSt st (mV a)).mir (Tag.arg (toLex (Sum.inl (Fin.castLE ⋯ ℓ)))) = encMap dt.ly zero one (mbW ℓ)) : dt.spineSem RF zero one vi mV sem₀ hmir a hp b = dt.passSem RF hzo hlin vi (dt.roundSt st (mV a)) hp mbW hm b

A carried pack is the pass's pack: so a family defined by spineSem discharges every position's hsem (new_last_next, new_last_trackOf).

What a gated position knows

The branch DescriptiveComplexity.Draw.Data.gatedAt takes is not merely the one where the machine runs the machinery: it is the one where the argument blocks are encodings, which is what a semantic pack needs to exist at all. DescriptiveComplexity.Draw.Data.gate_trichotomy says the three legs are exhaustive; read in the other direction it says a gated position's blocks encode points.

theorem DescriptiveComplexity.Draw.Data.isEnc_of_gatedAt {L : FirstOrder.Language} (dt : Data L) {A R : Type} [Fintype dt.SlotIx] [LinearOrder A] [LinearOrder R] [LinearOrder (OuterPh (EvalPh dt.nv dt.PMF))] [FirstOrder.Language.wide.Structure (Univ A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd)] [Finite A] {PR : Prog A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.CtlIx dt.SlotIx dt.KIx dt.dd} (RF : RegFile (Univ A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd)) [Nonempty A] [L.Structure A] (hzo : PR.zero ≠ PR.one) (hlin : IsLinOrd WMLe) (j : Fin dt.nv) (st : TapeStD dt A R (OuterPh (EvalPh dt.nv dt.PMF))) (hg : dt.gatedAt RF j st) (ℓ : Fin (dt.arOf (dt.varAt j))) : IsEnc dt.ly PR.zero PR.one (wmBlk st.mir (Tag.arg (toLex (Sum.inl (Fin.castLE ⋯ ℓ)))))

A gated position's argument blocks are encodings – the converse of testOf_of_encMap/wit_of_encMap/domHolds_of_encMap, off the trichotomy. This is what makes a position's semantic pack constructible rather than assumed: at a junk position no pack exists, and at a gated one the points are the blocks' own.

theorem DescriptiveComplexity.Draw.Data.gatedAt_of_isEnc {L : FirstOrder.Language} (dt : Data L) {A R : Type} [Fintype dt.SlotIx] [LinearOrder A] [LinearOrder R] [LinearOrder (OuterPh (EvalPh dt.nv dt.PMF))] [FirstOrder.Language.wide.Structure (Univ A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd)] [Finite A] {PR : Prog A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.CtlIx dt.SlotIx dt.KIx dt.dd} (RF : RegFile (Univ A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd)) [Nonempty A] [L.Structure A] (hzo : PR.zero ≠ PR.one) (hlin : IsLinOrd WMLe) (j : Fin dt.nv) (st : TapeStD dt A R (OuterPh (EvalPh dt.nv dt.PMF))) (henc : ∀ (ℓ : Fin (dt.arOf (dt.varAt j))), IsEnc dt.ly PR.zero PR.one (wmBlk st.mir (Tag.arg (toLex (Sum.inl (Fin.castLE ⋯ ℓ)))))) : dt.gatedAt RF j st

A position whose blocks are encodings is gated – the converse of isEnc_of_gatedAt, assembled from DescriptiveComplexity.Draw.Data.testOf_of_encMap, wit_of_encMap and domHolds_of_encMap. With the two directions together, gating at a position is «the blocks below that variable's arity encode points», which is the dichotomy a sweep's dictionary splits on – and it is per variable, since the arities differ.

noncomputable def DescriptiveComplexity.Draw.Data.gatedSem {L : FirstOrder.Language} (dt : Data L) {A R : Type} [Fintype dt.SlotIx] [LinearOrder A] [LinearOrder R] [LinearOrder (OuterPh (EvalPh dt.nv dt.PMF))] [FirstOrder.Language.wide.Structure (Univ A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd)] [Finite A] {PR : Prog A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.CtlIx dt.SlotIx dt.KIx dt.dd} (RF : RegFile (Univ A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd)) [Nonempty A] [L.Structure A] (hzo : PR.zero ≠ PR.one) (hlin : IsLinOrd WMLe) {v : Univ A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd → Prop} {ιV : Type} (mV : ιV → Univ A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd → Prop) (j : Fin dt.nv) (st : TapeStD dt A R (OuterPh (EvalPh dt.nv dt.PMF))) (hg : dt.gatedAt RF j st) (p : dt.Scratch A R (OuterPh (EvalPh dt.nv dt.PMF))) (a : ιV) (hp : ∀ (ℓ : Fin (dt.nIn (dt.varAt j))), dt.igPassP RF PR.zero PR.one (dt.varAt j) (varRdSt st p (mV a)) ℓ) (b : Fin (dt.natOf (dt.varAt j))) : dt.KindSem PR.zero PR.one (dt.varAt j) (dt.matSt (dt.varAt j) (varRdSt st p (mV a)) v ↑b) (dt.kindOf (dt.varAt j) b)

A gated position's semantic pack, built – not assumed. The blocks are encodings (isEnc_of_gatedAt), so their points are the valuation the pass decodes, and passSem builds the pack there; kindSemCast carries it to the state the matrix's atoms run at, which differs from it in the two scratch registers alone. This is what a branched leg's semT is.

Equations

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

noncomputable def DescriptiveComplexity.Draw.Data.gatedSem₀ {L : FirstOrder.Language} (dt : Data L) {A R : Type} [Fintype dt.SlotIx] [LinearOrder A] [LinearOrder R] [LinearOrder (OuterPh (EvalPh dt.nv dt.PMF))] [FirstOrder.Language.wide.Structure (Univ A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd)] [Finite A] {PR : Prog A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.CtlIx dt.SlotIx dt.KIx dt.dd} (RF : RegFile (Univ A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd)) [Nonempty A] [L.Structure A] (hzo : PR.zero ≠ PR.one) (hlin : IsLinOrd WMLe) {ιV : Type} (mV : ιV → Univ A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd → Prop) (j : Fin dt.nv) (st : TapeStD dt A R (OuterPh (EvalPh dt.nv dt.PMF))) (hg : dt.gatedAt RF j st) (a : ιV) (hp : ∀ (ℓ : Fin (dt.nIn (dt.varAt j))), dt.igPassP RF PR.zero PR.one (dt.varAt j) (dt.roundSt st (mV a)) ℓ) (b : Fin (dt.natOf (dt.varAt j))) : dt.KindSem PR.zero PR.one (dt.varAt j) (dt.roundSt st (mV a)) (dt.kindOf (dt.varAt j) b)

The gated position's pack at the round state – the same points, at the state the semantics names. gatedSem is this pack transported (gatedSem_eq_semCastT), which is what the VAL loop's bridge asks of a threaded family.

Equations

• dt.gatedSem₀ RF hzo hlin mV j st hg a hp b = dt.passSem RF hzo hlin (dt.varAt j) (dt.roundSt st (mV a)) hp (fun (ℓ : Fin (dt.arOf (dt.varAt j))) => Exists.choose ⋯) ⋯ b

theorem DescriptiveComplexity.Draw.Data.gatedSem_eq_semCastT {L : FirstOrder.Language} (dt : Data L) {A R : Type} [Fintype dt.SlotIx] [LinearOrder A] [LinearOrder R] [LinearOrder (OuterPh (EvalPh dt.nv dt.PMF))] [FirstOrder.Language.wide.Structure (Univ A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd)] [Finite A] {PR : Prog A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.CtlIx dt.SlotIx dt.KIx dt.dd} (RF : RegFile (Univ A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd)) [Nonempty A] [L.Structure A] {v : Univ A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd → Prop} (hzo : PR.zero ≠ PR.one) (hlin : IsLinOrd WMLe) {ιV : Type} (mV : ιV → Univ A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd → Prop) (j : Fin dt.nv) (st : TapeStD dt A R (OuterPh (EvalPh dt.nv dt.PMF))) (hg : dt.gatedAt RF j st) : dt.gatedSem RF hzo hlin mV j st hg = semCastT RF (dt.varAt j) st v mV (dt.gatedSem₀ RF hzo hlin mV j st hg)

A gated position's pack is one pack transported: its points are the address's blocks, which the scratch registers do not touch, so the family the machinery is run with is semCastT at DescriptiveComplexity.Draw.Data.gatedSem₀ – the hypothesis the VAL loop's bridge (varFMT_eq_varFM) is stated under.

theorem DescriptiveComplexity.Draw.Data.legBitB_gatedSem {L : FirstOrder.Language} (dt : Data L) {A R : Type} [Fintype dt.SlotIx] [LinearOrder A] [LinearOrder R] [LinearOrder (OuterPh (EvalPh dt.nv dt.PMF))] [FirstOrder.Language.wide.Structure (Univ A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd)] [Finite A] {PR : Prog A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.CtlIx dt.SlotIx dt.KIx dt.dd} (RF : RegFile (Univ A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd)) (hord : ∀ (x y : Univ A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd), WMLe x y ↔ tagTupleLe x y) [Nonempty A] [L.IsRelational] [L.Structure A] {v : Univ A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd → Prop} (hzo : PR.zero ≠ PR.one) (hlin : IsLinOrd WMLe) (hreg : ¬∃ (u : Univ A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd), v = RF.cell u) {ιV : Type} [LinearOrder ιV] [Finite ιV] {aT : ιV} (mV : ιV → Univ A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd → Prop) (j : Fin dt.nv) (st : TapeStD dt A R (OuterPh (EvalPh dt.nv dt.PMF))) (hg : dt.gatedAt RF j st) (f₀ : dt.CtlIx → A) : dt.legBitB RF hord mV j st (fun (hg' : dt.gatedAt RF j st) => dt.gatedSem RF hzo hlin mV j st hg') f₀ = (dt.varArgsOf PR.zero PR.one (dt.varAt j)).accBit (dt.legCtl RF hord mV j st (dt.tagAt j st) (dt.gatedSem₀ RF hzo hlin mV j st hg) f₀)

A gated position's stage bit is the verdict the semantics reads: the branched leg takes the gated leg there, its threaded fold is the unthreaded one (legCtlT_eq_legCtl), and its pack is one pack transported (gatedSem_eq_semCastT). This is new_last_next's hbOf at the family a sweep actually runs.

The per-position families, built

noncomputable def DescriptiveComplexity.Draw.Data.spineNode {L : FirstOrder.Language} (dt : Data L) {A R : Type} [Fintype dt.SlotIx] [LinearOrder A] [LinearOrder R] [LinearOrder (OuterPh (EvalPh dt.nv dt.PMF))] [FirstOrder.Language.wide.Structure (Univ A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd)] [Finite A] {PR : Prog A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.CtlIx dt.SlotIx dt.KIx dt.dd} (RF : RegFile (Univ A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd)) (hord : ∀ (x y : Univ A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd), WMLe x y ↔ tagTupleLe x y) [Nonempty A] [L.IsRelational] [L.Structure A] {v : Univ A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd → Prop} {ιV : Type} [LinearOrder ιV] {aT : ιV} (mV : ιV → Univ A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd → Prop) (st₀ : TapeStD dt A R (OuterPh (EvalPh dt.nv dt.PMF))) (f₀ : dt.CtlIx → A) (sem₀ : (j : Fin dt.nv) → (a : ιV) → (∀ (ℓ : Fin (dt.nIn (dt.varAt j))), dt.igPassP RF PR.zero PR.one (dt.varAt j) (dt.roundSt st₀ (mV a)) ℓ) → (b : Fin (dt.natOf (dt.varAt j))) → dt.KindSem PR.zero PR.one (dt.varAt j) (dt.roundSt st₀ (mV a)) (dt.kindOf (dt.varAt j) b)) (tOf : (j : Fin dt.nv) → Fin (dt.arOf (dt.varAt j)) → dt.X.Tag) : ℕ → (st : TapeStD dt A R (OuterPh (EvalPh dt.nv dt.PMF))) ×' 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 (spineSem).

Equations

• One or more equations did not get rendered due to their size.
• dt.spineNode RF hord mV st₀ f₀ sem₀ tOf 0 = ⟨st₀, ⟨⋯, f₀⟩⟩

noncomputable def DescriptiveComplexity.Draw.Data.spineStOf {L : FirstOrder.Language} (dt : Data L) {A R : Type} [Fintype dt.SlotIx] [LinearOrder A] [LinearOrder R] [LinearOrder (OuterPh (EvalPh dt.nv dt.PMF))] [FirstOrder.Language.wide.Structure (Univ A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd)] [Finite A] {PR : Prog A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.CtlIx dt.SlotIx dt.KIx dt.dd} (RF : RegFile (Univ A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd)) (hord : ∀ (x y : Univ A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd), WMLe x y ↔ tagTupleLe x y) [Nonempty A] [L.IsRelational] [L.Structure A] {v : Univ A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd → Prop} {ιV : Type} [LinearOrder ιV] {aT : ιV} (mV : ιV → Univ A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd → Prop) (st₀ : TapeStD dt A R (OuterPh (EvalPh dt.nv dt.PMF))) (f₀ : dt.CtlIx → A) (sem₀ : (j : Fin dt.nv) → (a : ιV) → (∀ (ℓ : Fin (dt.nIn (dt.varAt j))), dt.igPassP RF PR.zero PR.one (dt.varAt j) (dt.roundSt st₀ (mV a)) ℓ) → (b : Fin (dt.natOf (dt.varAt j))) → dt.KindSem PR.zero PR.one (dt.varAt j) (dt.roundSt st₀ (mV a)) (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)) : TapeStD dt A R (OuterPh (EvalPh dt.nv dt.PMF))

The tape family of the spine.

Equations

• dt.spineStOf RF hord mV st₀ f₀ sem₀ tOf k = (dt.spineNode RF hord mV st₀ f₀ sem₀ tOf ↑k).fst

noncomputable def DescriptiveComplexity.Draw.Data.spineFsOf {L : FirstOrder.Language} (dt : Data L) {A R : Type} [Fintype dt.SlotIx] [LinearOrder A] [LinearOrder R] [LinearOrder (OuterPh (EvalPh dt.nv dt.PMF))] [FirstOrder.Language.wide.Structure (Univ A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd)] [Finite A] {PR : Prog A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.CtlIx dt.SlotIx dt.KIx dt.dd} (RF : RegFile (Univ A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd)) (hord : ∀ (x y : Univ A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd), WMLe x y ↔ tagTupleLe x y) [Nonempty A] [L.IsRelational] [L.Structure A] {v : Univ A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd → Prop} {ιV : Type} [LinearOrder ιV] {aT : ιV} (mV : ιV → Univ A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd → Prop) (st₀ : TapeStD dt A R (OuterPh (EvalPh dt.nv dt.PMF))) (f₀ : dt.CtlIx → A) (sem₀ : (j : Fin dt.nv) → (a : ιV) → (∀ (ℓ : Fin (dt.nIn (dt.varAt j))), dt.igPassP RF PR.zero PR.one (dt.varAt j) (dt.roundSt st₀ (mV a)) ℓ) → (b : Fin (dt.natOf (dt.varAt j))) → dt.KindSem PR.zero PR.one (dt.varAt j) (dt.roundSt st₀ (mV a)) (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.CtlIx → A

The control family of the spine.

Equations

• dt.spineFsOf RF hord mV st₀ f₀ sem₀ tOf k = (dt.spineNode RF hord mV st₀ f₀ sem₀ tOf ↑k).snd.snd

theorem DescriptiveComplexity.Draw.Data.spineStOf_mir {L : FirstOrder.Language} (dt : Data L) {A R : Type} [Fintype dt.SlotIx] [LinearOrder A] [LinearOrder R] [LinearOrder (OuterPh (EvalPh dt.nv dt.PMF))] [FirstOrder.Language.wide.Structure (Univ A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd)] [Finite A] {PR : Prog A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.CtlIx dt.SlotIx dt.KIx dt.dd} (RF : RegFile (Univ A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd)) (hord : ∀ (x y : Univ A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd), WMLe x y ↔ tagTupleLe x y) [Nonempty A] [L.IsRelational] [L.Structure A] {v : Univ A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd → Prop} {ιV : Type} [LinearOrder ιV] {aT : ιV} (mV : ιV → Univ A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd → Prop) (st₀ : TapeStD dt A R (OuterPh (EvalPh dt.nv dt.PMF))) (f₀ : dt.CtlIx → A) (sem₀ : (j : Fin dt.nv) → (a : ιV) → (∀ (ℓ : Fin (dt.nIn (dt.varAt j))), dt.igPassP RF PR.zero PR.one (dt.varAt j) (dt.roundSt st₀ (mV a)) ℓ) → (b : Fin (dt.natOf (dt.varAt j))) → dt.KindSem PR.zero PR.one (dt.varAt j) (dt.roundSt st₀ (mV a)) (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.spineStOf RF hord mV st₀ f₀ sem₀ tOf k).mir = st₀.mir

The mirror rides the built family – by construction, not by the after-the-fact induction of spine_mir.

noncomputable def DescriptiveComplexity.Draw.Data.spineSemOf {L : FirstOrder.Language} (dt : Data L) {A R : Type} [Fintype dt.SlotIx] [LinearOrder A] [LinearOrder R] [LinearOrder (OuterPh (EvalPh dt.nv dt.PMF))] [FirstOrder.Language.wide.Structure (Univ A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd)] [Finite A] {PR : Prog A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.CtlIx dt.SlotIx dt.KIx dt.dd} (RF : RegFile (Univ A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd)) (hord : ∀ (x y : Univ A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd), WMLe x y ↔ tagTupleLe x y) [Nonempty A] [L.IsRelational] [L.Structure A] {v : Univ A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd → Prop} {ιV : Type} [LinearOrder ιV] {aT : ιV} (mV : ιV → Univ A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd → Prop) (st₀ : TapeStD dt A R (OuterPh (EvalPh dt.nv dt.PMF))) (f₀ : dt.CtlIx → A) (sem₀ : (j : Fin dt.nv) → (a : ιV) → (∀ (ℓ : Fin (dt.nIn (dt.varAt j))), dt.igPassP RF PR.zero PR.one (dt.varAt j) (dt.roundSt st₀ (mV a)) ℓ) → (b : Fin (dt.natOf (dt.varAt j))) → dt.KindSem PR.zero PR.one (dt.varAt j) (dt.roundSt st₀ (mV a)) (dt.kindOf (dt.varAt j) b)) (tOf : (j : Fin dt.nv) → Fin (dt.arOf (dt.varAt j)) → dt.X.Tag) (j : Fin dt.nv) (a : ιV) (hp : ∀ (ℓ : Fin (dt.nIn (dt.varAt j))), dt.igPassP RF PR.zero PR.one (dt.varAt j) (dt.roundSt (dt.spineStOf RF hord mV st₀ f₀ sem₀ tOf j.castSucc) (mV a)) ℓ) (b : Fin (dt.natOf (dt.varAt j))) : dt.KindSem PR.zero PR.one (dt.varAt j) (dt.roundSt (dt.spineStOf RF hord mV st₀ f₀ sem₀ tOf j.castSucc) (mV a)) (dt.kindOf (dt.varAt j) b)

The packs of the built family: the entry state's, carried.

Equations

• dt.spineSemOf RF hord mV st₀ f₀ sem₀ tOf j a hp b = dt.spineSem RF PR.zero PR.one (dt.varAt j) mV (sem₀ j) ⋯ a hp b

theorem DescriptiveComplexity.Draw.Data.spineFsOf_succ {L : FirstOrder.Language} (dt : Data L) {A R : Type} [Fintype dt.SlotIx] [LinearOrder A] [LinearOrder R] [LinearOrder (OuterPh (EvalPh dt.nv dt.PMF))] [FirstOrder.Language.wide.Structure (Univ A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd)] [Finite A] {PR : Prog A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.CtlIx dt.SlotIx dt.KIx dt.dd} (RF : RegFile (Univ A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd)) (hord : ∀ (x y : Univ A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd), WMLe x y ↔ tagTupleLe x y) [Nonempty A] [L.IsRelational] [L.Structure A] {v : Univ A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd → Prop} {ιV : Type} [LinearOrder ιV] {aT : ιV} (mV : ιV → Univ A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd → Prop) (st₀ : TapeStD dt A R (OuterPh (EvalPh dt.nv dt.PMF))) (f₀ : dt.CtlIx → A) (sem₀ : (j : Fin dt.nv) → (a : ιV) → (∀ (ℓ : Fin (dt.nIn (dt.varAt j))), dt.igPassP RF PR.zero PR.one (dt.varAt j) (dt.roundSt st₀ (mV a)) ℓ) → (b : Fin (dt.natOf (dt.varAt j))) → dt.KindSem PR.zero PR.one (dt.varAt j) (dt.roundSt st₀ (mV a)) (dt.kindOf (dt.varAt j) b)) (tOf : (j : Fin dt.nv) → Fin (dt.arOf (dt.varAt j)) → dt.X.Tag) (j : Fin dt.nv) : dt.spineFsOf RF hord mV st₀ f₀ sem₀ tOf j.succ = dt.legCtl RF hord mV j (dt.spineStOf RF hord mV st₀ f₀ sem₀ tOf j.castSucc) (tOf j) (dt.spineSemOf RF hord mV st₀ f₀ sem₀ tOf j) (dt.spineFsOf RF hord mV st₀ f₀ sem₀ tOf j.castSucc)

The control's cover equation – evalSpine_run's hfs.

theorem DescriptiveComplexity.Draw.Data.spineStOf_succ {L : FirstOrder.Language} (dt : Data L) {A R : Type} [Fintype dt.SlotIx] [LinearOrder A] [LinearOrder R] [LinearOrder (OuterPh (EvalPh dt.nv dt.PMF))] [FirstOrder.Language.wide.Structure (Univ A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd)] [Finite A] {PR : Prog A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.CtlIx dt.SlotIx dt.KIx dt.dd} (RF : RegFile (Univ A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd)) (hord : ∀ (x y : Univ A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd), WMLe x y ↔ tagTupleLe x y) [Nonempty A] [L.IsRelational] [L.Structure A] {v : Univ A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd → Prop} {ιV : Type} [LinearOrder ιV] {aT : ιV} (mV : ιV → Univ A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd → Prop) (st₀ : TapeStD dt A R (OuterPh (EvalPh dt.nv dt.PMF))) (f₀ : dt.CtlIx → A) (sem₀ : (j : Fin dt.nv) → (a : ιV) → (∀ (ℓ : Fin (dt.nIn (dt.varAt j))), dt.igPassP RF PR.zero PR.one (dt.varAt j) (dt.roundSt st₀ (mV a)) ℓ) → (b : Fin (dt.natOf (dt.varAt j))) → dt.KindSem PR.zero PR.one (dt.varAt j) (dt.roundSt st₀ (mV a)) (dt.kindOf (dt.varAt j) b)) (tOf : (j : Fin dt.nv) → Fin (dt.arOf (dt.varAt j)) → dt.X.Tag) (j : Fin dt.nv) : dt.spineStOf RF hord mV st₀ f₀ sem₀ tOf j.succ = dt.postVarSt v (dt.spineStOf RF hord mV st₀ f₀ sem₀ tOf j.castSucc) (mV aT) (dt.varList.get j) ((dt.varArgsOf PR.zero PR.one (dt.varAt j)).accBit (dt.legCtl RF hord mV j (dt.spineStOf RF hord mV st₀ f₀ sem₀ tOf j.castSucc) (tOf j) (dt.spineSemOf RF hord mV st₀ f₀ sem₀ tOf j) (dt.spineFsOf RF hord mV st₀ f₀ sem₀ tOf j.castSucc)))

The tape's cover equation – evalSpine_run's hst.

The per-position families, threaded

noncomputable def DescriptiveComplexity.Draw.Data.spineNodeT {L : FirstOrder.Language} (dt : Data L) {A R : Type} [Fintype dt.SlotIx] [LinearOrder A] [LinearOrder R] [LinearOrder (OuterPh (EvalPh dt.nv dt.PMF))] [FirstOrder.Language.wide.Structure (Univ A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd)] [Finite A] {PR : Prog A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.CtlIx dt.SlotIx dt.KIx dt.dd} (RF : RegFile (Univ A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd)) (hord : ∀ (x y : Univ A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd), WMLe x y ↔ tagTupleLe x y) [Nonempty A] [L.IsRelational] [L.Structure A] {v : Univ A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd → Prop} {ιV : Type} [LinearOrder ιV] {aT : ιV} (mV : ιV → Univ A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd → Prop) (st₀ : TapeStD dt A R (OuterPh (EvalPh dt.nv dt.PMF))) (f₀ : dt.CtlIx → A) (sem₀ : (j : Fin dt.nv) → (a : ιV) → (∀ (ℓ : Fin (dt.nIn (dt.varAt j))), dt.igPassP RF PR.zero PR.one (dt.varAt j) (dt.roundSt st₀ (mV a)) ℓ) → (b : Fin (dt.natOf (dt.varAt j))) → dt.KindSem PR.zero PR.one (dt.varAt j) (dt.roundSt st₀ (mV a)) (dt.kindOf (dt.varAt j) b)) (tOf : (j : Fin dt.nv) → Fin (dt.arOf (dt.varAt j)) → dt.X.Tag) : ℕ → (st : TapeStD dt A R (OuterPh (EvalPh dt.nv dt.PMF))) ×' st.mir = st₀.mir ×' (dt.CtlIx → A)

One node of the spine, threaded: as DescriptiveComplexity.Draw.Data.spineNode, 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.spineNodeT RF hord mV st₀ f₀ sem₀ tOf 0 = ⟨st₀, ⟨⋯, f₀⟩⟩

noncomputable def DescriptiveComplexity.Draw.Data.spineStOfT {L : FirstOrder.Language} (dt : Data L) {A R : Type} [Fintype dt.SlotIx] [LinearOrder A] [LinearOrder R] [LinearOrder (OuterPh (EvalPh dt.nv dt.PMF))] [FirstOrder.Language.wide.Structure (Univ A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd)] [Finite A] {PR : Prog A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.CtlIx dt.SlotIx dt.KIx dt.dd} (RF : RegFile (Univ A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd)) (hord : ∀ (x y : Univ A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd), WMLe x y ↔ tagTupleLe x y) [Nonempty A] [L.IsRelational] [L.Structure A] {v : Univ A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd → Prop} {ιV : Type} [LinearOrder ιV] {aT : ιV} (mV : ιV → Univ A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd → Prop) (st₀ : TapeStD dt A R (OuterPh (EvalPh dt.nv dt.PMF))) (f₀ : dt.CtlIx → A) (sem₀ : (j : Fin dt.nv) → (a : ιV) → (∀ (ℓ : Fin (dt.nIn (dt.varAt j))), dt.igPassP RF PR.zero PR.one (dt.varAt j) (dt.roundSt st₀ (mV a)) ℓ) → (b : Fin (dt.natOf (dt.varAt j))) → dt.KindSem PR.zero PR.one (dt.varAt j) (dt.roundSt st₀ (mV a)) (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)) : TapeStD dt A R (OuterPh (EvalPh dt.nv dt.PMF))

The threaded tape family of the spine.

Equations

• dt.spineStOfT RF hord mV st₀ f₀ sem₀ tOf k = (dt.spineNodeT RF hord mV st₀ f₀ sem₀ tOf ↑k).fst

noncomputable def DescriptiveComplexity.Draw.Data.spineFsOfT {L : FirstOrder.Language} (dt : Data L) {A R : Type} [Fintype dt.SlotIx] [LinearOrder A] [LinearOrder R] [LinearOrder (OuterPh (EvalPh dt.nv dt.PMF))] [FirstOrder.Language.wide.Structure (Univ A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd)] [Finite A] {PR : Prog A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.CtlIx dt.SlotIx dt.KIx dt.dd} (RF : RegFile (Univ A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd)) (hord : ∀ (x y : Univ A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd), WMLe x y ↔ tagTupleLe x y) [Nonempty A] [L.IsRelational] [L.Structure A] {v : Univ A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd → Prop} {ιV : Type} [LinearOrder ιV] {aT : ιV} (mV : ιV → Univ A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd → Prop) (st₀ : TapeStD dt A R (OuterPh (EvalPh dt.nv dt.PMF))) (f₀ : dt.CtlIx → A) (sem₀ : (j : Fin dt.nv) → (a : ιV) → (∀ (ℓ : Fin (dt.nIn (dt.varAt j))), dt.igPassP RF PR.zero PR.one (dt.varAt j) (dt.roundSt st₀ (mV a)) ℓ) → (b : Fin (dt.natOf (dt.varAt j))) → dt.KindSem PR.zero PR.one (dt.varAt j) (dt.roundSt st₀ (mV a)) (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.CtlIx → A

The threaded control family of the spine.

Equations

• dt.spineFsOfT RF hord mV st₀ f₀ sem₀ tOf k = (dt.spineNodeT RF hord mV st₀ f₀ sem₀ tOf ↑k).snd.snd

theorem DescriptiveComplexity.Draw.Data.spineStOfT_mir {L : FirstOrder.Language} (dt : Data L) {A R : Type} [Fintype dt.SlotIx] [LinearOrder A] [LinearOrder R] [LinearOrder (OuterPh (EvalPh dt.nv dt.PMF))] [FirstOrder.Language.wide.Structure (Univ A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd)] [Finite A] {PR : Prog A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.CtlIx dt.SlotIx dt.KIx dt.dd} (RF : RegFile (Univ A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd)) (hord : ∀ (x y : Univ A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd), WMLe x y ↔ tagTupleLe x y) [Nonempty A] [L.IsRelational] [L.Structure A] {v : Univ A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd → Prop} {ιV : Type} [LinearOrder ιV] {aT : ιV} (mV : ιV → Univ A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd → Prop) (st₀ : TapeStD dt A R (OuterPh (EvalPh dt.nv dt.PMF))) (f₀ : dt.CtlIx → A) (sem₀ : (j : Fin dt.nv) → (a : ιV) → (∀ (ℓ : Fin (dt.nIn (dt.varAt j))), dt.igPassP RF PR.zero PR.one (dt.varAt j) (dt.roundSt st₀ (mV a)) ℓ) → (b : Fin (dt.natOf (dt.varAt j))) → dt.KindSem PR.zero PR.one (dt.varAt j) (dt.roundSt st₀ (mV a)) (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.spineStOfT RF hord mV st₀ f₀ sem₀ tOf k).mir = st₀.mir

The mirror rides the threaded family too – by construction.

noncomputable def DescriptiveComplexity.Draw.Data.spineSemOfT {L : FirstOrder.Language} (dt : Data L) {A R : Type} [Fintype dt.SlotIx] [LinearOrder A] [LinearOrder R] [LinearOrder (OuterPh (EvalPh dt.nv dt.PMF))] [FirstOrder.Language.wide.Structure (Univ A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd)] [Finite A] {PR : Prog A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.CtlIx dt.SlotIx dt.KIx dt.dd} (RF : RegFile (Univ A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd)) (hord : ∀ (x y : Univ A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd), WMLe x y ↔ tagTupleLe x y) [Nonempty A] [L.IsRelational] [L.Structure A] {v : Univ A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd → Prop} {ιV : Type} [LinearOrder ιV] {aT : ιV} (mV : ιV → Univ A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd → Prop) (st₀ : TapeStD dt A R (OuterPh (EvalPh dt.nv dt.PMF))) (f₀ : dt.CtlIx → A) (sem₀ : (j : Fin dt.nv) → (a : ιV) → (∀ (ℓ : Fin (dt.nIn (dt.varAt j))), dt.igPassP RF PR.zero PR.one (dt.varAt j) (dt.roundSt st₀ (mV a)) ℓ) → (b : Fin (dt.natOf (dt.varAt j))) → dt.KindSem PR.zero PR.one (dt.varAt j) (dt.roundSt st₀ (mV a)) (dt.kindOf (dt.varAt j) b)) (tOf : (j : Fin dt.nv) → Fin (dt.arOf (dt.varAt j)) → dt.X.Tag) (j : Fin dt.nv) (p : dt.Scratch A R (OuterPh (EvalPh dt.nv dt.PMF))) (a : ιV) (hp : ∀ (ℓ : Fin (dt.nIn (dt.varAt j))), dt.igPassP RF PR.zero PR.one (dt.varAt j) (varRdSt (dt.spineStOfT RF hord mV st₀ f₀ sem₀ tOf j.castSucc) p (mV a)) ℓ) (b : Fin (dt.natOf (dt.varAt j))) : dt.KindSem PR.zero PR.one (dt.varAt j) (dt.matSt (dt.varAt j) (varRdSt (dt.spineStOfT RF hord mV st₀ f₀ sem₀ tOf j.castSucc) p (mV a)) v ↑b) (dt.kindOf (dt.varAt j) b)

The packs of the threaded family: the address's entry state's, transported to the loop's own states.

Equations

• dt.spineSemOfT RF hord mV st₀ f₀ sem₀ tOf j p a hp b = dt.spineSemT RF PR.zero PR.one (dt.varAt j) mV (sem₀ j) ⋯ p a hp b

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.legStB), 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.gatedSem 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 DescriptiveComplexity.Draw.Data.stEndB 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.gatedSem hzo hlin mV – and no semantic assumption about a position survives in the run layer.

noncomputable def DescriptiveComplexity.Draw.Data.spineNodeB {L : FirstOrder.Language} (dt : Data L) {A R : Type} [Fintype dt.SlotIx] [LinearOrder A] [LinearOrder R] [LinearOrder (OuterPh (EvalPh dt.nv dt.PMF))] [FirstOrder.Language.wide.Structure (Univ A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd)] [Finite A] {PR : Prog A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.CtlIx dt.SlotIx dt.KIx dt.dd} (RF : RegFile (Univ A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd)) (hord : ∀ (x y : Univ A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd), WMLe x y ↔ tagTupleLe x y) [Nonempty A] [L.IsRelational] [L.Structure A] {v : Univ A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd → Prop} {ιV : Type} [LinearOrder ιV] {aT : ιV} (mV : ιV → Univ A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd → Prop) (st₀ : TapeStD dt A R (OuterPh (EvalPh dt.nv dt.PMF))) (f₀ : dt.CtlIx → A) (semB : (w : Univ A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd → Prop) → (j : Fin dt.nv) → (st : TapeStD dt A R (OuterPh (EvalPh dt.nv dt.PMF))) → dt.gatedAt RF j st → (p : dt.Scratch A R (OuterPh (EvalPh dt.nv dt.PMF))) → (a : ιV) → (∀ (ℓ : Fin (dt.nIn (dt.varAt j))), dt.igPassP RF PR.zero PR.one (dt.varAt j) (varRdSt st p (mV a)) ℓ) → (b : Fin (dt.natOf (dt.varAt j))) → dt.KindSem PR.zero PR.one (dt.varAt j) (dt.matSt (dt.varAt j) (varRdSt st p (mV a)) w ↑b) (dt.kindOf (dt.varAt j) b)) : ℕ → (st : TapeStD dt A R (OuterPh (EvalPh dt.nv dt.PMF))) ×' 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.spineNodeB RF hord mV st₀ f₀ semB 0 = ⟨st₀, ⟨⋯, f₀⟩⟩

noncomputable def DescriptiveComplexity.Draw.Data.spineStOfB {L : FirstOrder.Language} (dt : Data L) {A R : Type} [Fintype dt.SlotIx] [LinearOrder A] [LinearOrder R] [LinearOrder (OuterPh (EvalPh dt.nv dt.PMF))] [FirstOrder.Language.wide.Structure (Univ A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd)] [Finite A] {PR : Prog A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.CtlIx dt.SlotIx dt.KIx dt.dd} (RF : RegFile (Univ A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd)) (hord : ∀ (x y : Univ A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd), WMLe x y ↔ tagTupleLe x y) [Nonempty A] [L.IsRelational] [L.Structure A] {v : Univ A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd → Prop} {ιV : Type} [LinearOrder ιV] {aT : ιV} (mV : ιV → Univ A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd → Prop) (st₀ : TapeStD dt A R (OuterPh (EvalPh dt.nv dt.PMF))) (f₀ : dt.CtlIx → A) (semB : (w : Univ A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd → Prop) → (j : Fin dt.nv) → (st : TapeStD dt A R (OuterPh (EvalPh dt.nv dt.PMF))) → dt.gatedAt RF j st → (p : dt.Scratch A R (OuterPh (EvalPh dt.nv dt.PMF))) → (a : ιV) → (∀ (ℓ : Fin (dt.nIn (dt.varAt j))), dt.igPassP RF PR.zero PR.one (dt.varAt j) (varRdSt st p (mV a)) ℓ) → (b : Fin (dt.natOf (dt.varAt j))) → dt.KindSem PR.zero PR.one (dt.varAt j) (dt.matSt (dt.varAt j) (varRdSt st p (mV a)) w ↑b) (dt.kindOf (dt.varAt j) b)) (k : Fin (dt.nv + 1)) : TapeStD dt A R (OuterPh (EvalPh dt.nv dt.PMF))

The branched tape family of the spine.

Equations

• dt.spineStOfB RF hord mV st₀ f₀ semB k = (dt.spineNodeB RF hord mV st₀ f₀ semB ↑k).fst

noncomputable def DescriptiveComplexity.Draw.Data.spineFsOfB {L : FirstOrder.Language} (dt : Data L) {A R : Type} [Fintype dt.SlotIx] [LinearOrder A] [LinearOrder R] [LinearOrder (OuterPh (EvalPh dt.nv dt.PMF))] [FirstOrder.Language.wide.Structure (Univ A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd)] [Finite A] {PR : Prog A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.CtlIx dt.SlotIx dt.KIx dt.dd} (RF : RegFile (Univ A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd)) (hord : ∀ (x y : Univ A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd), WMLe x y ↔ tagTupleLe x y) [Nonempty A] [L.IsRelational] [L.Structure A] {v : Univ A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd → Prop} {ιV : Type} [LinearOrder ιV] {aT : ιV} (mV : ιV → Univ A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd → Prop) (st₀ : TapeStD dt A R (OuterPh (EvalPh dt.nv dt.PMF))) (f₀ : dt.CtlIx → A) (semB : (w : Univ A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd → Prop) → (j : Fin dt.nv) → (st : TapeStD dt A R (OuterPh (EvalPh dt.nv dt.PMF))) → dt.gatedAt RF j st → (p : dt.Scratch A R (OuterPh (EvalPh dt.nv dt.PMF))) → (a : ιV) → (∀ (ℓ : Fin (dt.nIn (dt.varAt j))), dt.igPassP RF PR.zero PR.one (dt.varAt j) (varRdSt st p (mV a)) ℓ) → (b : Fin (dt.natOf (dt.varAt j))) → dt.KindSem PR.zero PR.one (dt.varAt j) (dt.matSt (dt.varAt j) (varRdSt st p (mV a)) w ↑b) (dt.kindOf (dt.varAt j) b)) (k : Fin (dt.nv + 1)) : dt.CtlIx → A

The branched control family of the spine.

Equations

• dt.spineFsOfB RF hord mV st₀ f₀ semB k = (dt.spineNodeB RF hord mV st₀ f₀ semB ↑k).snd.snd

theorem DescriptiveComplexity.Draw.Data.spineStOfB_mir {L : FirstOrder.Language} (dt : Data L) {A R : Type} [Fintype dt.SlotIx] [LinearOrder A] [LinearOrder R] [LinearOrder (OuterPh (EvalPh dt.nv dt.PMF))] [FirstOrder.Language.wide.Structure (Univ A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd)] [Finite A] {PR : Prog A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.CtlIx dt.SlotIx dt.KIx dt.dd} (RF : RegFile (Univ A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd)) (hord : ∀ (x y : Univ A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd), WMLe x y ↔ tagTupleLe x y) [Nonempty A] [L.IsRelational] [L.Structure A] {v : Univ A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd → Prop} {ιV : Type} [LinearOrder ιV] {aT : ιV} (mV : ιV → Univ A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd → Prop) (st₀ : TapeStD dt A R (OuterPh (EvalPh dt.nv dt.PMF))) (f₀ : dt.CtlIx → A) (semB : (w : Univ A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd → Prop) → (j : Fin dt.nv) → (st : TapeStD dt A R (OuterPh (EvalPh dt.nv dt.PMF))) → dt.gatedAt RF j st → (p : dt.Scratch A R (OuterPh (EvalPh dt.nv dt.PMF))) → (a : ιV) → (∀ (ℓ : Fin (dt.nIn (dt.varAt j))), dt.igPassP RF PR.zero PR.one (dt.varAt j) (varRdSt st p (mV a)) ℓ) → (b : Fin (dt.natOf (dt.varAt j))) → dt.KindSem PR.zero PR.one (dt.varAt j) (dt.matSt (dt.varAt j) (varRdSt st p (mV a)) w ↑b) (dt.kindOf (dt.varAt j) b)) (k : Fin (dt.nv + 1)) : (dt.spineStOfB RF hord mV st₀ f₀ semB k).mir = st₀.mir

The mirror rides the branched family – by construction.

noncomputable def DescriptiveComplexity.Draw.Data.spineSemOfB {L : FirstOrder.Language} (dt : Data L) {A R : Type} [Fintype dt.SlotIx] [LinearOrder A] [LinearOrder R] [LinearOrder (OuterPh (EvalPh dt.nv dt.PMF))] [FirstOrder.Language.wide.Structure (Univ A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd)] [Finite A] {PR : Prog A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.CtlIx dt.SlotIx dt.KIx dt.dd} (RF : RegFile (Univ A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd)) (hord : ∀ (x y : Univ A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd), WMLe x y ↔ tagTupleLe x y) [Nonempty A] [L.IsRelational] [L.Structure A] {v : Univ A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd → Prop} {ιV : Type} [LinearOrder ιV] {aT : ιV} (mV : ιV → Univ A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd → Prop) (st₀ : TapeStD dt A R (OuterPh (EvalPh dt.nv dt.PMF))) (f₀ : dt.CtlIx → A) (semB : (w : Univ A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd → Prop) → (j : Fin dt.nv) → (st : TapeStD dt A R (OuterPh (EvalPh dt.nv dt.PMF))) → dt.gatedAt RF j st → (p : dt.Scratch A R (OuterPh (EvalPh dt.nv dt.PMF))) → (a : ιV) → (∀ (ℓ : Fin (dt.nIn (dt.varAt j))), dt.igPassP RF PR.zero PR.one (dt.varAt j) (varRdSt st p (mV a)) ℓ) → (b : Fin (dt.natOf (dt.varAt j))) → dt.KindSem PR.zero PR.one (dt.varAt j) (dt.matSt (dt.varAt j) (varRdSt st p (mV a)) w ↑b) (dt.kindOf (dt.varAt j) b)) (j : Fin dt.nv) (hg : dt.gatedAt RF j (dt.spineStOfB RF hord mV st₀ f₀ semB j.castSucc)) (p : dt.Scratch A R (OuterPh (EvalPh dt.nv dt.PMF))) (a : ιV) (hp : ∀ (ℓ : Fin (dt.nIn (dt.varAt j))), dt.igPassP RF PR.zero PR.one (dt.varAt j) (varRdSt (dt.spineStOfB RF hord mV st₀ f₀ semB j.castSucc) p (mV a)) ℓ) (b : Fin (dt.natOf (dt.varAt j))) : dt.KindSem PR.zero PR.one (dt.varAt j) (dt.matSt (dt.varAt j) (varRdSt (dt.spineStOfB RF hord mV st₀ f₀ semB j.castSucc) p (mV a)) v ↑b) (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.spineSemOfB RF hord mV st₀ f₀ semB j hg p a hp b = semB v j (dt.spineStOfB RF hord mV st₀ f₀ semB j.castSucc) hg p a hp b

theorem DescriptiveComplexity.Draw.Data.spineFsOfB_succ {L : FirstOrder.Language} (dt : Data L) {A R : Type} [Fintype dt.SlotIx] [LinearOrder A] [LinearOrder R] [LinearOrder (OuterPh (EvalPh dt.nv dt.PMF))] [FirstOrder.Language.wide.Structure (Univ A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd)] [Finite A] {PR : Prog A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.CtlIx dt.SlotIx dt.KIx dt.dd} (RF : RegFile (Univ A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd)) (hord : ∀ (x y : Univ A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd), WMLe x y ↔ tagTupleLe x y) [Nonempty A] [L.IsRelational] [L.Structure A] {v : Univ A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd → Prop} {ιV : Type} [LinearOrder ιV] {aT : ιV} (mV : ιV → Univ A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd → Prop) (st₀ : TapeStD dt A R (OuterPh (EvalPh dt.nv dt.PMF))) (f₀ : dt.CtlIx → A) (semB : (w : Univ A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd → Prop) → (j : Fin dt.nv) → (st : TapeStD dt A R (OuterPh (EvalPh dt.nv dt.PMF))) → dt.gatedAt RF j st → (p : dt.Scratch A R (OuterPh (EvalPh dt.nv dt.PMF))) → (a : ιV) → (∀ (ℓ : Fin (dt.nIn (dt.varAt j))), dt.igPassP RF PR.zero PR.one (dt.varAt j) (varRdSt st p (mV a)) ℓ) → (b : Fin (dt.natOf (dt.varAt j))) → dt.KindSem PR.zero PR.one (dt.varAt j) (dt.matSt (dt.varAt j) (varRdSt st p (mV a)) w ↑b) (dt.kindOf (dt.varAt j) b)) (j : Fin dt.nv) : dt.spineFsOfB RF hord mV st₀ f₀ semB j.succ = dt.legCtlB RF hord mV j (dt.spineStOfB RF hord mV st₀ f₀ semB j.castSucc) (dt.spineSemOfB RF hord mV st₀ f₀ semB j) (dt.spineFsOfB RF hord mV st₀ f₀ semB j.castSucc)

The branched control's cover equation – evalSpineB_run's hfs.

theorem DescriptiveComplexity.Draw.Data.spineStOfB_succ {L : FirstOrder.Language} (dt : Data L) {A R : Type} [Fintype dt.SlotIx] [LinearOrder A] [LinearOrder R] [LinearOrder (OuterPh (EvalPh dt.nv dt.PMF))] [FirstOrder.Language.wide.Structure (Univ A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd)] [Finite A] {PR : Prog A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.CtlIx dt.SlotIx dt.KIx dt.dd} (RF : RegFile (Univ A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd)) (hord : ∀ (x y : Univ A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd), WMLe x y ↔ tagTupleLe x y) [Nonempty A] [L.IsRelational] [L.Structure A] {v : Univ A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd → Prop} {ιV : Type} [LinearOrder ιV] {aT : ιV} (mV : ιV → Univ A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd → Prop) (st₀ : TapeStD dt A R (OuterPh (EvalPh dt.nv dt.PMF))) (f₀ : dt.CtlIx → A) (semB : (w : Univ A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd → Prop) → (j : Fin dt.nv) → (st : TapeStD dt A R (OuterPh (EvalPh dt.nv dt.PMF))) → dt.gatedAt RF j st → (p : dt.Scratch A R (OuterPh (EvalPh dt.nv dt.PMF))) → (a : ιV) → (∀ (ℓ : Fin (dt.nIn (dt.varAt j))), dt.igPassP RF PR.zero PR.one (dt.varAt j) (varRdSt st p (mV a)) ℓ) → (b : Fin (dt.natOf (dt.varAt j))) → dt.KindSem PR.zero PR.one (dt.varAt j) (dt.matSt (dt.varAt j) (varRdSt st p (mV a)) w ↑b) (dt.kindOf (dt.varAt j) b)) (j : Fin dt.nv) : dt.spineStOfB RF hord mV st₀ f₀ semB j.succ = dt.legStB RF hord mV j (dt.spineStOfB RF hord mV st₀ f₀ semB j.castSucc) (dt.spineSemOfB RF hord mV st₀ f₀ semB j) (dt.spineFsOfB RF hord mV st₀ f₀ semB j.castSucc)

The branched tape's cover equation – evalSpineB_run's hst.

noncomputable def DescriptiveComplexity.Draw.Data.spineBitOfB {L : FirstOrder.Language} (dt : Data L) {A R : Type} [Fintype dt.SlotIx] [LinearOrder A] [LinearOrder R] [LinearOrder (OuterPh (EvalPh dt.nv dt.PMF))] [FirstOrder.Language.wide.Structure (Univ A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd)] [Finite A] {PR : Prog A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.CtlIx dt.SlotIx dt.KIx dt.dd} (RF : RegFile (Univ A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd)) (hord : ∀ (x y : Univ A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd), WMLe x y ↔ tagTupleLe x y) [Nonempty A] [L.IsRelational] [L.Structure A] {v : Univ A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd → Prop} {ιV : Type} [LinearOrder ιV] {aT : ιV} (mV : ιV → Univ A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd → Prop) (st₀ : TapeStD dt A R (OuterPh (EvalPh dt.nv dt.PMF))) (f₀ : dt.CtlIx → A) (semB : (w : Univ A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd → Prop) → (j : Fin dt.nv) → (st : TapeStD dt A R (OuterPh (EvalPh dt.nv dt.PMF))) → dt.gatedAt RF j st → (p : dt.Scratch A R (OuterPh (EvalPh dt.nv dt.PMF))) → (a : ιV) → (∀ (ℓ : Fin (dt.nIn (dt.varAt j))), dt.igPassP RF PR.zero PR.one (dt.varAt j) (varRdSt st p (mV a)) ℓ) → (b : Fin (dt.natOf (dt.varAt j))) → dt.KindSem PR.zero PR.one (dt.varAt j) (dt.matSt (dt.varAt j) (varRdSt st p (mV a)) w ↑b) (dt.kindOf (dt.varAt j) b)) (j : Fin dt.nv) : Prop

The verdicts of the branched family: at each position, the stage bit its own leg writes.

Equations

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

theorem DescriptiveComplexity.Draw.Data.spineStOfB_writesNew {L : FirstOrder.Language} (dt : Data L) {A R : Type} [Fintype dt.SlotIx] [LinearOrder A] [LinearOrder R] [LinearOrder (OuterPh (EvalPh dt.nv dt.PMF))] [FirstOrder.Language.wide.Structure (Univ A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd)] [Finite A] {PR : Prog A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.CtlIx dt.SlotIx dt.KIx dt.dd} (RF : RegFile (Univ A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd)) (hord : ∀ (x y : Univ A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd), WMLe x y ↔ tagTupleLe x y) [Nonempty A] [L.IsRelational] [L.Structure A] {v : Univ A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd → Prop} {ιV : Type} [LinearOrder ιV] {aT : ιV} (mV : ιV → Univ A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd → Prop) (st₀ : TapeStD dt A R (OuterPh (EvalPh dt.nv dt.PMF))) (f₀ : dt.CtlIx → A) (semB : (w : Univ A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd → Prop) → (j : Fin dt.nv) → (st : TapeStD dt A R (OuterPh (EvalPh dt.nv dt.PMF))) → dt.gatedAt RF j st → (p : dt.Scratch A R (OuterPh (EvalPh dt.nv dt.PMF))) → (a : ιV) → (∀ (ℓ : Fin (dt.nIn (dt.varAt j))), dt.igPassP RF PR.zero PR.one (dt.varAt j) (varRdSt st p (mV a)) ℓ) → (b : Fin (dt.natOf (dt.varAt j))) → dt.KindSem PR.zero PR.one (dt.varAt j) (dt.matSt (dt.varAt j) (varRdSt st p (mV a)) w ↑b) (dt.kindOf (dt.varAt j) b)) : dt.WritesNew (dt.spineStOfB RF hord mV st₀ f₀ semB) (dt.spineBitOfB RF hord mV st₀ f₀ semB)

The branched family writes what a spine writes – the projection of the cover equation the new tracks read, which is all the dictionary lemmas ask of a leg (DescriptiveComplexity.Draw.Data.legStB_new).

theorem DescriptiveComplexity.Draw.Data.spineRideB {L : FirstOrder.Language} (dt : Data L) {A R : Type} [Fintype dt.SlotIx] [LinearOrder A] [LinearOrder R] [LinearOrder (OuterPh (EvalPh dt.nv dt.PMF))] [FirstOrder.Language.wide.Structure (Univ A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd)] [Finite A] {PR : Prog A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.CtlIx dt.SlotIx dt.KIx dt.dd} (RF : RegFile (Univ A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd)) (hord : ∀ (x y : Univ A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd), WMLe x y ↔ tagTupleLe x y) [Nonempty A] [L.IsRelational] [L.Structure A] {v : Univ A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd → Prop} {ιV : Type} [LinearOrder ιV] {aT : ιV} (mV : ιV → Univ A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd → Prop) (st₀ : TapeStD dt A R (OuterPh (EvalPh dt.nv dt.PMF))) (f₀ : dt.CtlIx → A) (semB : (w : Univ A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd → Prop) → (j : Fin dt.nv) → (st : TapeStD dt A R (OuterPh (EvalPh dt.nv dt.PMF))) → dt.gatedAt RF j st → (p : dt.Scratch A R (OuterPh (EvalPh dt.nv dt.PMF))) → (a : ιV) → (∀ (ℓ : Fin (dt.nIn (dt.varAt j))), dt.igPassP RF PR.zero PR.one (dt.varAt j) (varRdSt st p (mV a)) ℓ) → (b : Fin (dt.natOf (dt.varAt j))) → dt.KindSem PR.zero PR.one (dt.varAt j) (dt.matSt (dt.varAt j) (varRdSt st p (mV a)) w ↑b) (dt.kindOf (dt.varAt j) b)) {β : Sort u_1} (F : TapeStD dt A R (OuterPh (EvalPh dt.nv dt.PMF)) → β) (hF : ∀ (j : Fin dt.nv) (st : TapeStD dt A R (OuterPh (EvalPh dt.nv dt.PMF))) (semT : dt.gatedAt RF j st → (p : dt.Scratch A R (OuterPh (EvalPh dt.nv dt.PMF))) → (a : ιV) → (∀ (ℓ : Fin (dt.nIn (dt.varAt j))), dt.igPassP RF PR.zero PR.one (dt.varAt j) (varRdSt st p (mV a)) ℓ) → (b : Fin (dt.natOf (dt.varAt j))) → dt.KindSem PR.zero PR.one (dt.varAt j) (dt.matSt (dt.varAt j) (varRdSt st p (mV a)) v ↑b) (dt.kindOf (dt.varAt j) b)) (f : dt.CtlIx → A), F (dt.legStB RF hord mV j st semT f) = F st) (k : Fin (dt.nv + 1)) : F (dt.spineStOfB RF hord mV st₀ f₀ semB k) = F st₀

A field no leg writes rides the branched spine.

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.new_last_trackOf_B {L : FirstOrder.Language} (dt : Data L) {A R : Type} [Fintype dt.SlotIx] [LinearOrder A] [LinearOrder R] [LinearOrder (OuterPh (EvalPh dt.nv dt.PMF))] [FirstOrder.Language.wide.Structure (Univ A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd)] [Finite A] [Finite R] [Finite (OuterPh (EvalPh dt.nv dt.PMF))] {PR : Prog A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.CtlIx dt.SlotIx dt.KIx dt.dd} (RF : RegFile (Univ A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd)) [Nonempty A] [L.IsRelational] [L.Structure A] [LinearOrder (dt.X.Map A)] {v : Univ A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd → Prop} {ιV : Type} [LinearOrder ιV] [Finite ιV] {aT : ιV} (mV : ιV → Univ A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd → Prop) (st₀ : TapeStD dt A R (OuterPh (EvalPh dt.nv dt.PMF))) (f₀ : dt.CtlIx → A) (hlin : IsLinOrd WMLe) (hord : ∀ (x y : Univ A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd), WMLe x y ↔ tagTupleLe x y) {a₀ : ιV} (hbotV : ∀ (a : ιV), a₀ ≤ a) (hmV0 : mV a₀ = fun (x : Univ A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd) => False) (hIncr : ∀ (a a' : ιV), a < a' → (∀ (b : ιV), ¬(a < b ∧ b < a')) → WMIncr WMLe (mV a) (mV a')) (hKin : ∀ (a : ιV) (t : Tag R (OuterPh (EvalPh dt.nv dt.PMF)) dt.KIx) (w : Fin dt.dd → A), mV a (t, w) → ∃ (jj : Fin dt.ki), t = argIn dt.ko jj) (hTop : ∀ (u : Univ A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd), dt.InnerFull (fun (u : Univ A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd) => tagBlk u.1) (mV aT) u) (hreg : ¬∃ (u : Univ A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd), v = RF.cell u) (hordP : ∀ (p q : dt.X.Map A), p ≤ q ↔ p ≤ q) (σ : dt.d.B.Assignment (dt.X.Map A)) (hmir₀ : st₀.mir = v) {Below : (Univ A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd → Prop) → Prop} (hdict : ∀ (iv : dt.d.B.ι) (s : Univ A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd → Prop), Below s → (st₀.old iv s ↔ trackOf dt.ly PR.zero PR.one ⋯ σ s)) (hbelow : ∀ (j : Fin dt.nv) (a : ιV) (iv : dt.d.B.ι) (ts : Fin (dt.d.B.arity iv) → Fin (dt.nOf (dt.varAt j))) (st : TapeStD dt A R (OuterPh (EvalPh dt.nv dt.PMF))), Below (dt.stageTgtD PR.zero (dt.varAt j) iv ts (dt.roundSt st (mV a)) v (dt.d.B.arity iv))) (i : dt.d.B.ι) : (dt.spineStOfB RF hord mV st₀ f₀ (fun (w : Univ A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd → Prop) (j : Fin dt.nv) (st : TapeStD dt A R (OuterPh (EvalPh dt.nv dt.PMF))) (hg : dt.gatedAt RF j st) => dt.gatedSem RF ⋯ hlin mV j st hg) (Fin.last dt.nv)).new i v ↔ trackOf dt.ly PR.zero PR.one ⋯ (dt.d.next σ) v

What the branched spine leaves at one address, per variable.

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.sweepPairG {L : FirstOrder.Language} (dt : Data L) {A R : Type} [FirstOrder.Language.wide.Structure (Univ A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd)] [Finite A] [Finite R] [Finite (OuterPh (EvalPh dt.nv dt.PMF))] [Finite dt.KIx] (stE : (Univ A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd → Prop) → TapeStD dt A R (OuterPh (EvalPh dt.nv dt.PMF)) → (dt.CtlIx → A) → TapeStD dt A R (OuterPh (EvalPh dt.nv dt.PMF))) (fsE : (Univ A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd → Prop) → TapeStD dt A R (OuterPh (EvalPh dt.nv dt.PMF)) → (dt.CtlIx → A) → dt.CtlIx → A) (hlin : IsLinOrd WMLe) (st₀ : TapeStD dt A R (OuterPh (EvalPh dt.nv dt.PMF))) (f₀ : dt.CtlIx → A) (w : Univ A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd → Prop) : TapeStD dt A R (OuterPh (EvalPh dt.nv dt.PMF)) × (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.sweepSWG {L : FirstOrder.Language} (dt : Data L) {A R : Type} [FirstOrder.Language.wide.Structure (Univ A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd)] [Finite A] [Finite R] [Finite (OuterPh (EvalPh dt.nv dt.PMF))] [Finite dt.KIx] (stE : (Univ A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd → Prop) → TapeStD dt A R (OuterPh (EvalPh dt.nv dt.PMF)) → (dt.CtlIx → A) → TapeStD dt A R (OuterPh (EvalPh dt.nv dt.PMF))) (fsE : (Univ A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd → Prop) → TapeStD dt A R (OuterPh (EvalPh dt.nv dt.PMF)) → (dt.CtlIx → A) → dt.CtlIx → A) (hlin : IsLinOrd WMLe) (st₀ : TapeStD dt A R (OuterPh (EvalPh dt.nv dt.PMF))) (f₀ : dt.CtlIx → A) (w : Univ A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd → Prop) : TapeStD dt A R (OuterPh (EvalPh dt.nv dt.PMF))

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

Equations

• dt.sweepSWG stE fsE hlin st₀ f₀ w = (dt.sweepPairG stE fsE hlin st₀ f₀ w).1

noncomputable def DescriptiveComplexity.Draw.Data.sweepFSG {L : FirstOrder.Language} (dt : Data L) {A R : Type} [FirstOrder.Language.wide.Structure (Univ A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd)] [Finite A] [Finite R] [Finite (OuterPh (EvalPh dt.nv dt.PMF))] [Finite dt.KIx] (stE : (Univ A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd → Prop) → TapeStD dt A R (OuterPh (EvalPh dt.nv dt.PMF)) → (dt.CtlIx → A) → TapeStD dt A R (OuterPh (EvalPh dt.nv dt.PMF))) (fsE : (Univ A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd → Prop) → TapeStD dt A R (OuterPh (EvalPh dt.nv dt.PMF)) → (dt.CtlIx → A) → dt.CtlIx → A) (hlin : IsLinOrd WMLe) (st₀ : TapeStD dt A R (OuterPh (EvalPh dt.nv dt.PMF))) (f₀ : dt.CtlIx → A) (w : Univ A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd → Prop) : dt.CtlIx → A

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

Equations

• dt.sweepFSG stE fsE hlin st₀ f₀ w = (dt.sweepPairG stE fsE hlin st₀ f₀ w).2

noncomputable def DescriptiveComplexity.Draw.Data.sweepStEG {L : FirstOrder.Language} (dt : Data L) {A R : Type} [FirstOrder.Language.wide.Structure (Univ A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd)] [Finite A] [Finite R] [Finite (OuterPh (EvalPh dt.nv dt.PMF))] [Finite dt.KIx] (stE : (Univ A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd → Prop) → TapeStD dt A R (OuterPh (EvalPh dt.nv dt.PMF)) → (dt.CtlIx → A) → TapeStD dt A R (OuterPh (EvalPh dt.nv dt.PMF))) (fsE : (Univ A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd → Prop) → TapeStD dt A R (OuterPh (EvalPh dt.nv dt.PMF)) → (dt.CtlIx → A) → dt.CtlIx → A) (hlin : IsLinOrd WMLe) (st₀ : TapeStD dt A R (OuterPh (EvalPh dt.nv dt.PMF))) (f₀ : dt.CtlIx → A) (w : Univ A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd → Prop) : TapeStD dt A R (OuterPh (EvalPh dt.nv dt.PMF))

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

Equations

• dt.sweepStEG stE fsE hlin st₀ f₀ w = stE w (dt.sweepSWG stE fsE hlin st₀ f₀ w) (dt.sweepFSG stE fsE hlin st₀ f₀ w)

noncomputable def DescriptiveComplexity.Draw.Data.sweepFsEG {L : FirstOrder.Language} (dt : Data L) {A R : Type} [FirstOrder.Language.wide.Structure (Univ A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd)] [Finite A] [Finite R] [Finite (OuterPh (EvalPh dt.nv dt.PMF))] [Finite dt.KIx] (stE : (Univ A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd → Prop) → TapeStD dt A R (OuterPh (EvalPh dt.nv dt.PMF)) → (dt.CtlIx → A) → TapeStD dt A R (OuterPh (EvalPh dt.nv dt.PMF))) (fsE : (Univ A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd → Prop) → TapeStD dt A R (OuterPh (EvalPh dt.nv dt.PMF)) → (dt.CtlIx → A) → dt.CtlIx → A) (hlin : IsLinOrd WMLe) (st₀ : TapeStD dt A R (OuterPh (EvalPh dt.nv dt.PMF))) (f₀ : dt.CtlIx → A) (w : Univ A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd → Prop) : dt.CtlIx → A

The control the sweep leaves each address in – reaches_sweep's fsE.

Equations

• dt.sweepFsEG stE fsE hlin st₀ f₀ w = fsE w (dt.sweepSWG stE fsE hlin st₀ f₀ w) (dt.sweepFSG stE fsE hlin st₀ f₀ w)

theorem DescriptiveComplexity.Draw.Data.sweepSWG_bot {L : FirstOrder.Language} (dt : Data L) {A R : Type} [FirstOrder.Language.wide.Structure (Univ A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd)] [Finite A] [Finite R] [Finite (OuterPh (EvalPh dt.nv dt.PMF))] [Finite dt.KIx] (stE : (Univ A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd → Prop) → TapeStD dt A R (OuterPh (EvalPh dt.nv dt.PMF)) → (dt.CtlIx → A) → TapeStD dt A R (OuterPh (EvalPh dt.nv dt.PMF))) (fsE : (Univ A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd → Prop) → TapeStD dt A R (OuterPh (EvalPh dt.nv dt.PMF)) → (dt.CtlIx → A) → dt.CtlIx → A) (hlin : IsLinOrd WMLe) (st₀ : TapeStD dt A R (OuterPh (EvalPh dt.nv dt.PMF))) (f₀ : dt.CtlIx → A) : (dt.sweepSWG stE fsE hlin st₀ f₀ fun (x : Univ A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd) => False) = st₀

theorem DescriptiveComplexity.Draw.Data.sweepFSG_bot {L : FirstOrder.Language} (dt : Data L) {A R : Type} [FirstOrder.Language.wide.Structure (Univ A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd)] [Finite A] [Finite R] [Finite (OuterPh (EvalPh dt.nv dt.PMF))] [Finite dt.KIx] (stE : (Univ A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd → Prop) → TapeStD dt A R (OuterPh (EvalPh dt.nv dt.PMF)) → (dt.CtlIx → A) → TapeStD dt A R (OuterPh (EvalPh dt.nv dt.PMF))) (fsE : (Univ A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd → Prop) → TapeStD dt A R (OuterPh (EvalPh dt.nv dt.PMF)) → (dt.CtlIx → A) → dt.CtlIx → A) (hlin : IsLinOrd WMLe) (st₀ : TapeStD dt A R (OuterPh (EvalPh dt.nv dt.PMF))) (f₀ : dt.CtlIx → A) : (dt.sweepFSG stE fsE hlin st₀ f₀ fun (x : Univ A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd) => False) = f₀

theorem DescriptiveComplexity.Draw.Data.sweepSWG_incr {L : FirstOrder.Language} (dt : Data L) {A R : Type} [FirstOrder.Language.wide.Structure (Univ A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd)] [Finite A] [Finite R] [Finite (OuterPh (EvalPh dt.nv dt.PMF))] [Finite dt.KIx] (stE : (Univ A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd → Prop) → TapeStD dt A R (OuterPh (EvalPh dt.nv dt.PMF)) → (dt.CtlIx → A) → TapeStD dt A R (OuterPh (EvalPh dt.nv dt.PMF))) (fsE : (Univ A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd → Prop) → TapeStD dt A R (OuterPh (EvalPh dt.nv dt.PMF)) → (dt.CtlIx → A) → dt.CtlIx → A) (hlin : IsLinOrd WMLe) (st₀ : TapeStD dt A R (OuterPh (EvalPh dt.nv dt.PMF))) (f₀ : dt.CtlIx → A) {w w' : Univ A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd → Prop} (hi : WMIncr WMLe w w') : dt.sweepSWG stE fsE hlin st₀ f₀ w' = have __src := dt.atSt (dt.sweepStEG stE fsE hlin st₀ f₀ w) w'; { mir := 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.

theorem DescriptiveComplexity.Draw.Data.sweepFSG_incr {L : FirstOrder.Language} (dt : Data L) {A R : Type} [FirstOrder.Language.wide.Structure (Univ A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd)] [Finite A] [Finite R] [Finite (OuterPh (EvalPh dt.nv dt.PMF))] [Finite dt.KIx] (stE : (Univ A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd → Prop) → TapeStD dt A R (OuterPh (EvalPh dt.nv dt.PMF)) → (dt.CtlIx → A) → TapeStD dt A R (OuterPh (EvalPh dt.nv dt.PMF))) (fsE : (Univ A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd → Prop) → TapeStD dt A R (OuterPh (EvalPh dt.nv dt.PMF)) → (dt.CtlIx → A) → dt.CtlIx → A) (hlin : IsLinOrd WMLe) (st₀ : TapeStD dt A R (OuterPh (EvalPh dt.nv dt.PMF))) (f₀ : dt.CtlIx → A) {w w' : Univ A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd → Prop} (hi : WMIncr WMLe w w') : dt.sweepFSG stE fsE hlin st₀ f₀ w' = dt.sweepFsEG stE fsE hlin st₀ f₀ w

The control's cover equation – reaches_sweep's hFS.

theorem DescriptiveComplexity.Draw.Data.sweepSWG_ride {L : FirstOrder.Language} (dt : Data L) {A R : Type} [FirstOrder.Language.wide.Structure (Univ A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd)] [Finite A] [Finite R] [Finite (OuterPh (EvalPh dt.nv dt.PMF))] [Finite dt.KIx] (stE : (Univ A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd → Prop) → TapeStD dt A R (OuterPh (EvalPh dt.nv dt.PMF)) → (dt.CtlIx → A) → TapeStD dt A R (OuterPh (EvalPh dt.nv dt.PMF))) (fsE : (Univ A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd → Prop) → TapeStD dt A R (OuterPh (EvalPh dt.nv dt.PMF)) → (dt.CtlIx → A) → dt.CtlIx → A) (hlin : IsLinOrd WMLe) (st₀ : TapeStD dt A R (OuterPh (EvalPh dt.nv dt.PMF))) (f₀ : dt.CtlIx → A) {β : Sort u_1} (F : TapeStD dt A R (OuterPh (EvalPh dt.nv dt.PMF)) → β) (hFE : ∀ (u : Univ A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd → Prop) (st : TapeStD dt A R (OuterPh (EvalPh dt.nv dt.PMF))) (f : dt.CtlIx → A), F (stE u st f) = F st) (hFa : ∀ (st : TapeSt dt A R (OuterPh (EvalPh dt.nv dt.PMF)) (Univ A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd)) (u : Univ A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd → Prop), F (have __src := dt.atSt st u; { mir := u, tgt := __src.tgt, sav := __src.sav, val := __src.val, old := __src.old, new := __src.new, wk := __src.wk, bot := __src.bot, ltp := __src.ltp }) = F st) {s₁ : Univ A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd → Prop} (w : Univ A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd → Prop) (hlb : WMSetLe WMLe (fun (x : Univ A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd) => False) w) (hub : WMSetLe WMLe w s₁) : F (dt.sweepSWG stE fsE hlin st₀ f₀ w) = F st₀

A field neither an address's evaluation nor the advance writes rides the whole sweep.

theorem DescriptiveComplexity.Draw.Data.sweepSWG_wk {L : FirstOrder.Language} (dt : Data L) {A R : Type} [FirstOrder.Language.wide.Structure (Univ A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd)] [Finite A] [Finite R] [Finite (OuterPh (EvalPh dt.nv dt.PMF))] [Finite dt.KIx] (stE : (Univ A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd → Prop) → TapeStD dt A R (OuterPh (EvalPh dt.nv dt.PMF)) → (dt.CtlIx → A) → TapeStD dt A R (OuterPh (EvalPh dt.nv dt.PMF))) (fsE : (Univ A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd → Prop) → TapeStD dt A R (OuterPh (EvalPh dt.nv dt.PMF)) → (dt.CtlIx → A) → dt.CtlIx → A) (hlin : IsLinOrd WMLe) (st₀ : TapeStD dt A R (OuterPh (EvalPh dt.nv dt.PMF))) (f₀ : dt.CtlIx → A) (hwk₀ : st₀.wk = fun (r : Univ A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd → Prop) => r = fun (x : Univ A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd) => False) {s₁ : Univ A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd → Prop} (w : Univ A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd → Prop) (hlb : WMSetLe WMLe (fun (x : Univ A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd) => False) w) (hub : WMSetLe WMLe w s₁) : (dt.sweepSWG stE fsE hlin st₀ f₀ w).wk = fun (r : Univ A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd → Prop) => r = w

The marker is at the address, at every entry state of the sweep.

theorem DescriptiveComplexity.Draw.Data.sweepSWG_mir {L : FirstOrder.Language} (dt : Data L) {A R : Type} [FirstOrder.Language.wide.Structure (Univ A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd)] [Finite A] [Finite R] [Finite (OuterPh (EvalPh dt.nv dt.PMF))] [Finite dt.KIx] (stE : (Univ A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd → Prop) → TapeStD dt A R (OuterPh (EvalPh dt.nv dt.PMF)) → (dt.CtlIx → A) → TapeStD dt A R (OuterPh (EvalPh dt.nv dt.PMF))) (fsE : (Univ A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd → Prop) → TapeStD dt A R (OuterPh (EvalPh dt.nv dt.PMF)) → (dt.CtlIx → A) → dt.CtlIx → A) (hlin : IsLinOrd WMLe) (st₀ : TapeStD dt A R (OuterPh (EvalPh dt.nv dt.PMF))) (f₀ : dt.CtlIx → A) (hmir₀ : st₀.mir = fun (x : Univ A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd) => False) {s₁ : Univ A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd → Prop} (w : Univ A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd → Prop) (hlb : WMSetLe WMLe (fun (x : Univ A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd) => False) w) (hub : WMSetLe WMLe w s₁) : (dt.sweepSWG stE fsE hlin st₀ f₀ w).mir = w

The mirror is at the address, at every entry state of the sweep.

theorem DescriptiveComplexity.Draw.Data.sweepStEG_wk {L : FirstOrder.Language} (dt : Data L) {A R : Type} [FirstOrder.Language.wide.Structure (Univ A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd)] [Finite A] [Finite R] [Finite (OuterPh (EvalPh dt.nv dt.PMF))] [Finite dt.KIx] (stE : (Univ A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd → Prop) → TapeStD dt A R (OuterPh (EvalPh dt.nv dt.PMF)) → (dt.CtlIx → A) → TapeStD dt A R (OuterPh (EvalPh dt.nv dt.PMF))) (fsE : (Univ A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd → Prop) → TapeStD dt A R (OuterPh (EvalPh dt.nv dt.PMF)) → (dt.CtlIx → A) → dt.CtlIx → A) (hlin : IsLinOrd WMLe) (st₀ : TapeStD dt A R (OuterPh (EvalPh dt.nv dt.PMF))) (f₀ : dt.CtlIx → A) (hFE : ∀ (u : Univ A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd → Prop) (st : TapeStD dt A R (OuterPh (EvalPh dt.nv dt.PMF))) (f : dt.CtlIx → A), (stE u st f).wk = st.wk) (hwk₀ : st₀.wk = fun (r : Univ A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd → Prop) => r = fun (x : Univ A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd) => False) {s₁ : Univ A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd → Prop} (w : Univ A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd → Prop) (hlb : WMSetLe WMLe (fun (x : Univ A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd) => False) w) (hub : WMSetLe WMLe w s₁) : (dt.sweepStEG stE fsE hlin st₀ f₀ w).wk = fun (r : Univ A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd → Prop) => r = w

reaches_sweep's hwkE: the marker is still at the address when the address's evaluation ends.

theorem DescriptiveComplexity.Draw.Data.sweepStEG_mir {L : FirstOrder.Language} (dt : Data L) {A R : Type} [FirstOrder.Language.wide.Structure (Univ A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd)] [Finite A] [Finite R] [Finite (OuterPh (EvalPh dt.nv dt.PMF))] [Finite dt.KIx] (stE : (Univ A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd → Prop) → TapeStD dt A R (OuterPh (EvalPh dt.nv dt.PMF)) → (dt.CtlIx → A) → TapeStD dt A R (OuterPh (EvalPh dt.nv dt.PMF))) (fsE : (Univ A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd → Prop) → TapeStD dt A R (OuterPh (EvalPh dt.nv dt.PMF)) → (dt.CtlIx → A) → dt.CtlIx → A) (hlin : IsLinOrd WMLe) (st₀ : TapeStD dt A R (OuterPh (EvalPh dt.nv dt.PMF))) (f₀ : dt.CtlIx → A) (hFE : ∀ (u : Univ A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd → Prop) (st : TapeStD dt A R (OuterPh (EvalPh dt.nv dt.PMF))) (f : dt.CtlIx → A), (stE u st f).mir = st.mir) (hmir₀ : st₀.mir = fun (x : Univ A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd) => False) {s₁ : Univ A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd → Prop} (w : Univ A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd → Prop) (hlb : WMSetLe WMLe (fun (x : Univ A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd) => False) w) (hub : WMSetLe WMLe w s₁) : (dt.sweepStEG stE fsE hlin st₀ f₀ w).mir = w

reaches_sweep's hmirE: so is the mirror.

theorem DescriptiveComplexity.Draw.Data.sweepStEG_ltp {L : FirstOrder.Language} (dt : Data L) {A R : Type} [FirstOrder.Language.wide.Structure (Univ A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd)] [Finite A] [Finite R] [Finite (OuterPh (EvalPh dt.nv dt.PMF))] [Finite dt.KIx] (stE : (Univ A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd → Prop) → TapeStD dt A R (OuterPh (EvalPh dt.nv dt.PMF)) → (dt.CtlIx → A) → TapeStD dt A R (OuterPh (EvalPh dt.nv dt.PMF))) (fsE : (Univ A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd → Prop) → TapeStD dt A R (OuterPh (EvalPh dt.nv dt.PMF)) → (dt.CtlIx → A) → dt.CtlIx → A) (hlin : IsLinOrd WMLe) (st₀ : TapeStD dt A R (OuterPh (EvalPh dt.nv dt.PMF))) (f₀ : dt.CtlIx → A) (hFE : ∀ (u : Univ A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd → Prop) (st : TapeStD dt A R (OuterPh (EvalPh dt.nv dt.PMF))) (f : dt.CtlIx → A), (stE u st f).ltp = st.ltp) {s₁ : Univ A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd → Prop} (w : Univ A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd → Prop) (hlb : WMSetLe WMLe (fun (x : Univ A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd) => False) w) (hub : WMSetLe WMLe w s₁) (hltp₀ : ¬st₀.ltp w) : ¬(dt.sweepStEG stE fsE hlin st₀ f₀ w).ltp w

reaches_sweep's hltpE: the address is not the marked end, the mark being where the reduction planted it.

theorem DescriptiveComplexity.Draw.Data.sweepStEG_mir' {L : FirstOrder.Language} (dt : Data L) {A R : Type} [FirstOrder.Language.wide.Structure (Univ A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd)] [Finite A] [Finite R] [Finite (OuterPh (EvalPh dt.nv dt.PMF))] [Finite dt.KIx] (stE : (Univ A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd → Prop) → TapeStD dt A R (OuterPh (EvalPh dt.nv dt.PMF)) → (dt.CtlIx → A) → TapeStD dt A R (OuterPh (EvalPh dt.nv dt.PMF))) (fsE : (Univ A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd → Prop) → TapeStD dt A R (OuterPh (EvalPh dt.nv dt.PMF)) → (dt.CtlIx → A) → dt.CtlIx → A) (hlin : IsLinOrd WMLe) (st₀ : TapeStD dt A R (OuterPh (EvalPh dt.nv dt.PMF))) (f₀ : dt.CtlIx → A) (hFE : ∀ (u : Univ A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd → Prop) (st : TapeStD dt A R (OuterPh (EvalPh dt.nv dt.PMF))) (f : dt.CtlIx → A), (stE u st f).mir = u) (w : Univ A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd → Prop) : (dt.sweepStEG stE fsE hlin st₀ f₀ w).mir = w

reaches_sweep's hmirE when the evaluation sets the mirror itself: the variant of DescriptiveComplexity.Draw.Data.sweepStEG_mir for an evaluation that normalizes the mirror to the address it is run at, which makes the invariant definitional instead of inductive.

The sweep's families

noncomputable def DescriptiveComplexity.Draw.Data.stEnd {L : FirstOrder.Language} (dt : Data L) {A R : Type} [Fintype dt.SlotIx] [LinearOrder A] [LinearOrder R] [LinearOrder (OuterPh (EvalPh dt.nv dt.PMF))] [FirstOrder.Language.wide.Structure (Univ A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd)] [Finite A] {PR : Prog A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.CtlIx dt.SlotIx dt.KIx dt.dd} (RF : RegFile (Univ A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd)) (hord : ∀ (x y : Univ A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd), WMLe x y ↔ tagTupleLe x y) [Nonempty A] [L.IsRelational] [L.Structure A] {ιV : Type} [LinearOrder ιV] {aT : ιV} (mV : ιV → Univ A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd → Prop) (semOf : (st : TapeStD dt A R (OuterPh (EvalPh dt.nv dt.PMF))) → (j : Fin dt.nv) → (a : ιV) → (∀ (ℓ : Fin (dt.nIn (dt.varAt j))), dt.igPassP RF PR.zero PR.one (dt.varAt j) (dt.roundSt st (mV a)) ℓ) → (b : Fin (dt.natOf (dt.varAt j))) → dt.KindSem PR.zero PR.one (dt.varAt j) (dt.roundSt st (mV a)) (dt.kindOf (dt.varAt j) b)) (tOf : TapeStD dt A R (OuterPh (EvalPh dt.nv dt.PMF)) → (j : Fin dt.nv) → Fin (dt.arOf (dt.varAt j)) → dt.X.Tag) (w : Univ A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd → Prop) (st : TapeStD dt A R (OuterPh (EvalPh dt.nv dt.PMF))) (f : dt.CtlIx → A) : TapeStD dt A R (OuterPh (EvalPh dt.nv dt.PMF))

The state one address's spine ends in, from the pair it starts with.

Equations

• dt.stEnd RF hord mV semOf tOf w st f = dt.spineStOf RF hord mV st f (semOf st) (tOf st) (Fin.last dt.nv)

noncomputable def DescriptiveComplexity.Draw.Data.fsEnd {L : FirstOrder.Language} (dt : Data L) {A R : Type} [Fintype dt.SlotIx] [LinearOrder A] [LinearOrder R] [LinearOrder (OuterPh (EvalPh dt.nv dt.PMF))] [FirstOrder.Language.wide.Structure (Univ A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd)] [Finite A] {PR : Prog A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.CtlIx dt.SlotIx dt.KIx dt.dd} (RF : RegFile (Univ A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd)) (hord : ∀ (x y : Univ A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd), WMLe x y ↔ tagTupleLe x y) [Nonempty A] [L.IsRelational] [L.Structure A] {ιV : Type} [LinearOrder ιV] {aT : ιV} (mV : ιV → Univ A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd → Prop) (semOf : (st : TapeStD dt A R (OuterPh (EvalPh dt.nv dt.PMF))) → (j : Fin dt.nv) → (a : ιV) → (∀ (ℓ : Fin (dt.nIn (dt.varAt j))), dt.igPassP RF PR.zero PR.one (dt.varAt j) (dt.roundSt st (mV a)) ℓ) → (b : Fin (dt.natOf (dt.varAt j))) → dt.KindSem PR.zero PR.one (dt.varAt j) (dt.roundSt st (mV a)) (dt.kindOf (dt.varAt j) b)) (tOf : TapeStD dt A R (OuterPh (EvalPh dt.nv dt.PMF)) → (j : Fin dt.nv) → Fin (dt.arOf (dt.varAt j)) → dt.X.Tag) (w : Univ A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd → Prop) (st : TapeStD dt A R (OuterPh (EvalPh dt.nv dt.PMF))) (f : dt.CtlIx → A) : dt.CtlIx → A

The control one address's spine ends in.

Equations

• dt.fsEnd RF hord mV semOf tOf w st f = dt.spineFsOf RF hord mV st f (semOf st) (tOf st) (Fin.last dt.nv)

The threaded per-address evaluation

The mirror is normalized to the address the evaluation is run at. It is already there – the advance sets it, and sweepSWG_mir proves it – but writing it makes the equation definitional, which is what lets the pack family be indexed by the address rather than quantified over arbitrary states. That is the same move as varRdSt one scale down, and for the same reason: a pack at a state whose mirror holds junk does not exist, so the mirror has to be pinned before the pack is asked for.

The branched evaluation's semantic parameter is the conditioned family of DescriptiveComplexity.Draw.Data.gatedSem, quantified over the address as well: DescriptiveComplexity.Draw.Data.stEndB runs the spine at v := w for an address bound after it.

noncomputable def DescriptiveComplexity.Draw.Data.stEndB {L : FirstOrder.Language} (dt : Data L) {A R : Type} [Fintype dt.SlotIx] [LinearOrder A] [LinearOrder R] [LinearOrder (OuterPh (EvalPh dt.nv dt.PMF))] [FirstOrder.Language.wide.Structure (Univ A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd)] [Finite A] {PR : Prog A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.CtlIx dt.SlotIx dt.KIx dt.dd} (RF : RegFile (Univ A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd)) (hord : ∀ (x y : Univ A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd), WMLe x y ↔ tagTupleLe x y) [Nonempty A] [L.IsRelational] [L.Structure A] {ιV : Type} [LinearOrder ιV] {aT : ιV} (mV : ιV → Univ A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd → Prop) (semAtB : (w : Univ A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd → Prop) → (j : Fin dt.nv) → (st : TapeStD dt A R (OuterPh (EvalPh dt.nv dt.PMF))) → dt.gatedAt RF j st → (p : dt.Scratch A R (OuterPh (EvalPh dt.nv dt.PMF))) → (a : ιV) → (∀ (ℓ : Fin (dt.nIn (dt.varAt j))), dt.igPassP RF PR.zero PR.one (dt.varAt j) (varRdSt st p (mV a)) ℓ) → (b : Fin (dt.natOf (dt.varAt j))) → dt.KindSem PR.zero PR.one (dt.varAt j) (dt.matSt (dt.varAt j) (varRdSt st p (mV a)) w ↑b) (dt.kindOf (dt.varAt j) b)) (w : Univ A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd → Prop) (st : TapeStD dt A R (OuterPh (EvalPh dt.nv dt.PMF))) (f : dt.CtlIx → A) : TapeStD dt A R (OuterPh (EvalPh dt.nv dt.PMF))

The state one address's evaluation ends in, with each position taking whichever leg its gates call for and the mirror pinned at the address – what a sweep over every address needs, gated or junk.

Equations

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

noncomputable def DescriptiveComplexity.Draw.Data.fsEndB {L : FirstOrder.Language} (dt : Data L) {A R : Type} [Fintype dt.SlotIx] [LinearOrder A] [LinearOrder R] [LinearOrder (OuterPh (EvalPh dt.nv dt.PMF))] [FirstOrder.Language.wide.Structure (Univ A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd)] [Finite A] {PR : Prog A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.CtlIx dt.SlotIx dt.KIx dt.dd} (RF : RegFile (Univ A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd)) (hord : ∀ (x y : Univ A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd), WMLe x y ↔ tagTupleLe x y) [Nonempty A] [L.IsRelational] [L.Structure A] {ιV : Type} [LinearOrder ιV] {aT : ιV} (mV : ιV → Univ A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd → Prop) (semAtB : (w : Univ A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd → Prop) → (j : Fin dt.nv) → (st : TapeStD dt A R (OuterPh (EvalPh dt.nv dt.PMF))) → dt.gatedAt RF j st → (p : dt.Scratch A R (OuterPh (EvalPh dt.nv dt.PMF))) → (a : ιV) → (∀ (ℓ : Fin (dt.nIn (dt.varAt j))), dt.igPassP RF PR.zero PR.one (dt.varAt j) (varRdSt st p (mV a)) ℓ) → (b : Fin (dt.natOf (dt.varAt j))) → dt.KindSem PR.zero PR.one (dt.varAt j) (dt.matSt (dt.varAt j) (varRdSt st p (mV a)) w ↑b) (dt.kindOf (dt.varAt j) b)) (w : Univ A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd → Prop) (st : TapeStD dt A R (OuterPh (EvalPh dt.nv dt.PMF))) (f : dt.CtlIx → A) : dt.CtlIx → A

The control one address's evaluation ends in, branched.

Equations

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

theorem DescriptiveComplexity.Draw.Data.stEndB_mir {L : FirstOrder.Language} (dt : Data L) {A R : Type} [Fintype dt.SlotIx] [LinearOrder A] [LinearOrder R] [LinearOrder (OuterPh (EvalPh dt.nv dt.PMF))] [FirstOrder.Language.wide.Structure (Univ A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd)] [Finite A] {PR : Prog A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.CtlIx dt.SlotIx dt.KIx dt.dd} (RF : RegFile (Univ A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd)) (hord : ∀ (x y : Univ A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd), WMLe x y ↔ tagTupleLe x y) [Nonempty A] [L.IsRelational] [L.Structure A] {ιV : Type} [LinearOrder ιV] {aT : ιV} (mV : ιV → Univ A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd → Prop) (semAtB : (w : Univ A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd → Prop) → (j : Fin dt.nv) → (st : TapeStD dt A R (OuterPh (EvalPh dt.nv dt.PMF))) → dt.gatedAt RF j st → (p : dt.Scratch A R (OuterPh (EvalPh dt.nv dt.PMF))) → (a : ιV) → (∀ (ℓ : Fin (dt.nIn (dt.varAt j))), dt.igPassP RF PR.zero PR.one (dt.varAt j) (varRdSt st p (mV a)) ℓ) → (b : Fin (dt.natOf (dt.varAt j))) → dt.KindSem PR.zero PR.one (dt.varAt j) (dt.matSt (dt.varAt j) (varRdSt st p (mV a)) w ↑b) (dt.kindOf (dt.varAt j) b)) (w : Univ A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd → Prop) (st : TapeStD dt A R (OuterPh (EvalPh dt.nv dt.PMF))) (f : dt.CtlIx → A) : (dt.stEndB RF hord mV semAtB w st f).mir = w

reaches_sweep's hmirE for the branched evaluation, by construction – through sweepStEG_mir'.

theorem DescriptiveComplexity.Draw.Data.stEndB_ride {L : FirstOrder.Language} (dt : Data L) {A R : Type} [Fintype dt.SlotIx] [LinearOrder A] [LinearOrder R] [LinearOrder (OuterPh (EvalPh dt.nv dt.PMF))] [FirstOrder.Language.wide.Structure (Univ A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd)] [Finite A] {PR : Prog A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.CtlIx dt.SlotIx dt.KIx dt.dd} (RF : RegFile (Univ A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd)) (hord : ∀ (x y : Univ A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd), WMLe x y ↔ tagTupleLe x y) [Nonempty A] [L.IsRelational] [L.Structure A] {ιV : Type} [LinearOrder ιV] {aT : ιV} (mV : ιV → Univ A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd → Prop) (semAtB : (w : Univ A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd → Prop) → (j : Fin dt.nv) → (st : TapeStD dt A R (OuterPh (EvalPh dt.nv dt.PMF))) → dt.gatedAt RF j st → (p : dt.Scratch A R (OuterPh (EvalPh dt.nv dt.PMF))) → (a : ιV) → (∀ (ℓ : Fin (dt.nIn (dt.varAt j))), dt.igPassP RF PR.zero PR.one (dt.varAt j) (varRdSt st p (mV a)) ℓ) → (b : Fin (dt.natOf (dt.varAt j))) → dt.KindSem PR.zero PR.one (dt.varAt j) (dt.matSt (dt.varAt j) (varRdSt st p (mV a)) w ↑b) (dt.kindOf (dt.varAt j) b)) {β : Sort u_1} (F : TapeStD dt A R (OuterPh (EvalPh dt.nv dt.PMF)) → β) (hFmir : ∀ (st : TapeStD dt A R (OuterPh (EvalPh dt.nv dt.PMF))) (m : Univ A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd → Prop), F { mir := m, tgt := st.tgt, sav := st.sav, val := st.val, old := st.old, new := st.new, wk := st.wk, bot := st.bot, ltp := st.ltp } = F st) (hFleg : ∀ (w : Univ A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd → Prop) (j : Fin dt.nv) (st : TapeStD dt A R (OuterPh (EvalPh dt.nv dt.PMF))) (semT : dt.gatedAt RF j st → (p : dt.Scratch A R (OuterPh (EvalPh dt.nv dt.PMF))) → (a : ιV) → (∀ (ℓ : Fin (dt.nIn (dt.varAt j))), dt.igPassP RF PR.zero PR.one (dt.varAt j) (varRdSt st p (mV a)) ℓ) → (b : Fin (dt.natOf (dt.varAt j))) → dt.KindSem PR.zero PR.one (dt.varAt j) (dt.matSt (dt.varAt j) (varRdSt st p (mV a)) w ↑b) (dt.kindOf (dt.varAt j) b)) (f : dt.CtlIx → A), F (dt.legStB RF hord mV j st semT f) = F st) (w : Univ A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd → Prop) (st : TapeStD dt A R (OuterPh (EvalPh dt.nv dt.PMF))) (f : dt.CtlIx → A) : F (dt.stEndB RF hord mV semAtB w st f) = F st

What the branched evaluation leaves alone – reaches_sweep's hwkE and hltpE through sweepStEG_wk and sweepStEG_ltp.

theorem DescriptiveComplexity.Draw.Data.stEndB_new_off {L : FirstOrder.Language} (dt : Data L) {A R : Type} [Fintype dt.SlotIx] [LinearOrder A] [LinearOrder R] [LinearOrder (OuterPh (EvalPh dt.nv dt.PMF))] [FirstOrder.Language.wide.Structure (Univ A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd)] [Finite A] {PR : Prog A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.CtlIx dt.SlotIx dt.KIx dt.dd} (RF : RegFile (Univ A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd)) (hord : ∀ (x y : Univ A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd), WMLe x y ↔ tagTupleLe x y) [Nonempty A] [L.IsRelational] [L.Structure A] {ιV : Type} [LinearOrder ιV] {aT : ιV} (mV : ιV → Univ A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd → Prop) (semAtB : (w : Univ A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd → Prop) → (j : Fin dt.nv) → (st : TapeStD dt A R (OuterPh (EvalPh dt.nv dt.PMF))) → dt.gatedAt RF j st → (p : dt.Scratch A R (OuterPh (EvalPh dt.nv dt.PMF))) → (a : ιV) → (∀ (ℓ : Fin (dt.nIn (dt.varAt j))), dt.igPassP RF PR.zero PR.one (dt.varAt j) (varRdSt st p (mV a)) ℓ) → (b : Fin (dt.natOf (dt.varAt j))) → dt.KindSem PR.zero PR.one (dt.varAt j) (dt.matSt (dt.varAt j) (varRdSt st p (mV a)) w ↑b) (dt.kindOf (dt.varAt j) b)) (w : Univ A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd → Prop) (st : TapeStD dt A R (OuterPh (EvalPh dt.nv dt.PMF))) (f : dt.CtlIx → A) (i : dt.d.B.ι) {r : Univ A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd → Prop} (hr : r ≠ w) : (dt.stEndB RF hord mV semAtB w st f).new i r ↔ st.new i r

Off the address it is run at, the branched evaluation leaves the stage tracks alone – a position writes its own cell only (spine_new_off).

noncomputable def DescriptiveComplexity.Draw.Data.sweepPair {L : FirstOrder.Language} (dt : Data L) {A R : Type} [Fintype dt.SlotIx] [LinearOrder A] [LinearOrder R] [LinearOrder (OuterPh (EvalPh dt.nv dt.PMF))] [FirstOrder.Language.wide.Structure (Univ A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd)] [Finite A] [Finite R] [Finite (OuterPh (EvalPh dt.nv dt.PMF))] {PR : Prog A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.CtlIx dt.SlotIx dt.KIx dt.dd} (RF : RegFile (Univ A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd)) (hord : ∀ (x y : Univ A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd), WMLe x y ↔ tagTupleLe x y) [Nonempty A] [L.IsRelational] [L.Structure A] [Finite dt.KIx] {ιV : Type} [LinearOrder ιV] {aT : ιV} (mV : ιV → Univ A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd → Prop) (semOf : (st : TapeStD dt A R (OuterPh (EvalPh dt.nv dt.PMF))) → (j : Fin dt.nv) → (a : ιV) → (∀ (ℓ : Fin (dt.nIn (dt.varAt j))), dt.igPassP RF PR.zero PR.one (dt.varAt j) (dt.roundSt st (mV a)) ℓ) → (b : Fin (dt.natOf (dt.varAt j))) → dt.KindSem PR.zero PR.one (dt.varAt j) (dt.roundSt st (mV a)) (dt.kindOf (dt.varAt j) b)) (tOf : TapeStD dt A R (OuterPh (EvalPh dt.nv dt.PMF)) → (j : Fin dt.nv) → Fin (dt.arOf (dt.varAt j)) → dt.X.Tag) (hlin : IsLinOrd WMLe) (st₀ : TapeStD dt A R (OuterPh (EvalPh dt.nv dt.PMF))) (f₀ : dt.CtlIx → A) (w : Univ A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd → Prop) : TapeStD dt A R (OuterPh (EvalPh dt.nv dt.PMF)) × (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 spine 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.sweepSW {L : FirstOrder.Language} (dt : Data L) {A R : Type} [Fintype dt.SlotIx] [LinearOrder A] [LinearOrder R] [LinearOrder (OuterPh (EvalPh dt.nv dt.PMF))] [FirstOrder.Language.wide.Structure (Univ A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd)] [Finite A] [Finite R] [Finite (OuterPh (EvalPh dt.nv dt.PMF))] {PR : Prog A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.CtlIx dt.SlotIx dt.KIx dt.dd} (RF : RegFile (Univ A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd)) (hord : ∀ (x y : Univ A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd), WMLe x y ↔ tagTupleLe x y) [Nonempty A] [L.IsRelational] [L.Structure A] [Finite dt.KIx] {ιV : Type} [LinearOrder ιV] {aT : ιV} (mV : ιV → Univ A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd → Prop) (semOf : (st : TapeStD dt A R (OuterPh (EvalPh dt.nv dt.PMF))) → (j : Fin dt.nv) → (a : ιV) → (∀ (ℓ : Fin (dt.nIn (dt.varAt j))), dt.igPassP RF PR.zero PR.one (dt.varAt j) (dt.roundSt st (mV a)) ℓ) → (b : Fin (dt.natOf (dt.varAt j))) → dt.KindSem PR.zero PR.one (dt.varAt j) (dt.roundSt st (mV a)) (dt.kindOf (dt.varAt j) b)) (tOf : TapeStD dt A R (OuterPh (EvalPh dt.nv dt.PMF)) → (j : Fin dt.nv) → Fin (dt.arOf (dt.varAt j)) → dt.X.Tag) (hlin : IsLinOrd WMLe) (st₀ : TapeStD dt A R (OuterPh (EvalPh dt.nv dt.PMF))) (f₀ : dt.CtlIx → A) (w : Univ A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd → Prop) : TapeStD dt A R (OuterPh (EvalPh dt.nv dt.PMF))

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

Equations

• dt.sweepSW RF hord mV semOf tOf hlin st₀ f₀ w = (dt.sweepPair RF hord mV semOf tOf hlin st₀ f₀ w).1

noncomputable def DescriptiveComplexity.Draw.Data.sweepFS {L : FirstOrder.Language} (dt : Data L) {A R : Type} [Fintype dt.SlotIx] [LinearOrder A] [LinearOrder R] [LinearOrder (OuterPh (EvalPh dt.nv dt.PMF))] [FirstOrder.Language.wide.Structure (Univ A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd)] [Finite A] [Finite R] [Finite (OuterPh (EvalPh dt.nv dt.PMF))] {PR : Prog A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.CtlIx dt.SlotIx dt.KIx dt.dd} (RF : RegFile (Univ A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd)) (hord : ∀ (x y : Univ A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd), WMLe x y ↔ tagTupleLe x y) [Nonempty A] [L.IsRelational] [L.Structure A] [Finite dt.KIx] {ιV : Type} [LinearOrder ιV] {aT : ιV} (mV : ιV → Univ A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd → Prop) (semOf : (st : TapeStD dt A R (OuterPh (EvalPh dt.nv dt.PMF))) → (j : Fin dt.nv) → (a : ιV) → (∀ (ℓ : Fin (dt.nIn (dt.varAt j))), dt.igPassP RF PR.zero PR.one (dt.varAt j) (dt.roundSt st (mV a)) ℓ) → (b : Fin (dt.natOf (dt.varAt j))) → dt.KindSem PR.zero PR.one (dt.varAt j) (dt.roundSt st (mV a)) (dt.kindOf (dt.varAt j) b)) (tOf : TapeStD dt A R (OuterPh (EvalPh dt.nv dt.PMF)) → (j : Fin dt.nv) → Fin (dt.arOf (dt.varAt j)) → dt.X.Tag) (hlin : IsLinOrd WMLe) (st₀ : TapeStD dt A R (OuterPh (EvalPh dt.nv dt.PMF))) (f₀ : dt.CtlIx → A) (w : Univ A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd → Prop) : dt.CtlIx → A

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

Equations

• dt.sweepFS RF hord mV semOf tOf hlin st₀ f₀ w = (dt.sweepPair RF hord mV semOf tOf hlin st₀ f₀ w).2

noncomputable def DescriptiveComplexity.Draw.Data.sweepStE {L : FirstOrder.Language} (dt : Data L) {A R : Type} [Fintype dt.SlotIx] [LinearOrder A] [LinearOrder R] [LinearOrder (OuterPh (EvalPh dt.nv dt.PMF))] [FirstOrder.Language.wide.Structure (Univ A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd)] [Finite A] [Finite R] [Finite (OuterPh (EvalPh dt.nv dt.PMF))] {PR : Prog A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.CtlIx dt.SlotIx dt.KIx dt.dd} (RF : RegFile (Univ A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd)) (hord : ∀ (x y : Univ A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd), WMLe x y ↔ tagTupleLe x y) [Nonempty A] [L.IsRelational] [L.Structure A] [Finite dt.KIx] {ιV : Type} [LinearOrder ιV] {aT : ιV} (mV : ιV → Univ A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd → Prop) (semOf : (st : TapeStD dt A R (OuterPh (EvalPh dt.nv dt.PMF))) → (j : Fin dt.nv) → (a : ιV) → (∀ (ℓ : Fin (dt.nIn (dt.varAt j))), dt.igPassP RF PR.zero PR.one (dt.varAt j) (dt.roundSt st (mV a)) ℓ) → (b : Fin (dt.natOf (dt.varAt j))) → dt.KindSem PR.zero PR.one (dt.varAt j) (dt.roundSt st (mV a)) (dt.kindOf (dt.varAt j) b)) (tOf : TapeStD dt A R (OuterPh (EvalPh dt.nv dt.PMF)) → (j : Fin dt.nv) → Fin (dt.arOf (dt.varAt j)) → dt.X.Tag) (hlin : IsLinOrd WMLe) (st₀ : TapeStD dt A R (OuterPh (EvalPh dt.nv dt.PMF))) (f₀ : dt.CtlIx → A) (w : Univ A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd → Prop) : TapeStD dt A R (OuterPh (EvalPh dt.nv dt.PMF))

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

Equations

• dt.sweepStE RF hord mV semOf tOf hlin st₀ f₀ w = dt.stEnd RF hord mV semOf tOf w (dt.sweepSW RF hord mV semOf tOf hlin st₀ f₀ w) (dt.sweepFS RF hord mV semOf tOf hlin st₀ f₀ w)

noncomputable def DescriptiveComplexity.Draw.Data.sweepFsE {L : FirstOrder.Language} (dt : Data L) {A R : Type} [Fintype dt.SlotIx] [LinearOrder A] [LinearOrder R] [LinearOrder (OuterPh (EvalPh dt.nv dt.PMF))] [FirstOrder.Language.wide.Structure (Univ A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd)] [Finite A] [Finite R] [Finite (OuterPh (EvalPh dt.nv dt.PMF))] {PR : Prog A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.CtlIx dt.SlotIx dt.KIx dt.dd} (RF : RegFile (Univ A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd)) (hord : ∀ (x y : Univ A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd), WMLe x y ↔ tagTupleLe x y) [Nonempty A] [L.IsRelational] [L.Structure A] [Finite dt.KIx] {ιV : Type} [LinearOrder ιV] {aT : ιV} (mV : ιV → Univ A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd → Prop) (semOf : (st : TapeStD dt A R (OuterPh (EvalPh dt.nv dt.PMF))) → (j : Fin dt.nv) → (a : ιV) → (∀ (ℓ : Fin (dt.nIn (dt.varAt j))), dt.igPassP RF PR.zero PR.one (dt.varAt j) (dt.roundSt st (mV a)) ℓ) → (b : Fin (dt.natOf (dt.varAt j))) → dt.KindSem PR.zero PR.one (dt.varAt j) (dt.roundSt st (mV a)) (dt.kindOf (dt.varAt j) b)) (tOf : TapeStD dt A R (OuterPh (EvalPh dt.nv dt.PMF)) → (j : Fin dt.nv) → Fin (dt.arOf (dt.varAt j)) → dt.X.Tag) (hlin : IsLinOrd WMLe) (st₀ : TapeStD dt A R (OuterPh (EvalPh dt.nv dt.PMF))) (f₀ : dt.CtlIx → A) (w : Univ A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd → Prop) : dt.CtlIx → A

The control the sweep leaves each address in – reaches_sweep's fsE.

Equations

• dt.sweepFsE RF hord mV semOf tOf hlin st₀ f₀ w = dt.fsEnd RF hord mV semOf tOf w (dt.sweepSW RF hord mV semOf tOf hlin st₀ f₀ w) (dt.sweepFS RF hord mV semOf tOf hlin st₀ f₀ w)

theorem DescriptiveComplexity.Draw.Data.sweepSW_bot {L : FirstOrder.Language} (dt : Data L) {A R : Type} [Fintype dt.SlotIx] [LinearOrder A] [LinearOrder R] [LinearOrder (OuterPh (EvalPh dt.nv dt.PMF))] [FirstOrder.Language.wide.Structure (Univ A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd)] [Finite A] [Finite R] [Finite (OuterPh (EvalPh dt.nv dt.PMF))] {PR : Prog A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.CtlIx dt.SlotIx dt.KIx dt.dd} (RF : RegFile (Univ A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd)) (hord : ∀ (x y : Univ A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd), WMLe x y ↔ tagTupleLe x y) [Nonempty A] [L.IsRelational] [L.Structure A] [Finite dt.KIx] {ιV : Type} [LinearOrder ιV] {aT : ιV} (mV : ιV → Univ A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd → Prop) (semOf : (st : TapeStD dt A R (OuterPh (EvalPh dt.nv dt.PMF))) → (j : Fin dt.nv) → (a : ιV) → (∀ (ℓ : Fin (dt.nIn (dt.varAt j))), dt.igPassP RF PR.zero PR.one (dt.varAt j) (dt.roundSt st (mV a)) ℓ) → (b : Fin (dt.natOf (dt.varAt j))) → dt.KindSem PR.zero PR.one (dt.varAt j) (dt.roundSt st (mV a)) (dt.kindOf (dt.varAt j) b)) (tOf : TapeStD dt A R (OuterPh (EvalPh dt.nv dt.PMF)) → (j : Fin dt.nv) → Fin (dt.arOf (dt.varAt j)) → dt.X.Tag) (hlin : IsLinOrd WMLe) (st₀ : TapeStD dt A R (OuterPh (EvalPh dt.nv dt.PMF))) (f₀ : dt.CtlIx → A) : (dt.sweepSW RF hord mV semOf tOf hlin st₀ f₀ fun (x : Univ A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd) => False) = st₀

theorem DescriptiveComplexity.Draw.Data.sweepSW_incr {L : FirstOrder.Language} (dt : Data L) {A R : Type} [Fintype dt.SlotIx] [LinearOrder A] [LinearOrder R] [LinearOrder (OuterPh (EvalPh dt.nv dt.PMF))] [FirstOrder.Language.wide.Structure (Univ A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd)] [Finite A] [Finite R] [Finite (OuterPh (EvalPh dt.nv dt.PMF))] {PR : Prog A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.CtlIx dt.SlotIx dt.KIx dt.dd} (RF : RegFile (Univ A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd)) (hord : ∀ (x y : Univ A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd), WMLe x y ↔ tagTupleLe x y) [Nonempty A] [L.IsRelational] [L.Structure A] [Finite dt.KIx] {ιV : Type} [LinearOrder ιV] {aT : ιV} (mV : ιV → Univ A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd → Prop) (semOf : (st : TapeStD dt A R (OuterPh (EvalPh dt.nv dt.PMF))) → (j : Fin dt.nv) → (a : ιV) → (∀ (ℓ : Fin (dt.nIn (dt.varAt j))), dt.igPassP RF PR.zero PR.one (dt.varAt j) (dt.roundSt st (mV a)) ℓ) → (b : Fin (dt.natOf (dt.varAt j))) → dt.KindSem PR.zero PR.one (dt.varAt j) (dt.roundSt st (mV a)) (dt.kindOf (dt.varAt j) b)) (tOf : TapeStD dt A R (OuterPh (EvalPh dt.nv dt.PMF)) → (j : Fin dt.nv) → Fin (dt.arOf (dt.varAt j)) → dt.X.Tag) (hlin : IsLinOrd WMLe) (st₀ : TapeStD dt A R (OuterPh (EvalPh dt.nv dt.PMF))) (f₀ : dt.CtlIx → A) {w w' : Univ A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd → Prop} (hi : WMIncr WMLe w w') : dt.sweepSW RF hord mV semOf tOf hlin st₀ f₀ w' = have __src := dt.atSt (dt.sweepStE RF hord mV semOf tOf hlin st₀ f₀ w) w'; { mir := 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 next address's entry state is this one's spine exit, its marker moved on and its mirror at the new address.

theorem DescriptiveComplexity.Draw.Data.sweepFS_incr {L : FirstOrder.Language} (dt : Data L) {A R : Type} [Fintype dt.SlotIx] [LinearOrder A] [LinearOrder R] [LinearOrder (OuterPh (EvalPh dt.nv dt.PMF))] [FirstOrder.Language.wide.Structure (Univ A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd)] [Finite A] [Finite R] [Finite (OuterPh (EvalPh dt.nv dt.PMF))] {PR : Prog A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.CtlIx dt.SlotIx dt.KIx dt.dd} (RF : RegFile (Univ A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd)) (hord : ∀ (x y : Univ A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd), WMLe x y ↔ tagTupleLe x y) [Nonempty A] [L.IsRelational] [L.Structure A] [Finite dt.KIx] {ιV : Type} [LinearOrder ιV] {aT : ιV} (mV : ιV → Univ A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd → Prop) (semOf : (st : TapeStD dt A R (OuterPh (EvalPh dt.nv dt.PMF))) → (j : Fin dt.nv) → (a : ιV) → (∀ (ℓ : Fin (dt.nIn (dt.varAt j))), dt.igPassP RF PR.zero PR.one (dt.varAt j) (dt.roundSt st (mV a)) ℓ) → (b : Fin (dt.natOf (dt.varAt j))) → dt.KindSem PR.zero PR.one (dt.varAt j) (dt.roundSt st (mV a)) (dt.kindOf (dt.varAt j) b)) (tOf : TapeStD dt A R (OuterPh (EvalPh dt.nv dt.PMF)) → (j : Fin dt.nv) → Fin (dt.arOf (dt.varAt j)) → dt.X.Tag) (hlin : IsLinOrd WMLe) (st₀ : TapeStD dt A R (OuterPh (EvalPh dt.nv dt.PMF))) (f₀ : dt.CtlIx → A) {w w' : Univ A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd → Prop} (hi : WMIncr WMLe w w') : dt.sweepFS RF hord mV semOf tOf hlin st₀ f₀ w' = dt.sweepFsE RF hord mV semOf tOf hlin st₀ f₀ w

The control's cover equation – reaches_sweep's hFS: the next address's entry control is this one's spine exit control.

What the sweep's entry and exit states hold

theorem DescriptiveComplexity.Draw.Data.sweepStE_ride {L : FirstOrder.Language} (dt : Data L) {A R : Type} [Fintype dt.SlotIx] [LinearOrder A] [LinearOrder R] [LinearOrder (OuterPh (EvalPh dt.nv dt.PMF))] [FirstOrder.Language.wide.Structure (Univ A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd)] [Finite A] [Finite R] [Finite (OuterPh (EvalPh dt.nv dt.PMF))] {PR : Prog A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.CtlIx dt.SlotIx dt.KIx dt.dd} (RF : RegFile (Univ A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd)) (hord : ∀ (x y : Univ A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd), WMLe x y ↔ tagTupleLe x y) [Nonempty A] [L.IsRelational] [L.Structure A] [Finite dt.KIx] {ιV : Type} [LinearOrder ιV] {aT : ιV} (mV : ιV → Univ A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd → Prop) (semOf : (st : TapeStD dt A R (OuterPh (EvalPh dt.nv dt.PMF))) → (j : Fin dt.nv) → (a : ιV) → (∀ (ℓ : Fin (dt.nIn (dt.varAt j))), dt.igPassP RF PR.zero PR.one (dt.varAt j) (dt.roundSt st (mV a)) ℓ) → (b : Fin (dt.natOf (dt.varAt j))) → dt.KindSem PR.zero PR.one (dt.varAt j) (dt.roundSt st (mV a)) (dt.kindOf (dt.varAt j) b)) (tOf : TapeStD dt A R (OuterPh (EvalPh dt.nv dt.PMF)) → (j : Fin dt.nv) → Fin (dt.arOf (dt.varAt j)) → dt.X.Tag) (hlin : IsLinOrd WMLe) (st₀ : TapeStD dt A R (OuterPh (EvalPh dt.nv dt.PMF))) (f₀ : dt.CtlIx → A) {β : Sort u_1} (F : TapeStD dt A R (OuterPh (EvalPh dt.nv dt.PMF)) → β) (hF : ∀ (u : Univ A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd → Prop) (st : TapeStD dt A R (OuterPh (EvalPh dt.nv dt.PMF))) (m : Univ A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd → Prop) (i : dt.d.B.ι) (b : Prop), F (dt.postVarSt u st m i b) = F st) (w : Univ A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd → Prop) : F (dt.sweepStE RF hord mV semOf tOf hlin st₀ f₀ w) = F (dt.sweepSW RF hord mV semOf tOf hlin st₀ f₀ w)

A field a leg's write leaves alone rides one address's spine.

theorem DescriptiveComplexity.Draw.Data.sweepSW_ride {L : FirstOrder.Language} (dt : Data L) {A R : Type} [Fintype dt.SlotIx] [LinearOrder A] [LinearOrder R] [LinearOrder (OuterPh (EvalPh dt.nv dt.PMF))] [FirstOrder.Language.wide.Structure (Univ A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd)] [Finite A] [Finite R] [Finite (OuterPh (EvalPh dt.nv dt.PMF))] {PR : Prog A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.CtlIx dt.SlotIx dt.KIx dt.dd} (RF : RegFile (Univ A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd)) (hord : ∀ (x y : Univ A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd), WMLe x y ↔ tagTupleLe x y) [Nonempty A] [L.IsRelational] [L.Structure A] [Finite dt.KIx] {ιV : Type} [LinearOrder ιV] {aT : ιV} (mV : ιV → Univ A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd → Prop) (semOf : (st : TapeStD dt A R (OuterPh (EvalPh dt.nv dt.PMF))) → (j : Fin dt.nv) → (a : ιV) → (∀ (ℓ : Fin (dt.nIn (dt.varAt j))), dt.igPassP RF PR.zero PR.one (dt.varAt j) (dt.roundSt st (mV a)) ℓ) → (b : Fin (dt.natOf (dt.varAt j))) → dt.KindSem PR.zero PR.one (dt.varAt j) (dt.roundSt st (mV a)) (dt.kindOf (dt.varAt j) b)) (tOf : TapeStD dt A R (OuterPh (EvalPh dt.nv dt.PMF)) → (j : Fin dt.nv) → Fin (dt.arOf (dt.varAt j)) → dt.X.Tag) (hlin : IsLinOrd WMLe) (st₀ : TapeStD dt A R (OuterPh (EvalPh dt.nv dt.PMF))) (f₀ : dt.CtlIx → A) {β : Sort u_1} (F : TapeStD dt A R (OuterPh (EvalPh dt.nv dt.PMF)) → β) (hF : ∀ (u : Univ A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd → Prop) (st : TapeStD dt A R (OuterPh (EvalPh dt.nv dt.PMF))) (m : Univ A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd → Prop) (i : dt.d.B.ι) (b : Prop), F (dt.postVarSt u st m i b) = F st) (hFa : ∀ (st : TapeSt dt A R (OuterPh (EvalPh dt.nv dt.PMF)) (Univ A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd)) (u : Univ A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd → Prop), F (have __src := dt.atSt st u; { mir := u, tgt := __src.tgt, sav := __src.sav, val := __src.val, old := __src.old, new := __src.new, wk := __src.wk, bot := __src.bot, ltp := __src.ltp }) = F st) {s₁ : Univ A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd → Prop} (w : Univ A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd → Prop) (hlb : WMSetLe WMLe (fun (x : Univ A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd) => False) w) (hub : WMSetLe WMLe w s₁) : F (dt.sweepSW RF hord mV semOf tOf hlin st₀ f₀ w) = F st₀

A field neither a leg nor the advance writes rides the whole sweep.

theorem DescriptiveComplexity.Draw.Data.sweepSW_wk {L : FirstOrder.Language} (dt : Data L) {A R : Type} [Fintype dt.SlotIx] [LinearOrder A] [LinearOrder R] [LinearOrder (OuterPh (EvalPh dt.nv dt.PMF))] [FirstOrder.Language.wide.Structure (Univ A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd)] [Finite A] [Finite R] [Finite (OuterPh (EvalPh dt.nv dt.PMF))] {PR : Prog A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.CtlIx dt.SlotIx dt.KIx dt.dd} (RF : RegFile (Univ A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd)) (hord : ∀ (x y : Univ A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd), WMLe x y ↔ tagTupleLe x y) [Nonempty A] [L.IsRelational] [L.Structure A] [Finite dt.KIx] {ιV : Type} [LinearOrder ιV] {aT : ιV} (mV : ιV → Univ A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd → Prop) (semOf : (st : TapeStD dt A R (OuterPh (EvalPh dt.nv dt.PMF))) → (j : Fin dt.nv) → (a : ιV) → (∀ (ℓ : Fin (dt.nIn (dt.varAt j))), dt.igPassP RF PR.zero PR.one (dt.varAt j) (dt.roundSt st (mV a)) ℓ) → (b : Fin (dt.natOf (dt.varAt j))) → dt.KindSem PR.zero PR.one (dt.varAt j) (dt.roundSt st (mV a)) (dt.kindOf (dt.varAt j) b)) (tOf : TapeStD dt A R (OuterPh (EvalPh dt.nv dt.PMF)) → (j : Fin dt.nv) → Fin (dt.arOf (dt.varAt j)) → dt.X.Tag) (hlin : IsLinOrd WMLe) (st₀ : TapeStD dt A R (OuterPh (EvalPh dt.nv dt.PMF))) (f₀ : dt.CtlIx → A) (hwk₀ : st₀.wk = fun (r : Univ A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd → Prop) => r = fun (x : Univ A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd) => False) {s₁ : Univ A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd → Prop} (w : Univ A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd → Prop) (hlb : WMSetLe WMLe (fun (x : Univ A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd) => False) w) (hub : WMSetLe WMLe w s₁) : (dt.sweepSW RF hord mV semOf tOf hlin st₀ f₀ w).wk = fun (r : Univ A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd → Prop) => r = w

The marker is at the address, at every entry state of the sweep.

theorem DescriptiveComplexity.Draw.Data.sweepSW_mir {L : FirstOrder.Language} (dt : Data L) {A R : Type} [Fintype dt.SlotIx] [LinearOrder A] [LinearOrder R] [LinearOrder (OuterPh (EvalPh dt.nv dt.PMF))] [FirstOrder.Language.wide.Structure (Univ A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd)] [Finite A] [Finite R] [Finite (OuterPh (EvalPh dt.nv dt.PMF))] {PR : Prog A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.CtlIx dt.SlotIx dt.KIx dt.dd} (RF : RegFile (Univ A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd)) (hord : ∀ (x y : Univ A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd), WMLe x y ↔ tagTupleLe x y) [Nonempty A] [L.IsRelational] [L.Structure A] [Finite dt.KIx] {ιV : Type} [LinearOrder ιV] {aT : ιV} (mV : ιV → Univ A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd → Prop) (semOf : (st : TapeStD dt A R (OuterPh (EvalPh dt.nv dt.PMF))) → (j : Fin dt.nv) → (a : ιV) → (∀ (ℓ : Fin (dt.nIn (dt.varAt j))), dt.igPassP RF PR.zero PR.one (dt.varAt j) (dt.roundSt st (mV a)) ℓ) → (b : Fin (dt.natOf (dt.varAt j))) → dt.KindSem PR.zero PR.one (dt.varAt j) (dt.roundSt st (mV a)) (dt.kindOf (dt.varAt j) b)) (tOf : TapeStD dt A R (OuterPh (EvalPh dt.nv dt.PMF)) → (j : Fin dt.nv) → Fin (dt.arOf (dt.varAt j)) → dt.X.Tag) (hlin : IsLinOrd WMLe) (st₀ : TapeStD dt A R (OuterPh (EvalPh dt.nv dt.PMF))) (f₀ : dt.CtlIx → A) (hmir₀ : st₀.mir = fun (x : Univ A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd) => False) {s₁ : Univ A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd → Prop} (w : Univ A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd → Prop) (hlb : WMSetLe WMLe (fun (x : Univ A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd) => False) w) (hub : WMSetLe WMLe w s₁) : (dt.sweepSW RF hord mV semOf tOf hlin st₀ f₀ w).mir = w

The mirror is at the address, at every entry state of the sweep.

theorem DescriptiveComplexity.Draw.Data.sweepStE_wk {L : FirstOrder.Language} (dt : Data L) {A R : Type} [Fintype dt.SlotIx] [LinearOrder A] [LinearOrder R] [LinearOrder (OuterPh (EvalPh dt.nv dt.PMF))] [FirstOrder.Language.wide.Structure (Univ A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd)] [Finite A] [Finite R] [Finite (OuterPh (EvalPh dt.nv dt.PMF))] {PR : Prog A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.CtlIx dt.SlotIx dt.KIx dt.dd} (RF : RegFile (Univ A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd)) (hord : ∀ (x y : Univ A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd), WMLe x y ↔ tagTupleLe x y) [Nonempty A] [L.IsRelational] [L.Structure A] [Finite dt.KIx] {ιV : Type} [LinearOrder ιV] {aT : ιV} (mV : ιV → Univ A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd → Prop) (semOf : (st : TapeStD dt A R (OuterPh (EvalPh dt.nv dt.PMF))) → (j : Fin dt.nv) → (a : ιV) → (∀ (ℓ : Fin (dt.nIn (dt.varAt j))), dt.igPassP RF PR.zero PR.one (dt.varAt j) (dt.roundSt st (mV a)) ℓ) → (b : Fin (dt.natOf (dt.varAt j))) → dt.KindSem PR.zero PR.one (dt.varAt j) (dt.roundSt st (mV a)) (dt.kindOf (dt.varAt j) b)) (tOf : TapeStD dt A R (OuterPh (EvalPh dt.nv dt.PMF)) → (j : Fin dt.nv) → Fin (dt.arOf (dt.varAt j)) → dt.X.Tag) (hlin : IsLinOrd WMLe) (st₀ : TapeStD dt A R (OuterPh (EvalPh dt.nv dt.PMF))) (f₀ : dt.CtlIx → A) (hwk₀ : st₀.wk = fun (r : Univ A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd → Prop) => r = fun (x : Univ A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd) => False) {s₁ : Univ A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd → Prop} (w : Univ A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd → Prop) (hlb : WMSetLe WMLe (fun (x : Univ A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd) => False) w) (hub : WMSetLe WMLe w s₁) : (dt.sweepStE RF hord mV semOf tOf hlin st₀ f₀ w).wk = fun (r : Univ A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd → Prop) => r = w

DescriptiveComplexity.Draw.Data.reaches_sweep's hwkE: the marker is still at the address when the address's spine ends.

theorem DescriptiveComplexity.Draw.Data.sweepStE_mir {L : FirstOrder.Language} (dt : Data L) {A R : Type} [Fintype dt.SlotIx] [LinearOrder A] [LinearOrder R] [LinearOrder (OuterPh (EvalPh dt.nv dt.PMF))] [FirstOrder.Language.wide.Structure (Univ A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd)] [Finite A] [Finite R] [Finite (OuterPh (EvalPh dt.nv dt.PMF))] {PR : Prog A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.CtlIx dt.SlotIx dt.KIx dt.dd} (RF : RegFile (Univ A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd)) (hord : ∀ (x y : Univ A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd), WMLe x y ↔ tagTupleLe x y) [Nonempty A] [L.IsRelational] [L.Structure A] [Finite dt.KIx] {ιV : Type} [LinearOrder ιV] {aT : ιV} (mV : ιV → Univ A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd → Prop) (semOf : (st : TapeStD dt A R (OuterPh (EvalPh dt.nv dt.PMF))) → (j : Fin dt.nv) → (a : ιV) → (∀ (ℓ : Fin (dt.nIn (dt.varAt j))), dt.igPassP RF PR.zero PR.one (dt.varAt j) (dt.roundSt st (mV a)) ℓ) → (b : Fin (dt.natOf (dt.varAt j))) → dt.KindSem PR.zero PR.one (dt.varAt j) (dt.roundSt st (mV a)) (dt.kindOf (dt.varAt j) b)) (tOf : TapeStD dt A R (OuterPh (EvalPh dt.nv dt.PMF)) → (j : Fin dt.nv) → Fin (dt.arOf (dt.varAt j)) → dt.X.Tag) (hlin : IsLinOrd WMLe) (st₀ : TapeStD dt A R (OuterPh (EvalPh dt.nv dt.PMF))) (f₀ : dt.CtlIx → A) (hmir₀ : st₀.mir = fun (x : Univ A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd) => False) {s₁ : Univ A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd → Prop} (w : Univ A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd → Prop) (hlb : WMSetLe WMLe (fun (x : Univ A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd) => False) w) (hub : WMSetLe WMLe w s₁) : (dt.sweepStE RF hord mV semOf tOf hlin st₀ f₀ w).mir = w

reaches_sweep's hmirE: so is the mirror.

theorem DescriptiveComplexity.Draw.Data.sweepStE_ltp_eq {L : FirstOrder.Language} (dt : Data L) {A R : Type} [Fintype dt.SlotIx] [LinearOrder A] [LinearOrder R] [LinearOrder (OuterPh (EvalPh dt.nv dt.PMF))] [FirstOrder.Language.wide.Structure (Univ A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd)] [Finite A] [Finite R] [Finite (OuterPh (EvalPh dt.nv dt.PMF))] {PR : Prog A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.CtlIx dt.SlotIx dt.KIx dt.dd} (RF : RegFile (Univ A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd)) (hord : ∀ (x y : Univ A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd), WMLe x y ↔ tagTupleLe x y) [Nonempty A] [L.IsRelational] [L.Structure A] [Finite dt.KIx] {ιV : Type} [LinearOrder ιV] {aT : ιV} (mV : ιV → Univ A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd → Prop) (semOf : (st : TapeStD dt A R (OuterPh (EvalPh dt.nv dt.PMF))) → (j : Fin dt.nv) → (a : ιV) → (∀ (ℓ : Fin (dt.nIn (dt.varAt j))), dt.igPassP RF PR.zero PR.one (dt.varAt j) (dt.roundSt st (mV a)) ℓ) → (b : Fin (dt.natOf (dt.varAt j))) → dt.KindSem PR.zero PR.one (dt.varAt j) (dt.roundSt st (mV a)) (dt.kindOf (dt.varAt j) b)) (tOf : TapeStD dt A R (OuterPh (EvalPh dt.nv dt.PMF)) → (j : Fin dt.nv) → Fin (dt.arOf (dt.varAt j)) → dt.X.Tag) (hlin : IsLinOrd WMLe) (st₀ : TapeStD dt A R (OuterPh (EvalPh dt.nv dt.PMF))) (f₀ : dt.CtlIx → A) {s₁ : Univ A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd → Prop} (w : Univ A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd → Prop) (hlb : WMSetLe WMLe (fun (x : Univ A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd) => False) w) (hub : WMSetLe WMLe w s₁) : (dt.sweepStE RF hord mV semOf tOf hlin st₀ f₀ w).ltp = st₀.ltp

The permanent ltp mark rides the sweep: neither a leg nor the advance writes it.

theorem DescriptiveComplexity.Draw.Data.sweepStE_ltp {L : FirstOrder.Language} (dt : Data L) {A R : Type} [Fintype dt.SlotIx] [LinearOrder A] [LinearOrder R] [LinearOrder (OuterPh (EvalPh dt.nv dt.PMF))] [FirstOrder.Language.wide.Structure (Univ A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd)] [Finite A] [Finite R] [Finite (OuterPh (EvalPh dt.nv dt.PMF))] {PR : Prog A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.CtlIx dt.SlotIx dt.KIx dt.dd} (RF : RegFile (Univ A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd)) (hord : ∀ (x y : Univ A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd), WMLe x y ↔ tagTupleLe x y) [Nonempty A] [L.IsRelational] [L.Structure A] [Finite dt.KIx] {ιV : Type} [LinearOrder ιV] {aT : ιV} (mV : ιV → Univ A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd → Prop) (semOf : (st : TapeStD dt A R (OuterPh (EvalPh dt.nv dt.PMF))) → (j : Fin dt.nv) → (a : ιV) → (∀ (ℓ : Fin (dt.nIn (dt.varAt j))), dt.igPassP RF PR.zero PR.one (dt.varAt j) (dt.roundSt st (mV a)) ℓ) → (b : Fin (dt.natOf (dt.varAt j))) → dt.KindSem PR.zero PR.one (dt.varAt j) (dt.roundSt st (mV a)) (dt.kindOf (dt.varAt j) b)) (tOf : TapeStD dt A R (OuterPh (EvalPh dt.nv dt.PMF)) → (j : Fin dt.nv) → Fin (dt.arOf (dt.varAt j)) → dt.X.Tag) (hlin : IsLinOrd WMLe) (st₀ : TapeStD dt A R (OuterPh (EvalPh dt.nv dt.PMF))) (f₀ : dt.CtlIx → A) {s₁ : Univ A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd → Prop} (w : Univ A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd → Prop) (hlb : WMSetLe WMLe (fun (x : Univ A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd) => False) w) (hub : WMSetLe WMLe w s₁) (hltp₀ : ¬st₀.ltp w) : ¬(dt.sweepStE RF hord mV semOf tOf hlin st₀ f₀ w).ltp w

reaches_sweep's hltpE: the address is not the marked end, the mark being where the reduction planted it.

The SAV/TGT gap

DescriptiveComplexity.Draw.Data.evalSpine_run asks, at every address, for hsavOf/htgtOf – the SAV and TARGET registers holding that address – because DescriptiveComplexity.Draw.Data.matrix_run reads them there. But the advance refreshes only the marker and the mirror (reaches_sweep's hSW is atSt … with mir := …), so those two registers ride the whole sweep, and the requirement is met at one address at most. The two lemmas below are that statement, not a workaround: whichever way the gap is closed – the advance copying the mirror into SAV and TARGET, the evaluation refreshing them at its entry, or matrix_run reading the mirror instead – the fix is in the program, not here.

theorem DescriptiveComplexity.Draw.Data.sweepSW_sav {L : FirstOrder.Language} (dt : Data L) {A R : Type} [Fintype dt.SlotIx] [LinearOrder A] [LinearOrder R] [LinearOrder (OuterPh (EvalPh dt.nv dt.PMF))] [FirstOrder.Language.wide.Structure (Univ A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd)] [Finite A] [Finite R] [Finite (OuterPh (EvalPh dt.nv dt.PMF))] {PR : Prog A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.CtlIx dt.SlotIx dt.KIx dt.dd} (RF : RegFile (Univ A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd)) (hord : ∀ (x y : Univ A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd), WMLe x y ↔ tagTupleLe x y) [Nonempty A] [L.IsRelational] [L.Structure A] [Finite dt.KIx] {ιV : Type} [LinearOrder ιV] {aT : ιV} (mV : ιV → Univ A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd → Prop) (semOf : (st : TapeStD dt A R (OuterPh (EvalPh dt.nv dt.PMF))) → (j : Fin dt.nv) → (a : ιV) → (∀ (ℓ : Fin (dt.nIn (dt.varAt j))), dt.igPassP RF PR.zero PR.one (dt.varAt j) (dt.roundSt st (mV a)) ℓ) → (b : Fin (dt.natOf (dt.varAt j))) → dt.KindSem PR.zero PR.one (dt.varAt j) (dt.roundSt st (mV a)) (dt.kindOf (dt.varAt j) b)) (tOf : TapeStD dt A R (OuterPh (EvalPh dt.nv dt.PMF)) → (j : Fin dt.nv) → Fin (dt.arOf (dt.varAt j)) → dt.X.Tag) (hlin : IsLinOrd WMLe) (st₀ : TapeStD dt A R (OuterPh (EvalPh dt.nv dt.PMF))) (f₀ : dt.CtlIx → A) {s₁ : Univ A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd → Prop} (w : Univ A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd → Prop) (hlb : WMSetLe WMLe (fun (x : Univ A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd) => False) w) (hub : WMSetLe WMLe w s₁) : (dt.sweepSW RF hord mV semOf tOf hlin st₀ f₀ w).sav = st₀.sav

SAV rides the sweep.

theorem DescriptiveComplexity.Draw.Data.eq_of_sweepSW_sav {L : FirstOrder.Language} (dt : Data L) {A R : Type} [Fintype dt.SlotIx] [LinearOrder A] [LinearOrder R] [LinearOrder (OuterPh (EvalPh dt.nv dt.PMF))] [FirstOrder.Language.wide.Structure (Univ A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd)] [Finite A] [Finite R] [Finite (OuterPh (EvalPh dt.nv dt.PMF))] {PR : Prog A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.CtlIx dt.SlotIx dt.KIx dt.dd} (RF : RegFile (Univ A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd)) (hord : ∀ (x y : Univ A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd), WMLe x y ↔ tagTupleLe x y) [Nonempty A] [L.IsRelational] [L.Structure A] [Finite dt.KIx] {ιV : Type} [LinearOrder ιV] {aT : ιV} (mV : ιV → Univ A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd → Prop) (semOf : (st : TapeStD dt A R (OuterPh (EvalPh dt.nv dt.PMF))) → (j : Fin dt.nv) → (a : ιV) → (∀ (ℓ : Fin (dt.nIn (dt.varAt j))), dt.igPassP RF PR.zero PR.one (dt.varAt j) (dt.roundSt st (mV a)) ℓ) → (b : Fin (dt.natOf (dt.varAt j))) → dt.KindSem PR.zero PR.one (dt.varAt j) (dt.roundSt st (mV a)) (dt.kindOf (dt.varAt j) b)) (tOf : TapeStD dt A R (OuterPh (EvalPh dt.nv dt.PMF)) → (j : Fin dt.nv) → Fin (dt.arOf (dt.varAt j)) → dt.X.Tag) (hlin : IsLinOrd WMLe) (st₀ : TapeStD dt A R (OuterPh (EvalPh dt.nv dt.PMF))) (f₀ : dt.CtlIx → A) {s₁ w₁ w₂ : Univ A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd → Prop} (hlb₁ : WMSetLe WMLe (fun (x : Univ A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd) => False) w₁) (hub₁ : WMSetLe WMLe w₁ s₁) (hlb₂ : WMSetLe WMLe (fun (x : Univ A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd) => False) w₂) (hub₂ : WMSetLe WMLe w₂ s₁) (h₁ : (dt.sweepSW RF hord mV semOf tOf hlin st₀ f₀ w₁).sav = w₁) (h₂ : (dt.sweepSW RF hord mV semOf tOf hlin st₀ f₀ w₂).sav = w₂) : w₁ = w₂

So SAV can hold the address at one address only: the spine's requirement (SW w).sav = w forces the sweep's range to be a single cell.

The sweep's per-address run

reaches_sweep asks for the evaluation's run at each address of the interval, from the pair the sweep arrives with to the pair it leaves. With the branched evaluation that is now provable outright: the entry state's mirror is the address (sweepSWG_mir, which the advance guarantees), so pinning it changes nothing, and the marker and the bottom mark ride from the sweep's base.

What a whole sweep leaves, in dictionary form

sweep_new at the branched evaluation: each address's own reading is new_last_trackOf_B, everything else it leaves alone is spine_new_off, and the next address's entry state is the sweep's own cover equation. Below the address reached, every stage track holds the dictionary of the next stage; elsewhere it still holds what the sweep started with.

theorem DescriptiveComplexity.Draw.Data.sweep_new_trackOf {L : FirstOrder.Language} (dt : Data L) {A R : Type} [Fintype dt.SlotIx] [LinearOrder A] [LinearOrder R] [LinearOrder (OuterPh (EvalPh dt.nv dt.PMF))] [FirstOrder.Language.wide.Structure (Univ A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd)] [Finite A] [Finite R] [Finite (OuterPh (EvalPh dt.nv dt.PMF))] {PR : Prog A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.CtlIx dt.SlotIx dt.KIx dt.dd} (RF : RegFile (Univ A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd)) [Nonempty A] [L.IsRelational] [L.Structure A] [Finite dt.KIx] [LinearOrder (dt.X.Map A)] {ιV : Type} [LinearOrder ιV] [Finite ιV] {aT : ιV} (mV : ιV → Univ A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd → Prop) (hlin : IsLinOrd WMLe) (st₀ : TapeStD dt A R (OuterPh (EvalPh dt.nv dt.PMF))) (f₀ : dt.CtlIx → A) (hord : ∀ (x y : Univ A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd), WMLe x y ↔ tagTupleLe x y) {a₀ : ιV} (hbotV : ∀ (a : ιV), a₀ ≤ a) (hmV0 : mV a₀ = fun (x : Univ A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd) => False) (hIncr : ∀ (a a' : ιV), a < a' → (∀ (b : ιV), ¬(a < b ∧ b < a')) → WMIncr WMLe (mV a) (mV a')) (hKin : ∀ (a : ιV) (t : Tag R (OuterPh (EvalPh dt.nv dt.PMF)) dt.KIx) (w : Fin dt.dd → A), mV a (t, w) → ∃ (jj : Fin dt.ki), t = argIn dt.ko jj) (hTop : ∀ (u : Univ A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd), dt.InnerFull (fun (u : Univ A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd) => tagBlk u.1) (mV aT) u) (hordP : ∀ (p q : dt.X.Map A), p ≤ q ↔ p ≤ q) (σ : dt.d.B.Assignment (dt.X.Map A)) {Below : (Univ A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd → Prop) → Prop} (hdict₀ : ∀ (iv : dt.d.B.ι) (s : Univ A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd → Prop), Below s → (st₀.old iv s ↔ trackOf dt.ly PR.zero PR.one ⋯ σ s)) (hbelow : ∀ (j : Fin dt.nv) (a : ιV) (iv : dt.d.B.ι) (ts : Fin (dt.d.B.arity iv) → Fin (dt.nOf (dt.varAt j))) (st : TapeStD dt A R (OuterPh (EvalPh dt.nv dt.PMF))) (w : Univ A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd → Prop), Below (dt.stageTgtD PR.zero (dt.varAt j) iv ts (dt.roundSt st (mV a)) w (dt.d.B.arity iv))) {gbot : Univ A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd} (hbot : ∀ (y : Univ A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd), WMLe gbot y) {s₁ : Univ A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd → Prop} (hs₁ : WMSetLt WMLe s₁ (RF.cell gbot)) (w : Univ A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd → Prop) : WMSetLe WMLe (fun (x : Univ A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd) => False) w → WMSetLe WMLe w s₁ → (∀ (i : dt.d.B.ι) (r : Univ A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd → Prop), WMSetLe WMLe (fun (x : Univ A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd) => False) r → WMSetLt WMLe r w → ((dt.sweepSWG (dt.stEndB RF hord mV fun (w' : Univ A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd → Prop) (j : Fin dt.nv) (st : TapeStD dt A R (OuterPh (EvalPh dt.nv dt.PMF))) (hg : dt.gatedAt RF j st) => dt.gatedSem RF ⋯ hlin mV j st hg) (dt.fsEndB RF hord mV fun (w' : Univ A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd → Prop) (j : Fin dt.nv) (st : TapeStD dt A R (OuterPh (EvalPh dt.nv dt.PMF))) (hg : dt.gatedAt RF j st) => dt.gatedSem RF ⋯ hlin mV j st hg) hlin st₀ f₀ w).new i r ↔ trackOf dt.ly PR.zero PR.one ⋯ (dt.d.next σ) r)) ∧ ∀ (i : dt.d.B.ι) (r : Univ A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd → Prop), ¬(WMSetLe WMLe (fun (x : Univ A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd) => False) r ∧ WMSetLt WMLe r w) → ((dt.sweepSWG (dt.stEndB RF hord mV fun (w' : Univ A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd → Prop) (j : Fin dt.nv) (st : TapeStD dt A R (OuterPh (EvalPh dt.nv dt.PMF))) (hg : dt.gatedAt RF j st) => dt.gatedSem RF ⋯ hlin mV j st hg) (dt.fsEndB RF hord mV fun (w' : Univ A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd → Prop) (j : Fin dt.nv) (st : TapeStD dt A R (OuterPh (EvalPh dt.nv dt.PMF))) (hg : dt.gatedAt RF j st) => dt.gatedSem RF ⋯ hlin mV j st hg) hlin st₀ f₀ w).new i r ↔ st₀.new i r)

A sweep rewrites the stage tracks of exactly the addresses it has passed, at the concrete branched evaluation.

theorem DescriptiveComplexity.Draw.Data.reaches_spineB {L : FirstOrder.Language} (dt : Data L) {A R : Type} [Fintype dt.SlotIx] [LinearOrder A] [LinearOrder R] [LinearOrder (OuterPh (EvalPh dt.nv dt.PMF))] [FirstOrder.Language.wide.Structure (Univ A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd)] [Finite A] [Finite R] [Finite (OuterPh (EvalPh dt.nv dt.PMF))] {PR : Prog A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.CtlIx dt.SlotIx dt.KIx dt.dd} (RF : RegFile (Univ A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd)) [Nonempty A] [L.IsRelational] [L.Structure A] [Finite dt.KIx] {ιV : Type} [LinearOrder ιV] [Finite ιV] {aT : ιV} (mV : ιV → Univ A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd → Prop) (semAtB : (w : Univ A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd → Prop) → (j : Fin dt.nv) → (st : TapeStD dt A R (OuterPh (EvalPh dt.nv dt.PMF))) → dt.gatedAt RF j st → (p : dt.Scratch A R (OuterPh (EvalPh dt.nv dt.PMF))) → (a : ιV) → (∀ (ℓ : Fin (dt.nIn (dt.varAt j))), dt.igPassP RF PR.zero PR.one (dt.varAt j) (varRdSt st p (mV a)) ℓ) → (b : Fin (dt.natOf (dt.varAt j))) → dt.KindSem PR.zero PR.one (dt.varAt j) (dt.matSt (dt.varAt j) (varRdSt st p (mV a)) w ↑b) (dt.kindOf (dt.varAt j) b)) (hlin : IsLinOrd WMLe) (st₀ : TapeStD dt A R (OuterPh (EvalPh dt.nv dt.PMF))) (f₀ : dt.CtlIx → A) {v' : Univ A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd → Prop} {rEmb : (i : dt.SEF) → dt.SESh i → R} {a₀ : ιV} (hrules : ∀ (i : dt.SEF) (ρ : dt.SESh i), PR.rules (rEmb i ρ) = dt.evalRuleF PR.zero PR.one (fun (w : dt.VarIx) => dt.varArgsOf PR.zero PR.one w) i ρ) (hR : PR.table.Reads) (hord : ∀ (x y : Univ A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd), WMLe x y ↔ tagTupleLe x y) {gtop gbot : Univ A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd} (htop : ∀ (y : Univ A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd), WMLe y gtop) (hbot : ∀ (y : Univ A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd), WMLe gbot y) (hwork : ∀ {r : Univ A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd → Prop}, ¬r gbot → ∀ (u : Univ A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd), WMSetLt WMLe r (RF.cell u)) (hbotV : ∀ (a : ιV), a₀ ≤ a) (htopV : ∀ (a : ιV), a ≤ aT) (hmV0 : mV a₀ = fun (x : Univ A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd) => False) (hIncr : ∀ (a a' : ιV), a < a' → (∀ (b : ιV), ¬(a < b ∧ b < a')) → WMIncr WMLe (mV a) (mV a')) (hTestT : ∀ (u : Univ A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd), dt.InnerFull (fun (u : Univ A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd) => tagBlk u.1) (mV aT) u) (hTestF : ∀ a < aT, ∃ (u : Univ A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd), ¬dt.InnerFull (fun (u : Univ A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd) => tagBlk u.1) (mV a) u) (hwk₀ : st₀.wk = fun (r : Univ A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd → Prop) => r = fun (x : Univ A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd) => False) (hmir₀ : st₀.mir = fun (x : Univ A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd) => False) (hbot₀ : st₀.bot = fun (r : Univ A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd → Prop) => r = fun (x : Univ A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd) => False) {s₁ w : Univ A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd → Prop} (hlb : WMSetLe WMLe (fun (x : Univ A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd) => False) w) (hub : WMSetLe WMLe w s₁) (hv : WMSetLt WMLe w (RF.cell gbot)) (hvi : WMIncr WMLe w v') : Relation.ReflTransGen (wideData (Univ A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd)).Step { state := Sum.inr (PR.stElt (OuterPh.evalP (EvalPh.chk 0)) (dt.sweepFSG (dt.stEndB RF hord mV semAtB) (dt.fsEndB RF hord mV semAtB) hlin st₀ f₀ w)), head := Sum.inl w, tape := wideTape (PR.trackTapeAt RF.cell Slot.val (dt.back RF.cell PR.zero PR.one ⋯ (dt.sweepSWG (dt.stEndB RF hord mV semAtB) (dt.fsEndB RF hord mV semAtB) hlin st₀ f₀ w)) (dt.sweepSWG (dt.stEndB RF hord mV semAtB) (dt.fsEndB RF hord mV semAtB) hlin st₀ f₀ w).val) (PR.syElt PR.blank) } { state := Sum.inr (PR.stElt (OuterPh.evalP (EvalPh.chk (Fin.last dt.nv))) (dt.sweepFsEG (dt.stEndB RF hord mV semAtB) (dt.fsEndB RF hord mV semAtB) hlin st₀ f₀ w)), head := Sum.inl w, tape := wideTape (PR.trackTapeAt RF.cell Slot.val (dt.back RF.cell PR.zero PR.one ⋯ (dt.sweepStEG (dt.stEndB RF hord mV semAtB) (dt.fsEndB RF hord mV semAtB) hlin st₀ f₀ w)) (dt.sweepStEG (dt.stEndB RF hord mV semAtB) (dt.fsEndB RF hord mV semAtB) hlin st₀ f₀ w).val) (PR.syElt PR.blank) }

DescriptiveComplexity.Draw.Data.reaches_sweep's hspine, at one address: the whole per-address evaluation runs, whichever legs each position's gates call for.

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