The program, assembled

The last shape layer: the tower of DescriptiveComplexity.Problems.Wide.DrawTower is plugged together into one DescriptiveComplexity.Draw.Assembly – the gates and the matrix into one variable's machinery, one copy of that per fixed-point variable (and one for the output), those into the evaluation's spine, and the spine into the outer loop – so that DescriptiveComplexity.Draw.Assembly.prog and DescriptiveComplexity.Draw.Assembly.sep deliver the program together with its determinism.

The semantic parameters ride in one pack per variable (DescriptiveComplexity.Draw.Data.VarArgs): the per-atom and per-block parameter packs, the loop and fold updates, the stage slot the variable writes and the accumulator its verdict is read from. Separation never reads any of them, so the assembly is complete before their content is fixed – that happens with the runs.

Where the machinery goes, in one glance (the flow of DescriptiveComplexity.Draw.Data.varRuleF): the entry checkpoint enters the gates; the gates' failing block clears the verdict flag and lands on the verdict checkpoint, which either writes False into the stage slot and leaves, or clears the VAL register and enters the matrix; the matrix's exit is the post-matrix checkpoint, which folds and tests VAL for exhaustion – increment and matrix again, or the exit checkpoint, which writes the variable's next-stage bit at the marker.

The semantic parameters, per variable

noncomputable def DescriptiveComplexity.Draw.Data.GateArgs {L : FirstOrder.Language} (dt : Data L) {A Q : Type} : Type

The parameter pack of a gate block's tag-branched domain evaluation.

Equations

• dt.GateArgs = DescriptiveComplexity.Draw.TagArgs A Q dt.SlotIx (Fintype.card dt.X.Tag) dt.X.Tag dt.domNr

structure DescriptiveComplexity.Draw.Data.VarArgs {L : FirstOrder.Language} (dt : Data L) {A Q : Type} (v : dt.VarIx) : Type

The semantic parameters of one variable's machinery: the per-atom packs of its matrix and the per-block packs of its gates, the control updates the checkpoints carry, the stage slot it writes and the flags its verdicts are read from. Separation reads none of them.

• argsA (a : Fin (dt.natOf v)) : dt.KindArgs (dt.kindOf v a)

  The parameter pack of each classified atom of the matrix.

• enterAtomSt : Fin (dt.natOf v) → (Q → A) → (dt.SlotIx → A) → Q → A

  The control update entering each atom.

• argsG : Fin (dt.arOf v) → dt.GateArgs

  The parameter pack of each argument block's domain evaluation.

• wellGOf : Fin (dt.arOf v) → (dt.SlotIx → A) → Prop

  The well-shapedness question of each argument block.

• setFail : (Q → A) → (dt.SlotIx → A) → Q → A

  Clearing the gates' verdict flag.

• enterBlockSt : Fin (dt.arOf v) → (Q → A) → (dt.SlotIx → A) → Q → A

  The control update entering each gate block.

• argsIG : Fin (dt.nIn v) → dt.GateArgs

  The parameter pack of each quantified level's inner gate.

• wellIGOf : Fin (dt.nIn v) → (dt.SlotIx → A) → Prop

  The well-shapedness question of each inner gate.

• setFailIGOf : Fin (dt.nIn v) → (Q → A) → (dt.SlotIx → A) → Q → A

  Clearing the level's polarity flag on a failed inner gate.

• enterIGSt : Fin (dt.nIn v) → (Q → A) → (dt.SlotIx → A) → Q → A

  The control update entering each inner gate block – the first one resets the round's two flags.

• existFlag : Q

  The ∃-levels' gate flag.

• allFlag : Q

  The ∀-levels' gate flag.

• newSlot : dt.SlotIx

  The stage slot the variable writes.

• gateFlag : Q

  The gates' verdict flag.

• accBit : (Q → A) → Prop

  The verdict the exit checkpoint writes.

• enterSt : (Q → A) → (dt.SlotIx → A) → Q → A

  The control update entering the machinery: where the gates' verdict flag is set, since every block conjoins into it and a variable with no argument blocks never touches it.

