Skip to content

feat(ppt): lift plain deterministic certificates to pure programs #813

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
SamuelSchlesinger merged 1 commit into from
Oct 24, 2026
Merged

feat(ppt): lift plain deterministic certificates to pure programs #813

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
13 changes: 12 additions & 1 deletion Complexity/Computability/Probabilistic/PPT.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -9,6 +9,8 @@ module

public import Complexity.Computability.Machines.Turing.MultiTape.Probabilistic.Deterministic
public import Complexity.Computability.Machines.Turing.MultiTape.Complexity.PolyTime
public import Complexity.Computability.Machines.Turing.MultiTape.PolyTime
import Complexity.Computability.Machines.Turing.MultiTape.Complexity.PolyTime.Plain
import Complexity.Probability.PMF.Event
import Complexity.Computability.Machines.Turing.MultiTape.Plumbing.Tidy.Run

Expand Down Expand Up @@ -44,7 +46,7 @@ control type, as the upstream tidy calculus does, instead of imposing a separate

## Main results

* `Turing.MultiTapeTM.ComputableTidilyInPolyTime.isPPTOn`: deterministic certificates lift to PPT.
* `Turing.MultiTapeTM.ComputableInPolyTime.isPPTOn`: deterministic certificates lift to PPT.
* `Cslib.Probability.IsPPTOn.length_le`: every supported encoded output is polynomially bounded.
-/

Expand Down Expand Up @@ -110,3 +112,12 @@ theorem Turing.MultiTapeTM.ComputableTidilyInPolyTime.isPPTOn {α β : Type}
refine ⟨k, State, hfinite, Turing.MultiTapePTM.ofDeterministic machine, c, d, fun a => ?_⟩
rw [Cslib.ProbComp.eval_pure, PMF.pure_map, Turing.MultiTapePTM.eval_runClosed_ofDeterministic]
exact congrArg PMF.pure ((hmachine a).mono (ht a) le_rfl).runFrom_initCfg.2.symm

/-- A plain deterministic polynomial-time certificate gives a fair-coin machine that ignores
its sampled bits, with the same encoded result distribution. -/
@[fun_prop]
theorem Turing.MultiTapeTM.ComputableInPolyTime.isPPTOn {α β : Type}
{input : α ↪ List Bool} {output : β ↪ List Bool} {f : α → β}
(h : ComputableInPolyTime f input output) :
Cslib.Probability.IsPPTOn input output (fun a => pure (f a)) :=
h.tidy.isPPTOn
1 change: 1 addition & 0 deletions ComplexityTests.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -343,6 +343,7 @@ import ComplexityTests.PRGStretch
import ComplexityTests.Parameterized
import ComplexityTests.PlainAutomationSupport
import ComplexityTests.PlainLawfulBEq
import ComplexityTests.PlainPurePPT
import ComplexityTests.PolySpaceFold
import ComplexityTests.PolyTimeBinaryWord
import ComplexityTests.PolyTimeContracts
Expand Down
22 changes: 22 additions & 0 deletions ComplexityTests/PlainPurePPT.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1,22 @@
/-
Copyright (c) 2026 Samuel Schlesinger. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Samuel Schlesinger
-/

import Complexity.Computability.Probabilistic.PPT

/-! Plain deterministic certificates lift through ordinary imports, with full typed context. -/

open Turing.MultiTapeTM Cslib.Probability

example {α β : Type} {input : α ↪ List Bool} {output : β ↪ List Bool} {f : α → β}
(h : ComputableInPolyTime f input output) :
IsPPTOn input output (fun a => pure (f a)) :=
ComputableInPolyTime.isPPTOn h

example {α β : Type} {input : α ↪ List Bool} {output : β ↪ List Bool} {f : α → β}
(h : ComputableInPolyTime f input output) :
IsPPTOn input output (fun a => pure (f a)) := by
fail_if_success (clear h; fun_prop)
fun_prop
Loading