The clocked evaluation at the file the channel hands over

A program that lays its file puts the registers at consecutive addresses, each one bit above the last. This file prices the clocked evaluation at the file the register channel hands over instead, where the registers are the cells the channel writes and a step of a walk across the file can cost as much as the whole file (DescriptiveComplexity.Draw.Data.nexIxEvalB_regLaid_reachesIn).

The four widths are regW, regWP, regWR, regWK (DescriptiveComplexity.Draw.Data.regW and its neighbors), each bounded by one number, regWidthBound: three of the four are linear in the file's own bound, and the seek is quadratic, being a pass of the file per bit of its target.

One number above the register file's four widths

def DescriptiveComplexity.Draw.Data.regWidthBound (t B : ℕ) : ℕ

One number above all four widths of the handed file: the file's bound and the walk across it, squared, with room for the constants.

Equations

• DescriptiveComplexity.Draw.Data.regWidthBound t B = 16 * (B + t * B + 16) ^ 2

@[reducible, inline]

noncomputable abbrev DescriptiveComplexity.Draw.Data.regWidthBd {L : FirstOrder.Language} (dt : Data L) (A R' P' : Type) [FirstOrder.Language.wide.Structure (Univ A R' P' dt.KIx dt.dd)] : ℕ

The register file's widths, under one number: the bound every address of the file is under, and the number of registers.

Equations

• dt.regWidthBd A R' P' = DescriptiveComplexity.Draw.Data.regWidthBound (Nat.card dt.RegIx) dt.regBound

The two bridges at the handed file

DescriptiveComplexity.Draw.Data.passEnc_regLaid and gateEnc_regLaid discharge the gates' bridges at the file the channel hands over. The generic lemmas they come from ask only that the registers stand for distinct elements, that the layout order is linear, and that a register's block and tuple are its element's – all of which the handed file has.

theorem DescriptiveComplexity.Draw.Data.passEnc_regLaid {L : FirstOrder.Language} {dt : Data L} {A R' P' : Type} [Fintype dt.SlotIx] [LinearOrder A] [LinearOrder R'] [LinearOrder P'] [Finite A] [Finite R'] [Finite P'] [Finite dt.KIx] [Nonempty A] [L.Structure A] [FirstOrder.Language.wide.Structure (Univ A R' P' dt.KIx dt.dd)] {PR : Prog A R' P' dt.CtlIx dt.SlotIx dt.KIx dt.dd} (h : IsLinOrd WMLe) (hord : ∀ (x y : Univ A R' P' dt.KIx dt.dd), WMLe x y ↔ tagTupleLe x y) (hzo : PR.zero ≠ PR.one) (vi : dt.VarIx) (stV : TapeSt dt A R' P' dt.RegIx) (ℓ : Fin (dt.nIn vi)) : dt.ixIGPassP (regLaid h hord) PR.zero PR.one vi stV ℓ ↔ IsEnc dt.ly PR.zero PR.one (wmBlk (ixAddr (fun (u : dt.RegIx) => ↑u) stV.val) (Tag.arg (toLex (dt.igBlk vi ℓ))))

The inner gates' bridge at the handed file: hpassEnc, discharged.

theorem DescriptiveComplexity.Draw.Data.gateEnc_regLaid {L : FirstOrder.Language} {dt : Data L} {A R' P' : Type} [Fintype dt.SlotIx] [LinearOrder A] [LinearOrder R'] [LinearOrder P'] [Finite A] [Finite R'] [Finite P'] [Finite dt.KIx] [Nonempty A] [L.Structure A] [FirstOrder.Language.wide.Structure (Univ A R' P' dt.KIx dt.dd)] [Finite (Univ A R' P' dt.KIx dt.dd)] {PR : Prog A R' P' dt.CtlIx dt.SlotIx dt.KIx dt.dd} (h : IsLinOrd WMLe) (hord : ∀ (x y : Univ A R' P' dt.KIx dt.dd), WMLe x y ↔ tagTupleLe x y) (hzo : PR.zero ≠ PR.one) (j : Fin dt.nv) (st : TapeSt dt A R' P' dt.RegIx) : dt.ixGatedAt (regLaid h hord) j st ↔ ∀ (ℓ : Fin (dt.arOf (dt.varAt j))), IsEnc dt.ly PR.zero PR.one (wmBlk (ixAddr (fun (u : dt.RegIx) => ↑u) st.mir) (Tag.arg (toLex (Sum.inl (Fin.castLE ⋯ ℓ)))))

