feat(machines): expose plain product and oracle-run certificates

Complexity/Computability/Machines/Turing/MultiTape/Complexity/PolyTime/Int/Binary.lean

@@ -9,6 +9,8 @@ module
 
 public import Complexity.Computability.Machines.Turing.MultiTape.Complexity.PolyTime.Nat.Binary
 public import Complexity.Computability.Machines.Turing.MultiTape.Encodings.IntBinary
+public import Complexity.Computability.Machines.Turing.MultiTape.PolyTime
+import Complexity.Computability.Machines.Turing.MultiTape.Complexity.PolyTime.Plain
 import Mathlib.Algebra.BigOperators.Group.List.Basic
 
 /-!
@@ -29,6 +31,9 @@ the binary length bounds of `Int.size_natAbs_add_le` and `Int.size_natAbs_mul_le
 
 ## Main results
 
+* `Turing.MultiTapeTM.ComputableInPolyTime.intBin_mul'`: multiply two plain-certified binary
+  integers from the same complete input encoding.
+
 * `Int.size_natAbs_add_le`, `Int.size_natAbs_sub_le`, `Int.size_natAbs_mul_le`,
   `Int.size_natAbs_pow_le`, `Int.size_natAbs_sum_le`, `Int.size_natAbs_prod_le`: binary lengths of
   magnitudes of sums, differences, products, powers, list sums and list products.
@@ -373,3 +378,15 @@ theorem intBin_prod_range {α : Type} {enc : α ↪ List Bool}
     List.prod_toFinset (fun i => f (a, i)) (l := List.range (r a)) List.nodup_range
 
 end Turing.MultiTapeTM.ComputableTidilyInPolyTime
