fix(polytime): certify plain verifiers and document bounded mixed search

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

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`.

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

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