The native machine characterization of UP

The parsimonious #P characterization preserves the at-most-one accepting-count condition in the verifier definition of UP [Pap94a]. Ambiguity counts accepting transition occurrence traces, not distinct final configurations or all branches. Rejecting branches are unrestricted in number, and enlarging an adequate clock does not multiply halted branches.

The tape count, finite control, machine and polynomial clock are fixed before the input. Every branch halts without getting stuck on the encoding image; encBits covers all binary inputs. No decoder or halting/correctness contract outside that image is assumed.

Main results

• Cslib.Complexity.mem_UP_iff_exists_machine: UP is native polynomial time with at most one accepting occurrence trace per encoded input.

References

• C. H. Papadimitriou, Computational Complexity

The actual guess-and-verify construction and its formalization credits are in Classes.SharpP.Characterization; this module transports the ambiguity bound through its exact accepting-count equality.

theorem Cslib.Complexity.mem_UP_iff_exists_machine {α : Type} {enc : α ↪ List Bool} {A : Set α} : A ∈ UP enc ↔ ∃ (k : ℕ) (State : Type) (_ : Finite State) (machine : Turing.MultiTapeCTM k Bool State) (clock : Polynomial ℕ), machine.Nonblocking ∧ ∀ (a : α), machine.HaltsWithin (Polynomial.eval (enc a).length clock) (Turing.Cfg.init machine.initial (enc a)) ∧ machine.acceptCount (Polynomial.eval (enc a).length clock) (Turing.Cfg.init machine.initial (enc a)) ≤ 1 ∧ (a ∈ A ↔ machine.acceptCount (Polynomial.eval (enc a).length clock) (Turing.Cfg.init machine.initial (enc a)) = 1)

UP is exactly native polynomial-time computation with at most one accepting branch. All machine parameters precede the input; the ambiguity bound concerns accepting branches only. The all-branches clock is in encoded input length, with no halting claim outside the encoding.