The clocked program's whole run, and its clock

The two halves are counted separately – the opening and the evaluation (DescriptiveComplexity.Draw.Data.nexEval_reachesIn) – and this file puts them together and compares the sum with the clock.

The opening is DescriptiveComplexity.Draw.Data.reachesIn_openingRegion, here: the approach walk up to the file's base, the file-laying sweep, and the guess along the region below the file – one bit per address, which is what the guessed relations are – for 2·R + 2·base + (the guessed stretch out and back) + 4, and openingRegion_le bounds that by the number of addresses.

Two things are worth naming. The presentation bridge: the opening is stated with the tape walked along the mirror track and the evaluation along VAL, and the two are the same tape whenever both marks are the background's own (DescriptiveComplexity.Draw.trackTape_of_back), so the caller hands that equality over rather than either run being restated. And the arithmetic: the total is «opening + rounds × width», which is mul_add_lt_two_pow's shape – so what the clock asks is that the opening and each of the evaluation's two factors fit the region, with one surplus block of slack for the additive term. The opening is a bare number there (nexTotal_lt_two_pow), so either shape of it is compared the same way.

The initial end is here as well, and it is three small facts. DescriptiveComplexity.Draw.Prog.trackTapeAt_initBack says the all-blank tape is the pass-layer presentation at any file – which a clocked program needs, because its file does not exist at time zero – and DescriptiveComplexity.Draw.Data.startBack with startBack_frame / startBack_wr is the background the opening's first step leaves: the one it started from with the marker planted, which is the frame condition and the write that step asks for.

The forward direction lands here too (nexProg_wideAccept): an accepting run of fewer than 2 ^ n steps from the initial configuration is a yes-instance of DescriptiveComplexity.WideAccept. Two of its hypotheses are rfl at the assembled program, and that is the point of the program declining the input channel's marks: with mark the blank, the tape is blank everywhere at time zero and the channel's ruler is not there to be mistaken for a register (trackTape_blank_congr for the presentations).

The backward direction's foundation is here as well: nexProg_sepOn – the program separates at every post-guess phase, across sites by the owner map and within a site by nexSep_postGuess – and nexProg_uniqueFrom, which is what a reduction reads its certificate off an arbitrary accepting run with. The fact it stands on – that the evaluation's rules never leave the post-guess phases – is proved, not assumed: nexEvalRuleF_postGuess, and under it a chain of «this machinery leaves only into its own phases or its exit» lemmas, one per builder, down to the trips.

The opening, with the guess over the region

The state a clocked program starts in

Its first step plants the marker at the empty address and nothing else has been written, so the state is clear but for the marker – and its background is the blank tape everywhere off the file, which is what the opening's frame hypotheses (hbelow, habove, hwr) ask of the caller.

noncomputable def DescriptiveComplexity.Draw.Data.nexEntrySt {L : FirstOrder.Language} (dt : Data L) {A R' PE I : Type} (v : Univ A R' (NexPh (Option dt.KIx) PE) dt.KIx dt.dd → Prop) : TapeSt dt A R' (NexPh (Option dt.KIx) PE) I

The state a clocked program enters its opening in: every register and every track clear, the marker and the bottom mark at the address the head stands on – the two the opening's first step writes, and the two the evaluation's walks read.

Equations

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

