A guessing program, deterministic after its guess

A reduction into DescriptiveComplexity.WideAccept has to read its certificate off an arbitrary accepting run, so the program cannot be deterministic: its guessing phase is exactly the place where two runs part. What makes the reading survivable is that it parts there and nowhere else, and the notion that says so is DescriptiveComplexity.TMData.UniqueFrom – every configuration reachable from a given one has at most one successor – which all the read-off lemmas of DescriptiveComplexity.Problems.Machine.DetRun are stated at.

This file joins the two halves. DescriptiveComplexity.Draw.Table.SepOn is the program's obligation, discharged rule by rule as DescriptiveComplexity.Draw.Table.Sep is; hclosed says the phases it separates at are never left; and the conclusion is uniqueness from any configuration whose state has one of those phases. Global determinism is the case Ph = fun _ => True, where hclosed is free.

theorem DescriptiveComplexity.Draw.Table.uniqueFrom_of_sepOn {A R P K : Type} {c dd : ℕ} {T : Table A R P K c dd} [LinearOrder R] [LinearOrder P] [LinearOrder K] [LinearOrder A] [FirstOrder.Language.wide.Structure (Univ A R P K dd)] [Finite A] [Finite R] [Finite P] [Finite K] (hR : T.Reads) (hlin : IsLinOrd WMLe) {Ph : P → Prop} (hsep : T.SepOn Ph) (hclosed : ∀ (r : R), Ph (T.srcPh r) → Ph (T.dstPh r)) {cfg : Config (WPoint (Univ A R P K dd))} (hcfg : ∀ (p : P) (f : Fin c → A), cfg.state = Sum.inr (stateElt T.zero p f) → Ph p) : (wideData (Univ A R P K dd)).UniqueFrom cfg

A program that separates at the phases it can reach is unique from there. The invariant is “the state's phase satisfies Ph”: a rule fired from such a phase lands in one again by hclosed, and at such a state the transition is pinned by DescriptiveComplexity.Draw.Table.tr_unique_of_sepOn. This is what a guessing program has in place of determinism.