Intrinsically halting PPT realizations

Every strict clocked PPT certificate admits a finite machine that actually halts in polynomial time with the same output distribution. The clock compiler starts with blank tapes and charges preparation of its unary budget. Its bound and finite control are uniform over all inputs.

Main results

• Turing.MultiTapePTM.exists_halting_clock: compile a polynomial cutoff under fair-coin semantics.
• Cslib.Probability.IsPPTOn.exists_halting_machine: choose an intrinsically halting PPT witness.

References

Adapts Computability/Probabilistic/Clock.lean on the cslib crypto branch at 5ff69ca93402e7c947208dc56396d6d86203ccd8, using the common machine compilers and existing tidy functional budget generation.

theorem Turing.MultiTapePTM.exists_halting_clock {k : ℕ} {State : Type} [Finite State] (machine : MultiTapePTM k Bool State) (coefficient degree : ℕ) : ∃ (k' : ℕ) (State' : Type) (_ : Finite State') (target : MultiTapePTM k' Bool State') (c : ℕ) (d : ℕ), ∀ (input : List Bool), (target.runClosed (c * (input.length + 1) ^ d) input).eval = (machine.runClosed (coefficient * (input.length + 1) ^ degree) input).eval ∧ ∀ final ∈ (Cslib.ProbComp.eval (target.runConfigFrom (Cslib.ProbComp.uniform Bool) Empty.elim (c * (input.length + 1) ^ d) (MultiTapeMachine.initialConfig target input))).support, final.tapes.state = none

A polynomial cutoff can be implemented by a finite machine that halts under fair-coin semantics, with one polynomial bound on all inputs and every supported execution.

theorem Cslib.Probability.IsPPTOn.exists_halting_machine {α β : Type} {input : α ↪ List Bool} {output : β ↪ List Bool} {program : α → ProbComp β} (h : IsPPTOn input output program) : ∃ (k : ℕ) (State : Type) (_ : Finite State) (machine : Turing.MultiTapePTM k Bool State) (c : ℕ) (d : ℕ), (∀ (a : α), PMF.map (⇑output) (program a).eval = (machine.runClosed (c * ((input a).length + 1) ^ d) (input a)).eval) ∧ ∀ (word : List Bool), ∀ final ∈ (ProbComp.eval (machine.runConfigFrom (ProbComp.uniform Bool) Empty.elim (c * (word.length + 1) ^ d) (Turing.MultiTapeMachine.initialConfig machine word))).support, final.tapes.state = none

Replace a strict clocked certificate by an intrinsically halting finite realization. The new machine and bound are fixed before choosing an input. It halts on every raw word, including words outside the declared input encoding.