The outer composition: the sweep's rounds

One round of the outer sweep, at the concrete program: the whole per-address evaluation (DescriptiveComplexity.Draw.Data.evalSpine_run), the boundary dispatch into ADVANCE (the last checkpoint's erasing rule, off the ltp cell), the advance itself (DescriptiveComplexity.Draw.Data.reaches_sweepAdv), the exit dispatch into the next address's first checkpoint and its walk back. The walk is handed between the VAL track (the evaluation's presentation) and the MIRROR track (the advance's) by DescriptiveComplexity.Draw.Data.trackTape_back_swap, which costs nothing because the background carries every register's digits at its own slot.

The evaluation's rules, at the program

The two boundary pieces of a round

The post-sweep reset and mirror clear

One round of the sweep

The whole sweep

theorem DescriptiveComplexity.Draw.Data.reaches_sweep {L : FirstOrder.Language} {dt : Data L} {A : Type} {zero one : A} [LinearOrder A] [Fintype dt.SlotIx] {hzo : zero ≠ one} {args : (v : dt.VarIx) → dt.VarArgs v} [LinearOrder (dt.RIx zero one hzo args)] [LinearOrder dt.PF] {hpl : Fintype.card (dt.CtlIx ⊕ dt.SlotIx) ≤ dt.dd} [FirstOrder.Language.wide.Structure (Univ A (dt.RIx zero one hzo args) dt.PF dt.KIx dt.dd)] [Finite A] [Finite (dt.RIx zero one hzo args)] [Finite dt.PF] [Finite dt.KIx] (hR : (dt.prog zero one hzo args hpl).table.Reads) (hlin : IsLinOrd WMLe) (hord : ∀ (x y : Univ A (dt.RIx zero one hzo args) dt.PF dt.KIx dt.dd), WMLe x y ↔ tagTupleLe x y) {gtop gbot : Univ A (dt.RIx zero one hzo args) dt.PF dt.KIx dt.dd} (htop : ∀ (y : Univ A (dt.RIx zero one hzo args) dt.PF dt.KIx dt.dd), WMLe y gtop) (hbot : ∀ (y : Univ A (dt.RIx zero one hzo args) dt.PF dt.KIx dt.dd), WMLe gbot y) {s₀ s₁ : Univ A (dt.RIx zero one hzo args) dt.PF dt.KIx dt.dd → Prop} (hs₀ : WMSetLe WMLe s₀ s₁) (hs₁ : WMSetLt WMLe s₁ (wmSeg gbot)) {SW stE : (Univ A (dt.RIx zero one hzo args) dt.PF dt.KIx dt.dd → Prop) → TapeStD dt A (dt.RIx zero one hzo args) dt.PF} {FS fsE : (Univ A (dt.RIx zero one hzo args) dt.PF dt.KIx dt.dd → Prop) → dt.CtlIx → A} (hspine : ∀ (v : Univ A (dt.RIx zero one hzo args) dt.PF dt.KIx dt.dd → Prop), WMSetLe WMLe s₀ v → WMSetLt WMLe v s₁ → Relation.ReflTransGen (wideData (Univ A (dt.RIx zero one hzo args) dt.PF dt.KIx dt.dd)).Step { state := Sum.inr ((dt.prog zero one hzo args hpl).stElt (OuterPh.evalP (EvalPh.chk 0)) (FS v)), head := Sum.inl v, tape := wideTape ((dt.prog zero one hzo args hpl).trackTapeAt wmSeg Slot.val (dt.back wmSeg zero one ⋯ (SW v)) (SW v).val) ((dt.prog zero one hzo args hpl).syElt (dt.prog zero one hzo args hpl).blank) } { state := Sum.inr ((dt.prog zero one hzo args hpl).stElt (OuterPh.evalP (EvalPh.chk (Fin.last dt.nv))) (fsE v)), head := Sum.inl v, tape := wideTape ((dt.prog zero one hzo args hpl).trackTapeAt wmSeg Slot.val (dt.back wmSeg zero one ⋯ (stE v)) (stE v).val) ((dt.prog zero one hzo args hpl).syElt (dt.prog zero one hzo args hpl).blank) }) (hwkE : ∀ (v : Univ A (dt.RIx zero one hzo args) dt.PF dt.KIx dt.dd → Prop), WMSetLe WMLe s₀ v → WMSetLt WMLe v s₁ → (stE v).wk = fun (r : Univ A (dt.RIx zero one hzo args) dt.PF dt.KIx dt.dd → Prop) => r = v) (hmirE : ∀ (v : Univ A (dt.RIx zero one hzo args) dt.PF dt.KIx dt.dd → Prop), WMSetLe WMLe s₀ v → WMSetLt WMLe v s₁ → (stE v).mir = v) (hltpE : ∀ (v : Univ A (dt.RIx zero one hzo args) dt.PF dt.KIx dt.dd → Prop), WMSetLe WMLe s₀ v → WMSetLt WMLe v s₁ → ¬(stE v).ltp v) (hSW : ∀ (v v' : Univ A (dt.RIx zero one hzo args) dt.PF dt.KIx dt.dd → Prop), WMIncr WMLe v v' → WMSetLe WMLe s₀ v → WMSetLe WMLe v' s₁ → SW v' = have __src := dt.atSt (stE v) v'; { mir := v', tgt := __src.tgt, sav := __src.sav, val := __src.val, old := __src.old, new := __src.new, wk := __src.wk, bot := __src.bot, ltp := __src.ltp }) (hFS : ∀ (v v' : Univ A (dt.RIx zero one hzo args) dt.PF dt.KIx dt.dd → Prop), WMIncr WMLe v v' → WMSetLe WMLe s₀ v → WMSetLe WMLe v' s₁ → FS v' = fsE v) : Relation.ReflTransGen (wideData (Univ A (dt.RIx zero one hzo args) dt.PF dt.KIx dt.dd)).Step { state := Sum.inr ((dt.prog zero one hzo args hpl).stElt (OuterPh.evalP (EvalPh.chk 0)) (FS s₀)), head := Sum.inl s₀, tape := wideTape ((dt.prog zero one hzo args hpl).trackTapeAt wmSeg Slot.val (dt.back wmSeg zero one ⋯ (SW s₀)) (SW s₀).val) ((dt.prog zero one hzo args hpl).syElt (dt.prog zero one hzo args hpl).blank) } { state := Sum.inr ((dt.prog zero one hzo args hpl).stElt (OuterPh.evalP (EvalPh.chk 0)) (FS s₁)), head := Sum.inl s₁, tape := wideTape ((dt.prog zero one hzo args hpl).trackTapeAt wmSeg Slot.val (dt.back wmSeg zero one ⋯ (SW s₁)) (SW s₁).val) ((dt.prog zero one hzo args hpl).syElt (dt.prog zero one hzo args hpl).blank) }

The outer sweep: from the first checkpoint at the bottom of the stretch to the first checkpoint at its top, one round per address – each round the per-address evaluation and the advance, glued by DescriptiveComplexity.Draw.Data.sweepRound. The evaluation runs, the end-state facts and the two cover equations (the tape and control threads across addresses) are per-address hypotheses; everything else is DescriptiveComplexity.reaches_of_wideRounds.

Entering the convergence sweep

A plain sweep cannot be entered from the left of the empty address, so clearMir2's verdict exit is COMPARE's first step: it tests the empty address's cell and lands at its successor, in exactly the sweep's state there. The sweep then continues from the successor (DescriptiveComplexity.Draw.FlagSweepKit.reaches is general in its stretch, which reaches_compareFrom exposes).

The compare verdicts, and the copy-back ring

At the ltp cell the sweep's verdict dispatches: passing to the output's walk home, failing to the copy-back's. The copy-back has the same folded entry as the sweep it corrects: homeCmp's exit rewrites the empty address's cell and lands at its successor, and the copy exits at the ltp cell into its own walk home, whose exit re-enters the evaluation.

Closing a stage

After the sweep's last round the machine stands at the first checkpoint on the ltp cell. One more evaluation runs there (its writes are junk the copy never propagates and nothing reads), then the erasing .dspB exit, the reset, the mirror clear and the convergence sweep. Its verdict closes the stage: failing, the copy-back rewrites every old track and the walk home re-enters the evaluation – the next stage's entry; passing, the walk home enters the out machinery.

MAIN

The loop: one sweep and one stage-closing ring per stage, iterated while the convergence sweep fails, and the passing ring at the first stage that stabilizes. Everything semantic – the per-stage tape and control families and the runs themselves – is a hypothesis family; the loop is a plain induction on the first converged index.

theorem DescriptiveComplexity.Draw.Data.reaches_main {L : FirstOrder.Language} {dt : Data L} {A : Type} {zero one : A} [LinearOrder A] [Fintype dt.SlotIx] {hzo : zero ≠ one} {args : (v : dt.VarIx) → dt.VarArgs v} [LinearOrder (dt.RIx zero one hzo args)] [LinearOrder dt.PF] {hpl : Fintype.card (dt.CtlIx ⊕ dt.SlotIx) ≤ dt.dd} [FirstOrder.Language.wide.Structure (Univ A (dt.RIx zero one hzo args) dt.PF dt.KIx dt.dd)] [Finite A] [Finite (dt.RIx zero one hzo args)] [Finite dt.PF] [Finite dt.KIx] (hR : (dt.prog zero one hzo args hpl).table.Reads) (hlin : IsLinOrd WMLe) (hord : ∀ (x y : Univ A (dt.RIx zero one hzo args) dt.PF dt.KIx dt.dd), WMLe x y ↔ tagTupleLe x y) {gtop gbot : Univ A (dt.RIx zero one hzo args) dt.PF dt.KIx dt.dd} (htop : ∀ (y : Univ A (dt.RIx zero one hzo args) dt.PF dt.KIx dt.dd), WMLe y gtop) (hbot : ∀ (y : Univ A (dt.RIx zero one hzo args) dt.PF dt.KIx dt.dd), WMLe gbot y) {ltpAddr : Univ A (dt.RIx zero one hzo args) dt.PF dt.KIx dt.dd → Prop} (hlt : WMSetLt WMLe ltpAddr (wmSeg gbot)) (hneT : ∃ (x : Univ A (dt.RIx zero one hzo args) dt.PF dt.KIx dt.dd), ltpAddr x) {v₁ : Univ A (dt.RIx zero one hzo args) dt.PF dt.KIx dt.dd → Prop} (hiE : WMIncr WMLe (fun (x : Univ A (dt.RIx zero one hzo args) dt.PF dt.KIx dt.dd) => False) v₁) {N : ℕ} {entrySt topSt stT : ℕ → TapeStD dt A (dt.RIx zero one hzo args) dt.PF} {entryFs topFs fsT : ℕ → dt.CtlIx → A} (hsweep : ∀ n ≤ N, Relation.ReflTransGen (wideData (Univ A (dt.RIx zero one hzo args) dt.PF dt.KIx dt.dd)).Step { state := Sum.inr ((dt.prog zero one hzo args hpl).stElt (OuterPh.evalP (EvalPh.chk 0)) (entryFs n)), head := Sum.inl fun (x : Univ A (dt.RIx zero one hzo args) dt.PF dt.KIx dt.dd) => False, tape := wideTape ((dt.prog zero one hzo args hpl).trackTapeAt wmSeg Slot.val (dt.back wmSeg zero one ⋯ (entrySt n)) (entrySt n).val) ((dt.prog zero one hzo args hpl).syElt (dt.prog zero one hzo args hpl).blank) } { state := Sum.inr ((dt.prog zero one hzo args hpl).stElt (OuterPh.evalP (EvalPh.chk 0)) (topFs n)), head := Sum.inl ltpAddr, tape := wideTape ((dt.prog zero one hzo args hpl).trackTapeAt wmSeg Slot.val (dt.back wmSeg zero one ⋯ (topSt n)) (topSt n).val) ((dt.prog zero one hzo args hpl).syElt (dt.prog zero one hzo args hpl).blank) }) (hspineT : ∀ n ≤ N, Relation.ReflTransGen (wideData (Univ A (dt.RIx zero one hzo args) dt.PF dt.KIx dt.dd)).Step { state := Sum.inr ((dt.prog zero one hzo args hpl).stElt (OuterPh.evalP (EvalPh.chk 0)) (topFs n)), head := Sum.inl ltpAddr, tape := wideTape ((dt.prog zero one hzo args hpl).trackTapeAt wmSeg Slot.val (dt.back wmSeg zero one ⋯ (topSt n)) (topSt n).val) ((dt.prog zero one hzo args hpl).syElt (dt.prog zero one hzo args hpl).blank) } { state := Sum.inr ((dt.prog zero one hzo args hpl).stElt (OuterPh.evalP (EvalPh.chk (Fin.last dt.nv))) (fsT n)), head := Sum.inl ltpAddr, tape := wideTape ((dt.prog zero one hzo args hpl).trackTapeAt wmSeg Slot.val (dt.back wmSeg zero one ⋯ (stT n)) (stT n).val) ((dt.prog zero one hzo args hpl).syElt (dt.prog zero one hzo args hpl).blank) }) (hwkT : ∀ n ≤ N, (stT n).wk = fun (r : Univ A (dt.RIx zero one hzo args) dt.PF dt.KIx dt.dd → Prop) => r = ltpAddr) (hltpT : ∀ n ≤ N, (stT n).ltp = fun (r : Univ A (dt.RIx zero one hzo args) dt.PF dt.KIx dt.dd → Prop) => r = ltpAddr) (hbotT : ∀ n ≤ N, (stT n).bot = fun (r : Univ A (dt.RIx zero one hzo args) dt.PF dt.KIx dt.dd → Prop) => r = fun (x : Univ A (dt.RIx zero one hzo args) dt.PF dt.KIx dt.dd) => False) (hnotconv : ∀ n < N, ¬∀ (r : Univ A (dt.RIx zero one hzo args) dt.PF dt.KIx dt.dd → Prop), WMSetLt WMLe r ltpAddr → ∀ (i : dt.d.B.ι), (stT n).old i r ↔ (stT n).new i r) (hconv : ∀ (r : Univ A (dt.RIx zero one hzo args) dt.PF dt.KIx dt.dd → Prop), WMSetLt WMLe r ltpAddr → ∀ (i : dt.d.B.ι), (stT N).old i r ↔ (stT N).new i r) (hnextSt : ∀ n < N, entrySt (n + 1) = dt.copySt zero one hzo args (have __src := dt.atSt (dt.offSt (stT n)) fun (x : Univ A (dt.RIx zero one hzo args) dt.PF dt.KIx dt.dd) => False; { mir := fun (x : Univ A (dt.RIx zero one hzo args) dt.PF dt.KIx dt.dd) => False, tgt := __src.tgt, sav := __src.sav, val := __src.val, old := __src.old, new := __src.new, wk := __src.wk, bot := __src.bot, ltp := __src.ltp }) ltpAddr) (hnextFs : ∀ n < N, entryFs (n + 1) = fsT n) : Relation.ReflTransGen (wideData (Univ A (dt.RIx zero one hzo args) dt.PF dt.KIx dt.dd)).Step { state := Sum.inr ((dt.prog zero one hzo args hpl).stElt (OuterPh.evalP (EvalPh.chk 0)) (entryFs 0)), head := Sum.inl fun (x : Univ A (dt.RIx zero one hzo args) dt.PF dt.KIx dt.dd) => False, tape := wideTape ((dt.prog zero one hzo args hpl).trackTapeAt wmSeg Slot.val (dt.back wmSeg zero one ⋯ (entrySt 0)) (entrySt 0).val) ((dt.prog zero one hzo args hpl).syElt (dt.prog zero one hzo args hpl).blank) } { state := Sum.inr ((dt.prog zero one hzo args hpl).stElt (OuterPh.evalP (EvalPh.sub dt.smEntryOut)) (fsT N)), head := Sum.inl v₁, tape := wideTape ((dt.prog zero one hzo args hpl).trackTapeAt wmSeg Slot.val (dt.back wmSeg zero one ⋯ (have __src := dt.atSt (dt.offSt (stT N)) fun (x : Univ A (dt.RIx zero one hzo args) dt.PF dt.KIx dt.dd) => False; { mir := fun (x : Univ A (dt.RIx zero one hzo args) dt.PF dt.KIx dt.dd) => False, tgt := __src.tgt, sav := __src.sav, val := __src.val, old := __src.old, new := __src.new, wk := __src.wk, bot := __src.bot, ltp := __src.ltp })) (have __src := dt.atSt (dt.offSt (stT N)) fun (x : Univ A (dt.RIx zero one hzo args) dt.PF dt.KIx dt.dd) => False; { mir := fun (x : Univ A (dt.RIx zero one hzo args) dt.PF dt.KIx dt.dd) => False, tgt := __src.tgt, sav := __src.sav, val := __src.val, old := __src.old, new := __src.new, wk := __src.wk, bot := __src.bot, ltp := __src.ltp }).val) ((dt.prog zero one hzo args hpl).syElt (dt.prog zero one hzo args hpl).blank) }

The MAIN loop: from the first stage's entry at the empty address, through one sweep and one closing ring per stage, to the out machinery's entry checkpoint at the first stage whose convergence sweep passes.