From 388751580f88ecd30fce70678cf9188281886d99 Mon Sep 17 00:00:00 2001 From: Samuel Giuseppe Schlesinger Date: Sat, 24 Oct 2026 15:16:27 -0400 Subject: [PATCH] feat(machines): expose plain signed-product and oracle-run certificates --- .../Complexity/PolyTime/Int/Binary.lean | 17 +++++++ .../Probabilistic/Replay/Simulation.lean | 21 ++++++++ ComplexityTests.lean | 1 + ComplexityTests/PlainIntMulOracleRun.lean | 51 +++++++++++++++++++ 4 files changed, 90 insertions(+) create mode 100644 ComplexityTests/PlainIntMulOracleRun.lean diff --git a/Complexity/Computability/Machines/Turing/MultiTape/Complexity/PolyTime/Int/Binary.lean b/Complexity/Computability/Machines/Turing/MultiTape/Complexity/PolyTime/Int/Binary.lean index 653ba37ab3..d3253143bb 100644 --- a/Complexity/Computability/Machines/Turing/MultiTape/Complexity/PolyTime/Int/Binary.lean +++ b/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 diff --git a/Complexity/Computability/Machines/Turing/MultiTape/Probabilistic/Replay/Simulation.lean b/Complexity/Computability/Machines/Turing/MultiTape/Probabilistic/Replay/Simulation.lean index 0359f1fc14..b82e603650 100644 --- a/Complexity/Computability/Machines/Turing/MultiTape/Probabilistic/Replay/Simulation.lean +++ b/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. -/ diff --git a/ComplexityTests.lean b/ComplexityTests.lean index 367a9da0c6..b35ef90d47 100644 --- a/ComplexityTests.lean +++ b/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 diff --git a/ComplexityTests/PlainIntMulOracleRun.lean b/ComplexityTests/PlainIntMulOracleRun.lean new file mode 100644 index 0000000000..5bca7ba045 --- /dev/null +++ b/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