A partial fixed point that holds makes the machine accept

The forward half of the EXPSPACE reduction, assembled: from the initial configuration – the marks over the blank – through the startup, MAIN and the output evaluation, to the accepting phase. Every leg is a theorem of the run layer; what this file does is choose the parameters those legs are stated at and discharge their hypotheses.

The choices, once:

• the end marker is the last logical address (DescriptiveComplexity.Draw.logicalTop), which is what the startup's pattern write leaves in TARGET (DescriptiveComplexity.Draw.Data.tgtTopSt_tgt);
• the VAL enumeration is the increment chain of DescriptiveComplexity.Draw.Data.exists_valEnum, indexed by Fin (n + 1) so that its bottom and top are 0 and Fin.last n;
• the stage the machine stops at is the first stable one (DescriptiveComplexity.StepDef.exists_least_stable), which exists because a definition whose value is read converges.

The two constraints on the layout the assembly needs are the ones DescriptiveComplexity.Draw.Data.wmSetLt_stageTgtD_logicalTop asks for: one coordinate of slack beyond the encoding budget (dd0 < dd) and one argument block to name (dt.KIx nonempty).

The end marker the startup plants

theorem DescriptiveComplexity.Draw.Data.tgtTopSt_tgt {L : FirstOrder.Language} (dt : Data L) {A R' P' : Type} : dt.tgtTopSt.tgt = logicalTop

The pattern the startup writes into TARGET is the last logical address: a tag has a block exactly when it is an argument tag. This is what pins the end marker of the whole run, and with it the interval every dictionary statement of the layer is read over.

theorem DescriptiveComplexity.Draw.Data.startupSt_wk {L : FirstOrder.Language} {dt : Data L} {A R' P' : Type} : dt.startupSt.wk = fun (r : Univ A R' P' dt.KIx dt.dd → Prop) => r = fun (x : Univ A R' P' dt.KIx dt.dd) => False

The startup leaves the marker at the empty address.

theorem DescriptiveComplexity.Draw.Data.startupSt_mir {L : FirstOrder.Language} {dt : Data L} {A R' P' : Type} : dt.startupSt.mir = fun (x : Univ A R' P' dt.KIx dt.dd) => False

The startup leaves the mirror home.

theorem DescriptiveComplexity.Draw.Data.startupSt_bot {L : FirstOrder.Language} {dt : Data L} {A R' P' : Type} : dt.startupSt.bot = fun (r : Univ A R' P' dt.KIx dt.dd → Prop) => r = fun (x : Univ A R' P' dt.KIx dt.dd) => False

The startup leaves the bottom mark at the empty address.

theorem DescriptiveComplexity.Draw.Data.startupSt_ltp {L : FirstOrder.Language} {dt : Data L} {A R' P' : Type} : dt.startupSt.ltp = fun (r : Tag R' P' dt.KIx × (Fin dt.dd → A) → Prop) => r = logicalTop

The startup leaves the end marker at the last logical address.

The forward run

theorem DescriptiveComplexity.Draw.Data.wmSetLt_congr_rel {α : Type} {Le Le' : α → α → Prop} (h : ∀ (x y : α), Le x y ↔ Le' x y) (s u : α → Prop) : WMSetLt Le s u ↔ WMSetLt Le' s u

The strict order on addresses depends on the order of the elements only through its extension – the companion of DescriptiveComplexity.Draw.Table.wmSetLe_congr_rel, and what carries the layout's own placement lemmas to the instance's order.

