From 410b9e3d58bd104dbd83f2f0da0f3bb55b689371 Mon Sep 17 00:00:00 2001
From: Samuel Giuseppe Schlesinger <sgschlesinger@gmail.com>
Date: Sat, 24 Oct 2026 11:32:07 -0400
Subject: [PATCH] feat(ppt): lift plain deterministic certificates to pure
 programs

---
 .../Computability/Probabilistic/PPT.lean      | 13 ++++++++++-
 ComplexityTests.lean                          |  1 +
 ComplexityTests/PlainPurePPT.lean             | 22 +++++++++++++++++++
 3 files changed, 35 insertions(+), 1 deletion(-)
 create mode 100644 ComplexityTests/PlainPurePPT.lean

diff --git a/Complexity/Computability/Probabilistic/PPT.lean b/Complexity/Computability/Probabilistic/PPT.lean
index 9410a5a76..59a5110c9 100644
--- a/Complexity/Computability/Probabilistic/PPT.lean
+++ b/Complexity/Computability/Probabilistic/PPT.lean
@@ -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
 
@@ -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.
 -/
 
@@ -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
diff --git a/ComplexityTests.lean b/ComplexityTests.lean
index 1f459e058..92182d6a2 100644
--- a/ComplexityTests.lean
+++ b/ComplexityTests.lean
@@ -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
diff --git a/ComplexityTests/PlainPurePPT.lean b/ComplexityTests/PlainPurePPT.lean
new file mode 100644
index 000000000..59f108faa
--- /dev/null
+++ b/ComplexityTests/PlainPurePPT.lean
@@ -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