The gates' bridge at the handed file: hgateEnc, discharged.

The evaluation itself

@[reducible, inline]

abbrev DescriptiveComplexity.Draw.Data.NexRegIx {L : FirstOrder.Language} (dt : Data L) (A R B : Type) [FirstOrder.Language.wide.Structure (Univ A R (NexPh B (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd)] : Type

The handed file's index at the clocked phases.

Equations

• dt.NexRegIx A R B = dt.RegIx

@[reducible, inline]

abbrev DescriptiveComplexity.Draw.Data.regElt {L : FirstOrder.Language} (dt : Data L) (A R B : Type) [FirstOrder.Language.wide.Structure (Univ A R (NexPh B (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd)] (u : dt.NexRegIx A R B) : Univ A R (NexPh B (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd

The element a register stands for: itself.

Equations

• dt.regElt A R B u = ↑u

@[reducible, inline]

noncomputable abbrev DescriptiveComplexity.Draw.Data.nexRegW {L : FirstOrder.Language} (dt : Data L) (A R B : Type) [FirstOrder.Language.wide.Structure (Univ A R (NexPh B (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd)] : ℕ

The handed file's four widths, at the clocked phases.

Equations

• dt.nexRegW A R B = dt.regW

@[reducible, inline]

noncomputable abbrev DescriptiveComplexity.Draw.Data.nexRegWP {L : FirstOrder.Language} (dt : Data L) (A R B : Type) [FirstOrder.Language.wide.Structure (Univ A R (NexPh B (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd)] : ℕ

The handed file's four widths, at the clocked phases.

Equations

• dt.nexRegWP A R B = dt.regWP

@[reducible, inline]

noncomputable abbrev DescriptiveComplexity.Draw.Data.nexRegWR {L : FirstOrder.Language} (dt : Data L) (A R B : Type) [FirstOrder.Language.wide.Structure (Univ A R (NexPh B (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd)] : ℕ

The handed file's four widths, at the clocked phases.

Equations

• dt.nexRegWR A R B = dt.regWR

@[reducible, inline]

noncomputable abbrev DescriptiveComplexity.Draw.Data.nexRegWK {L : FirstOrder.Language} (dt : Data L) (A R B : Type) [FirstOrder.Language.wide.Structure (Univ A R (NexPh B (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd)] : ℕ

The handed file's four widths, at the clocked phases.

Equations

• dt.nexRegWK A R B = dt.regWK

theorem DescriptiveComplexity.Draw.Data.regElt_injective {L : FirstOrder.Language} (dt : Data L) (A R B : Type) [FirstOrder.Language.wide.Structure (Univ A R (NexPh B (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd)] : Function.Injective (dt.regElt A R B)

Distinct registers stand for distinct elements.

theorem DescriptiveComplexity.Draw.Data.nexIxEvalB_regLaid_reachesIn {L : FirstOrder.Language} (dt : Data L) {A R B : Type} [Fintype dt.SlotIx] [LinearOrder A] [LinearOrder R] [LinearOrder (NexPh B (EvalPh dt.nv dt.PMF))] [FirstOrder.Language.wide.Structure (Univ A R (NexPh B (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd)] [Finite A] [Finite R] [Finite (NexPh B (EvalPh dt.nv dt.PMF))] [Finite (Univ A R (NexPh B (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd)] {PR : Prog A R (NexPh B (EvalPh dt.nv dt.PMF)) dt.CtlIx dt.SlotIx dt.KIx dt.dd} [Nonempty A] [L.IsRelational] [L.Structure A] [Finite dt.KIx] (h : IsLinOrd WMLe) {rEmb : (i : dt.SEF) → dt.NexSESh i → R} (hrules : ∀ (i : dt.SEF) (ρ : dt.NexSESh i), PR.rules (rEmb i ρ) = dt.nexEvalRuleF PR.zero PR.one (fun (w : dt.VarIx) => dt.varArgsOf PR.zero PR.one w) i ρ) (hR : PR.table.Reads) (hord : ∀ (x y : Univ A R (NexPh B (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd), WMLe x y ↔ tagTupleLe x y) {e₀ : Univ A R (NexPh B (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd} (he₀ : ∀ (y : Univ A R (NexPh B (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd), WMLe e₀ y) (harg : ∀ (b : Fin dt.ko ⊕ Fin dt.ki) (c : Fin dt.dd0 → A), WMHasInp (Tag.arg (toLex b), padTup PR.zero c)) (hargall : ∀ (x : Univ A R (NexPh B (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd), (∃ (i : dt.KIx), x.1 = Tag.arg i) → WMHasInp x) (hupinp : ∀ (x y : Univ A R (NexPh B (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd), WMLe x y → WMHasInp x → WMHasInp y) {bot : Univ A R (NexPh B (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd} (hbotm : WMHasInp bot) (hleast : ∀ (y : Univ A R (NexPh B (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd), WMHasInp y → WMLe bot y) (hbotarg : ∀ (i : dt.KIx), bot.1 ≠ Tag.arg i) (gtop gbot : dt.NexRegIx A R B) (htopF : ∀ (u : dt.RegIx), (regLaid h hord).le u gtop) (hbotF : ∀ (u : dt.RegIx), (regLaid h hord).le gbot u) {v v' : Univ A R (NexPh B (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd → Prop} (hv : WMSetLt WMLe v ((regLaid h hord).cell gbot)) (hvlog : ∀ (x : Univ A R (NexPh B (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd), v x → ∃ (i : dt.KIx), x.1 = Tag.arg i) (hvi : WMIncr WMLe v v') {ιV : Type} [LinearOrder ιV] [Finite ιV] {a₀ aT : ιV} (hbotV : ∀ (a : ιV), a₀ ≤ a) (htopV : ∀ (a : ιV), a ≤ aT) (mV : ιV → dt.NexRegIx A R B → Prop) (hmV0 : mV a₀ = fun (x : dt.NexRegIx A R B) => False) (hIncr : ∀ (a a' : ιV), a < a' → (∀ (b : ιV), ¬(a < b ∧ b < a')) → WMIncr (regLaid h hord).le (mV a) (mV a')) (hTestT : ∀ (u : dt.RegIx), dt.InnerFull (regLaid h hord).blk (mV aT) u) (hTestF : ∀ a < aT, ∃ (u : dt.RegIx), ¬dt.InnerFull (regLaid h hord).blk (mV a) u) (stOf : Fin (dt.nv + 1) → TapeSt dt A R (NexPh B (EvalPh dt.nv dt.PMF)) (dt.NexRegIx A R B)) (fsOf : Fin (dt.nv + 1) → dt.CtlIx → A) (hwkOf : ∀ (k : Fin (dt.nv + 1)), (stOf k).wk = fun (r : Univ A R (NexPh B (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd → Prop) => r = v) (hmirOf : ∀ (j : Fin dt.nv), (stOf j.castSucc).mir = ixMark (dt.regElt A R B) v) (hbotOf : ∀ (j : Fin dt.nv), (stOf j.castSucc).bot = fun (r : Univ A R (NexPh B (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd → Prop) => r = fun (x : Univ A R (NexPh B (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd) => False) (semTJ : (j : Fin dt.nv) → dt.ixGatedAt (regLaid h hord) j (stOf j.castSucc) → (p : dt.IxScratch A R (NexPh B (EvalPh dt.nv dt.PMF)) (dt.NexRegIx A R B)) → (a : ιV) → (∀ (ℓ : Fin (dt.nIn (dt.varAt j))), dt.ixIGPassP (regLaid h hord) PR.zero PR.one (dt.varAt j) (ixVarRdSt (stOf j.castSucc) 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 (stOf j.castSucc) p (mV a)) v ↑b) (dt.regElt A R B) (dt.kindOf (dt.varAt j) b)) (hst : ∀ (j : Fin dt.nv), stOf j.succ = dt.ixLegStB (regLaid h hord) ⋯ ⋯ ⋯ mV j (stOf j.castSucc) (semTJ j) (fsOf j.castSucc)) (hfs : ∀ (j : Fin dt.nv), fsOf j.succ = dt.ixLegCtlB (regLaid h hord) ⋯ ⋯ ⋯ mV j (stOf j.castSucc) (semTJ j) (fsOf j.castSucc)) {rEmbO : (i : dt.VarSiteF none) → dt.VarShF none i → R} (hrulesOut : ∀ (i : dt.VarSiteF none) (ρ : dt.VarShF none i), PR.rules (rEmbO i ρ) = dt.varRuleF PR.zero PR.one none (dt.varArgsOf PR.zero PR.one none) (fun (p : dt.VarPhF none) => NexPh.evalP (EvalPh.sub (Sum.inr p))) NexPh.acceptP i ρ) (TestOf : Fin (dt.arOf none) → dt.NexRegIx A R B → Prop) (hcompatOf : ∀ (ℓ : Fin (dt.arOf none)) (u : dt.NexRegIx A R B), dt.wellShapedG PR.zero PR.one (Sum.inl (Fin.castLE ⋯ ℓ)) (PR.passTracksAt (regLaid h hord).cell Slot.mir (dt.ixBack (regLaid h hord).toLayout PR.zero PR.one ⋯ (stOf (Fin.last dt.nv))) (stOf (Fin.last dt.nv)).mir ((regLaid h hord).cell u)) ↔ TestOf ℓ u) (tOf : Fin (dt.arOf none) → dt.X.Tag) (hwitOf : ∀ (ℓ : Fin (dt.arOf none)) (t' : dt.X.Tag), wmBlk (ixAddr (dt.regElt A R B) (stOf (Fin.last dt.nv)).mir) (Tag.arg (toLex (Sum.inl (Fin.castLE ⋯ ℓ)))) (encTagTup dt.ly PR.zero PR.one t') ↔ t' = tOf ℓ) (hmirL : (stOf (Fin.last dt.nv)).mir = ixMark (dt.regElt A R B) v) (hbotL : (stOf (Fin.last dt.nv)).bot = fun (r : Univ A R (NexPh B (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd → Prop) => r = fun (x : Univ A R (NexPh B (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd) => False) (hsavL : (stOf (Fin.last dt.nv)).sav = ixMark (dt.regElt A R B) v) (htgtL : (stOf (Fin.last dt.nv)).tgt = ixMark (dt.regElt A R B) v) (semOf : (a : ιV) → (∀ (ℓ : Fin (dt.nIn none)), dt.ixIGPassP (regLaid h hord) PR.zero PR.one none (dt.ixRoundSt (stOf (Fin.last dt.nv)) (mV a)) ℓ) → (b : Fin (dt.natOf none)) → dt.IxKindSem PR.zero PR.one none (dt.ixRoundSt (stOf (Fin.last dt.nv)) (mV a)) (dt.regElt A R B) (dt.kindOf none b)) (hDom : ∀ (ℓ : Fin (dt.arOf none)), ExpExpansion.DomHolds (tOf ℓ, decRho dt.ly PR.zero PR.one (wmBlk (ixAddr (dt.regElt A R B) (stOf (Fin.last dt.nv)).mir) (Tag.arg (toLex (Sum.inl (Fin.castLE ⋯ ℓ))))))) (hTestOf : ∀ (ℓ : Fin (dt.arOf none)) (u : dt.NexRegIx A R B), TestOf ℓ u) (hacc : (dt.varArgsOf PR.zero PR.one none).accBit (dt.ixOutCtl (regLaid h hord) ⋯ ⋯ ⋯ mV (stOf (Fin.last dt.nv)) tOf semOf (fsOf (Fin.last dt.nv)))) : (wideData (Univ A R (NexPh B (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd)).ReachesIn (1 + (dt.ixLegCost A (dt.nexRegW A R B) (dt.nexRegWP A R B) (dt.nexRegWR A R B) (dt.nexRegWK A R B) (Nat.card ιV) + 2) * dt.nv + 1 + dt.ixOutLegCost A (dt.nexRegW A R B) (dt.nexRegWP A R B) (dt.nexRegWR A R B) (dt.nexRegWK A R B) (Nat.card ιV)) { state := Sum.inr (PR.stElt (NexPh.evalP (EvalPh.chk 0)) (fsOf 0)), head := Sum.inl v', tape := wideTape (PR.trackTapeAt (regLaid h hord).cell Slot.val (dt.ixBack (regLaid h hord).toLayout PR.zero PR.one ⋯ (stOf 0)) (stOf 0).val) (PR.syElt PR.blank) } { state := Sum.inr (PR.stElt NexPh.acceptP (dt.ixOutCtl (regLaid h hord) ⋯ ⋯ ⋯ mV (stOf (Fin.last dt.nv)) tOf semOf (fsOf (Fin.last dt.nv)))), head := Sum.inl v', tape := wideTape (PR.trackTapeAt (regLaid h hord).cell Slot.val (dt.ixBack (regLaid h hord).toLayout PR.zero PR.one ⋯ (dt.ixRoundSt (stOf (Fin.last dt.nv)) (mV aT))) (mV aT)) (PR.syElt PR.blank) }

The clocked evaluation at the handed file: the walk-back the opening's dispatch owes, the branched spine over the spine's positions, and the exit into the accepting phase, charged the handed file's own widths. This is DescriptiveComplexity.Draw.Data.nexIxEvalB_reachesIn with every coherence of the register channel's file discharged; what is left is the program's own, and what the reduction still owes is its marking – the arguments, one element below them, and nothing else.

The thread, and the run from the sentence alone

noncomputable def DescriptiveComplexity.Draw.Data.regGatedSem {L : FirstOrder.Language} (dt : Data L) {A R B : Type} [Fintype dt.SlotIx] [LinearOrder A] [LinearOrder R] [LinearOrder (NexPh B (EvalPh dt.nv dt.PMF))] [FirstOrder.Language.wide.Structure (Univ A R (NexPh B (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd)] [Finite A] [Finite R] [Finite (NexPh B (EvalPh dt.nv dt.PMF))] [Finite (Univ A R (NexPh B (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd)] {PR : Prog A R (NexPh B (EvalPh dt.nv dt.PMF)) dt.CtlIx dt.SlotIx dt.KIx dt.dd} [Nonempty A] [L.Structure A] [Finite dt.KIx] (h : IsLinOrd WMLe) (hord : ∀ (x y : Univ A R (NexPh B (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd), WMLe x y ↔ tagTupleLe x y) (hzo : PR.zero ≠ PR.one) {ιV : Type} (mV : ιV → dt.NexRegIx A R B → Prop) (w : Univ A R (NexPh B (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd → Prop) (j : Fin dt.nv) (st : TapeSt dt A R (NexPh B (EvalPh dt.nv dt.PMF)) (dt.NexRegIx A R B)) : dt.ixGatedAt (regLaid h hord) j st → (p : dt.IxScratch A R (NexPh B (EvalPh dt.nv dt.PMF)) (dt.NexRegIx A R B)) → (a : ιV) → (∀ (ℓ : Fin (dt.nIn (dt.varAt j))), dt.ixIGPassP (regLaid h hord) 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) (dt.regElt A R B) (dt.kindOf (dt.varAt j) b)

The packs at the handed file, built: the conditioned family the branched thread takes as a parameter, from the gates' bridge and the inner gates' (gateEnc_regLaid, passEnc_regLaid) rather than assumed.

Equations

• dt.regGatedSem h hord hzo mV w j st hg p a hp b = dt.ixGatedSem (DescriptiveComplexity.Draw.Data.regLaid h hord) ⋯ ⋯ hzo h mV j st hg p a hp b