• initSt : (Q → A) → (dt.SlotIx → A) → Q → A

  The folds at the empty valuation.

• postFold : (Q → A) → (dt.SlotIx → A) → Q → A

  The folds after a matrix pass.

• storeCarry : dt.CarryB → (Q → A) → (dt.SlotIx → A) → Q → A

  The folds at an increment's carry block.

One variable's machinery, plugged in

noncomputable def DescriptiveComplexity.Draw.Data.varRuleF {L : FirstOrder.Language} (dt : Data L) {A Q P : Type} (zero one : A) (v : dt.VarIx) (args : dt.VarArgs v) (emb : dt.VarPhF v → P) (exitPh : P) (i : dt.VarSiteF v) : dt.VarShF v i → Rule A Q dt.SlotIx P

The rules of one variable's machinery, the gates and the matrix plugged into the spine of DescriptiveComplexity.Problems.Wide.DrawVar.

Equations

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

theorem DescriptiveComplexity.Draw.Data.varHosrcF {L : FirstOrder.Language} {dt : Data L} {A Q P : Type} (zero one : A) (v : dt.VarIx) (args : dt.VarArgs v) {emb : dt.VarPhF v → P} (exitPh : P) (i : dt.VarSiteF v) (ρ : dt.VarShF v i) : ∃ (p : dt.VarPhF v), (dt.varRuleF zero one v args emb exitPh i ρ).srcPh = emb p ∧ dt.varOwnF v p = i

Every rule of one variable's machinery fires from a phase its site owns.

theorem DescriptiveComplexity.Draw.Data.varRuleF_dstIn {L : FirstOrder.Language} {dt : Data L} {A Q P : Type} (zero one : A) (v : dt.VarIx) (args : dt.VarArgs v) {emb : dt.VarPhF v → P} (exitPh : P) {S : P → Prop} (hemb : ∀ (p : dt.VarPhF v), S (emb p)) (hexit : S exitPh) (i : dt.VarSiteF v) (ρ : dt.VarShF v i) : S (dt.varRuleF zero one v args emb exitPh i ρ).dstPh

A property of one variable machinery's phases and its exit holds of every phase it can move to: the gates, the round and the matrix all stay inside, and only the two verdict dispatches leave. This is the fact a determinism-after-the-guess argument asks of the evaluation (DescriptiveComplexity.Draw.Data.nexProg_uniqueFrom).

