The accepting phase is a dead end

The side condition every discharge of a no-instance in DescriptiveComplexity.Problems.Machine.DetRun asks for, at the EXPSPACE program: accepting configurations are stuck. With it, DescriptiveComplexity.TMData.not_acceptsSpace_of_reaches_dead (a run that ends badly) and DescriptiveComplexity.TMData.not_acceptsSpace_of_chain (a run that never ends) are the two ways the reduction rejects, and no invariant over the program's rules is needed for either.

DescriptiveComplexity.Draw.Assembly already carries the fact, in its owner/howner fields: every rule fires from a phase its own site owns, so a phase whose owning site contributes no rules is the source of none (DescriptiveComplexity.Draw.Assembly.srcPh_ne_of_isEmpty). The accepting phase is such a phase – OuterSh … .accept is Empty – whence DescriptiveComplexity.Draw.Data.srcPh_ne_acceptP and, at the machine, DescriptiveComplexity.Draw.Data.stuck_acc. That is what makes a false output a rejection rather than a detour, and it costs one case analysis on the tag of a transition rather than one per rule.

A phase whose site has no rules

theorem DescriptiveComplexity.Draw.Assembly.srcPh_ne_of_isEmpty {A Q W P S : Type} [Fintype Q] [Fintype W] (asm : Assembly A Q W P S) {p : P} (hp : IsEmpty (asm.Sh (asm.owner p))) (i : S) (ρ : asm.Sh i) : (asm.rule i ρ).srcPh ≠ p

A phase owned by a site with no rules is the source of no rule. Every rule fires from a phase its own site owns (Assembly.howner), so a rule with that source phase would be a rule of that site – and there are none.

The emitted machine is stuck in its accepting phase

theorem DescriptiveComplexity.Draw.Data.srcPh_ne_acceptP {L : FirstOrder.Language} {dt : Data L} {A Q : Type} {zero one : A} [LinearOrder A] [Fintype Q] [Fintype dt.SlotIx] {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} (r : dt.RIx zero one hzo args) : ((dt.prog zero one hzo args hpl).rules r).srcPh ≠ OuterPh.acceptP

No rule of the program leaves the accepting phase: its site (DescriptiveComplexity.Draw.OuterSite.accept) contributes none.

theorem DescriptiveComplexity.Draw.Data.stuck_of_srcPh_ne {L : FirstOrder.Language} {dt : Data L} {A Q : Type} {zero one : A} [LinearOrder A] [Fintype Q] [Fintype dt.SlotIx] {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} [LinearOrder dt.KIx] [FirstOrder.Language.wide.Structure (Univ A (dt.RIx zero one hzo args) dt.PF dt.KIx dt.dd)] (hR : (dt.prog zero one hzo args hpl).table.Reads) {p : dt.PF} (hp : ∀ (r : dt.RIx zero one hzo args), ((dt.prog zero one hzo args hpl).rules r).srcPh ≠ p) {w : Fin dt.dd → A} {e : Config (WPoint (Univ A (dt.RIx zero one hzo args) dt.PF dt.KIx dt.dd))} (hst : e.state = Sum.inr (Tag.phase p, w)) (e' : Config (WPoint (Univ A (dt.RIx zero one hzo args) dt.PF dt.KIx dt.dd))) : ¬(wideData (Univ A (dt.RIx zero one hzo args) dt.PF dt.KIx dt.dd)).Step e e'

A configuration in a phase no rule leaves is stuck. A step needs a transition whose source state is the machine's, and a transition's source state carries the source phase of its rule in its tag – so the case analysis is on the tag, not on the rules.

theorem DescriptiveComplexity.Draw.Data.stuck_acc {L : FirstOrder.Language} {dt : Data L} {A Q : Type} {zero one : A} [LinearOrder A] [Fintype Q] [Fintype dt.SlotIx] {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} [LinearOrder dt.KIx] [FirstOrder.Language.wide.Structure (Univ A (dt.RIx zero one hzo args) dt.PF dt.KIx dt.dd)] (hR : (dt.prog zero one hzo args hpl).table.Reads) (e : Config (WPoint (Univ A (dt.RIx zero one hzo args) dt.PF dt.KIx dt.dd))) (hacc : (wideData (Univ A (dt.RIx zero one hzo args) dt.PF dt.KIx dt.dd)).Acc e.state) (e' : Config (WPoint (Univ A (dt.RIx zero one hzo args) dt.PF dt.KIx dt.dd))) : ¬(wideData (Univ A (dt.RIx zero one hzo args) dt.PF dt.KIx dt.dd)).Step e e'

Accepting configurations of the emitted machine are stuck – the hsink side condition of DescriptiveComplexity.Problems.Machine.DetRun. An accepting state is a phase-tagged element whose phase the program accepts, and the program accepts only acceptP.