theorem DescriptiveComplexity.Draw.Data.reachesIn_openingRegion {L : FirstOrder.Language} {dt : Data L} {A R' PE SE : Type} {ShE : SE → Type} [Fintype dt.CtlIx] [Fintype dt.SlotIx] [DecidableEq dt.SlotIx] [LinearOrder A] [LinearOrder R'] [Nonempty A] [Finite A] [Finite R'] [Finite dt.KIx] [LinearOrder (NexPh (Option dt.KIx) PE)] [Finite (NexPh (Option dt.KIx) PE)] [FirstOrder.Language.wide.Structure (Univ A R' (NexPh (Option dt.KIx) PE) dt.KIx dt.dd)] [Finite (Univ A R' (NexPh (Option dt.KIx) PE) dt.KIx dt.dd)] {PR : Prog A R' (NexPh (Option dt.KIx) PE) dt.CtlIx dt.SlotIx dt.KIx dt.dd} {coord : Fin dt.dd → dt.CtlIx} {f₀ : dt.CtlIx → A} {ruleE : (e : SE) → ShE e → Rule A dt.CtlIx dt.SlotIx (NexPh (Option dt.KIx) PE)} {evalEntry : PE} (hcoord : Function.Injective coord) (hR : PR.table.Reads) (h : IsLinOrd WMLe) {base : ℕ} (hpos : 0 < base) (hbase : base + Nat.card (Wide.BlkIx dt.KIx A dt.dd) < Nat.card { p : WPoint (Univ A R' (NexPh (Option dt.KIx) PE) dt.KIx dt.dd) // (wideData (Univ A R' (NexPh (Option dt.KIx) PE) dt.KIx dt.dd)).Posn p }) {st : TapeSt dt A R' (NexPh (Option dt.KIx) PE) (Wide.BlkIx dt.KIx A dt.dd)} (hmir : ∀ (u : Wide.BlkIx dt.KIx A dt.dd), ¬st.mir u) (htgt : ∀ (u : Wide.BlkIx dt.KIx A dt.dd), ¬st.tgt u) (hsav : ∀ (u : Wide.BlkIx dt.KIx A dt.dd), ¬st.sav u) (hval : ∀ (u : Wide.BlkIx dt.KIx A dt.dd), ¬st.val u) (hwk : ∀ (v : Wide.BlkIx dt.KIx A dt.dd), ¬st.wk ((dt.blkLaid h hpos ⋯).cell v)) (hbotR : ∀ (v : Wide.BlkIx dt.KIx A dt.dd), ¬st.bot ((dt.blkLaid h hpos ⋯).cell v)) (hltp : ∀ (v : Wide.BlkIx dt.KIx A dt.dd), ¬st.ltp ((dt.blkLaid h hpos ⋯).cell v)) (hold : ∀ (i : dt.d.B.ι) (v : Wide.BlkIx dt.KIx A dt.dd), ¬st.old i ((dt.blkLaid h hpos ⋯).cell v)) (hnew : ∀ (i : dt.d.B.ι) (v : Wide.BlkIx dt.KIx A dt.dd), ¬st.new i ((dt.blkLaid h hpos ⋯).cell v)) {v v' v₁ x s₀ top : Univ A R' (NexPh (Option dt.KIx) PE) dt.KIx dt.dd → Prop} (hwkS : st.wk = fun (r : Univ A R' (NexPh (Option dt.KIx) PE) dt.KIx dt.dd → Prop) => r = v) (hv0 : wideRank v = 0) (hle : WMSetLe WMLe v ((dt.blkLaid h hpos ⋯).cell (blkTop A dt.KIx dt.dd))) (hvi₁ : WMIncr WMLe v v₁) (hwalk : WMSetLe WMLe v₁ x) (hxb : WMIncr WMLe x ((dt.blkLaid h hpos ⋯).cell (blkBot A dt.KIx dt.dd))) (hs₀ : WMIncr WMLe v s₀) (hvi' : WMIncr WMLe v v') {bg bg₀ : (Univ A R' (NexPh (Option dt.KIx) PE) dt.KIx dt.dd → Prop) → dt.SlotIx → A} (hframe : ∀ (r : Univ A R' (NexPh (Option dt.KIx) PE) dt.KIx dt.dd → Prop), r ≠ v → bg₀ r = bg r) (hwr : PR.passTracksAt (dt.blkLaid h hpos ⋯).cell Slot.mir bg₀ (fun (x : Wide.BlkIx dt.KIx A dt.dd) => False) v = Function.update (Function.update (PR.passTracksAt (dt.blkLaid h hpos ⋯).cell Slot.mir bg (fun (x : Wide.BlkIx dt.KIx A dt.dd) => False) v) Slot.wk PR.one) Slot.bot PR.one) (hbelow : ∀ (r : Univ A R' (NexPh (Option dt.KIx) PE) dt.KIx dt.dd → Prop), WMSetLt WMLe r ((dt.blkLaid h hpos ⋯).cell (blkBot A dt.KIx dt.dd)) → dt.ixBack (dt.blkLaid h hpos ⋯).toLayout PR.zero PR.one ⋯ st r = bg₀ r) (habove : ∀ (r : Univ A R' (NexPh (Option dt.KIx) PE) dt.KIx dt.dd → Prop), ¬WMSetLt WMLe r (ixSegTop (Wide.BlkIx dt.KIx A dt.dd) h base) → dt.ixBack (dt.blkLaid h hpos ⋯).toLayout PR.zero PR.one ⋯ st r = bg₀ r) (σ : dt.d.B.ι → (Univ A R' (NexPh (Option dt.KIx) PE) dt.KIx dt.dd → Prop) → Prop) (htop : WMSetLe WMLe s₀ top) (htopne : ∃ (y : Univ A R' (NexPh (Option dt.KIx) PE) dt.KIx dt.dd), top y) (hout : ∀ (i : dt.d.B.ι) (r : Univ A R' (NexPh (Option dt.KIx) PE) dt.KIx dt.dd → Prop), WMSetLt WMLe r s₀ ∨ ¬WMSetLt WMLe r top → (σ i r ↔ st.old i r)) (hexB : dt.exitG PR.one (PR.passTracksAt (dt.blkLaid h hpos ⋯).cell Slot.mir (dt.ixBack (dt.blkLaid h hpos ⋯).toLayout PR.zero PR.one ⋯ st) (fun (x : Wide.BlkIx dt.KIx A dt.dd) => False) v)) (hexG : dt.exitG PR.one (PR.passTracksAt (dt.blkLaid h hpos ⋯).cell Slot.mir (dt.ixBack (dt.blkLaid h hpos ⋯).toLayout PR.zero PR.one ⋯ { mir := st.mir, tgt := st.tgt, sav := st.sav, val := st.val, old := σ, new := st.new, wk := st.wk, bot := st.bot, ltp := st.ltp }) (fun (x : Wide.BlkIx dt.KIx A dt.dd) => False) v)) {rEmb0 : (i : NexSite SE) → NexSh SE (Option dt.KIx) (dt.d.B.ι → Bool) ShE i → R'} (hrules0 : ∀ (i : NexSite SE) (ρ : NexSh SE (Option dt.KIx) (dt.d.B.ι → Bool) ShE i), PR.rules (rEmb0 i ρ) = dt.nexRule PR.one (dt.buildSpec PR.zero PR.one coord) (dt.regionSpec PR.zero PR.one) ruleE evalEntry (blkBot A dt.KIx dt.dd).1 i ρ) : (wideData (Univ A R' (NexPh (Option dt.KIx) PE) dt.KIx dt.dd)).ReachesIn (2 * Nat.card (Wide.BlkIx dt.KIx A dt.dd) + 2 * base + (wideRank top - wideRank s₀ + wideRank top) + 4) { state := Sum.inr (PR.stElt NexPh.start (dt.ctlOf coord f₀ (blkBot A dt.KIx dt.dd).2)), head := Sum.inl v, tape := wideTape (PR.trackTapeAt (dt.blkLaid h hpos ⋯).cell Slot.mir bg fun (x : Wide.BlkIx dt.KIx A dt.dd) => False) (PR.syElt PR.blank) } { state := Sum.inr (PR.stElt (NexPh.evalP evalEntry) (dt.ctlOf coord f₀ (blkBot A dt.KIx dt.dd).2)), head := Sum.inl v', tape := wideTape (PR.trackTapeAt (dt.blkLaid h hpos ⋯).cell Slot.mir (dt.ixBack (dt.blkLaid h hpos ⋯).toLayout PR.zero PR.one ⋯ { mir := st.mir, tgt := st.tgt, sav := st.sav, val := st.val, old := σ, new := st.new, wk := st.wk, bot := st.bot, ltp := st.ltp }) fun (x : Wide.BlkIx dt.KIx A dt.dd) => False) (PR.syElt PR.blank) }

The clocked program's opening: the opening step, the approach walk up to the file's base, the file-laying phase, the walk home with the turn into the guess, the region-wide guess with its stop and its own walk home, and the dispatch into the evaluation.

The file is laid above the program's data and the certificate is guessed below it, which is what lets a stage atom seek to a dictionary entry: the entry is a logical address and every logical address is below every register. The approach is the price of that arrangement – the base is not the marker's neighbor, so getting there is a walk and not a step – and where it stops is the program's choice, a machine having no landmark but the cell it started on.

What the guess writes

The stage tracks a clocked program guesses are an assignment's, restricted to the stretch the guess sweeps – the file's first register up to the end marker. Restricting them is what makes the opening's frame condition true (outside that stretch the tracks are the entry state's, which is empty), and it costs the dictionary nothing, since every entry the evaluation reads is inside the stretch (a track marks no empty address, nonempty_of_trackOf).

def DescriptiveComplexity.Draw.Data.guessTracks {L : FirstOrder.Language} (dt : Data L) {A R' PE : Type} [LinearOrder A] [L.Structure A] [FirstOrder.Language.wide.Structure (Univ A R' (NexPh (Option dt.KIx) PE) dt.KIx dt.dd)] (zero one : A) (σ : dt.d.B.Assignment (dt.X.Map A)) (bot top : Univ A R' (NexPh (Option dt.KIx) PE) dt.KIx dt.dd → Prop) : dt.d.B.ι → (Univ A R' (NexPh (Option dt.KIx) PE) dt.KIx dt.dd → Prop) → Prop