theorem DescriptiveComplexity.Draw.Data.varSepF {L : FirstOrder.Language} {dt : Data L} {A Q P : Type} (zero one : A) (hzo : zero ≠ one) (v : dt.VarIx) (args : dt.VarArgs v) {emb : dt.VarPhF v → P} (hemb : Function.Injective emb) (exitPh : P) (i : dt.VarSiteF v) (ρ ρ' : dt.VarShF v i) (f : Q → A) (g : dt.SlotIx → A) : (dt.varRuleF zero one v args emb exitPh i ρ).guard f g → (dt.varRuleF zero one v args emb exitPh i ρ').guard f g → (dt.varRuleF zero one v args emb exitPh i ρ).srcPh = (dt.varRuleF zero one v args emb exitPh i ρ').srcPh → ρ = ρ'

One variable's machinery separates in-shape.

The evaluation's machineries

noncomputable def DescriptiveComplexity.Draw.Data.smRule {L : FirstOrder.Language} (dt : Data L) {A Q : Type} (zero one : A) (args : (v : dt.VarIx) → dt.VarArgs v) (s : dt.SMF) : dt.SMSh s → Rule A Q dt.SlotIx (OuterPh dt.PEF)

The rules of the evaluation's machineries: one copy of the variable machinery per spine position – its exit the next checkpoint – and the output's, whose exit is the accepting phase (the verdict itself is read from the control by the program's accepting predicate).

Equations

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

noncomputable def DescriptiveComplexity.Draw.Data.smEntry {L : FirstOrder.Language} (dt : Data L) (j : Fin dt.nv) : dt.PMF

The entry phase of the machinery at a spine position.

Equations

• dt.smEntry j = Sum.inl ⟨j, DescriptiveComplexity.Draw.VarPh.vchk0⟩

noncomputable def DescriptiveComplexity.Draw.Data.smEntryOut {L : FirstOrder.Language} (dt : Data L) : dt.PMF

The entry phase of the output's machinery.

Equations

• dt.smEntryOut = Sum.inr DescriptiveComplexity.Draw.VarPh.vchk0

theorem DescriptiveComplexity.Draw.Data.smHosrc {L : FirstOrder.Language} {dt : Data L} {A Q : Type} (zero one : A) (args : (v : dt.VarIx) → dt.VarArgs v) (s : dt.SMF) (ρ : dt.SMSh s) : ∃ (p : dt.PMF), (dt.smRule zero one args s ρ).srcPh = OuterPh.evalP (EvalPh.sub p) ∧ dt.smOwn p = s

Every rule of the evaluation's machineries fires from a phase its site owns.

theorem DescriptiveComplexity.Draw.Data.smSep {L : FirstOrder.Language} {dt : Data L} {A Q : Type} (zero one : A) (hzo : zero ≠ one) (args : (v : dt.VarIx) → dt.VarArgs v) (s : dt.SMF) (ρ ρ' : dt.SMSh s) (f : Q → A) (g : dt.SlotIx → A) : (dt.smRule zero one args s ρ).guard f g → (dt.smRule zero one args s ρ').guard f g → (dt.smRule zero one args s ρ).srcPh = (dt.smRule zero one args s ρ').srcPh → ρ = ρ'

The evaluation's machineries separate in-shape.

The whole program

noncomputable def DescriptiveComplexity.Draw.Data.evalRuleF {L : FirstOrder.Language} (dt : Data L) {A Q : Type} (zero one : A) (args : (v : dt.VarIx) → dt.VarArgs v) (e : dt.SEF) : dt.SESh e → Rule A Q dt.SlotIx (OuterPh dt.PEF)

The rules of the evaluation: the spine over the machineries.

Equations

• dt.evalRuleF zero one args = dt.evalRule zero one (dt.smRule zero one args) dt.smEntry

theorem DescriptiveComplexity.Draw.Data.evalHosrcF {L : FirstOrder.Language} {dt : Data L} {A Q : Type} (zero one : A) (args : (v : dt.VarIx) → dt.VarArgs v) (e : dt.SEF) (ρ : dt.SESh e) : ∃ (p : dt.PEF), (dt.evalRuleF zero one args e ρ).srcPh = OuterPh.evalP p ∧ dt.seOwn p = e

Every evaluation rule fires from a phase its site owns.

theorem DescriptiveComplexity.Draw.Data.evalSepF {L : FirstOrder.Language} {dt : Data L} {A Q : Type} (zero one : A) (hzo : zero ≠ one) (args : (v : dt.VarIx) → dt.VarArgs v) (e : dt.SEF) (ρ ρ' : dt.SESh e) (f : Q → A) (g : dt.SlotIx → A) : (dt.evalRuleF zero one args e ρ).guard f g → (dt.evalRuleF zero one args e ρ').guard f g → (dt.evalRuleF zero one args e ρ).srcPh = (dt.evalRuleF zero one args e ρ').srcPh → ρ = ρ'

The evaluation separates in-shape.

noncomputable def DescriptiveComplexity.Draw.Data.progAsm {L : FirstOrder.Language} (dt : Data L) {A Q : Type} (zero one : A) [Fintype Q] [Fintype dt.SlotIx] (hzo : zero ≠ one) (args : (v : dt.VarIx) → dt.VarArgs v) : Assembly A Q dt.SlotIx dt.PF dt.SF

The program's assembly: every site of the outer loop, of the evaluation's spine, of each variable's machinery and of each atom's subroutine, with its rules, its owner and its in-shape separation. This is the EXPSPACE program's rule set, complete; DescriptiveComplexity.Draw.Assembly.prog turns it into a DescriptiveComplexity.Draw.Prog and DescriptiveComplexity.Draw.Assembly.sep into its determinism.

Equations

• dt.progAsm zero one hzo args = dt.outerAsm zero one ⋯ hzo ⋯

@[reducible, inline]

noncomputable abbrev DescriptiveComplexity.Draw.Data.RIx {L : FirstOrder.Language} (dt : Data L) {A Q : Type} (zero one : A) [Fintype Q] [Fintype dt.SlotIx] (hzo : zero ≠ one) (args : (v : dt.VarIx) → dt.VarArgs v) : Type

The rule names of the program: a site and one of its rules.

Equations

• dt.RIx zero one hzo args = ((i : dt.SF) × (dt.progAsm zero one hzo args).Sh i)

The machine

The remaining fields of a DescriptiveComplexity.Draw.Prog are the reduction's constants: the start phase and an all-clear pointer, the accepting predicate – the output machinery's exit phase, with its verdict read from the control, so that a false output halts and rejects – the blank symbol, and the mark of DescriptiveComplexity.Draw.slotMark.

noncomputable def DescriptiveComplexity.Draw.Data.prog {L : FirstOrder.Language} (dt : Data L) {A Q : Type} (zero one : A) [Fintype Q] [Fintype dt.SlotIx] [LinearOrder A] (hzo : zero ≠ one) (args : (v : dt.VarIx) → dt.VarArgs v) [LinearOrder (dt.RIx zero one hzo args)] [LinearOrder dt.PF] (hpl : Fintype.card (Q ⊕ dt.SlotIx) ≤ dt.dd) : Prog A (dt.RIx zero one hzo args) dt.PF Q dt.SlotIx dt.KIx dt.dd

The EXPSPACE program: the assembled rule set with the reduction's constants.

Equations

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

theorem DescriptiveComplexity.Draw.Data.prog_sep {L : FirstOrder.Language} (dt : Data L) {A Q : Type} (zero one : A) [Fintype Q] [Fintype dt.SlotIx] [LinearOrder A] (hzo : zero ≠ one) (args : (v : dt.VarIx) → dt.VarArgs v) [LinearOrder (dt.RIx zero one hzo args)] [LinearOrder dt.PF] (hpl : Fintype.card (Q ⊕ dt.SlotIx) ≤ dt.dd) : (dt.prog zero one hzo args hpl).table.Sep

The program is deterministic: separation by the assembly, site by site.

theorem DescriptiveComplexity.Draw.Data.prog_mark_mir {L : FirstOrder.Language} {dt : Data L} {A Q : Type} {zero one : A} [Fintype Q] [Fintype dt.SlotIx] [LinearOrder A] {hzo : zero ≠ one} {args : (v : dt.VarIx) → dt.VarArgs v} [LinearOrder (dt.RIx zero one hzo args)] [LinearOrder dt.PF] (hpl : Fintype.card (Q ⊕ dt.SlotIx) ≤ dt.dd) (x : Univ A (dt.RIx zero one hzo args) dt.PF dt.KIx dt.dd) : (dt.prog zero one hzo args hpl).mark x Slot.mir = (dt.prog zero one hzo args hpl).zero

The mirror track is clear at time zero – on the register file and off it alike – so it is the track the initial tape is presented along (DescriptiveComplexity.Draw.Prog.trackTape_initBack).

theorem DescriptiveComplexity.Draw.Data.prog_blank_mir {L : FirstOrder.Language} {dt : Data L} {A Q : Type} {zero one : A} [Fintype Q] [Fintype dt.SlotIx] [LinearOrder A] {hzo : zero ≠ one} {args : (v : dt.VarIx) → dt.VarArgs v} [LinearOrder (dt.RIx zero one hzo args)] [LinearOrder dt.PF] (hpl : Fintype.card (Q ⊕ dt.SlotIx) ≤ dt.dd) : (dt.prog zero one hzo args hpl).blank Slot.mir = (dt.prog zero one hzo args hpl).zero