theorem DescriptiveComplexity.Draw.Data.outLeg_verdict {L : FirstOrder.Language} {dt : Data L} {A : Type} {zero one : A} [LinearOrder A] [Fintype dt.SlotIx] [Finite A] [Finite dt.KIx] [Nonempty A] [L.IsRelational] [L.Structure A] {hzo : zero ≠ one} [LinearOrder (dt.RIx zero one hzo fun (w : dt.VarIx) => dt.varArgsOf zero one w)] [LinearOrder dt.PF] {hpl : Fintype.card (dt.CtlIx ⊕ dt.SlotIx) ≤ dt.dd} [FirstOrder.Language.wide.Structure (Univ A (dt.RIx zero one hzo fun (w : dt.VarIx) => dt.varArgsOf zero one w) dt.PF dt.KIx dt.dd)] [Finite (dt.RIx zero one hzo fun (w : dt.VarIx) => dt.varArgsOf zero one w)] [Finite dt.PF] [LinearOrder (dt.X.Map A)] (hR : (dt.progOf zero one hzo hpl).table.Reads) (hlin : IsLinOrd WMLe) (hord : ∀ (x y : Univ A (dt.RIx zero one hzo fun (w : dt.VarIx) => dt.varArgsOf zero one w) dt.PF dt.KIx dt.dd), WMLe x y ↔ tagTupleLe x y) {gtop gbot : Univ A (dt.RIx zero one hzo fun (w : dt.VarIx) => dt.varArgsOf zero one w) dt.PF dt.KIx dt.dd} (htop : ∀ (y : Univ A (dt.RIx zero one hzo fun (w : dt.VarIx) => dt.varArgsOf zero one w) dt.PF dt.KIx dt.dd), WMLe y gtop) (hbot : ∀ (y : Univ A (dt.RIx zero one hzo fun (w : dt.VarIx) => dt.varArgsOf zero one w) dt.PF dt.KIx dt.dd), WMLe gbot y) {v₁ : Univ A (dt.RIx zero one hzo fun (w : dt.VarIx) => dt.varArgsOf zero one w) dt.PF dt.KIx dt.dd → Prop} (hiE : WMIncr WMLe (fun (x : Univ A (dt.RIx zero one hzo fun (w : dt.VarIx) => dt.varArgsOf zero one w) dt.PF dt.KIx dt.dd) => False) v₁) {nV : ℕ} (mV : Fin (nV + 1) → Univ A (dt.RIx zero one hzo fun (w : dt.VarIx) => dt.varArgsOf zero one w) dt.PF dt.KIx dt.dd → Prop) (hmV0 : mV 0 = fun (x : Univ A (dt.RIx zero one hzo fun (w : dt.VarIx) => dt.varArgsOf zero one w) dt.PF dt.KIx dt.dd) => False) (hIncr : ∀ (a a' : Fin (nV + 1)), a < a' → (∀ (b : Fin (nV + 1)), ¬(a < b ∧ b < a')) → WMIncr WMLe (mV a) (mV a')) (hTestT : ∀ (u : Univ A (dt.RIx zero one hzo fun (w : dt.VarIx) => dt.varArgsOf zero one w) dt.PF dt.KIx dt.dd), dt.InnerFull (fun (u : Univ A (dt.RIx zero one hzo fun (w : dt.VarIx) => dt.varArgsOf zero one w) dt.PF dt.KIx dt.dd) => tagBlk u.1) (mV (Fin.last nV)) u) (hTestF : ∀ a < Fin.last nV, ∃ (u : Univ A (dt.RIx zero one hzo fun (w : dt.VarIx) => dt.varArgsOf zero one w) dt.PF dt.KIx dt.dd), ¬dt.InnerFull (fun (u : Univ A (dt.RIx zero one hzo fun (w : dt.VarIx) => dt.varArgsOf zero one w) dt.PF dt.KIx dt.dd) => tagBlk u.1) (mV a) u) (hKin : ∀ (a : Fin (nV + 1)) (t : Tag (dt.RIx zero one hzo fun (w : dt.VarIx) => dt.varArgsOf zero one w) dt.PF dt.KIx) (w : Fin dt.dd → A), mV a (t, w) → ∃ (j : Fin dt.ki), t = argIn dt.ko j) (hordP : ∀ (p q : dt.X.Map A), p ≤ q ↔ p ≤ q) (st : TapeStD dt A (dt.RIx zero one hzo fun (w : dt.VarIx) => dt.varArgsOf zero one w) dt.PF) (hwkSt : st.wk = fun (r : Univ A (dt.RIx zero one hzo fun (w : dt.VarIx) => dt.varArgsOf zero one w) dt.PF dt.KIx dt.dd → Prop) => r = fun (x : Univ A (dt.RIx zero one hzo fun (w : dt.VarIx) => dt.varArgsOf zero one w) dt.PF dt.KIx dt.dd) => False) (hmirSt : st.mir = fun (x : Univ A (dt.RIx zero one hzo fun (w : dt.VarIx) => dt.varArgsOf zero one w) dt.PF dt.KIx dt.dd) => False) (hbotSt : st.bot = fun (r : Univ A (dt.RIx zero one hzo fun (w : dt.VarIx) => dt.varArgsOf zero one w) dt.PF dt.KIx dt.dd → Prop) => r = fun (x : Univ A (dt.RIx zero one hzo fun (w : dt.VarIx) => dt.varArgsOf zero one w) dt.PF dt.KIx dt.dd) => False) (σ : dt.d.B.Assignment (dt.X.Map A)) (hdict : ∀ (iv : dt.d.B.ι) (s : Univ A (dt.RIx zero one hzo fun (w : dt.VarIx) => dt.varArgsOf zero one w) dt.PF dt.KIx dt.dd → Prop), WMSetLt WMLe s logicalTop → (st.old iv s ↔ trackOf dt.ly zero one ⋯ σ s)) (hbelow : ∀ (a : Fin (nV + 1)) (iv : dt.d.B.ι) (ts : Fin (dt.d.B.arity iv) → Fin (dt.nOf none)), WMSetLt WMLe (dt.stageTgtD zero none iv ts (dt.roundSt st (mV a)) (fun (x : Univ A (dt.RIx zero one hzo fun (w : dt.VarIx) => dt.varArgsOf zero one w) dt.PF dt.KIx dt.dd) => False) (dt.d.B.arity iv)) logicalTop) (f₀ : dt.CtlIx → A) : ∃ (cfg : Config (WPoint (Univ A (dt.RIx zero one hzo fun (w : dt.VarIx) => dt.varArgsOf zero one w) dt.PF dt.KIx dt.dd))) (f : dt.CtlIx → A), Relation.ReflTransGen (wideData (Univ A (dt.RIx zero one hzo fun (w : dt.VarIx) => dt.varArgsOf zero one w) dt.PF dt.KIx dt.dd)).Step { state := Sum.inr ((dt.progOf zero one hzo hpl).stElt (OuterPh.evalP (EvalPh.sub dt.smEntryOut)) f₀), head := Sum.inl v₁, tape := wideTape ((dt.progOf zero one hzo hpl).trackTapeAt wmSeg Slot.val (dt.back wmSeg zero one ⋯ st) st.val) ((dt.progOf zero one hzo hpl).syElt (dt.progOf zero one hzo hpl).blank) } cfg ∧ cfg.state = Sum.inr ((dt.progOf zero one hzo hpl).stElt OuterPh.acceptP f) ∧ ((dt.progOf zero one hzo hpl).accept OuterPh.acceptP f ↔ dt.X.Map A ⊨ dt.d.out)

The output leg lands in the accepting phase with the output sentence as its verdict, at any state whose tracks hold a stage. The output variable is nullary, so its argument block is empty and every hypothesis the machinery asks about the working address's blocks is a function on Fin 0; what is left is the verdict, which is DescriptiveComplexity.Draw.Data.accVerdict_out – an equivalence, so this one leg settles both the accepting and the rejecting case.

theorem DescriptiveComplexity.Draw.Data.reaches_outVerdict {L : FirstOrder.Language} {dt : Data L} {A : Type} {zero one : A} [LinearOrder A] [Fintype dt.SlotIx] [Finite A] [Finite dt.KIx] [Nonempty A] [L.IsRelational] [L.Structure A] {hzo : zero ≠ one} [LinearOrder (dt.RIx zero one hzo fun (w : dt.VarIx) => dt.varArgsOf zero one w)] [LinearOrder dt.PF] {hpl : Fintype.card (dt.CtlIx ⊕ dt.SlotIx) ≤ dt.dd} [FirstOrder.Language.wide.Structure (Univ A (dt.RIx zero one hzo fun (w : dt.VarIx) => dt.varArgsOf zero one w) dt.PF dt.KIx dt.dd)] [Finite (dt.RIx zero one hzo fun (w : dt.VarIx) => dt.varArgsOf zero one w)] [Finite dt.PF] [LinearOrder (dt.X.Map A)] (hR : (dt.progOf zero one hzo hpl).table.Reads) (hdd : dt.dd0 < dt.dd) (i₀ : dt.KIx) (hordP : ∀ (p q : dt.X.Map A), p ≤ q ↔ p ≤ q) (hcv : dt.d.PFPConverges (dt.X.Map A)) : ∃ (cfg : Config (WPoint (Univ A (dt.RIx zero one hzo fun (w : dt.VarIx) => dt.varArgsOf zero one w) dt.PF dt.KIx dt.dd))) (f : dt.CtlIx → A), Relation.ReflTransGen (wideData (Univ A (dt.RIx zero one hzo fun (w : dt.VarIx) => dt.varArgsOf zero one w) dt.PF dt.KIx dt.dd)).Step { state := Sum.inr ((dt.progOf zero one hzo hpl).stElt (dt.progOf zero one hzo hpl).startPh (dt.progOf zero one hzo hpl).startSt), head := Sum.inl fun (x : Univ A (dt.RIx zero one hzo fun (w : dt.VarIx) => dt.varArgsOf zero one w) dt.PF dt.KIx dt.dd) => False, tape := wideTape ((dt.progOf zero one hzo hpl).trackTapeAt wmSeg Slot.mir (dt.progOf zero one hzo hpl).initBack fun (x : Univ A (dt.RIx zero one hzo fun (w : dt.VarIx) => dt.varArgsOf zero one w) dt.PF dt.KIx dt.dd) => False) ((dt.progOf zero one hzo hpl).syElt (dt.progOf zero one hzo hpl).blank) } cfg ∧ cfg.state = Sum.inr ((dt.progOf zero one hzo hpl).stElt OuterPh.acceptP f) ∧ ((dt.progOf zero one hzo hpl).accept OuterPh.acceptP f ↔ dt.d.PFPHolds (dt.X.Map A))

The whole run, from the initial configuration to the accepting phase, with the accepting predicate at the state it stops in equivalent to the value of the partial fixed point. Convergence is all that is asked: it is what makes MAIN's loop stop, and the verdict the output leg then writes is the sentence read at the stable stage (DescriptiveComplexity.StepDef.partStage_eq_of_isFixedPt making that stage the one PFPHolds speaks of).

theorem DescriptiveComplexity.Draw.Data.dwideAcceptSpace_of_pfpHolds {L : FirstOrder.Language} {dt : Data L} {A : Type} {zero one : A} [LinearOrder A] [Fintype dt.SlotIx] [Finite A] [Finite dt.KIx] [Nonempty A] [L.IsRelational] [L.Structure A] {hzo : zero ≠ one} [LinearOrder (dt.RIx zero one hzo fun (w : dt.VarIx) => dt.varArgsOf zero one w)] [LinearOrder dt.PF] {hpl : Fintype.card (dt.CtlIx ⊕ dt.SlotIx) ≤ dt.dd} [FirstOrder.Language.wide.Structure (Univ A (dt.RIx zero one hzo fun (w : dt.VarIx) => dt.varArgsOf zero one w) dt.PF dt.KIx dt.dd)] [Finite (dt.RIx zero one hzo fun (w : dt.VarIx) => dt.varArgsOf zero one w)] [Finite dt.PF] [LinearOrder (dt.X.Map A)] (hR : (dt.progOf zero one hzo hpl).table.Reads) (hdd : dt.dd0 < dt.dd) (i₀ : dt.KIx) (hordP : ∀ (p q : dt.X.Map A), p ≤ q ↔ p ≤ q) (hpfp : dt.d.PFPHolds (dt.X.Map A)) : DWideAcceptSpace.Holds (Univ A (dt.RIx zero one hzo fun (w : dt.VarIx) => dt.varArgsOf zero one w) dt.PF dt.KIx dt.dd)

A partial fixed point that holds makes the emitted instance a yes-instance: the two promises of DescriptiveComplexity.DWideAcceptSpace – well-formedness for free, determinism from the program's separation argument – together with the run of DescriptiveComplexity.Draw.Data.reaches_outVerdict.