The handed program, with room on its clock

DescriptiveComplexity.Draw.Data.nexProgHanded is the program a reduction into DescriptiveComplexity.WideRegAccept emits, and its clock is 2 ^ |Tag| at its own rule names. The clock's one remaining obligation (clock_count_of_tags) is that those names outnumber a constant of the kernel – and a program may always have more of them, since a rule whose guard is False changes nothing (PadRules.lean).

This file is that program: the same rules at the same sites, plus n sites carrying a rule that never fires. Its record, its channel, its marks and its phases are the originals – only the rule names are wider – so every constant the clock is measured against is unchanged and the count goes up by n.

@[reducible, inline]

abbrev DescriptiveComplexity.Draw.Data.NexRIxPad {L : FirstOrder.Language} (dt : Data L) (G : Type) (n : ℕ) : Type

The rule names of the padded program: the clocked program's sites, and n more carrying a rule that never fires.

Equations

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

@[reducible, inline]

abbrev DescriptiveComplexity.Draw.Data.NexITagPad {L : FirstOrder.Language} (dt : Data L) (G : Type) (n : ℕ) : Type

The tags of the padded machine's universe: the padded rule names, the alphabet's, the phases and the argument blocks.

Equations

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

noncomputable def DescriptiveComplexity.Draw.Data.nexProgHandedPad {L : FirstOrder.Language} (dt : Data L) {A G : Type} [Fintype dt.SlotIx] [DecidableEq dt.SlotIx] [LinearOrder A] (zero one : A) [LinearOrder (NexPh (Option dt.KIx) (EvalPh dt.nv dt.PMF))] (hzo : zero ≠ one) (hpl : Fintype.card (dt.CtlIx ⊕ dt.SlotIx) ≤ dt.dd) (γ : GuessSpec A dt.CtlIx dt.SlotIx (Option dt.KIx) G) (args : (v : dt.VarIx) → dt.VarArgs v) (bot : Option dt.KIx) (n : ℕ) [LinearOrder (dt.NexRIxPad G n)] : Prog A (dt.NexRIxPad G n) (NexPh (Option dt.KIx) (EvalPh dt.nv dt.PMF)) dt.CtlIx dt.SlotIx dt.KIx dt.dd

The handed program with n junk rule names: the same program, its rule names padded.

Equations

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

@[reducible]

noncomputable def DescriptiveComplexity.Draw.Data.nexProgHandedPadAt {L : FirstOrder.Language} (dt : Data L) {A : Type} [Fintype dt.SlotIx] [DecidableEq dt.SlotIx] [LinearOrder A] [Finite A] [Nonempty A] {zero one : A} [LinearOrder (NexPh (Option dt.KIx) (EvalPh dt.nv dt.PMF))] [L.IsRelational] [L.Structure A] (hzo : zero ≠ one) (hpl : Fintype.card (dt.CtlIx ⊕ dt.SlotIx) ≤ dt.dd) (bot : Option dt.KIx) (n : ℕ) [LinearOrder (dt.NexRIxPad (dt.d.B.ι → Bool) n)] : Prog A (dt.NexRIxPad (dt.d.B.ι → Bool) n) (NexPh (Option dt.KIx) (EvalPh dt.nv dt.PMF)) dt.CtlIx dt.SlotIx dt.KIx dt.dd

The padded program a clocked reduction emits: nexProgHanded with n junk rule names.

Equations

• dt.nexProgHandedPadAt hzo hpl bot n = dt.nexProgHandedPad zero one hzo hpl (dt.regionSpec zero one) (fun (w : dt.VarIx) => dt.varArgsOf zero one w) bot n

The interpretation, and that it reads the padded table

noncomputable def DescriptiveComplexity.Draw.Data.nexInterpHandedPad {L : FirstOrder.Language} (dt : Data L) [Fintype dt.SlotIx] [DecidableEq dt.SlotIx] [LinearOrder (NexPh (Option dt.KIx) (EvalPh dt.nv dt.PMF))] {args : (e : Env L) → (v : dt.VarIx) → dt.VarArgs v} (hpl : Fintype.card (dt.CtlIx ⊕ dt.SlotIx) ≤ dt.dd) (h : ∀ (v : dt.VarIx), UVarArgsDef v fun (e : Env L) => args e v) (bot : Option dt.KIx) (n : ℕ) [LinearOrder (dt.NexRIxPad (dt.d.B.ι → Bool) n)] : FOInterpretation (L.sum FirstOrder.Language.order) FirstOrder.Language.wide (dt.ITagOf (NexSite dt.SEF ⊕ Fin n) (padSh (NexSh dt.SEF (Option dt.KIx) (dt.d.B.ι → Bool) dt.NexSESh) n) (NexPh (Option dt.KIx) (EvalPh dt.nv dt.PMF))) dt.dd

