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

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

One position's write

The spine's writes

@[reducible, inline]

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

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

Equations

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

The spine's semantic reading

What a whole sweep leaves behind

The address's cell, in dictionary form

The semantic pack, transported along the spine

The per-position families, built

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.ixLegStB), and is otherwise the same recursion – the mirror still rides, because no leg writes it.

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

noncomputable def DescriptiveComplexity.Draw.Data.ixSpineNodeB {L : FirstOrder.Language} (dt : Data L) {A R : Type} [Fintype dt.SlotIx] [LinearOrder A] [LinearOrder R] {P : Type} [LinearOrder P] [FirstOrder.Language.wide.Structure (Univ A R P dt.KIx dt.dd)] [Finite A] {PR : Prog A R P dt.CtlIx dt.SlotIx dt.KIx dt.dd} {I : Type} (F : LaidFile dt A R P I) {elt : I → Univ A R P dt.KIx dt.dd} (hinj : Function.Injective elt) (hhasP : F.toLayout.HasName PR.zero) (heltP : ∀ (b : Fin dt.ko ⊕ Fin dt.ki) (c : Fin dt.dd0 → A), elt (F.toLayout.reg hhasP b c) = dt.blkElt b (pad PR.zero c)) [Nonempty A] [L.IsRelational] [L.Structure A] {v : Univ A R P dt.KIx dt.dd → Prop} {ιV : Type} [LinearOrder ιV] {aT : ιV} (mV : ιV → I → Prop) (st₀ : TapeSt dt A R P I) (f₀ : dt.CtlIx → A) (semB : (w : Univ A R P dt.KIx dt.dd → Prop) → (j : Fin dt.nv) → (st : TapeSt dt A R P I) → dt.ixGatedAt F j st → (p : dt.IxScratch A R P I) → (a : ιV) → (∀ (ℓ : Fin (dt.nIn (dt.varAt j))), dt.ixIGPassP F PR.zero PR.one (dt.varAt j) (ixVarRdSt st p (mV a)) ℓ) → (b : Fin (dt.natOf (dt.varAt j))) → dt.IxKindSem PR.zero PR.one (dt.varAt j) (dt.ixMatSt (dt.varAt j) (ixVarRdSt st p (mV a)) w ↑b) elt (dt.kindOf (dt.varAt j) b)) : ℕ → (st : TapeSt dt A R P I) ×' st.mir = st₀.mir ×' (dt.CtlIx → A)

One node of the spine, branched.

Equations

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

noncomputable def DescriptiveComplexity.Draw.Data.ixSpineStOfB {L : FirstOrder.Language} (dt : Data L) {A R : Type} [Fintype dt.SlotIx] [LinearOrder A] [LinearOrder R] {P : Type} [LinearOrder P] [FirstOrder.Language.wide.Structure (Univ A R P dt.KIx dt.dd)] [Finite A] {PR : Prog A R P dt.CtlIx dt.SlotIx dt.KIx dt.dd} {I : Type} (F : LaidFile dt A R P I) {elt : I → Univ A R P dt.KIx dt.dd} (hinj : Function.Injective elt) (hhasP : F.toLayout.HasName PR.zero) (heltP : ∀ (b : Fin dt.ko ⊕ Fin dt.ki) (c : Fin dt.dd0 → A), elt (F.toLayout.reg hhasP b c) = dt.blkElt b (pad PR.zero c)) [Nonempty A] [L.IsRelational] [L.Structure A] {v : Univ A R P dt.KIx dt.dd → Prop} {ιV : Type} [LinearOrder ιV] {aT : ιV} (mV : ιV → I → Prop) (st₀ : TapeSt dt A R P I) (f₀ : dt.CtlIx → A) (semB : (w : Univ A R P dt.KIx dt.dd → Prop) → (j : Fin dt.nv) → (st : TapeSt dt A R P I) → dt.ixGatedAt F j st → (p : dt.IxScratch A R P I) → (a : ιV) → (∀ (ℓ : Fin (dt.nIn (dt.varAt j))), dt.ixIGPassP F PR.zero PR.one (dt.varAt j) (ixVarRdSt st p (mV a)) ℓ) → (b : Fin (dt.natOf (dt.varAt j))) → dt.IxKindSem PR.zero PR.one (dt.varAt j) (dt.ixMatSt (dt.varAt j) (ixVarRdSt st p (mV a)) w ↑b) elt (dt.kindOf (dt.varAt j) b)) (k : Fin (dt.nv + 1)) : TapeSt dt A R P I

The branched tape family of the spine.

Equations

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

noncomputable def DescriptiveComplexity.Draw.Data.ixSpineFsOfB {L : FirstOrder.Language} (dt : Data L) {A R : Type} [Fintype dt.SlotIx] [LinearOrder A] [LinearOrder R] {P : Type} [LinearOrder P] [FirstOrder.Language.wide.Structure (Univ A R P dt.KIx dt.dd)] [Finite A] {PR : Prog A R P dt.CtlIx dt.SlotIx dt.KIx dt.dd} {I : Type} (F : LaidFile dt A R P I) {elt : I → Univ A R P dt.KIx dt.dd} (hinj : Function.Injective elt) (hhasP : F.toLayout.HasName PR.zero) (heltP : ∀ (b : Fin dt.ko ⊕ Fin dt.ki) (c : Fin dt.dd0 → A), elt (F.toLayout.reg hhasP b c) = dt.blkElt b (pad PR.zero c)) [Nonempty A] [L.IsRelational] [L.Structure A] {v : Univ A R P dt.KIx dt.dd → Prop} {ιV : Type} [LinearOrder ιV] {aT : ιV} (mV : ιV → I → Prop) (st₀ : TapeSt dt A R P I) (f₀ : dt.CtlIx → A) (semB : (w : Univ A R P dt.KIx dt.dd → Prop) → (j : Fin dt.nv) → (st : TapeSt dt A R P I) → dt.ixGatedAt F j st → (p : dt.IxScratch A R P I) → (a : ιV) → (∀ (ℓ : Fin (dt.nIn (dt.varAt j))), dt.ixIGPassP F PR.zero PR.one (dt.varAt j) (ixVarRdSt st p (mV a)) ℓ) → (b : Fin (dt.natOf (dt.varAt j))) → dt.IxKindSem PR.zero PR.one (dt.varAt j) (dt.ixMatSt (dt.varAt j) (ixVarRdSt st p (mV a)) w ↑b) elt (dt.kindOf (dt.varAt j) b)) (k : Fin (dt.nv + 1)) : dt.CtlIx → A

The branched control family of the spine.

Equations

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

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.

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.

The sweep's families

The stage atom's restore, as an algebra

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

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