The alternating bridge at one block: ATMAccept 1 true is NP-complete

The base case of the machine bridge for the polynomial hierarchy, and the sanity check on the alternating model: at k = 1 the only block is 0, its polarity is the starting one, so for start = true no state is universal and DescriptiveComplexity.ATMData.AltAccepts is DescriptiveComplexity.TMData.Accepts (DescriptiveComplexity.ATMData.altAccepts_true_iff_accepts). The alternating problem is therefore the same problem as DescriptiveComplexity.NTMAccept, up to the mark – and up to the mark is exactly what a reduction is for.

Both directions are identity interpretations – one dimension, one tag – in the style of DescriptiveComplexity.DetToNondet.detInterp:

• DescriptiveComplexity.MarkOne.markInterp copies a machine and marks every element as a state of block 0, so the promise DescriptiveComplexity.ATMData.BlocksWellFormed holds in the image by construction;
• DescriptiveComplexity.ForgetOne.forgetInterp copies an alternating machine and forgets the mark, keeping the accepting states only when the promise holds in the source – the guard trick again, so that an instance failing the promise becomes a no-instance rather than a machine that might accept.

Together they make ATMAccept 1 true NP-complete: membership travels backwards along forgetInterp, hardness forwards along markInterp. Nothing here is specific to one block except the two k = 1 facts of DescriptiveComplexity.Problems.Machine.AltDefs; the general bridge replaces them by the collapse lemmas of DescriptiveComplexity.MachinesAltPlay.

Marking a machine: NTMAccept ≤ᶠᵒ ATMAccept 1 true

noncomputable def DescriptiveComplexity.MarkOne.markInterp : FOInterpretation FirstOrder.Language.turing (FirstOrder.Language.turingAlt 1) Unit 1

The identity interpretation that marks every element. Every symbol of the machine vocabulary is copied, and the single block mark holds of everything, so the interpreted instance carries a well-formed block structure.

Equations

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

@[reducible, inline]

noncomputable abbrev DescriptiveComplexity.MarkOne.toBase {A : Type} (x : markInterp.Map A) : A

The universe of the image is the universe of the source.

Equations

• DescriptiveComplexity.MarkOne.toBase x = (DescriptiveComplexity.MarkOne.markInterp.mapEquivSelf A) x

theorem DescriptiveComplexity.MarkOne.blk_map {A : Type} [FirstOrder.Language.turing.Structure A] (x : markInterp.Map A) : ATMBlk 0 x

Every element of the image is a state of block 0.

theorem DescriptiveComplexity.MarkOne.agree (A : Type) [FirstOrder.Language.turing.Structure A] : TMData.Agree (markInterp.mapEquivSelf A) (atmData 1 (markInterp.Map A)).toTMData (tmData A)

A marked machine is the machine it was built from.

theorem DescriptiveComplexity.MarkOne.correct (A : Type) [FirstOrder.Language.turing.Structure A] [Finite A] [Nonempty A] : NTMAccept.Holds A ↔ (ATMAccept 1 true).Holds (markInterp.Map A)

The reduction is correct: marking every element changes nothing, since at one existential block the alternating semantics is the nondeterministic one.

noncomputable def DescriptiveComplexity.ntmAccept_fo_reduction_atmAccept_one : FOReduction NTMAccept (ATMAccept 1 true)

Machine acceptance reduces to alternating acceptance at one block: mark every element as a state of the single block.

Equations

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

Forgetting the mark: ATMAccept 1 true ≤ᶠᵒ NTMAccept

noncomputable def DescriptiveComplexity.ForgetOne.markedG (γ : Type) : (FirstOrder.Language.turingAlt 1).Formula γ

The promise of DescriptiveComplexity.ATMAccept at one block – every element is marked – as a first-order formula whose free variables are unused: the guard the image puts on its accepting states.

Equations

• DescriptiveComplexity.ForgetOne.markedG γ = FirstOrder.Language.Formula.iAlls (Fin 1) ((FirstOrder.Language.atmBlk 0).formula₁ (FirstOrder.Language.var (Sum.inr 0)))

noncomputable def DescriptiveComplexity.ForgetOne.forgetInterp : FOInterpretation (FirstOrder.Language.turingAlt 1) FirstOrder.Language.turing Unit 1

The identity interpretation that forgets the mark, with a guarded accepting predicate.

Equations

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

@[simp]

theorem DescriptiveComplexity.ForgetOne.markedG_realize {A : Type} [(FirstOrder.Language.turingAlt 1).Structure A] {γ : Type} (v : γ → A) : (markedG γ).Realize v ↔ ∀ (q : A), ATMBlk 0 q

@[reducible, inline]

noncomputable abbrev DescriptiveComplexity.ForgetOne.toBase {A : Type} (x : forgetInterp.Map A) : A

The universe of the image is the universe of the source.

Equations

• DescriptiveComplexity.ForgetOne.toBase x = (DescriptiveComplexity.ForgetOne.forgetInterp.mapEquivSelf A) x

@[simp]

theorem DescriptiveComplexity.ForgetOne.acc_map {A : Type} [(FirstOrder.Language.turingAlt 1).Structure A] (x : forgetInterp.Map A) : TMAcc x ↔ (∀ (q : A), ATMBlk 0 q) ∧ ATMAcc (toBase x)

The accepting states of the image are guarded: an element is accepting there exactly when the source carries its promise and it is accepting in the source.

theorem DescriptiveComplexity.ForgetOne.agree_of_marked {A : Type} [(FirstOrder.Language.turingAlt 1).Structure A] (hm : ∀ (q : A), ATMBlk 0 q) : TMData.Agree (forgetInterp.mapEquivSelf A) (tmData (forgetInterp.Map A)) (atmData 1 A).toTMData

An instance carrying its promise is copied verbatim.

theorem DescriptiveComplexity.ForgetOne.not_accepts_of_not_marked {A : Type} [(FirstOrder.Language.turingAlt 1).Structure A] (hm : ¬∀ (q : A), ATMBlk 0 q) : ¬(tmData (forgetInterp.Map A)).Accepts

An instance failing its promise has no accepting state in the image.

theorem DescriptiveComplexity.ForgetOne.correct (A : Type) [(FirstOrder.Language.turingAlt 1).Structure A] [Finite A] [Nonempty A] : (ATMAccept 1 true).Holds A ↔ NTMAccept.Holds (forgetInterp.Map A)

The reduction is correct: forgetting the mark is harmless on instances that carry the promise, and the guard turns the others into no-instances.

noncomputable def DescriptiveComplexity.atmAccept_one_fo_reduction_ntmAccept : FOReduction (ATMAccept 1 true) NTMAccept

Alternating acceptance at one block reduces to machine acceptance: forget the mark, keeping the accepting states only when the promise holds.

Equations

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

The bridge at one block

theorem DescriptiveComplexity.atmAccept_one_mem_NP : NP.Mem (ATMAccept 1 true)

Alternating acceptance at one existential block is in NP.

theorem DescriptiveComplexity.atmAccept_one_NP_hard : NP.Hard (ATMAccept 1 true)

Alternating acceptance at one existential block is NP-hard.

theorem DescriptiveComplexity.atmAccept_one_NP_complete : NP.Complete (ATMAccept 1 true)

The bridge at one block: ATMAccept 1 true is NP-complete, the level-1 case of the machine bridge for the polynomial hierarchy.