The padded machine, written down: the interpretation whose universe is tagged by the padded rule names – the clock's budget, widened by the junk sites and by nothing else.

Equations

• dt.nexInterpHandedPad hpl h bot n = DescriptiveComplexity.Draw.Data.drawInterp hpl ⋯ ⋯ DescriptiveComplexity.Draw.NexPh.start (DescriptiveComplexity.Draw.Data.regFileMarkArg hpl)

The padded program separates just as the program does

The marking's consequences, at any program with that channel

What a backward reading needs of the rules

def DescriptiveComplexity.Draw.Data.NexCovered {L : FirstOrder.Language} {dt : Data L} {A R' : Type} [Fintype dt.SlotIx] [DecidableEq dt.SlotIx] (PR : Prog A R' (NexPh (Option dt.KIx) (EvalPh dt.nv dt.PMF)) dt.CtlIx dt.SlotIx dt.KIx dt.dd) {G : Type} (γ : GuessSpec A dt.CtlIx dt.SlotIx (Option dt.KIx) G) (args : (v : dt.VarIx) → dt.VarArgs v) (bot : Option dt.KIx) : Prop

The rules a program of this shape has: at every rule name, either the rule of a site of the clocked program, or a rule that never fires. That is all a backward reading asks – it meets a rule by the name a step carries, not by the site it was written at – and both the emitted program and the padded one answer it, the second by its junk names.

Equations

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

What a reduction's program provides, in one record