The tracks the guess writes: an assignment's, inside the swept stretch.

Equations

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

The opening of a program that is handed its file

A program handed its file has nothing to lay: its file-laying phase is the two steps of nullSpec and the rest of the opening is the same. So the whole opening is stated here at an arbitrary file – the five steps of NexBuild's AnyFile section, the sweep that is over at once, the two walks home and the guess, which was generic already. Nothing of the file is read but its cells.

theorem DescriptiveComplexity.Draw.Data.reachesIn_openingHanded {L : FirstOrder.Language} {dt : Data L} {A R' PE SE : Type} {ShE : SE → Type} [Fintype dt.CtlIx] [Fintype dt.SlotIx] [DecidableEq dt.SlotIx] [LinearOrder A] [LinearOrder R'] [Finite A] [Finite R'] [Finite dt.KIx] [LinearOrder (NexPh (Option dt.KIx) PE)] [Finite (NexPh (Option dt.KIx) PE)] [FirstOrder.Language.wide.Structure (Univ A R' (NexPh (Option dt.KIx) PE) dt.KIx dt.dd)] [Finite (Univ A R' (NexPh (Option dt.KIx) PE) dt.KIx dt.dd)] {PR : Prog A R' (NexPh (Option dt.KIx) PE) dt.CtlIx dt.SlotIx dt.KIx dt.dd} {ruleE : (e : SE) → ShE e → Rule A dt.CtlIx dt.SlotIx (NexPh (Option dt.KIx) PE)} {evalEntry : PE} {I : Type} {F : LaidFile dt A R' (NexPh (Option dt.KIx) PE) I} {betaS : SweepSpec A dt.CtlIx dt.SlotIx (Option dt.KIx)} {botS : Option dt.KIx} (hR : PR.table.Reads) (h : IsLinOrd WMLe) {st : TapeSt dt A R' (NexPh (Option dt.KIx) PE) I} {v : Univ A R' (NexPh (Option dt.KIx) PE) dt.KIx dt.dd → Prop} (hwkS : st.wk = fun (r : Univ A R' (NexPh (Option dt.KIx) PE) dt.KIx dt.dd → Prop) => r = v) {v₁ x y y' s₀ s₁ v' : Univ A R' (NexPh (Option dt.KIx) PE) dt.KIx dt.dd → Prop} (hvi₁ : WMIncr WMLe v v₁) (hwalk : WMSetLe WMLe v₁ x) (hxy : WMIncr WMLe x y) (hyy' : WMIncr WMLe y y') (hyv : WMSetLe WMLe v y) (hvs₀ : WMIncr WMLe v s₀) (hle : WMSetLe WMLe s₀ s₁) (hne₁ : ∃ (z : Univ A R' (NexPh (Option dt.KIx) PE) dt.KIx dt.dd), s₁ z) (hvv' : WMIncr WMLe v v') {bg bg₀ : (Univ A R' (NexPh (Option dt.KIx) PE) dt.KIx dt.dd → Prop) → dt.SlotIx → A} (hframe : ∀ (r : Univ A R' (NexPh (Option dt.KIx) PE) dt.KIx dt.dd → Prop), r ≠ v → bg₀ r = bg r) (hwr : PR.passTracksAt F.cell Slot.mir bg₀ (fun (x : I) => False) v = Function.update (Function.update (PR.passTracksAt F.cell Slot.mir bg (fun (x : I) => False) v) Slot.wk PR.one) Slot.bot PR.one) (hback : bg₀ = dt.ixBack F.toLayout PR.zero PR.one ⋯ st) (f : dt.CtlIx → A) (hroll : betaS.Roll botS f) (hdone : betaS.Done botS f) (hstRoll : betaS.stRoll botS f (PR.passTracksAt F.cell Slot.mir bg₀ (fun (x : I) => False) y) = f) (hwrS : betaS.wr botS f (PR.passTracksAt F.cell Slot.mir bg₀ (fun (x : I) => False) y) = PR.passTracksAt F.cell Slot.mir bg₀ (fun (x : I) => False) y) (hexB : dt.exitG PR.one (PR.passTracksAt F.cell Slot.mir bg₀ (fun (x : I) => False) v)) (σ : dt.d.B.ι → (Univ A R' (NexPh (Option dt.KIx) PE) dt.KIx dt.dd → Prop) → Prop) (hout : ∀ (i : dt.d.B.ι) (r : Univ A R' (NexPh (Option dt.KIx) PE) dt.KIx dt.dd → Prop), WMSetLt WMLe r s₀ ∨ ¬WMSetLt WMLe r s₁ → (σ i r ↔ st.old i r)) (hexG : dt.exitG PR.one (PR.passTracksAt F.cell Slot.mir (dt.ixBack F.toLayout PR.zero PR.one ⋯ { mir := st.mir, tgt := st.tgt, sav := st.sav, val := st.val, old := σ, new := st.new, wk := st.wk, bot := st.bot, ltp := st.ltp }) (fun (x : I) => False) v)) {rEmbS : (i : NexSite SE) → NexSh SE (Option dt.KIx) (dt.d.B.ι → Bool) ShE i → R'} (hrulesS : ∀ (i : NexSite SE) (ρ : NexSh SE (Option dt.KIx) (dt.d.B.ι → Bool) ShE i), PR.rules (rEmbS i ρ) = dt.nexRule PR.one betaS (dt.regionSpec PR.zero PR.one) ruleE evalEntry botS i ρ) {rHomeB rHomeG : HomeKit.HomeRule → R'} (hrulesHB : ∀ (ρ : HomeKit.HomeRule), PR.rules (rHomeB ρ) = { t := Slot.mir, wk := Slot.wk, ph := NexPh.homeBuildP }.rule PR.one ρ) (hrulesHG : ∀ (ρ : HomeKit.HomeRule), PR.rules (rHomeG ρ) = { t := Slot.mir, wk := Slot.wk, ph := NexPh.homeGuessP }.rule PR.one ρ) : (wideData (Univ A R' (NexPh (Option dt.KIx) PE) dt.KIx dt.dd)).ReachesIn (wideRank x - wideRank v₁ + (wideRank y - wideRank v) + (wideRank s₁ - wideRank s₀ + (wideRank s₁ - wideRank v)) + 7) { state := Sum.inr (PR.stElt NexPh.start f), head := Sum.inl v, tape := wideTape (PR.trackTapeAt F.cell Slot.mir bg fun (x : I) => False) (PR.syElt PR.blank) } { state := Sum.inr (PR.stElt (NexPh.evalP evalEntry) (betaS.st0 f (PR.passTracksAt F.cell Slot.mir bg₀ (fun (x : I) => False) v))), head := Sum.inl v', tape := wideTape (PR.trackTapeAt F.cell Slot.mir (dt.ixBack F.toLayout PR.zero PR.one ⋯ { mir := st.mir, tgt := st.tgt, sav := st.sav, val := st.val, old := σ, new := st.new, wk := st.wk, bot := st.bot, ltp := st.ltp }) fun (x : I) => False) (PR.syElt PR.blank) }

The whole opening of a program that is handed its file: plant the two marks, walk up, run the sweep that lays nothing, turn round, walk home, guess the certificate over the stretch, walk home again, and step into the evaluation. Its cost is the two walks up and back, the guess's stretch out and back, and six single steps.

theorem DescriptiveComplexity.Draw.Data.nexTotal_lt_two_pow' {k j m o e a b : ℕ} (hk : 1 ≤ k) (hkj : k + 1 < j) (hm : 0 < m) (he : e ≤ a * b) (ha : a ≤ 2 ^ (k * m)) (hb : b ≤ 2 ^ (k * m)) (hopen : o + 1 ≤ 2 ^ ((k + 1) * m)) : o + e + 1 < 2 ^ ((k + j) * m)

The clock comparison, with the opening at twice the region: the shape a program that lays a file and guesses over the region actually meets – its opening is two sweeps, not a fraction of one. One working block is enough (1 ≤ k), and the rest is mul_add_lt_two_pow'.

The forward direction at the assembled program

theorem DescriptiveComplexity.Draw.Data.nexProg_initBack {L : FirstOrder.Language} {dt : Data L} {A G : Type} [Fintype dt.CtlIx] [Fintype dt.SlotIx] [DecidableEq dt.SlotIx] [LinearOrder A] [Finite A] [Finite dt.KIx] [Nonempty A] {zero one : A} [FirstOrder.Language.wide.Structure (Univ A dt.NexRIx (NexPh (Option dt.KIx) (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd)] (hzo : zero ≠ one) (hpl : Fintype.card (dt.CtlIx ⊕ dt.SlotIx) ≤ dt.dd) (coord : Fin dt.dd → dt.CtlIx) (β : SweepSpec A dt.CtlIx dt.SlotIx (Option dt.KIx)) (γ : GuessSpec A dt.CtlIx dt.SlotIx (Option dt.KIx) G) (args : (v : dt.VarIx) → dt.VarArgs v) (bot : Option dt.KIx) : (dt.nexProg zero one hzo hpl coord β γ args bot).initBack = fun (x : Univ A dt.NexRIx (NexPh (Option dt.KIx) (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd → Prop) (x_1 : dt.SlotIx) => zero

A clocked program starts on a blank tape: it declines the input channel's marks – its mark is the blank – so its initial background is the constant blank, and the tape it starts on is the one its opening runs from whatever file it means to lay.

Determinism after the guess