From f204da57a692b8857702876205e76a2794d772a6 Mon Sep 17 00:00:00 2001 From: Samuel Giuseppe Schlesinger Date: Fri, 23 Oct 2026 17:55:09 -0400 Subject: [PATCH 1/3] fix(polytime): certify plain verifiers and document bounded mixed search --- .../Classes/SharpP/Combinators.lean | 31 +++++++ .../MultiTape/Complexity/PolyTime/Plain.lean | 25 ++++++ ComplexityTests.lean | 1 + ComplexityTests/PolyTimeMixes.lean | 86 +++++++++++++++++++ 4 files changed, 143 insertions(+) create mode 100644 ComplexityTests/PolyTimeMixes.lean diff --git a/Complexity/Computability/Complexity/Classes/SharpP/Combinators.lean b/Complexity/Computability/Complexity/Classes/SharpP/Combinators.lean index 8b4b7cf45f..ad6133316b 100644 --- a/Complexity/Computability/Complexity/Classes/SharpP/Combinators.lean +++ b/Complexity/Computability/Complexity/Classes/SharpP/Combinators.lean @@ -50,6 +50,10 @@ independent random choices [Arora and Barak, Chapters 7 and 17][AroraBarak09]. `Cslib.Complexity.computableTidilyInPolyTime_orVerifier`, `Cslib.Complexity.computableTidilyInPolyTime_selectVerifier`: the combined verifiers are polynomial-time. +* `Cslib.Complexity.computableInPolyTime_andVerifier`, + `Cslib.Complexity.computableInPolyTime_orVerifier`, + `Cslib.Complexity.computableInPolyTime_selectVerifier`: plain `fun_prop` rules accepting plain + verifier hypotheses. ## References @@ -123,6 +127,15 @@ theorem computableTidilyInPolyTime_andVerifier {enc : α ↪ List Bool} {k : α unfold andVerifier fun_prop +/-- Independent conjunction of plain polynomial-time verifiers is polynomial-time. -/ +@[fun_prop] +theorem computableInPolyTime_andVerifier {enc : α ↪ List Bool} {k : α → ℕ} + {V₁ V₂ : α × List Bool → Bool} (hk : ComputableInPolyTime k enc encUnary) + (hV₁ : ComputableInPolyTime V₁ (encPair enc encBits) encBool) + (hV₂ : ComputableInPolyTime V₂ (encPair enc encBits) encBool) : + ComputableInPolyTime (andVerifier k V₁ V₂) (encPair enc encBits) encBool := + .of_tidy (computableTidilyInPolyTime_andVerifier hk.tidy hV₁.tidy hV₂.tidy) + /-! ### Disjunction on disjoint parts of the string -/ /-- Run `V₁` on the first `k a` bits and `V₂` on the remaining bits, and accept when either @@ -151,6 +164,15 @@ theorem computableTidilyInPolyTime_orVerifier {enc : α ↪ List Bool} {k : α unfold orVerifier fun_prop +/-- Independent disjunction of plain polynomial-time verifiers is polynomial-time. -/ +@[fun_prop] +theorem computableInPolyTime_orVerifier {enc : α ↪ List Bool} {k : α → ℕ} + {V₁ V₂ : α × List Bool → Bool} (hk : ComputableInPolyTime k enc encUnary) + (hV₁ : ComputableInPolyTime V₁ (encPair enc encBits) encBool) + (hV₂ : ComputableInPolyTime V₂ (encPair enc encBits) encBool) : + ComputableInPolyTime (orVerifier k V₁ V₂) (encPair enc encBits) encBool := + .of_tidy (computableTidilyInPolyTime_orVerifier hk.tidy hV₁.tidy hV₂.tidy) + /-! ### Choosing by the first bit -/ /-- Run `V₀` on the remaining bits when the first bit is `false`, and `V₁` when it is `true`. -/ @@ -177,4 +199,13 @@ theorem computableTidilyInPolyTime_selectVerifier {enc : α ↪ List Bool} unfold selectVerifier fun_prop +/-- Selection by the first bit preserves plain polynomial-time verification. -/ +@[fun_prop] +theorem computableInPolyTime_selectVerifier {enc : α ↪ List Bool} + {V₀ V₁ : α × List Bool → Bool} + (hV₀ : ComputableInPolyTime V₀ (encPair enc encBits) encBool) + (hV₁ : ComputableInPolyTime V₁ (encPair enc encBits) encBool) : + ComputableInPolyTime (selectVerifier V₀ V₁) (encPair enc encBits) encBool := + .of_tidy (computableTidilyInPolyTime_selectVerifier hV₀.tidy hV₁.tidy) + end Cslib.Complexity diff --git a/Complexity/Computability/Machines/Turing/MultiTape/Complexity/PolyTime/Plain.lean b/Complexity/Computability/Machines/Turing/MultiTape/Complexity/PolyTime/Plain.lean index 869d50fa88..91cfc4ba80 100644 --- a/Complexity/Computability/Machines/Turing/MultiTape/Complexity/PolyTime/Plain.lean +++ b/Complexity/Computability/Machines/Turing/MultiTape/Complexity/PolyTime/Plain.lean @@ -44,6 +44,31 @@ through the transition, from tidy certificates. A tidy certificate stated for a such as the `…WithInput` scans, is not reached this way; use `polytime`, or `.of_tidy` around a tidy `fun_prop` proof. +## Mixing plain hypotheses with tidy certificates + +There is deliberately no `fun_prop` transition from plain to tidy: registering it together with +the reverse transition would create a search cycle. In particular, a tidy goal such as +`ComputableTidilyInPolyTime (fun a => [f a]) enc (encList encIntBin)` cannot use a plain certificate +for `f` directly. This occurs when constructing singleton target lists in `WPP/Robustness.lean` +and `WPP/TwoSided.lean`. Unbounded `fun_prop` can exhaust its heartbeat budget while looking for +another certificate. Restate the needed hypothesis with `have hf := hf.tidy` before `fun_prop`, +or use `polytime` from `Complexity.Tactic.PolyTime`, which prepares plain hypotheses for tidy +search. When trying composition speculatively, use +`fun_prop (config := { maxSteps := 32 })` to bound that attempt, then supply a certificate or +switch tactics. This is a search budget, not a guarantee that every unsuccessful search is cheap. + +`selectVerifier`, `andVerifier` and `orVerifier` have plain `fun_prop` rules in +`Classes/SharpP/Combinators.lean`, so plain verifier hypotheses need no manual `.tidy` conversion +for a plain goal. Their tidy rules remain available for proofs using the tidy calculus. + +For a tidy certificate covering a whole composite whose intermediate encoding is difficult to +infer, prefer `polytime`, or convert the hypotheses with `.tidy` and use +`.of_tidy (by fun_prop)`. Two representative cases are the binary threshold +`fun a => 3 * (k a * 2 ^ q.eval (enc a).length)` in `inter_mem_SBP_of_mem_BPP` (where `k` uses +`encNat`, while the exponent uses `encUnary`), and the input-dependent `sharpTest` verifier in +`Classes/Toda.lean`. `polytime` proves both directly from plain hypotheses. The mixed-encoding +examples and the bounded singleton failure are checked in `ComplexityTests/PolyTimeMixes.lean`. + Upstream `Turing.MultiTapeTM.DecidableInTimeAndSpace` decides a problem through its Boolean indicator. `Turing.MultiTapeTM.decidableInTimeAndSpace_iff` restates it for any Boolean function deciding membership, the form used by the classes in `Cslib.Complexity`. diff --git a/ComplexityTests.lean b/ComplexityTests.lean index 711475f8f7..a4f35c86e6 100644 --- a/ComplexityTests.lean +++ b/ComplexityTests.lean @@ -336,6 +336,7 @@ import ComplexityTests.Parameterized import ComplexityTests.PolySpaceFold import ComplexityTests.PolyTimeContracts import ComplexityTests.PolyTimeMetadata +import ComplexityTests.PolyTimeMixes import ComplexityTests.PolyTimePlain import ComplexityTests.PolyTimeScans import ComplexityTests.PolyTimeSearch diff --git a/ComplexityTests/PolyTimeMixes.lean b/ComplexityTests/PolyTimeMixes.lean new file mode 100644 index 0000000000..fd4cc3a8c4 --- /dev/null +++ b/ComplexityTests/PolyTimeMixes.lean @@ -0,0 +1,86 @@ +/- +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.Tactic.PolyTime +import Complexity.Computability.Complexity.Classes.SharpP.Combinators +import Complexity.Computability.Complexity.Classes.Toda.Counting +import Complexity.Computability.Machines.Turing.MultiTape.Complexity.PolyTime.Int.Binary + +/-! Plain/tidy automation boundaries from #558: bounded failure, verifier rules, the SBP +binary threshold and Toda's input-dependent counting verifier. -/ + +namespace ComplexityTests.PolyTimeMixes + +open Cslib Cslib.Complexity Turing.MultiTapeTM +variable {α : Type} {enc : α ↪ List Bool} + +set_option maxHeartbeats 2000 in +-- Check that a bounded failed attempt and the explicit certificate fit a small heartbeat budget. +/-- The WPP singleton target: bound a failed tidy search before explicitly preparing the plain +hypothesis. The default search on this shape can run to its heartbeat limit. -/ +example {f : α → ℤ} (hf : ComputableInPolyTime f enc encIntBin) : + ComputableTidilyInPolyTime (fun a => [f a]) enc (encList encIntBin) := by + fail_if_success fun_prop (config := { maxSteps := 32 }) + have hf := hf.tidy + fun_prop + +/-- `polytime` prepares the same plain hypothesis without a manual conversion. -/ +example {f : α → ℤ} (hf : ComputableInPolyTime f enc encIntBin) : + ComputableTidilyInPolyTime (fun a => [f a]) enc (encList encIntBin) := by polytime + +/-- Before: prepare each verifier for the existing tidy rule, then convert its result. -/ +example {k : α → ℕ} {V W : α × List Bool → Bool} + (hk : ComputableInPolyTime k enc encUnary) + (hV : ComputableInPolyTime V (encPair enc encBits) encBool) + (hW : ComputableInPolyTime W (encPair enc encBits) encBool) : + ComputableInPolyTime (andVerifier k V W) (encPair enc encBits) encBool := + .of_tidy (computableTidilyInPolyTime_andVerifier hk.tidy hV.tidy hW.tidy) + +/-- After: the plain rule lets `fun_prop` use the plain hypotheses directly. -/ +example {k : α → ℕ} {V W : α × List Bool → Bool} + (hk : ComputableInPolyTime k enc encUnary) + (hV : ComputableInPolyTime V (encPair enc encBits) encBool) + (hW : ComputableInPolyTime W (encPair enc encBits) encBool) : + ComputableInPolyTime (andVerifier k V W) (encPair enc encBits) encBool := by fun_prop + +example {k : α → ℕ} {V W : α × List Bool → Bool} + (hk : ComputableInPolyTime k enc encUnary) + (hV : ComputableInPolyTime V (encPair enc encBits) encBool) + (hW : ComputableInPolyTime W (encPair enc encBits) encBool) : + ComputableInPolyTime (orVerifier k V W) (encPair enc encBits) encBool := by fun_prop + +example {V W : α × List Bool → Bool} + (hV : ComputableInPolyTime V (encPair enc encBits) encBool) + (hW : ComputableInPolyTime W (encPair enc encBits) encBool) : + ComputableInPolyTime (selectVerifier V W) (encPair enc encBits) encBool := by fun_prop + +/-- The plain rules still accept a mixture of plain and tidy verifier certificates. -/ +example {V W : α × List Bool → Bool} + (hV : ComputableInPolyTime V (encPair enc encBits) encBool) + (hW : ComputableTidilyInPolyTime W (encPair enc encBits) encBool) : + ComputableInPolyTime (selectVerifier V W) (encPair enc encBits) encBool := by fun_prop + +/-- Before: convert the binary input certificate, search tidily, and convert the result back. -/ +example {k : α → ℕ} (hk : ComputableInPolyTime k enc encNat) (q : Polynomial ℕ) : + ComputableInPolyTime (fun a => 3 * (k a * 2 ^ q.eval (enc a).length)) enc encNat := by + have hk := hk.tidy + exact .of_tidy (by fun_prop) + +/-- The SBP threshold mixes binary `k`, unary exponents, multiplication and exponentiation. -/ +example {k : α → ℕ} (hk : ComputableInPolyTime k enc encNat) (q : Polynomial ℕ) : + ComputableInPolyTime (fun a => 3 * (k a * 2 ^ q.eval (enc a).length)) enc encNat := by + polytime + +/-- Toda's `sharpTest` carries the original input through two witness arguments. -/ +example {V : (α × List Bool) × List Bool → Bool} + (hV : ComputableInPolyTime V (encPair (encPair enc encBits) encBits) encBool) + (R Z : Polynomial ℕ) : + ComputableInPolyTime (fun x : α × List Bool => + Toda.sharpTest (fun r z => V ((x.1, r), z)) (R.eval (enc x.1).length) + (Z.eval (enc x.1).length) x.2) (encPair enc encBits) encBool := by + polytime + +end ComplexityTests.PolyTimeMixes From e1fc28ba17ad66259e58e99602519167a27ace1e Mon Sep 17 00:00:00 2001 From: Samuel Giuseppe Schlesinger Date: Fri, 23 Oct 2026 18:27:16 -0400 Subject: [PATCH 2/3] style(polytime): place heartbeat justification before the option --- ComplexityTests/PolyTimeMixes.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/ComplexityTests/PolyTimeMixes.lean b/ComplexityTests/PolyTimeMixes.lean index fd4cc3a8c4..065255f60a 100644 --- a/ComplexityTests/PolyTimeMixes.lean +++ b/ComplexityTests/PolyTimeMixes.lean @@ -17,8 +17,8 @@ namespace ComplexityTests.PolyTimeMixes open Cslib Cslib.Complexity Turing.MultiTapeTM variable {α : Type} {enc : α ↪ List Bool} -set_option maxHeartbeats 2000 in -- Check that a bounded failed attempt and the explicit certificate fit a small heartbeat budget. +set_option maxHeartbeats 2000 in /-- The WPP singleton target: bound a failed tidy search before explicitly preparing the plain hypothesis. The default search on this shape can run to its heartbeat limit. -/ example {f : α → ℤ} (hf : ComputableInPolyTime f enc encIntBin) : From c5ef20884610fed938dd3032ad2eef6d5e39a14c Mon Sep 17 00:00:00 2001 From: Samuel Giuseppe Schlesinger Date: Fri, 23 Oct 2026 18:44:59 -0400 Subject: [PATCH 3/3] style(polytime): retain the scoped option justification after the option --- ComplexityTests/PolyTimeMixes.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/ComplexityTests/PolyTimeMixes.lean b/ComplexityTests/PolyTimeMixes.lean index 065255f60a..fd4cc3a8c4 100644 --- a/ComplexityTests/PolyTimeMixes.lean +++ b/ComplexityTests/PolyTimeMixes.lean @@ -17,8 +17,8 @@ namespace ComplexityTests.PolyTimeMixes open Cslib Cslib.Complexity Turing.MultiTapeTM variable {α : Type} {enc : α ↪ List Bool} --- Check that a bounded failed attempt and the explicit certificate fit a small heartbeat budget. set_option maxHeartbeats 2000 in +-- Check that a bounded failed attempt and the explicit certificate fit a small heartbeat budget. /-- The WPP singleton target: bound a failed tidy search before explicitly preparing the plain hypothesis. The default search on this shape can run to its heartbeat limit. -/ example {f : α → ℤ} (hf : ComputableInPolyTime f enc encIntBin) :