+
+namespace Turing.MultiTapeTM.ComputableInPolyTime
+
+/-- Multiply computed binary integers, preserving the complete input encoding. -/
+@[fun_prop]
+theorem intBin_mul' {α : Type} {input : α ↪ List Bool} {left right : α → ℤ}
+    (hleft : ComputableInPolyTime left input encIntBin)
+    (hright : ComputableInPolyTime right input encIntBin) :
+    ComputableInPolyTime (fun a => left a * right a) input encIntBin :=
+  .of_tidy (ComputableTidilyInPolyTime.intBin_mul' hleft.tidy hright.tidy)
+
+end Turing.MultiTapeTM.ComputableInPolyTime

Complexity/Computability/Machines/Turing/MultiTape/Probabilistic/Replay/Simulation.lean

@@ -8,6 +8,8 @@ module
 -- upstream: candidate
 
 public import Complexity.Computability.Machines.Turing.MultiTape.Complexity.BigO
+public import Complexity.Computability.Machines.Turing.MultiTape.ResourceBounds
+import Complexity.Computability.Machines.Turing.MultiTape.Complexity.BigO.Plain
 public import Complexity.Computability.Machines.Turing.MultiTape.Complexity.PolyTime.Configuration
 public import Complexity.Computability.Machines.Turing.MultiTape.Machine.Finite
 public import Complexity.Computability.Machines.Turing.MultiTape.Probabilistic.Replay.Deterministic
@@ -54,6 +56,8 @@ run are polynomial-time (`Turing.MultiTapePTM.computableTidilyInPolyTime_answerS
 * `Turing.MultiTapePTM.interpret_run_pure_false`: a coin-fixed run is an iteration of
   `answerStep`.
 * `Turing.MultiTapePTM.answerStep_inO`: the bounds of an instruction.
+* `Turing.MultiTapePTM.exists_computableInO_run`: the plain charged-time/workspace frontend,
+  retaining the independent bounds and exact clocked run.
 * `Turing.MultiTapePTM.exists_computableTidilyInO_run`: a clocked run against an oracle computed
   within polynomial space is computable within polynomial space.
 * `Turing.MultiTapePTM.computableTidilyInPolyTime_answerStep`: an instruction against a
@@ -421,6 +425,23 @@ theorem exists_computableTidilyInO_run [Finite Operation] {α : Type} {input : 
       cf * (L + c * (L + 1) ^ d + 1 + 1) + (c * (L + 1) ^ d + 1) +
       (cf * (L + c * (L + 1) ^ d + 1 + 1) + 1) ^ do') (by fun_prop)) fun a => le_rfl
 
+
+omit [Fintype Operation] in
+/-- A clocked coin-false run against a plain oracle decider is computable within polynomial
+space. Both oracle and run certificates charge encoded output in workspace. The independent
+time and workspace bounds are exactly those of the tidy simulation; only the realizing-machine
+presentation changes. No polynomial time bound on the oracle is assumed. -/
+theorem exists_computableInO_run [Finite Operation] {α : Type} {input : α ↪ List Bool}
+    {g : List Bool → Bool} {Tg Sg : List Bool → ℕ}
+    (hg : ComputableInO g encBits encBool Tg Sg) (hSg : PolyBounded List.length Sg)
+    (c d : ℕ) :
+    ∃ T S, PolyBounded (fun a => (input a).length) S ∧
+      ComputableInO (fun a => OracleComp.interpret (m := Id) (fun q => [g q.2])
+        (machine.run (pure false) (fun op word => OracleComp.query (op, word))
+          (c * ((input a).length + 1) ^ d) (input a))) input encBits T S := by
+  obtain ⟨T, S, hS, hrun⟩ := machine.exists_computableTidilyInO_run hg.tidy hSg c d
+  exact ⟨T, S, hS, .of_tidy hrun⟩
+
 /-- **An instruction against a polynomial-time oracle is polynomial-time.** Against an oracle
 answering `[g w]` to a request `w`, with `g` polynomial-time, an instruction is polynomial-time in
 the encoded configuration: it either installs `g` of the pending request or is local. -/

ComplexityTests.lean

@@ -345,6 +345,7 @@ import ComplexityTests.Parameterized
 import ComplexityTests.PartialMCSP
 import ComplexityTests.PlainAutomationSupport
 import ComplexityTests.PlainCapturedMap
+import ComplexityTests.PlainIntMulOracleRun
 import ComplexityTests.PlainLawfulBEq
 import ComplexityTests.PlainPurePPT
 import ComplexityTests.PolySpaceFold

ComplexityTests/PlainIntMulOracleRun.lean

@@ -0,0 +1,51 @@
+/-
+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.Machines.Turing.MultiTape.Complexity.PolyTime.Int.Binary
+import Complexity.Computability.Machines.Turing.MultiTape.Probabilistic.Replay.Simulation
+
+/-! Plain signed products and uniform oracle-run resource certificates. -/
+
+open Cslib Turing MultiTapeTM
+
+example {α : Type} {input : α ↪ List Bool} {left right : α → ℤ}
+    (hleft : ComputableInPolyTime left input encIntBin)
+    (hright : ComputableInPolyTime right input encIntBin) :
+    ComputableInPolyTime (fun a => left a * right a) input encIntBin := by
+  fail_if_success (clear hleft; fun_prop)
+  fail_if_success (clear hright; fun_prop)
+  fun_prop
+
+example : ComputableInPolyTime (fun p : ℤ × ℤ => p.1 * p.2)
+    (encPair encIntBin encIntBin) encIntBin :=
+  .intBin_mul' (.fst _ _) (.snd _ _)
+
+example : (-7 : ℤ) * 3 = -21 ∧ (0 : ℤ) * (-3) = 0 := by decide
+
+-- No chosen enumeration of the operation type, polynomial oracle-time bound, or fixed input
+-- dimension is assumed. Time and charged workspace remain independent existential witnesses.
+example {k : ℕ} {Control Operation α : Type} [Finite Control] [Finite Operation]
+    [DecidableEq Operation] (machine : MultiTapePTM k Bool Control Operation)
+    {input : α ↪ List Bool} {g : List Bool → Bool} {Tg Sg : List Bool → ℕ}
+    (hg : ComputableInO g encBits encBool Tg Sg) (hSg : PolyBounded List.length Sg)
+    (c d : ℕ) :
+    ∃ T S, PolyBounded (fun a => (input a).length) S ∧
+      ComputableInO (fun a => OracleComp.interpret (m := Id) (fun q => [g q.2])
+        (machine.run (pure false) (fun op word => OracleComp.query (op, word))
+          (c * ((input a).length + 1) ^ d) (input a))) input encBits T S :=
+  machine.exists_computableInO_run hg hSg c d
+
+-- The zero clock remains admissible; it is not replaced by a positivity premise.
+example {k : ℕ} {Control Operation : Type} [Finite Control] [Finite Operation]
+    [DecidableEq Operation] (machine : MultiTapePTM k Bool Control Operation)
+    {g : List Bool → Bool} {Tg Sg : List Bool → ℕ}
+    (hg : ComputableInO g encBits encBool Tg Sg) (hSg : PolyBounded List.length Sg) :
+    ∃ T S, PolyBounded List.length S ∧
+      ComputableInO (fun word => OracleComp.interpret (m := Id) (fun q => [g q.2])
+        (machine.run (pure false) (fun op word => OracleComp.query (op, word))
+          0 word)) encBits encBits T S := by
+  simpa [encBits] using
+    machine.exists_computableInO_run (input := encBits) hg hSg 0 0