structure DescriptiveComplexity.Draw.Data.NexEmitted {L : FirstOrder.Language} [L.IsRelational] {dt : Data L} {A R' : Type} [Fintype dt.SlotIx] [DecidableEq dt.SlotIx] [L.Structure A] [LinearOrder A] [Finite A] [Nonempty A] [LinearOrder R'] [LinearOrder (NexPh (Option dt.KIx) (EvalPh dt.nv dt.PMF))] (PR : Prog A R' (NexPh (Option dt.KIx) (EvalPh dt.nv dt.PMF)) dt.CtlIx dt.SlotIx dt.KIx dt.dd) (bot : Option dt.KIx) : Type

The facts a clocked program of this shape provides, collected: its rules at the named sites, its channel's marks, its constants, its accepting predicate and the separation its determinism is read off. Every layer of the run takes this one hypothesis, and the two programs a reduction may emit – the plain one and the padded one that buys the clock its room – provide it the same way, by rfl at each field.

• site (i : NexSite dt.SEF) : NexSh dt.SEF (Option dt.KIx) (dt.d.B.ι → Bool) dt.NexSESh i → R'

  The rule name of a site and a shape.

• rules_site (i : NexSite dt.SEF) (ρ : NexSh dt.SEF (Option dt.KIx) (dt.d.B.ι → Bool) dt.NexSESh i) : PR.rules (self.site i ρ) = dt.nexRule PR.one (dt.nullSpec (Option dt.KIx)) (dt.regionSpec PR.zero PR.one) (dt.nexEvalRuleF PR.zero PR.one fun (w : dt.VarIx) => dt.varArgsOf PR.zero PR.one w) (EvalPh.chk 0) bot i ρ

  And the rule it names is the clocked one.

• homeBuild : HomeKit.HomeRule → R'

  The rule name of a step of the walk home after the file is laid.

• rules_homeBuild (ρ : HomeKit.HomeRule) : PR.rules (self.homeBuild ρ) = { t := Slot.mir, wk := Slot.wk, ph := NexPh.homeBuildP }.rule PR.one ρ

  And it names that step.

• homeGuess : HomeKit.HomeRule → R'

  The rule name of a step of the walk home after the guess.

• rules_homeGuess (ρ : HomeKit.HomeRule) : PR.rules (self.homeGuess ρ) = { t := Slot.mir, wk := Slot.wk, ph := NexPh.homeGuessP }.rule PR.one ρ

  And it names that step.

• covered : NexCovered PR (dt.regionSpec PR.zero PR.one) (fun (w : dt.VarIx) => dt.varArgsOf PR.zero PR.one w) bot

  Every rule name carries a site's rule or one that never fires.

• mark (x : Univ A R' (NexPh (Option dt.KIx) (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd) : PR.mark x = regSlotMark PR.zero PR.one ⋯ x

  The mark the channel writes.

• marked (x : Univ A R' (NexPh (Option dt.KIx) (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd) : PR.marked x ↔ (∃ (k : dt.KIx), x.1 = Tag.arg k) ∨ IsTopNonArg x

  And who it writes for: the argument elements and the one below them.

• blank (s : dt.SlotIx) : PR.blank s = PR.zero

  The tape is blank where the channel wrote nothing.

• startPh : PR.startPh = NexPh.start

  The machine starts in the start phase …

• startSt : PR.startSt = fun (x : dt.CtlIx) => PR.zero

  … with its control clear.

• accept_iff (p : NexPh (Option dt.KIx) (EvalPh dt.nv dt.PMF)) (f : dt.CtlIx → A) : PR.accept p f ↔ p = NexPh.acceptP ∧ (dt.varArgsOf PR.zero PR.one none).accBit f

  It accepts in the accepting phase, at the output variable's bit.

• sepOn : PR.table.SepOn NexPh.PostGuess

  Two rules firing on the same data after the guess are the same rule.

• dstPh_postGuess (r : R') : (PR.table.srcPh r).PostGuess → (PR.table.dstPh r).PostGuess

  The post-guess phases are closed.

• srcPh_ne_acceptP (r : R') : PR.table.srcPh r ≠ NexPh.acceptP

  And no rule fires from the accepting phase.

theorem DescriptiveComplexity.Draw.Data.NexEmitted.uniqueFrom {L : FirstOrder.Language} [L.IsRelational] {dt : Data L} {A R' : Type} [Fintype dt.SlotIx] [DecidableEq dt.SlotIx] [L.Structure A] [LinearOrder A] [Finite A] [Nonempty A] [Finite dt.KIx] [LinearOrder R'] [Finite R'] [LinearOrder (NexPh (Option dt.KIx) (EvalPh dt.nv dt.PMF))] [FirstOrder.Language.wide.Structure (Univ A R' (NexPh (Option dt.KIx) (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd)] {PR : Prog A R' (NexPh (Option dt.KIx) (EvalPh dt.nv dt.PMF)) dt.CtlIx dt.SlotIx dt.KIx dt.dd} {bot : Option dt.KIx} (hE : NexEmitted PR bot) (hR : PR.table.Reads) (hlin : IsLinOrd WMLe) (cfg : Config (WPoint (Univ A R' (NexPh (Option dt.KIx) (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd))) (hcfg : ∀ (p : NexPh (Option dt.KIx) (EvalPh dt.nv dt.PMF)) (f : Fin (Fintype.card (dt.CtlIx ⊕ dt.SlotIx)) → A), cfg.state = Sum.inr (stateElt PR.zero p f) → p.PostGuess) : (wideData (Univ A R' (NexPh (Option dt.KIx) (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd)).UniqueFrom cfg

The machine is deterministic after its guess, at any program of this shape: separation there, and the post-guess phases closed.

theorem DescriptiveComplexity.Draw.Data.NexEmitted.acceptPh {L : FirstOrder.Language} [L.IsRelational] {dt : Data L} {A R' : Type} [Fintype dt.SlotIx] [DecidableEq dt.SlotIx] [L.Structure A] [LinearOrder A] [Finite A] [Nonempty A] [LinearOrder R'] [LinearOrder (NexPh (Option dt.KIx) (EvalPh dt.nv dt.PMF))] {PR : Prog A R' (NexPh (Option dt.KIx) (EvalPh dt.nv dt.PMF)) dt.CtlIx dt.SlotIx dt.KIx dt.dd} {bot : Option dt.KIx} (hE : NexEmitted PR bot) (p : NexPh (Option dt.KIx) (EvalPh dt.nv dt.PMF)) (f : dt.CtlIx → A) (h : PR.accept p f) : p = NexPh.acceptP

An accepting control is in the accepting phase.

Determinism after the guess, at any program of this shape

The opening, at any program with those rules

theorem DescriptiveComplexity.Draw.Data.reachesIn_openingReg {L : FirstOrder.Language} [L.IsRelational] {dt : Data L} {A R' : Type} [Fintype dt.SlotIx] [DecidableEq dt.SlotIx] [L.Structure A] [LinearOrder A] [Finite A] [Nonempty A] [Nonempty dt.KIx] [Finite dt.KIx] [LinearOrder R'] [Finite R'] [LinearOrder (NexPh (Option dt.KIx) (EvalPh dt.nv dt.PMF))] [FirstOrder.Language.wide.Structure (Univ A R' (NexPh (Option dt.KIx) (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd)] {PR : Prog A R' (NexPh (Option dt.KIx) (EvalPh dt.nv dt.PMF)) dt.CtlIx dt.SlotIx dt.KIx dt.dd} (_hpl : Fintype.card (dt.CtlIx ⊕ dt.SlotIx) ≤ dt.dd) {bot : Option dt.KIx} {rEmbS : (i : NexSite dt.SEF) → NexSh dt.SEF (Option dt.KIx) (dt.d.B.ι → Bool) dt.NexSESh i → R'} (hrulesS : ∀ (i : NexSite dt.SEF) (ρ : NexSh dt.SEF (Option dt.KIx) (dt.d.B.ι → Bool) dt.NexSESh i), PR.rules (rEmbS i ρ) = dt.nexRule PR.one (dt.nullSpec (Option dt.KIx)) (dt.regionSpec PR.zero PR.one) (dt.nexEvalRuleF PR.zero PR.one fun (w : dt.VarIx) => dt.varArgsOf PR.zero PR.one w) (EvalPh.chk 0) bot 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 ρ) (hmark : ∀ (x : Univ A R' (NexPh (Option dt.KIx) (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd), PR.mark x = regSlotMark PR.zero PR.one ⋯ x) (hmk : ∀ (x : Univ A R' (NexPh (Option dt.KIx) (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd), PR.marked x ↔ (∃ (k : dt.KIx), x.1 = Tag.arg k) ∨ IsTopNonArg x) (hblank : ∀ (s : dt.SlotIx), PR.blank s = PR.zero) (hstartPh : PR.startPh = NexPh.start) (hstartSt : PR.startSt = fun (x : dt.CtlIx) => PR.zero) (hR : PR.table.Reads) (hlin : IsLinOrd WMLe) (hord : ∀ (x y : Univ A R' (NexPh (Option dt.KIx) (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd), WMLe x y ↔ tagTupleLe x y) {v v₁ x y y' s₀ s₁ v' : Univ A R' (NexPh (Option dt.KIx) (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd → Prop} (hvreg : ∀ (z : Univ A R' (NexPh (Option dt.KIx) (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd), (∃ (k : dt.KIx), z.1 = Tag.arg k) ∨ IsTopNonArg z → v ≠ wmRegSeg z) (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) (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd), s₁ z) (hvv' : WMIncr WMLe v v') (hexB : dt.exitG PR.one (PR.passTracksAt (regLaid hlin hord).cell Slot.mir (dt.ixBack (regLaid hlin hord).toLayout PR.zero PR.one ⋯ (dt.nexEntrySt v)) (fun (x : dt.RegIx) => False) v)) (σ : dt.d.B.ι → (Univ A R' (NexPh (Option dt.KIx) (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd → Prop) → Prop) (hout : ∀ (i : dt.d.B.ι) (r : Univ A R' (NexPh (Option dt.KIx) (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd → Prop), WMSetLt WMLe r s₀ ∨ ¬WMSetLt WMLe r s₁ → ¬σ i r) (hexG : dt.exitG PR.one (PR.passTracksAt (regLaid hlin hord).cell Slot.mir (dt.ixBack (regLaid hlin hord).toLayout PR.zero PR.one ⋯ (have __src := dt.nexEntrySt v; { mir := __src.mir, tgt := __src.tgt, sav := __src.sav, val := __src.val, old := σ, new := __src.new, wk := __src.wk, bot := __src.bot, ltp := __src.ltp })) (fun (x : dt.RegIx) => False) v)) : (wideData (Univ A R' (NexPh (Option dt.KIx) (EvalPh dt.nv dt.PMF)) 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 PR.startPh PR.startSt), head := Sum.inl v, tape := wideTape (PR.trackTapeAt (regLaid hlin hord).cell Slot.mir PR.initBackReg fun (x : dt.RegIx) => False) (PR.syElt PR.blank) } { state := Sum.inr (PR.stElt (NexPh.evalP (EvalPh.chk 0)) fun (x : dt.CtlIx) => PR.zero), head := Sum.inl v', tape := wideTape (PR.trackTapeAt (regLaid hlin hord).cell Slot.mir (dt.ixBack (regLaid hlin hord).toLayout PR.zero PR.one ⋯ (have __src := dt.nexEntrySt v; { mir := __src.mir, tgt := __src.tgt, sav := __src.sav, val := __src.val, old := σ, new := __src.new, wk := __src.wk, bot := __src.bot, ltp := __src.ltp })) fun (x : dt.RegIx) => False) (PR.syElt PR.blank) }