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

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

The enumeration of the variables

One position's write

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.

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).

What a whole sweep leaves behind

The address's cell, in dictionary form

The semantic pack, transported along the spine

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)

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

The per-position families, threaded

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

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)

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.

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

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₀

What the sweep's entry and exit states hold

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.

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.

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.