A partial fixed point that fails makes the machine reject

The converse half of the EXPSPACE reduction, in the case the iteration converges. No invariant over the program's rules appears: the machine is deterministic, so the configurations reachable from its initial one are linearly ordered, and it is enough to exhibit one run that ends badly (DescriptiveComplexity.TMData.not_acceptsSpace_of_reaches_dead). That run is the one DescriptiveComplexity.Draw.Data.reaches_outVerdict already produces: it lands in the accepting phase whatever the verdict, and the accepting predicate there is equivalent to the value of the fixed point. So a fixed point that fails leaves the machine in a phase it cannot leave (DescriptiveComplexity.Draw.Data.stuck_acc) and does not accept in.

What is left of soundness is the diverging case, where the machine has no halting configuration to reach at all and DescriptiveComplexity.TMData.not_acceptsSpace_of_chain takes over.

theorem DescriptiveComplexity.Draw.Data.accept_of_isAcc {L : FirstOrder.Language} {dt : Data L} {A : Type} {zero one : A} [LinearOrder A] [Fintype dt.SlotIx] [Finite A] [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} {p : dt.PF} {f : dt.CtlIx → A} (h : (dt.progOf zero one hzo hpl).table.IsAcc ((dt.progOf zero one hzo hpl).stElt p f)) : (dt.progOf zero one hzo hpl).accept p f

The machine's accepting predicate is the program's, read back: the converse of DescriptiveComplexity.Draw.Prog.accept_table, the pointer being recovered from the state's payload by the same equation.

theorem DescriptiveComplexity.Draw.Data.not_dwideAcceptSpace_of_converges {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)) (hno : ¬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 converging fixed point that fails makes the emitted instance a no-instance. The run of reaches_outVerdict ends in the accepting phase, which no rule leaves, with the accepting predicate equivalent to the value of the fixed point – so when that value is False the run has reached a dead end that does not accept, and a deterministic machine has no other run.

theorem DescriptiveComplexity.Draw.Data.not_dwideAcceptSpace_of_diverges {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) (hdv : ¬dt.d.PFPConverges (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 diverging fixed point makes the emitted instance a no-instance. The machine has no clock: when no stage is stable it keeps sweeping, so its run passes an unbounded chain of stage entries (DescriptiveComplexity.Draw.Data.transGen_stageB, each link at least one step) and reaches no halting configuration at all – whence DescriptiveComplexity.TMData.not_acceptsSpace_of_chain.

The reduction is correct

theorem DescriptiveComplexity.Draw.Data.dwideAcceptSpace_iff_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) : DWideAcceptSpace.Holds (Univ A (dt.RIx zero one hzo fun (w : dt.VarIx) => dt.varArgsOf zero one w) dt.PF dt.KIx dt.dd) ↔ dt.d.PFPHolds (dt.X.Map A)

The emitted instance is a yes-instance exactly when the partial fixed point holds. The three cases of the trichotomy are the three theorems above: a fixed point that holds is run into the accepting phase; one that converges and fails leaves the machine at a dead end; and one that diverges keeps it sweeping for ever. Nothing here is an induction over the program's rules – the machine's determinism does that work, and the only side condition is that its accepting phase is a dead end.