diff --git a/CslibFrontier.lean b/CslibFrontier.lean index 3f504cc98c..a4695fbe8e 100644 --- a/CslibFrontier.lean +++ b/CslibFrontier.lean @@ -2274,6 +2274,7 @@ public import CslibFrontier.Computability.Complexity.FineGrained.CountingSparsif public import CslibFrontier.Computability.Complexity.FineGrained.CountingTreeBound public import CslibFrontier.Computability.Complexity.FineGrained.DensityBranchCounting public import CslibFrontier.Computability.Complexity.FineGrained.Diameter +public import CslibFrontier.Computability.Complexity.FineGrained.DisjointInstances public import CslibFrontier.Computability.Complexity.FineGrained.ExhaustiveSearch public import CslibFrontier.Computability.Complexity.FineGrained.Exponents public import CslibFrontier.Computability.Complexity.FineGrained.FunctionRates @@ -2660,6 +2661,7 @@ public import CslibFrontier.Computability.Complexity.Problems.XORSAT.Dense public import CslibFrontier.Computability.Complexity.ProofSystem public import CslibFrontier.Computability.Complexity.Reduction public import CslibFrontier.Computability.Complexity.Reduction.Autoreducibility +public import CslibFrontier.Computability.Complexity.Reduction.BoundedOracle public import CslibFrontier.Computability.Complexity.Reduction.Equiv public import CslibFrontier.Computability.Complexity.Reduction.Guard public import CslibFrontier.Computability.Complexity.Reduction.Isomorphism diff --git a/CslibFrontier/Computability/Complexity/FineGrained/DisjointInstances.lean b/CslibFrontier/Computability/Complexity/FineGrained/DisjointInstances.lean new file mode 100644 index 0000000000..a7cf2ca9a0 --- /dev/null +++ b/CslibFrontier/Computability/Complexity/FineGrained/DisjointInstances.lean @@ -0,0 +1,1921 @@ +/- +Copyright (c) 2026 Samuel Schlesinger. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Samuel Schlesinger +-/ + +module +-- upstream: candidate + +public import CslibFrontier.Computability.Complexity.Classes.SharpP.Completeness +public import CslibFrontier.Computability.Complexity.FineGrained +public import CslibFrontier.Computability.Complexity.FineGrained.SearchStep +public import CslibFrontier.Computability.Complexity.Reduction +public import CslibFrontier.Computability.Complexity.FineGrained.Reduction +public import CslibFrontier.Computability.Machines.Turing.MultiTape.Complexity.PolySpace.Plain +public import CslibFrontier.Computability.Machines.Turing.MultiTape.Encodings.Structure +public import CslibFrontier.Foundations.Data.BinaryBranching +public import CslibFrontier.Logics.Propositional.CNF.ModelCount.Declared +import CslibFrontier.Computability.Complexity.FineGrained.Bounds +import CslibFrontier.Computability.Machines.Turing.MultiTape.Complexity.BigO.Lists +import CslibFrontier.Computability.Machines.Turing.MultiTape.Complexity.PolyTime.Basic +import CslibFrontier.Computability.Machines.Turing.MultiTape.Complexity.PolyTime.Bounds +import CslibFrontier.Computability.Machines.Turing.MultiTape.Complexity.PolyTime.List +import CslibFrontier.Computability.Machines.Turing.MultiTape.Complexity.PolyTime.Nat +import CslibFrontier.Computability.Machines.Turing.MultiTape.Complexity.PolyTime.Nat.Binary +import CslibFrontier.Computability.Machines.Turing.MultiTape.Encodings.List.Size +import CslibFrontier.Computability.Machines.Turing.MultiTape.Encodings.NatPower +import CslibFrontier.Computability.Machines.Turing.MultiTape.Internal.OCombinators +import CslibFrontier.Computability.Machines.Turing.MultiTape.Internal.OCountedIteration +import CslibFrontier.Computability.Machines.Turing.MultiTape.Internal.OLoops +import CslibFrontier.Computability.Machines.Turing.MultiTape.ResourceBounds.Polynomial.Automation + +/-! +# Size-sensitive reductions, summed disjoint-instance lists, and live-workspace accumulation + +Fine-grained and exact exponential reductions fall into three reusable patterns: + +1. **Single-instance size-sensitive reductions (`Cslib.Complexity.SizeSensitiveReduction`):** a + polynomial-time map `toFun : α → β` with an explicit affine parameter bound + `μB (toFun a) ≤ scale * μA a + offset`. Keeping `scale` and `offset` separate preserves the + exact multiplicative rate `scale * δ` when transferring `2 ^ (δ * μB)` bounds, while absorbing + `2 ^ (δ * offset)` into the leading constant (`SizeSensitiveReduction.decidableInExpTime`, + `SizeSensitiveReduction.decidableInSubexpTime`) and bounding workspace in terms of input, + intermediate instance length, and simulated space rather than simulated running time + (`SizeSensitiveReduction.exists_computableInO_comp`). +2. **Materialized disjoint-instance batches (`Cslib.Complexity.InstanceBatch`, + `Cslib.Complexity.CNFInstanceBatch`, `Cslib.Complexity.DisjointBatchReduction`):** a batch of + instances `xs : InstanceBatch β` with summed parameter `xs.sumMeasure μ = (xs.items.map μ).sum` + processed sequentially via `Turing.MultiTapeTM.ComputableInO.foldl`, together with a capped + binary counter `Cslib.Complexity.CappedNatAcc` keeping live accumulator bit-length polynomial + during exact counting sums. +3. **Depth-first stack accumulation (`Cslib.Complexity.StackAccumulationSpec`):** sequential + depth-first generation and accumulation over up to `2 ^ ν(a)` leaf subinstances without + materializing the exponentially long output list, abstracting the disjoint-list / sparsification + search pattern (`Cslib.BinaryBranching`). Time accumulates across all rounds while maximum live + workspace depends only on the live stack, accumulator, binary round counter, and single-leaf + solver space. + +## Main definitions + +* `Cslib.Complexity.SizeSensitiveReduction`: polynomial-time map with + `μB (f a) ≤ scale * μA a + offset`. +* `Cslib.Complexity.InstanceBatch`, `Cslib.Complexity.CNFInstanceBatch`: instance lists with summed + parameter measures and `enc_structure`-backed declared-variable CNF batches. +* `Cslib.Complexity.CappedNatAcc`: `enc_structure`-backed capped binary sum accumulator with + polynomially bounded bit length. +* `Cslib.Complexity.DisjointBatchReduction`: polynomial-time reduction producing an `InstanceBatch` + with linearly bounded `sumMeasure`. +* `Cslib.Complexity.StackSearchState`, `Cslib.Complexity.StackNodeInput`, + `Cslib.Complexity.StackCombineInput`, `Cslib.Complexity.StackAccumulationSpec`: depth-first stack + generation and sequential leaf accumulation with independent time and live-workspace bounds. + +## Main results + +* `Cslib.Complexity.SizeSensitiveReduction.refl`, `.trans`, `.decidableInExpTime`, + `.decidableInSubexpTime`, `.exists_computableInO_comp`, `.computableInPolySpace_comp`. +* `Cslib.Complexity.DisjointBatchReduction.exists_computableInO_foldl`, + `.decidableInExpTime_or`, `.decidableInSubexpTime_or`, `.exists_computableInO_cappedSum`. +* `Cslib.Complexity.StackAccumulationSpec.exists_computableInO_run`, + `.decidableInExpTime_of_stack`, `.decidableInSubexpTime_of_stack`, + `.exists_computableInO_cappedSum_of_stack`, `.run_eq_foldl_leafWords`, + `.run_cappedSum_eq_root`. + +## References + +* [R. Impagliazzo, R. Paturi, F. Zane, *Which problems have strongly exponential + complexity?*][ImpagliazzoPaturiZane2001] +* [M. Cygan, F. V. Fomin, Ł. Kowalik, D. Lokshtanov, D. Marx, M. Pilipczuk, M. Pilipczuk, + S. Saurabh, *Parameterized Algorithms*][CyganEtAl2015] +-/ + +public section + +namespace Cslib.Complexity + +open Cslib.Logic.PL Turing.MultiTapeTM + +/-! ### Single-instance size-sensitive reductions -/ + +/-- A **size-sensitive reduction** from `(α, encA, μA)` to `(β, encB, μB)` +[ImpagliazzoPaturiZane2001]: a polynomial-time map `toFun : α → β` with explicit multiplicative +scale `scale` and additive offset `offset` bounding `μB (toFun a) ≤ scale * μA a + offset`. -/ +structure SizeSensitiveReduction {α β : Type} (encA : α ↪ List Bool) (encB : β ↪ List Bool) + (μA : α → ℕ) (μB : β → ℕ) where + /-- The instance map. -/ + toFun : α → β + /-- Multiplicative parameter factor. -/ + scale : ℕ + /-- Additive parameter offset. -/ + offset : ℕ + /-- Polynomial-time certificate for `toFun`. -/ + computableInPolyTime_toFun : ComputableInPolyTime toFun encA encB + /-- Affine parameter bound on reduced instances. -/ + measure_le : ∀ a, μB (toFun a) ≤ scale * μA a + offset + +namespace SizeSensitiveReduction + +variable {α β γ : Type} {encA : α ↪ List Bool} {encB : β ↪ List Bool} {encC : γ ↪ List Bool} + {μA : α → ℕ} {μB : β → ℕ} {μC : γ → ℕ} + +/-- Identity size-sensitive reduction (`scale = 1`, `offset = 0`). -/ +@[expose] +def refl (encA : α ↪ List Bool) (μA : α → ℕ) : SizeSensitiveReduction encA encA μA μA where + toFun := id + scale := 1 + offset := 0 + computableInPolyTime_toFun := .id' + measure_le a := by simp + +/-- Composition of size-sensitive reductions, multiplying scales and composing offsets. -/ +@[expose] +def trans (r : SizeSensitiveReduction encA encB μA μB) + (s : SizeSensitiveReduction encB encC μB μC) : SizeSensitiveReduction encA encC μA μC where + toFun := s.toFun ∘ r.toFun + scale := s.scale * r.scale + offset := s.scale * r.offset + s.offset + computableInPolyTime_toFun := s.computableInPolyTime_toFun.comp r.computableInPolyTime_toFun + measure_le a := by + have h₁ := s.measure_le (r.toFun a) + have h₂ := r.measure_le a + calc μC (s.toFun (r.toFun a)) + ≤ s.scale * μB (r.toFun a) + s.offset := h₁ + _ ≤ s.scale * (r.scale * μA a + r.offset) + s.offset := + Nat.add_le_add_right (Nat.mul_le_mul_left s.scale h₂) s.offset + _ = (s.scale * r.scale) * μA a + (s.scale * r.offset + s.offset) := by ring + +@[simp] +theorem refl_toFun (encA : α ↪ List Bool) (μA : α → ℕ) : + (refl encA μA).toFun = id := rfl + +@[simp] +theorem trans_toFun (r : SizeSensitiveReduction encA encB μA μB) + (s : SizeSensitiveReduction encB encC μB μC) : + (r.trans s).toFun = s.toFun ∘ r.toFun := rfl + +/-- Encoded output length of a size-sensitive reduction is polynomially bounded in encoded input +length. -/ +theorem polyBounded_output_length (r : SizeSensitiveReduction encA encB μA μB) : + PolyBounded (fun a => (encA a).length) (fun a => (encB (r.toFun a)).length) := + r.computableInPolyTime_toFun.polyBounded_length + +/-- A membership-preserving `SizeSensitiveReduction` induces `PolyTimeReducible`. -/ +theorem toPolyTimeReducible (r : SizeSensitiveReduction encA encB μA μB) + {A : Set α} {B : Set β} (hAB : ∀ a, a ∈ A ↔ r.toFun a ∈ B) : + PolyTimeReducible encA encB A B := + ⟨r.toFun, r.computableInPolyTime_toFun, hAB⟩ + +/-- A count-preserving `SizeSensitiveReduction` induces `ParsimoniousReducible`. -/ +theorem toParsimoniousReducible (r : SizeSensitiveReduction encA encB μA μB) + {f : α → ℕ} {g : β → ℕ} (hfg : ∀ a, f a = g (r.toFun a)) : + ParsimoniousReducible encA encB f g := + ⟨r.toFun, r.computableInPolyTime_toFun, hfg⟩ + +/-- **Exact-scale exponential-time transfer.** A decider for `B` within time +`2 ^ (δ * μB b) * poly(|b|)` transfers along `r` to a decider for `A` within time +`2 ^ (r.scale * δ * μA a) * poly(|a|)`, keeping `r.scale * δ` independent of `r.offset`. -/ +theorem decidableInExpTime (r : SizeSensitiveReduction encA encB μA μB) + {A : Set α} {B : Set β} (hAB : ∀ a, a ∈ A ↔ r.toFun a ∈ B) + {δ : ℝ} (hδ : 0 ≤ δ) (hB : DecidableInExpTime B encB μB δ) : + DecidableInExpTime A encA μA (r.scale * δ) := by + obtain ⟨e, h⟩ := hB + obtain ⟨g, t, k, hg, hgB, ht⟩ := h.exists_computableInO + obtain ⟨d, _, hf⟩ := r.computableInPolyTime_toFun.exists_degree + obtain ⟨l, hl⟩ := hf.inO.length_le_time + set K : ℝ := 1 + k * 2 ^ (δ * r.offset) * (2 * l + 1) ^ e + k + refine DecidableInExpTime.of_computableInO (hg.comp hf.inO) + (fun a => (hAB a).trans (hgB (r.toFun a))) ⌈K⌉₊ (d * (e + 1)) fun a => ?_ + set P : ℝ := ((encA a).length + 1 : ℝ) ^ d + set X : ℝ := 2 ^ ((r.scale * δ) * μA a) + have hP : 1 ≤ P := one_le_pow₀ (le_add_of_nonneg_left (Nat.cast_nonneg _)) + have hX : 1 ≤ X := Real.one_le_rpow (by norm_num) (by positivity) + have hexp : (2 : ℝ) ^ (δ * μB (r.toFun a)) ≤ 2 ^ (δ * r.offset) * X := by + rw [← Real.rpow_add (by norm_num)] + refine Real.rpow_le_rpow_of_exponent_le (by norm_num) ?_ + have hm : (μB (r.toFun a) : ℝ) ≤ r.scale * μA a + r.offset := by + exact_mod_cast r.measure_le a + nlinarith + have hsum : P + (t (r.toFun a) : ℝ) ≤ K * (X * P ^ (e + 1)) := + reduction_add_time_le (C := (2 : ℝ) ^ (δ * r.offset)) hP hX (by positivity) + (by dsimp only [P]; exact_mod_cast hl a) hexp (ht (r.toFun a)) + push_cast + rw [pow_mul] + exact hsum.trans (mul_le_mul_of_nonneg_right (Nat.le_ceil K) (by positivity)) + +/-- **Subexponential-time transfer along a size-sensitive reduction.** -/ +theorem decidableInSubexpTime (r : SizeSensitiveReduction encA encB μA μB) + {A : Set α} {B : Set β} (hAB : ∀ a, a ∈ A ↔ r.toFun a ∈ B) + (hB : DecidableInSubexpTime B encB μB) : DecidableInSubexpTime A encA μA := by + intro ε hε + set δ : ℝ := ε / (r.scale + 1) + refine (r.decidableInExpTime hAB (by positivity : 0 ≤ δ) (hB δ (by positivity))).mono ?_ + dsimp only [δ] + rw [mul_div_assoc', div_le_iff₀ (by positivity)] + nlinarith + +/-- **Independent time and live-workspace composition.** Composing `g` (`ComputableInO g encB encC +Tg Sg`) with `r` bounds workspace by a polynomial in `|encA a|` plus `Sg (r.toFun a)` (never by +`Tg (r.toFun a)`), so polynomial space transfers without bounding space by simulated time. -/ +theorem exists_computableInO_comp (r : SizeSensitiveReduction encA encB μA μB) + {g : β → γ} {Tg Sg : β → ℕ} (hg : ComputableInO g encB encC Tg Sg) + (hSg : PolyBounded (fun b => (encB b).length) Sg) : + ∃ d : ℕ, ∃ S : α → ℕ, + PolyBounded (fun a => (encA a).length) S ∧ + ComputableInO (g ∘ r.toFun) encA encC + (fun a => ((encA a).length + 1) ^ d + Tg (r.toFun a)) S := by + obtain ⟨d, _, hf⟩ := r.computableInPolyTime_toFun.exists_degree + have hcomp := hg.comp hf.inO + have hS : PolyBounded (fun a => (encA a).length) + (fun a => ((encA a).length + 1) ^ d + Sg (r.toFun a)) := by + have hpow : PolyBounded (fun a => (encA a).length) + (fun a => ((encA a).length + 1) ^ d) := by growth_poly + exact hpow.add (hSg.comp r.polyBounded_output_length) + exact ⟨d, _, hS, hcomp⟩ + +/-- Polynomial space transfers along any `SizeSensitiveReduction`. -/ +theorem computableInPolySpace_comp (r : SizeSensitiveReduction encA encB μA μB) + {g : β → γ} (hg : ComputableInPolySpace g encB encC) : + ComputableInPolySpace (g ∘ r.toFun) encA encC := + hg.comp (.of_polyTime r.computableInPolyTime_toFun) + +end SizeSensitiveReduction + +/-! ### Summed parameter lists and capped binary accumulators -/ + +@[expose] section +/-- A batch of subinstances `items : List α`, used to track summed and maximum parameter measures +across disjoint-instance reductions. -/ +@[ext] +structure InstanceBatch (α : Type) where + /-- The ordered list of subinstances. -/ + items : List α + deriving DecidableEq, Repr +end + +namespace InstanceBatch + +variable {α : Type} + +/-- The empty batch of subinstances. -/ +@[expose] def nil : InstanceBatch α := ⟨[]⟩ + +/-- A single-element batch. -/ +@[expose] def singleton (a : α) : InstanceBatch α := ⟨[a]⟩ + +/-- Concatenation of two subinstance batches. -/ +@[expose] def append (xs ys : InstanceBatch α) : InstanceBatch α := ⟨xs.items ++ ys.items⟩ + +/-- Number of subinstances in the batch. -/ +@[expose] def length (xs : InstanceBatch α) : ℕ := xs.items.length + +/-- Summed parameter measure `∑ a ∈ xs.items, μ a`. -/ +@[expose] def sumMeasure (μ : α → ℕ) (xs : InstanceBatch α) : ℕ := + (xs.items.map μ).sum + +/-- Maximum parameter measure `max_{a ∈ xs.items} μ a` (`0` on the empty batch). -/ +@[expose] def maxMeasure (μ : α → ℕ) (xs : InstanceBatch α) : ℕ := + listMax μ xs.items + +@[simp] theorem sumMeasure_nil (μ : α → ℕ) : (nil : InstanceBatch α).sumMeasure μ = 0 := rfl + +@[simp] theorem sumMeasure_singleton (μ : α → ℕ) (a : α) : + (singleton a).sumMeasure μ = μ a := by + simp [singleton, sumMeasure] + +@[simp] theorem sumMeasure_append (μ : α → ℕ) (xs ys : InstanceBatch α) : + (xs.append ys).sumMeasure μ = xs.sumMeasure μ + ys.sumMeasure μ := by + simp [append, sumMeasure, List.map_append, List.sum_append] + +@[simp] theorem length_nil : (nil : InstanceBatch α).length = 0 := rfl + +@[simp] theorem length_singleton (a : α) : (singleton a).length = 1 := rfl + +@[simp] theorem length_append (xs ys : InstanceBatch α) : + (xs.append ys).length = xs.length + ys.length := by + simp [append, length] + +/-- Every subinstance in a batch has measure at most the batch's summed measure. -/ +theorem le_sumMeasure_of_mem (μ : α → ℕ) {xs : InstanceBatch α} {a : α} (ha : a ∈ xs.items) : + μ a ≤ xs.sumMeasure μ := + List.single_le_sum (fun _ _ => Nat.zero_le _) (μ a) (List.mem_map_of_mem ha) + +/-- The maximum subinstance measure is bounded by the summed measure. -/ +theorem maxMeasure_le_sumMeasure (μ : α → ℕ) (xs : InstanceBatch α) : + xs.maxMeasure μ ≤ xs.sumMeasure μ := + listMax_le fun _ ha => le_sumMeasure_of_mem μ ha + +end InstanceBatch + +/-- Encoding of `InstanceBatch α` as the framed list of its items (`encList encA`). -/ +@[expose] +def encInstanceBatch {α : Type} (encA : α ↪ List Bool) : InstanceBatch α ↪ List Bool := + (⟨InstanceBatch.items, fun _ _ h => InstanceBatch.ext h⟩ : InstanceBatch α ↪ List α).trans + (encList encA) + +@[simp] +theorem encInstanceBatch_apply {α : Type} (encA : α ↪ List Bool) (xs : InstanceBatch α) : + encInstanceBatch encA xs = encList encA xs.items := rfl + +@[fun_prop] +theorem computableInPolyTime_instanceBatch_items {α γ : Type} {encIn : γ ↪ List Bool} + {encA : α ↪ List Bool} {f : γ → InstanceBatch α} + (hf : ComputableInPolyTime f encIn (encInstanceBatch encA)) : + ComputableInPolyTime (fun x => (f x).items) encIn (encList encA) := + hf.of_enc_eq fun _ => rfl + +@[fun_prop] +theorem computableInPolyTime_instanceBatch_mk {α γ : Type} {encIn : γ ↪ List Bool} + {encA : α ↪ List Bool} {f : γ → List α} + (hf : ComputableInPolyTime f encIn (encList encA)) : + ComputableInPolyTime (fun x => InstanceBatch.mk (f x)) encIn (encInstanceBatch encA) := + hf.of_enc_eq fun _ => rfl + +@[expose] section +/-- A concrete batch of CNF formulas over a shared number `declaredVars` of declared variables, +as produced by disjoint/counting sparsification. -/ +@[ext] +structure CNFInstanceBatch where + /-- Shared number of declared variables `0, …, declaredVars - 1`. -/ + declaredVars : ℕ + /-- Disjoint subformulas whose satisfying assignments partition or cover the target set. -/ + formulas : List (CNF ℕ) + deriving DecidableEq, Repr +end + +/-- Framed encoding of a `CNFInstanceBatch`: `declaredVars` in unary followed by the framed list of +CNF formulas. -/ +enc_structure encCNFInstanceBatch : CNFInstanceBatch where + declaredVars : encUnary, formulas : (encList encCNF) + +namespace CNFInstanceBatch + +/-- View a `CNFInstanceBatch` as an `InstanceBatch (CNF ℕ)`. -/ +@[expose] def toInstanceBatch (b : CNFInstanceBatch) : InstanceBatch (CNF ℕ) := ⟨b.formulas⟩ + +/-- Sum of declared-variable model counts across all formulas in `b`. -/ +@[expose] noncomputable def totalModelCountOn (b : CNFInstanceBatch) : ℕ := + (b.formulas.map fun ψ => ψ.modelCountOn (Finset.range b.declaredVars)).sum + +/-- Disjunctive satisfiability across the formulas in `b`. -/ +@[expose] def anySatisfiable (b : CNFInstanceBatch) : Prop := + ∃ ψ ∈ b.formulas, ψ ∈ SAT + +/-- Summed distinct-variable measure across the formulas in `b`. -/ +@[expose] def sumNumVars (b : CNFInstanceBatch) : ℕ := + b.toInstanceBatch.sumMeasure CNF.numVars + +end CNFInstanceBatch + +@[expose] section +/-- A capped binary accumulator `(cap, total)` keeping `total ≤ cap` at every step so its encoded +bit-length stays bounded by `O(log₂ cap)` regardless of the number of accumulated terms. -/ +@[ext] +structure CappedNatAcc where + /-- Upper cap on the running sum. -/ + cap : ℕ + /-- Current capped sum (`total ≤ cap` along initialized runs). -/ + total : ℕ + deriving DecidableEq, Repr +end + +/-- Framed binary encoding of `CappedNatAcc`. -/ +enc_structure encCappedNatAcc : CappedNatAcc where + cap : encNat, total : encNat + +namespace CappedNatAcc + +/-- Initialize a capped accumulator at `0` with cap `c`. -/ +@[expose] def init (c : ℕ) : CappedNatAcc := ⟨c, 0⟩ + +/-- Add `v` to `acc`, clamping at `acc.cap`. -/ +@[expose] def add (acc : CappedNatAcc) (v : ℕ) : CappedNatAcc := + ⟨acc.cap, min acc.cap (acc.total + v)⟩ + +@[simp] theorem init_cap (c : ℕ) : (init c).cap = c := rfl +@[simp] theorem init_total (c : ℕ) : (init c).total = 0 := rfl +@[simp] theorem add_cap (acc : CappedNatAcc) (v : ℕ) : (acc.add v).cap = acc.cap := rfl +@[simp] theorem add_total (acc : CappedNatAcc) (v : ℕ) : + (acc.add v).total = min acc.cap (acc.total + v) := rfl + +theorem add_total_le_cap (acc : CappedNatAcc) (v : ℕ) : (acc.add v).total ≤ acc.cap := + Nat.min_le_left _ _ + +/-- Folding `CappedNatAcc.add` over `xs` preserves `cap` and computes `min cap (acc.total + sum)`. +-/ +theorem foldl_add_eq {β : Type} (g : β → ℕ) (xs : List β) (acc : CappedNatAcc) + (hacc : acc.total ≤ acc.cap) : + xs.foldl (fun s b => s.add (g b)) acc = + ⟨acc.cap, min acc.cap (acc.total + (xs.map g).sum)⟩ := by + induction xs generalizing acc with + | nil => + ext + · rfl + · simp [Nat.min_eq_right hacc] + | cons b xs ih => + simp only [List.foldl_cons, List.map_cons, List.sum_cons] + rw [ih (acc.add (g b)) (acc.add_total_le_cap (g b))] + ext + · rfl + · simp only [add_cap, add_total] + omega + +/-- Folding `CappedNatAcc.add` from `init c` yields `min c ((xs.map g).sum)`. -/ +theorem foldl_add_init_total {β : Type} (g : β → ℕ) (xs : List β) (c : ℕ) : + (xs.foldl (fun s b => s.add (g b)) (init c)).total = min c ((xs.map g).sum) := by + rw [foldl_add_eq g xs (init c) (Nat.zero_le c)] + simp + +/-- When the true sum does not exceed `c`, the capped fold computes `(xs.map g).sum` exactly. -/ +theorem foldl_add_init_total_eq_sum {β : Type} (g : β → ℕ) (xs : List β) {c : ℕ} + (hsum : (xs.map g).sum ≤ c) : + (xs.foldl (fun s b => s.add (g b)) (init c)).total = (xs.map g).sum := by + rw [foldl_add_init_total, Nat.min_eq_right hsum] + +/-- Whenever `acc.total ≤ acc.cap` and `acc.cap ≤ 2 ^ k`, the framed binary encoding of `acc` has +length at most `3 * (k + 1) + 2`. -/ +theorem length_encCappedNatAcc_le_of_le_two_pow {acc : CappedNatAcc} {k : ℕ} + (htot : acc.total ≤ acc.cap) (hcap : acc.cap ≤ 2 ^ k) : + (encCappedNatAcc acc).length ≤ 3 * (k + 1) + 2 := by + have hpow : (encNat (2 ^ k)).length = k + 1 := by + rw [encNat_two_pow, List.length_append, List.length_replicate, List.length_singleton] + have hc : (encNat acc.cap).length ≤ k + 1 := hpow ▸ length_encNat_mono hcap + have ht : (encNat acc.total).length ≤ k + 1 := + hpow ▸ length_encNat_mono (htot.trans hcap) + rw [encCappedNatAcc_apply] + simp only [encCappedNatAccFields, length_encPair] + omega + +open ComputableInPolyTime in +@[fun_prop] +theorem computableInPolyTime_init {α : Type} {encA : α ↪ List Bool} {c : α → ℕ} + (hc : ComputableInPolyTime c encA encNat) : + ComputableInPolyTime (fun a => init (c a)) encA encCappedNatAcc := by + unfold init + fun_prop + +open ComputableInPolyTime in +@[fun_prop] +theorem computableInPolyTime_add : + ComputableInPolyTime (fun p : CappedNatAcc × ℕ => p.1.add p.2) + (encPair encCappedNatAcc encNat) encCappedNatAcc := by + have hsum : ComputableInPolyTime (fun p : CappedNatAcc × ℕ => p.1.total + p.2) + (encPair encCappedNatAcc encNat) encNat := + ComputableTidilyInPolyTime.computableInPolyTime <| + ComputableTidilyInPolyTime.binary_add.comp + ((encCappedNatAcc_total_polyTime (fst encCappedNatAcc encNat)).tidy.prod + (snd encCappedNatAcc encNat).tidy) + have hcap : ComputableInPolyTime (fun p : CappedNatAcc × ℕ => p.1.cap) + (encPair encCappedNatAcc encNat) encNat := + encCappedNatAcc_cap_polyTime (fst encCappedNatAcc encNat) + have hle : ComputableInPolyTime (fun p : CappedNatAcc × ℕ => decide (p.1.cap ≤ p.1.total + p.2)) + (encPair encCappedNatAcc encNat) encBool := + ComputableTidilyInPolyTime.computableInPolyTime <| + ComputableTidilyInPolyTime.binary_le.comp (hcap.tidy.prod hsum.tidy) + have hmin : ComputableInPolyTime + (fun p : CappedNatAcc × ℕ => min p.1.cap (p.1.total + p.2)) + (encPair encCappedNatAcc encNat) encNat := + (ComputableInPolyTime.ite' hle hcap hsum).of_enc_eq fun p => by + by_cases h : p.1.cap ≤ p.1.total + p.2 <;> simp [h, Nat.min_def] + exact encCappedNatAcc_mk_polyTime hcap hmin + +end CappedNatAcc + +private theorem cast_listMax_le {β : Type} (f : β → ℕ) (xs : List β) {B : ℝ} (hB0 : 0 ≤ B) + (hf : ∀ b ∈ xs, (f b : ℝ) ≤ B) : (listMax f xs : ℝ) ≤ B := by + induction xs with + | nil => + simp only [listMax, List.map_nil, List.foldr_nil, Nat.cast_zero] + exact hB0 + | cons b xs ih => + simp only [listMax, List.map_cons, List.foldr_cons, Nat.cast_max] + exact max_le (hf b (List.mem_cons_self ..)) + (ih fun b' hb' => hf b' (List.mem_cons_of_mem b hb')) + +/-! ### Materialized disjoint-instance list reductions with summed measure -/ + +/-- A polynomial-time reduction mapping each source instance `a : α` to an `InstanceBatch β` whose +summed target measure `sumMeasure μB` is bounded by `scale * μA a + offset`. -/ +structure DisjointBatchReduction {α β : Type} (encA : α ↪ List Bool) (encB : β ↪ List Bool) + (μA : α → ℕ) (μB : β → ℕ) where + /-- Batch generator. -/ + toBatch : α → InstanceBatch β + /-- Multiplicative parameter factor on the summed target measure. -/ + scale : ℕ + /-- Additive parameter offset on the summed target measure. -/ + offset : ℕ + /-- Polynomial-time certificate for `toBatch`. -/ + computableInPolyTime_toBatch : ComputableInPolyTime toBatch encA (encInstanceBatch encB) + /-- Summed measure bound `∑ b ∈ (toBatch a).items, μB b ≤ scale * μA a + offset`. -/ + sumMeasure_le : ∀ a, (toBatch a).sumMeasure μB ≤ scale * μA a + offset + +namespace DisjointBatchReduction + +variable {α β γ δ : Type} {encA : α ↪ List Bool} {encB : β ↪ List Bool} + {encG : γ ↪ List Bool} {encD : δ ↪ List Bool} {μA : α → ℕ} {μB : β → ℕ} + +/-- Every `SizeSensitiveReduction` embeds as a singleton `DisjointBatchReduction` with the same +`scale` and `offset`. -/ +@[expose] +def ofSizeSensitive (r : SizeSensitiveReduction encA encB μA μB) : + DisjointBatchReduction encA encB μA μB where + toBatch a := InstanceBatch.singleton (r.toFun a) + scale := r.scale + offset := r.offset + computableInPolyTime_toBatch := by + have hcons : ComputableInPolyTime (fun a => [r.toFun a]) encA (encList encB) := + ComputableTidilyInPolyTime.computableInPolyTime <| + ComputableTidilyInPolyTime.cons' r.computableInPolyTime_toFun.tidy (.const []) + exact computableInPolyTime_instanceBatch_mk hcons + sumMeasure_le a := by + rw [InstanceBatch.sumMeasure_singleton] + exact r.measure_le a + +/-- Every subinstance in `r.toBatch a` individually satisfies `μB b ≤ r.scale * μA a + r.offset`. +-/ +theorem measure_mem_le (r : DisjointBatchReduction encA encB μA μB) (a : α) {b : β} + (hb : b ∈ (r.toBatch a).items) : + μB b ≤ r.scale * μA a + r.offset := + (InstanceBatch.le_sumMeasure_of_mem μB hb).trans (r.sumMeasure_le a) + +/-- Encoded length of the materialized batch `r.toBatch a` is polynomially bounded in `|encA a|`. -/ +theorem polyBounded_batch_length (r : DisjointBatchReduction encA encB μA μB) : + PolyBounded (fun a => (encA a).length) + (fun a => (encList encB (r.toBatch a).items).length) := by + simpa only [encInstanceBatch_apply] using r.computableInPolyTime_toBatch.polyBounded_length + +private theorem listMax_exp_le (r : DisjointBatchReduction encA encB μA μB) + {t : β → ℕ} {δ : ℝ} (hδ : 0 ≤ δ) {k e : ℕ} + (ht : ∀ b, (t b : ℝ) ≤ k * (2 ^ (δ * μB b) * ((encB b).length + 1) ^ e) + k) (a : α) : + (listMax t (r.toBatch a).items : ℝ) ≤ + k * 2 ^ (δ * r.offset) * 2 ^ ((r.scale * δ) * μA a) * + (((encList encB (r.toBatch a).items).length : ℝ) + 1) ^ e + k := by + refine cast_listMax_le t (r.toBatch a).items (by positivity) fun b hb => ?_ + have hexp : (2 : ℝ) ^ (δ * μB b) ≤ 2 ^ (δ * r.offset) * 2 ^ ((r.scale * δ) * μA a) := by + rw [← Real.rpow_add (by norm_num)] + refine Real.rpow_le_rpow_of_exponent_le (by norm_num) ?_ + have hm : (μB b : ℝ) ≤ r.scale * μA a + r.offset := by exact_mod_cast r.measure_mem_le a hb + nlinarith + have hblen : ((encB b).length : ℝ) ≤ (encList encB (r.toBatch a).items).length := by + exact_mod_cast length_le_encList_of_mem encB hb + have hpow : (((encB b).length : ℝ) + 1) ^ e ≤ + (((encList encB (r.toBatch a).items).length : ℝ) + 1) ^ e := by gcongr + have hmul := mul_le_mul_of_nonneg_left (mul_le_mul hexp hpow (by positivity) (by positivity)) + (Nat.cast_nonneg k : (0 : ℝ) ≤ k) + linarith [ht b] + +private theorem batch_exp_absorb_le {base itemsLen listLen perItem maxT Cp k e offset : ℕ} + {δ X P : ℝ} (hP0 : 0 ≤ P) (hX1 : 1 ≤ X) + (hitems : itemsLen ≤ listLen) + (hpoly : (base : ℝ) + ((listLen : ℝ) + 1) * ((perItem : ℝ) + ((listLen : ℝ) + 1) ^ e) ≤ + Cp * P) + (hmax : (maxT : ℝ) ≤ k * 2 ^ (δ * offset) * X * ((listLen : ℝ) + 1) ^ e + k) : + ((base + (itemsLen + 1) * (perItem + maxT) : ℕ) : ℝ) ≤ + Cp * (1 + k * 2 ^ (δ * offset) + k) * (X * P) := by + have hl_e : ((listLen : ℝ) + 1) * ((listLen : ℝ) + 1) ^ e ≤ Cp * P := by + have h0 : (0 : ℝ) ≤ (base : ℝ) + ((listLen : ℝ) + 1) * (perItem : ℝ) := by positivity + linarith + have hl_1 : ((listLen : ℝ) + 1) ≤ Cp * P := by + have hge1 : (1 : ℝ) ≤ ((listLen : ℝ) + 1) ^ e := + one_le_pow₀ (le_add_of_nonneg_left (Nat.cast_nonneg _)) + nlinarith + have hit_len : ((itemsLen : ℝ) + 1) ≤ (listLen : ℝ) + 1 := by + exact_mod_cast Nat.add_le_add_right hitems 1 + have hXP : P ≤ X * P := le_mul_of_one_le_left hP0 hX1 + have hbase_le : (base : ℝ) + ((itemsLen : ℝ) + 1) * (perItem : ℝ) ≤ Cp * (X * P) := by + have h₁ : ((itemsLen : ℝ) + 1) * (perItem : ℝ) ≤ + ((listLen : ℝ) + 1) * ((perItem : ℝ) + ((listLen : ℝ) + 1) ^ e) := by + have : (0 : ℝ) ≤ ((listLen : ℝ) + 1) ^ e := by positivity + exact mul_le_mul hit_len (by linarith) (by positivity) (by positivity) + have h₂ : (Cp : ℝ) * P ≤ Cp * (X * P) := + mul_le_mul_of_nonneg_left hXP (Nat.cast_nonneg Cp) + linarith + have hmax_mul : ((itemsLen : ℝ) + 1) * (maxT : ℝ) ≤ + Cp * (k * 2 ^ (δ * offset) + k) * (X * P) := by + have h₁ := mul_le_mul hit_len hmax (by positivity) (by positivity) + have h₂ := mul_le_mul_of_nonneg_left hl_e + (by positivity : (0 : ℝ) ≤ k * 2 ^ (δ * offset) * X) + have h₃ : ((listLen : ℝ) + 1) * k ≤ Cp * k * (X * P) := by + have hk := mul_le_mul_of_nonneg_right hl_1 (Nat.cast_nonneg k) + have hk' : Cp * P * (k : ℝ) ≤ Cp * (X * P) * k := + mul_le_mul_of_nonneg_right (mul_le_mul_of_nonneg_left hXP (Nat.cast_nonneg Cp)) + (Nat.cast_nonneg k) + linarith + linarith + push_cast + linarith + +/-- **Sequential left-fold resource transfer with bounded live workspace.** +Evaluating `g : β → γ` sequentially across `(r.toBatch a).items` and folding answers via a +polynomial-time `combine : δ → γ → δ` whose prefix accumulators stay polynomially bounded in bit +length runs in polynomial live workspace whenever `g` has polynomial workspace `Sg`, and within +accumulated time `O(poly(|a|) + ((r.toBatch a).length + 1) * (poly(|a|) + listMax Tg ...))`. -/ +theorem exists_computableInO_foldl (r : DisjointBatchReduction encA encB μA μB) + {init : α → δ} (hinit : ComputableInPolyTime init encA encD) + {combine : δ → γ → δ} + (hcombine : ComputableInPolyTime (fun p : δ × γ => combine p.1 p.2) + (encPair encD encG) encD) + {g : β → γ} {Tg Sg : β → ℕ} (hg : ComputableInO g encB encG Tg Sg) + (hSg : PolyBounded (fun b => (encB b).length) Sg) + {accBound : α → ℕ} (haccPoly : PolyBounded (fun a => (encA a).length) accBound) + (hacc : ∀ a, ∀ i ≤ (r.toBatch a).items.length, + (encD (((r.toBatch a).items.take i).foldl (fun s b => combine s (g b)) (init a))).length ≤ + accBound a) : + ∃ c e : ℕ, ∃ S : α → ℕ, + PolyBounded (fun a => (encA a).length) S ∧ + ComputableInO + (fun a => ((r.toBatch a).items).foldl (fun s b => combine s (g b)) (init a)) + encA encD + (fun a => c * ((encA a).length + 1) ^ e + + ((r.toBatch a).length + 1) * + (c * ((encA a).length + 1) ^ e + listMax Tg (r.toBatch a).items)) + S := by + have hlist_pt : ComputableInPolyTime (fun a => (r.toBatch a).items) encA (encList encB) := + computableInPolyTime_instanceBatch_items r.computableInPolyTime_toBatch + obtain ⟨dl, _, hlist⟩ := hlist_pt.exists_degree + obtain ⟨di, _, hi⟩ := hinit.exists_degree + obtain ⟨dc, _, hc⟩ := hcombine.exists_degree + obtain ⟨kg, hglen⟩ := hg.length_le + have hstep_raw := hc.inO.comp ((ComputableInO.fst encD encB).prod + (hg.comp (ComputableInO.snd encD encB))) + have hpair_gb (p : δ × β) : + ((encPair encD encG (p.1, g p.2)).length + 1) ^ dc ≤ + (4 * (kg + 1)) ^ dc * ((encPair encD encB p).length + Sg p.2 + 1) ^ dc := by + rw [← mul_pow] + refine Nat.pow_le_pow_left ?_ dc + have hgl := hglen p.2 + simp only [length_encPair] + nlinarith + have hstep : ComputableInO (fun p : δ × β => combine p.1 (g p.2)) + (encPair encD encB) encD + (fun p => ((encPair encD encB p).length + Sg p.2 + 1) ^ dc + + (encPair encD encB p).length + Tg p.2) + (fun p => ((encPair encD encB p).length + Sg p.2 + 1) ^ dc + + (encPair encD encB p).length + Sg p.2) := by + refine hstep_raw.mono ((4 * (kg + 1)) ^ dc + 2) (fun p => ?_) (fun p => ?_) <;> + · simp only [Function.comp_apply] + have hp := hpair_gb p + have h1 : 1 ≤ (4 * (kg + 1)) ^ dc := Nat.one_le_pow _ _ (by positivity) + generalize (4 * (kg + 1)) ^ dc = F at hp h1 ⊢ + generalize ((encPair encD encB p).length + Sg p.2 + 1) ^ dc = Q at hp ⊢ + generalize ((encPair encD encG (p.1, g p.2)).length + 1) ^ dc = R at hp ⊢ + generalize (encPair encD encB p).length = L + nlinarith + obtain ⟨cs, ds, hSg_le⟩ := hSg.exists_le + let listLen (a : α) : ℕ := (encList encB (r.toBatch a).items).length + let sgMax (a : α) : ℕ := cs * (listLen a + 1) ^ ds + have hsg_mem (a : α) {b : β} (hb : b ∈ (r.toBatch a).items) : Sg b ≤ sgMax a := by + have hblen : (encB b).length ≤ listLen a := length_le_encList_of_mem encB hb + exact (hSg_le b).trans (Nat.mul_le_mul_left cs + (Nat.pow_le_pow_left (Nat.add_le_add_right hblen 1) ds)) + let pairBound (a : α) : ℕ := 2 * accBound a + listLen a + 1 + let Q (a : α) : ℕ := (pairBound a + sgMax a + 1) ^ dc + pairBound a + sgMax a + let R (a : α) : ℕ := (pairBound a + sgMax a + 1) ^ dc + pairBound a + + listMax Tg (r.toBatch a).items + have hfold := ComputableInO.foldl (encL := encList encB) hlist.inO hi.inO hstep + (R := R) (Q := Q) (B := accBound) + (fun a i hi => by + have hmem := List.getElem_mem hi + have hblen : (encB (r.toBatch a).items[i]).length ≤ listLen a := + length_le_encList_of_mem encB hmem + have hacc_i := hacc a i hi.le + have hp : (encPair encD encB + (((r.toBatch a).items.take i).foldl (fun s b => combine s (g b)) (init a), + (r.toBatch a).items[i])).length ≤ pairBound a := by + simp only [length_encPair, pairBound] + omega + have hsg := hsg_mem a hmem + have htg := le_listMax (f := Tg) hmem + have hpow := Nat.pow_le_pow_left (Nat.add_le_add_right (Nat.add_le_add hp hsg) 1) dc + dsimp only [R] + omega) + (fun a i hi => by + have hmem := List.getElem_mem hi + have hblen : (encB (r.toBatch a).items[i]).length ≤ listLen a := + length_le_encList_of_mem encB hmem + have hacc_i := hacc a i hi.le + have hp : (encPair encD encB + (((r.toBatch a).items.take i).foldl (fun s b => combine s (g b)) (init a), + (r.toBatch a).items[i])).length ≤ pairBound a := by + simp only [length_encPair, pairBound] + omega + have hsg := hsg_mem a hmem + have hpow := Nat.pow_le_pow_left (Nat.add_le_add_right (Nat.add_le_add hp hsg) 1) dc + dsimp only [Q] + omega) + (fun a i hi => hacc a i hi) + have hlistPoly : PolyBounded (fun a => (encA a).length) listLen := r.polyBounded_batch_length + have hOverhead : PolyBounded (fun a => (encA a).length) + (fun a => ((encA a).length + 1) ^ dl + ((encA a).length + 1) ^ di + + (pairBound a + sgMax a + 1) ^ dc + pairBound a + sgMax a + accBound a + listLen a) := by + dsimp only [pairBound, sgMax] + growth_poly + obtain ⟨c, e, hce⟩ := hOverhead.exists_le + refine ⟨c, e, fun a => c * ((encA a).length + 1) ^ e, by growth_poly, ?_⟩ + refine hfold.mono_le (fun a => ?_) (fun a => ?_) + · have h₁ := hce a + dsimp only [InstanceBatch.length, R, listLen] at h₁ ⊢ + exact Nat.add_le_add (by omega) (Nat.mul_le_mul_left _ (by omega)) + · have h₁ := hce a + dsimp only [Q, listLen] at h₁ ⊢ + omega + +/-- **Exponential-time OR transfer over a summed-measure disjoint-instance batch.** +If `a ∈ A ↔ ∃ b ∈ (r.toBatch a).items, b ∈ B`, then a decider for `B` within time +`2 ^ (δ * μB b) * poly(|b|)` transfers to a decider for `A` within time +`2 ^ (r.scale * δ * μA a) * poly(|a|)`. -/ +theorem decidableInExpTime_or (r : DisjointBatchReduction encA encB μA μB) + {A : Set α} {B : Set β} (hAB : ∀ a, a ∈ A ↔ ∃ b ∈ (r.toBatch a).items, b ∈ B) + {δ : ℝ} (hδ : 0 ≤ δ) (hB : DecidableInExpTime B encB μB δ) : + DecidableInExpTime A encA μA (r.scale * δ) := by + obtain ⟨e, h⟩ := hB + obtain ⟨g, t, k, hg, hgB, ht⟩ := h.exists_computableInO + have hlist_pt : ComputableInPolyTime (fun a => (r.toBatch a).items) encA (encList encB) := + computableInPolyTime_instanceBatch_items r.computableInPolyTime_toBatch + obtain ⟨dl, _, hlist⟩ := hlist_pt.exists_degree + obtain ⟨do', _, hor⟩ := ComputableInPolyTime.bool_or.exists_degree + have hstep_raw := hor.inO.comp ((ComputableInO.fst encBool encB).prod + (hg.comp (ComputableInO.snd encBool encB))) + have h4 (p : Bool × Bool) : (encPair encBool encBool p).length = 4 := by simp + have hstep : ComputableInO (fun p : Bool × β => p.1 || g p.2) (encPair encBool encB) encBool + (fun p => (encPair encBool encB p).length + t p.2) + (fun p => (encPair encBool encB p).length + t p.2) := by + refine hstep_raw.mono (5 ^ do' + 3) (fun p => ?_) (fun p => ?_) <;> + · simp only [Function.comp_apply, h4] + have hF : 1 ≤ (4 + 1) ^ do' := Nat.one_le_pow _ _ (by norm_num) + generalize (4 + 1) ^ do' = F at hF ⊢ + generalize (encPair encBool encB p).length = L + generalize t p.2 = T + nlinarith + let listLen (a : α) : ℕ := (encList encB (r.toBatch a).items).length + let R (a : α) : ℕ := 3 + listLen a + listMax t (r.toBatch a).items + have hfold := ComputableInO.foldl (encL := encList encB) (step := fun s b => s || g b) + hlist.inO (.const false) hstep + (R := R) (Q := R) (B := fun _ => 1) + (fun a i hi => by + have hmem := List.getElem_mem hi + have hblen : (encB (r.toBatch a).items[i]).length ≤ listLen a := + length_le_encList_of_mem encB hmem + have htg := le_listMax (f := t) hmem + dsimp only [R] + simp only [length_encPair, encBool_apply, List.length_singleton] + omega) + (fun a i hi => by + have hmem := List.getElem_mem hi + have hblen : (encB (r.toBatch a).items[i]).length ≤ listLen a := + length_le_encList_of_mem encB hmem + have htg := le_listMax (f := t) hmem + dsimp only [R] + simp only [length_encPair, encBool_apply, List.length_singleton] + omega) + (fun _ _ _ => by simp) + have hfold_eq (xs : List β) (acc : Bool) : + xs.foldl (fun s b => s || g b) acc = (acc || xs.any g) := by + induction xs generalizing acc with + | nil => simp + | cons b xs ih => rw [List.foldl_cons, ih, List.any_cons, Bool.or_assoc] + have hpoly : PolyBounded (fun a => (encA a).length) + (fun a => ((encA a).length + 1) ^ dl + (encA a).length + + (listLen a + 1) * (4 + 2 * listLen a + (listLen a + 1) ^ e)) := by + have hll : PolyBounded (fun a => (encA a).length) listLen := r.polyBounded_batch_length + growth_poly + obtain ⟨Cp, E, hCp⟩ := hpoly.exists_le + set K : ℝ := Cp * (1 + k * 2 ^ (δ * r.offset) + k) + refine DecidableInExpTime.of_computableInO hfold + (fun a => by + rw [hAB a, hfold_eq, Bool.false_or, List.any_eq_true] + exact ⟨fun ⟨b, hb, hB'⟩ => ⟨b, hb, (hgB b).mp hB'⟩, + fun ⟨b, hb, hg'⟩ => ⟨b, hb, (hgB b).mpr hg'⟩⟩) + ⌈K⌉₊ E fun a => ?_ + set P : ℝ := (((encA a).length : ℝ) + 1) ^ E + set X : ℝ := 2 ^ ((r.scale * δ) * μA a) + have hCp_a : ((((encA a).length + 1) ^ dl + (encA a).length : ℕ) : ℝ) + + ((listLen a : ℝ) + 1) * ((4 + 2 * listLen a : ℕ) + ((listLen a : ℝ) + 1) ^ e) ≤ Cp * P := by + dsimp only [P] + exact_mod_cast hCp a + have habs := batch_exp_absorb_le (by positivity) + (Real.one_le_rpow (by norm_num) (by positivity) : 1 ≤ X) + (SizedListEncoding.length_le (encA := encB) (encL := encList encB) (r.toBatch a).items) + hCp_a (r.listMax_exp_le hδ ht a) + have htotal : (((((encA a).length + 1) ^ dl + (encA a).length + + ((r.toBatch a).items.length + 1) * (R a + 1 + listLen a) : ℕ) : ℝ)) ≤ K * (X * P) := by + have heq : R a + 1 + listLen a = + (4 + 2 * listLen a) + listMax t (r.toBatch a).items := by dsimp only [R]; omega + rw [heq] + exact habs + exact htotal.trans (mul_le_mul_of_nonneg_right (Nat.le_ceil K) (by positivity)) + +/-- **Subexponential-time OR transfer over a summed-measure disjoint-instance batch.** -/ +theorem decidableInSubexpTime_or (r : DisjointBatchReduction encA encB μA μB) + {A : Set α} {B : Set β} (hAB : ∀ a, a ∈ A ↔ ∃ b ∈ (r.toBatch a).items, b ∈ B) + (hB : DecidableInSubexpTime B encB μB) : DecidableInSubexpTime A encA μA := by + intro ε hε + set δ : ℝ := ε / (r.scale + 1) + refine (r.decidableInExpTime_or hAB (by positivity : 0 ≤ δ) (hB δ (by positivity))).mono ?_ + dsimp only [δ] + rw [mul_div_assoc', div_le_iff₀ (by positivity)] + nlinarith + +/-- **Capped summed-counting transfer with polynomial live workspace.** +When `countA a = ((r.toBatch a).items.map countB).sum ≤ 2 ^ capBits a` with `capBits` computable +in polynomial time in unary, and `countB` has `ComputableInO countB encB encNat Tg Sg` with +`PolyBounded length Sg` and `Tg b ≤ k * (2 ^ (δ * μB b) * (|b| + 1) ^ e) + k`, `countA` is +computable in time `O(2 ^ (r.scale * δ * μA a) * (|a| + 1) ^ E)` AND polynomial live workspace +(`ComputableInPolySpace countA encA encNat`). -/ +theorem exists_computableInO_cappedSum (r : DisjointBatchReduction encA encB μA μB) + {countA : α → ℕ} {countB : β → ℕ} {capBits : α → ℕ} + (hcap : ComputableInPolyTime capBits encA encUnary) + (hsum : ∀ a, countA a = ((r.toBatch a).items.map countB).sum) + (hle : ∀ a, countA a ≤ 2 ^ capBits a) + {Tg Sg : β → ℕ} (hg : ComputableInO countB encB encNat Tg Sg) + (hSg : PolyBounded (fun b => (encB b).length) Sg) + {δ : ℝ} (hδ : 0 ≤ δ) {k e : ℕ} + (hTg : ∀ b, (Tg b : ℝ) ≤ k * (2 ^ (δ * μB b) * ((encB b).length + 1) ^ e) + k) : + ∃ T S : α → ℕ, ∃ C₀ E : ℕ, + PolyBounded (fun a => (encA a).length) S ∧ + ComputableInO countA encA encNat T S ∧ + ComputableInPolySpace countA encA encNat ∧ + ∀ a, (T a : ℝ) ≤ + C₀ * (2 ^ ((r.scale * δ) * μA a) * (((encA a).length : ℝ) + 1) ^ E) + C₀ := by + have hcapPow : ComputableInPolyTime (fun a => 2 ^ capBits a) encA encNat := + ComputableTidilyInPolyTime.computableInPolyTime <| + ComputableTidilyInPolyTime.binary_two_pow.comp hcap.tidy + have hinit : ComputableInPolyTime (fun a => CappedNatAcc.init (2 ^ capBits a)) + encA encCappedNatAcc := + CappedNatAcc.computableInPolyTime_init hcapPow + have hcapPoly : PolyBounded (fun a => (encA a).length) capBits := by + simpa only [encUnary_apply, List.length_replicate] using hcap.polyBounded_length + have haccPoly : PolyBounded (fun a => (encA a).length) + (fun a => 3 * (capBits a + 1) + 2) := by growth_poly + have haccBound (a : α) (i : ℕ) (_ : i ≤ (r.toBatch a).items.length) : + (encCappedNatAcc (((r.toBatch a).items.take i).foldl + (fun s b => s.add (countB b)) (CappedNatAcc.init (2 ^ capBits a)))).length ≤ + 3 * (capBits a + 1) + 2 := by + rw [CappedNatAcc.foldl_add_eq countB _ _ (Nat.zero_le _)] + exact CappedNatAcc.length_encCappedNatAcc_le_of_le_two_pow (Nat.min_le_left _ _) le_rfl + obtain ⟨cf, ef, S₀, hS₀, hfold⟩ := r.exists_computableInO_foldl hinit + CappedNatAcc.computableInPolyTime_add hg hSg haccPoly haccBound + obtain ⟨dtot, _, htot_pt⟩ := (encCappedNatAcc_total_polyTime + (ComputableInPolyTime.id' (encIn := encCappedNatAcc))).exists_degree + have hout := (htot_pt.inO.comp hfold).of_enc_eq (g := countA) fun a => by + simp only [Function.comp_apply] + rw [CappedNatAcc.foldl_add_init_total_eq_sum countB (r.toBatch a).items + (by rw [← hsum a]; exact hle a), ← hsum a] + set listLen : α → ℕ := fun a => (encList encB (r.toBatch a).items).length + have hpoly : PolyBounded (fun a => (encA a).length) + (fun a => (3 * (capBits a + 1) + 3) ^ dtot + cf * ((encA a).length + 1) ^ ef + + (listLen a + 1) * (cf * ((encA a).length + 1) ^ ef + (listLen a + 1) ^ e)) := by + have hll : PolyBounded (fun a => (encA a).length) listLen := r.polyBounded_batch_length + growth_poly + obtain ⟨Cp, E, hCp⟩ := hpoly.exists_le + have hacc_fin (a : α) : + (encCappedNatAcc (((r.toBatch a).items).foldl + (fun s b => s.add (countB b)) (CappedNatAcc.init (2 ^ capBits a)))).length ≤ + 3 * (capBits a + 1) + 2 := by + have ha := haccBound a (r.toBatch a).items.length le_rfl + rwa [List.take_length] at ha + have hS_upper : PolyBounded (fun a => (encA a).length) + (fun a => S₀ a + (3 * (capBits a + 1) + 3) ^ dtot) := by growth_poly + have hS_full : PolyBounded (fun a => (encA a).length) + (fun a => S₀ a + + ((encCappedNatAcc (((r.toBatch a).items).foldl + (fun s b => s.add (countB b)) (CappedNatAcc.init (2 ^ capBits a)))).length + 1) ^ dtot) := + hS_upper.mono fun a => by + have ha := hacc_fin a + exact Nat.add_le_add_left (Nat.pow_le_pow_left (by omega) dtot) (S₀ a) + have hps : ComputableInPolySpace countA encA encNat := + ComputableInPolySpace.of_inSpace hS_full (ComputableInSpace.of_inO hout) + set K : ℝ := Cp * (1 + k * 2 ^ (δ * r.offset) + k) + refine ⟨_, _, ⌈K⌉₊, E, hS_full, hout, hps, fun a => ?_⟩ + set P : ℝ := (((encA a).length : ℝ) + 1) ^ E + set X : ℝ := 2 ^ ((r.scale * δ) * μA a) + have hCp_nat : ((((3 * (capBits a + 1) + 3) ^ dtot + cf * ((encA a).length + 1) ^ ef : ℕ) : ℝ)) + + ((listLen a : ℝ) + 1) * + ((cf * ((encA a).length + 1) ^ ef : ℕ) + ((listLen a : ℝ) + 1) ^ e) ≤ Cp * P := by + dsimp only [P] + exact_mod_cast hCp a + have habs := batch_exp_absorb_le (by positivity) + (Real.one_le_rpow (by norm_num) (by positivity) : 1 ≤ X) + (SizedListEncoding.length_le (encA := encB) (encL := encList encB) (r.toBatch a).items) + hCp_nat (r.listMax_exp_le hδ hTg a) + have hpost_le : ((encCappedNatAcc (((r.toBatch a).items).foldl + (fun s b => s.add (countB b)) (CappedNatAcc.init (2 ^ capBits a)))).length + 1) ^ dtot ≤ + (3 * (capBits a + 1) + 3) ^ dtot := + Nat.pow_le_pow_left (Nat.add_le_add_right (hacc_fin a) 1) dtot + have hnat_le : cf * ((encA a).length + 1) ^ ef + + ((r.toBatch a).length + 1) * + (cf * ((encA a).length + 1) ^ ef + listMax Tg (r.toBatch a).items) + + ((encCappedNatAcc (((r.toBatch a).items).foldl + (fun s b => s.add (countB b)) (CappedNatAcc.init (2 ^ capBits a)))).length + 1) ^ dtot ≤ + ((3 * (capBits a + 1) + 3) ^ dtot + cf * ((encA a).length + 1) ^ ef) + + ((r.toBatch a).length + 1) * + (cf * ((encA a).length + 1) ^ ef + listMax Tg (r.toBatch a).items) := by omega + have htotal : ((cf * ((encA a).length + 1) ^ ef + + ((r.toBatch a).length + 1) * + (cf * ((encA a).length + 1) ^ ef + listMax Tg (r.toBatch a).items) + + ((encCappedNatAcc (((r.toBatch a).items).foldl + (fun s b => s.add (countB b)) (CappedNatAcc.init (2 ^ capBits a)))).length + 1) ^ dtot : + ℕ) : ℝ) ≤ K * (X * P) := + (Nat.cast_le.mpr hnat_le).trans habs + exact (htotal.trans (mul_le_mul_of_nonneg_right (Nat.le_ceil K) (by positivity))).trans + (le_add_of_nonneg_right (Nat.cast_nonneg _)) + +end DisjointBatchReduction + +/-! ### Depth-first stack accumulation over exponentially many disjoint subinstances -/ + +@[expose] section +/-- State of a depth-first stack accumulation: immutable runtime context `ctx`, live node stack +`stack`, and running answer accumulator `acc`. -/ +@[ext] +structure StackSearchState (κ σ δ : Type) where + /-- Captured runtime context. -/ + ctx : κ + /-- Pending search nodes (top of stack is head). -/ + stack : List σ + /-- Running answer accumulator. -/ + acc : δ + deriving DecidableEq, Repr + +/-- Node-inspection input pairing the runtime context with the current top-of-stack node. -/ +@[ext] +structure StackNodeInput (κ σ : Type) where + /-- Captured runtime context. -/ + ctx : κ + /-- Current node inspected at the top of the stack. -/ + node : σ + deriving DecidableEq, Repr + +/-- Leaf-update input pairing the runtime context, current accumulator, and leaf solver answer. -/ +@[ext] +structure StackCombineInput (κ δ γ : Type) where + /-- Captured runtime context. -/ + ctx : κ + /-- Current running accumulator. -/ + acc : δ + /-- Leaf solver output on the popped leaf subinstance. -/ + leafVal : γ + deriving DecidableEq, Repr +end + +/-- Framed encoding of `StackSearchState κ σ δ`. -/ +@[expose] +def encStackSearchState {κ σ δ : Type} (encK : κ ↪ List Bool) (encS : σ ↪ List Bool) + (encD : δ ↪ List Bool) : StackSearchState κ σ δ ↪ List Bool := + (⟨fun s => (s.ctx, s.stack, s.acc), + fun x y h => by cases x; cases y; simp_all⟩ : StackSearchState κ σ δ ↪ _).trans + (encPair encK (encPair (encList encS) encD)) + +@[simp] +theorem encStackSearchState_apply {κ σ δ : Type} (encK : κ ↪ List Bool) (encS : σ ↪ List Bool) + (encD : δ ↪ List Bool) (s : StackSearchState κ σ δ) : + encStackSearchState encK encS encD s = + encPair encK (encPair (encList encS) encD) (s.ctx, s.stack, s.acc) := rfl + +/-- Framed encoding of `StackNodeInput κ σ`. -/ +@[expose] +def encStackNodeInput {κ σ : Type} (encK : κ ↪ List Bool) (encS : σ ↪ List Bool) : + StackNodeInput κ σ ↪ List Bool := + (⟨fun s => (s.ctx, s.node), + fun x y h => by cases x; cases y; simp_all⟩ : StackNodeInput κ σ ↪ _).trans + (encPair encK encS) + +@[simp] +theorem encStackNodeInput_apply {κ σ : Type} (encK : κ ↪ List Bool) (encS : σ ↪ List Bool) + (s : StackNodeInput κ σ) : + encStackNodeInput encK encS s = encPair encK encS (s.ctx, s.node) := rfl + +/-- Framed encoding of `StackCombineInput κ δ γ`. -/ +@[expose] +def encStackCombineInput {κ δ γ : Type} (encK : κ ↪ List Bool) (encD : δ ↪ List Bool) + (encG : γ ↪ List Bool) : StackCombineInput κ δ γ ↪ List Bool := + (⟨fun s => (s.ctx, s.acc, s.leafVal), + fun x y h => by cases x; cases y; simp_all⟩ : StackCombineInput κ δ γ ↪ _).trans + (encPair encK (encPair encD encG)) + +section StackEncPolyTime + +open ComputableInPolyTime + +variable {α κ σ δ γ : Type} {encIn : α ↪ List Bool} + {encK : κ ↪ List Bool} {encS : σ ↪ List Bool} {encD : δ ↪ List Bool} {encG : γ ↪ List Bool} + +private theorem stackSearchState_parts : + ComputableInPolyTime (fun s : StackSearchState κ σ δ => (s.ctx, s.stack, s.acc)) + (encStackSearchState encK encS encD) (encPair encK (encPair (encList encS) encD)) := + of_eq fun _ => rfl + +@[fun_prop] +theorem computableInPolyTime_stackSearchState_ctx {f : α → StackSearchState κ σ δ} + (hf : ComputableInPolyTime f encIn (encStackSearchState encK encS encD)) : + ComputableInPolyTime (fun a => (f a).ctx) encIn encK := + stackSearchState_parts.fst'.comp hf + +@[fun_prop] +theorem computableInPolyTime_stackSearchState_stack {f : α → StackSearchState κ σ δ} + (hf : ComputableInPolyTime f encIn (encStackSearchState encK encS encD)) : + ComputableInPolyTime (fun a => (f a).stack) encIn (encList encS) := + stackSearchState_parts.snd'.fst'.comp hf + +@[fun_prop] +theorem computableInPolyTime_stackSearchState_acc {f : α → StackSearchState κ σ δ} + (hf : ComputableInPolyTime f encIn (encStackSearchState encK encS encD)) : + ComputableInPolyTime (fun a => (f a).acc) encIn encD := + stackSearchState_parts.snd'.snd'.comp hf + +@[fun_prop] +theorem computableInPolyTime_stackSearchState_mk + {c : α → κ} {stk : α → List σ} {ac : α → δ} + (hc : ComputableInPolyTime c encIn encK) + (hstk : ComputableInPolyTime stk encIn (encList encS)) + (hac : ComputableInPolyTime ac encIn encD) : + ComputableInPolyTime (fun a => StackSearchState.mk (c a) (stk a) (ac a)) + encIn (encStackSearchState encK encS encD) := + (hc.prod (hstk.prod hac)).of_enc_eq fun _ => rfl + +private theorem stackNodeInput_parts : + ComputableInPolyTime (fun s : StackNodeInput κ σ => (s.ctx, s.node)) + (encStackNodeInput encK encS) (encPair encK encS) := + of_eq fun _ => rfl + +@[fun_prop] +theorem computableInPolyTime_stackNodeInput_ctx {f : α → StackNodeInput κ σ} + (hf : ComputableInPolyTime f encIn (encStackNodeInput encK encS)) : + ComputableInPolyTime (fun a => (f a).ctx) encIn encK := + stackNodeInput_parts.fst'.comp hf + +@[fun_prop] +theorem computableInPolyTime_stackNodeInput_node {f : α → StackNodeInput κ σ} + (hf : ComputableInPolyTime f encIn (encStackNodeInput encK encS)) : + ComputableInPolyTime (fun a => (f a).node) encIn encS := + stackNodeInput_parts.snd'.comp hf + +@[fun_prop] +theorem computableInPolyTime_stackNodeInput_mk {c : α → κ} {nd : α → σ} + (hc : ComputableInPolyTime c encIn encK) (hnd : ComputableInPolyTime nd encIn encS) : + ComputableInPolyTime (fun a => StackNodeInput.mk (c a) (nd a)) + encIn (encStackNodeInput encK encS) := + (hc.prod hnd).of_enc_eq fun _ => rfl + +private theorem stackCombineInput_parts : + ComputableInPolyTime (fun s : StackCombineInput κ δ γ => (s.ctx, s.acc, s.leafVal)) + (encStackCombineInput encK encD encG) (encPair encK (encPair encD encG)) := + of_eq fun _ => rfl + +@[fun_prop] +theorem computableInPolyTime_stackCombineInput_ctx {f : α → StackCombineInput κ δ γ} + (hf : ComputableInPolyTime f encIn (encStackCombineInput encK encD encG)) : + ComputableInPolyTime (fun a => (f a).ctx) encIn encK := + stackCombineInput_parts.fst'.comp hf + +@[fun_prop] +theorem computableInPolyTime_stackCombineInput_acc {f : α → StackCombineInput κ δ γ} + (hf : ComputableInPolyTime f encIn (encStackCombineInput encK encD encG)) : + ComputableInPolyTime (fun a => (f a).acc) encIn encD := + stackCombineInput_parts.snd'.fst'.comp hf + +@[fun_prop] +theorem computableInPolyTime_stackCombineInput_leafVal {f : α → StackCombineInput κ δ γ} + (hf : ComputableInPolyTime f encIn (encStackCombineInput encK encD encG)) : + ComputableInPolyTime (fun a => (f a).leafVal) encIn encG := + stackCombineInput_parts.snd'.snd'.comp hf + +@[fun_prop] +theorem computableInPolyTime_stackCombineInput_mk {c : α → κ} {ac : α → δ} {lv : α → γ} + (hc : ComputableInPolyTime c encIn encK) (hac : ComputableInPolyTime ac encIn encD) + (hlv : ComputableInPolyTime lv encIn encG) : + ComputableInPolyTime (fun a => StackCombineInput.mk (c a) (ac a) (lv a)) + encIn (encStackCombineInput encK encD encG) := + (hc.prod (hac.prod hlv)).of_enc_eq fun _ => rfl + +end StackEncPolyTime + +/-- **Depth-first stack accumulation specification.** +Packages a polynomial-time stack generator and accumulator over nodes `σ` producing leaf +subinstances `β` whose solver outputs `γ` are folded into `δ` over `rounds a` binary-counted +iterations without materializing the exponentially long leaf list. -/ +structure StackAccumulationSpec {α κ σ β γ δ : Type} + (encA : α ↪ List Bool) (encK : κ ↪ List Bool) (encS : σ ↪ List Bool) + (encB : β ↪ List Bool) (encG : γ ↪ List Bool) (encD : δ ↪ List Bool) where + /-- Fallback node used by `List.headD` on empty stacks (never inspected on active steps). -/ + defaultNode : σ + /-- Runtime context extracted from input `a`. -/ + initCtx : α → κ + /-- Initial node stack extracted from input `a`. -/ + initStack : α → List σ + /-- Initial accumulator extracted from input `a`. -/ + initAcc : α → δ + /-- Binary round budget for the depth-first traversal. -/ + rounds : α → ℕ + /-- Leaf test on `(ctx, topNode)`. -/ + isLeaf : StackNodeInput κ σ → Bool + /-- Leaf subinstance extracted at a leaf node `(ctx, topNode)`. -/ + leafInstance : StackNodeInput κ σ → β + /-- Children pushed in place of a non-leaf node `(ctx, topNode)`. -/ + expand : StackNodeInput κ σ → List σ + /-- Accumulator update at a leaf given `(ctx, acc, leafVal)`. -/ + combine : StackCombineInput κ δ γ → δ + /-- Polynomial-time certificate for `initCtx`. -/ + computableInPolyTime_initCtx : ComputableInPolyTime initCtx encA encK + /-- Polynomial-time certificate for `initStack`. -/ + computableInPolyTime_initStack : ComputableInPolyTime initStack encA (encList encS) + /-- Polynomial-time certificate for `initAcc`. -/ + computableInPolyTime_initAcc : ComputableInPolyTime initAcc encA encD + /-- Polynomial-time certificate for `rounds` in binary (`encNat`). -/ + computableInPolyTime_rounds : ComputableInPolyTime rounds encA encNat + /-- Polynomial-time certificate for `isLeaf`. -/ + computableInPolyTime_isLeaf : ComputableInPolyTime isLeaf (encStackNodeInput encK encS) encBool + /-- Polynomial-time certificate for `leafInstance`. -/ + computableInPolyTime_leafInstance : + ComputableInPolyTime leafInstance (encStackNodeInput encK encS) encB + /-- Polynomial-time certificate for `expand`. -/ + computableInPolyTime_expand : + ComputableInPolyTime expand (encStackNodeInput encK encS) (encList encS) + /-- Polynomial-time certificate for `combine`. -/ + computableInPolyTime_combine : + ComputableInPolyTime combine (encStackCombineInput encK encD encG) encD + +namespace StackAccumulationSpec + +variable {α κ σ β γ δ : Type} + {encA : α ↪ List Bool} {encK : κ ↪ List Bool} {encS : σ ↪ List Bool} + {encB : β ↪ List Bool} {encG : γ ↪ List Bool} {encD : δ ↪ List Bool} + +/-- Initial `StackSearchState` on input `a`. -/ +@[expose] +def initState (S : StackAccumulationSpec encA encK encS encB encG encD) (a : α) : + StackSearchState κ σ δ := + ⟨S.initCtx a, S.initStack a, S.initAcc a⟩ + +/-- Current `(ctx, head)` node pair on top of `st.stack`. -/ +@[expose] +def topNode (S : StackAccumulationSpec encA encK encS encB encG encD) + (st : StackSearchState κ σ δ) : StackNodeInput κ σ := + ⟨st.ctx, st.stack.headD S.defaultNode⟩ + +/-- Whether `st` is at an active leaf step (`st.stack` is nonempty and its head is a leaf). -/ +@[expose] +def isActiveLeaf (S : StackAccumulationSpec encA encK encS encB encG encD) + (st : StackSearchState κ σ δ) : Bool := + !st.stack.isEmpty && S.isLeaf (S.topNode st) + +/-- One step of depth-first stack accumulation with leaf solver `g : β → γ`. -/ +@[expose] +def step (S : StackAccumulationSpec encA encK encS encB encG encD) (g : β → γ) + (st : StackSearchState κ σ δ) : StackSearchState κ σ δ := + if st.stack.isEmpty then st + else if S.isLeaf (S.topNode st) then + ⟨st.ctx, st.stack.tail, S.combine ⟨st.ctx, st.acc, g (S.leafInstance (S.topNode st))⟩⟩ + else + ⟨st.ctx, S.expand (S.topNode st) ++ st.stack.tail, st.acc⟩ + +/-- Execute `S.rounds a` depth-first steps and return the final accumulator. -/ +@[expose] +def run (S : StackAccumulationSpec encA encK encS encB encG encD) (g : β → γ) (a : α) : δ := + ((S.step g)^[S.rounds a] (S.initState a)).acc + +@[simp] +theorem step_empty (S : StackAccumulationSpec encA encK encS encB encG encD) (g : β → γ) + (c : κ) (ac : δ) : + S.step g ⟨c, [], ac⟩ = ⟨c, [], ac⟩ := rfl + +theorem iterate_step_empty (S : StackAccumulationSpec encA encK encS encB encG encD) (g : β → γ) + (c : κ) (ac : δ) (n : ℕ) : + (S.step g)^[n] ⟨c, [], ac⟩ = ⟨c, [], ac⟩ := + Function.iterate_fixed (S.step_empty g c ac) n + +theorem iterate_step_ctx (S : StackAccumulationSpec encA encK encS encB encG encD) (g : β → γ) + (st : StackSearchState κ σ δ) (n : ℕ) : + ((S.step g)^[n] st).ctx = st.ctx := by + induction n generalizing st with + | zero => rfl + | succ n ih => + rw [Function.iterate_succ_apply, ih] + unfold step + split_ifs <;> rfl + +open ComputableInPolyTime in +/-- **Single-step independent time and space bound** via `exists_computableInO_searchStep`. -/ +theorem exists_computableInO_step (S : StackAccumulationSpec encA encK encS encB encG encD) + {g : β → γ} {Tg Sg : β → ℕ} (hg : ComputableInO g encB encG Tg Sg) : + ∃ d : ℕ, ComputableInO (S.step g) + (encStackSearchState encK encS encD) (encStackSearchState encK encS encD) + (fun st => ((encStackSearchState encK encS encD st).length + 1) ^ d + + if st.stack.isEmpty = false ∧ S.isLeaf (S.topNode st) = true then + Tg (S.leafInstance (S.topNode st)) + + ((encStackSearchState encK encS encD st).length + + (encG (g (S.leafInstance (S.topNode st)))).length + 1) ^ d + else 0) + (fun st => ((encStackSearchState encK encS encD st).length + 1) ^ d + + if st.stack.isEmpty = false ∧ S.isLeaf (S.topNode st) = true then + Sg (S.leafInstance (S.topNode st)) + + ((encStackSearchState encK encS encD st).length + + (encG (g (S.leafInstance (S.topNode st)))).length + 1) ^ d + else 0) := by + let encSt := encStackSearchState encK encS encD + have hstk : ComputableInPolyTime (fun st : StackSearchState κ σ δ => st.stack) + encSt (encList encS) := + computableInPolyTime_stackSearchState_stack .id' + have hctx : ComputableInPolyTime (fun st : StackSearchState κ σ δ => st.ctx) encSt encK := + computableInPolyTime_stackSearchState_ctx .id' + have hacc : ComputableInPolyTime (fun st : StackSearchState κ σ δ => st.acc) encSt encD := + computableInPolyTime_stackSearchState_acc .id' + have hdone : ComputableInPolyTime (fun st : StackSearchState κ σ δ => st.stack.isEmpty) + encSt encBool := + ComputableTidilyInPolyTime.computableInPolyTime <| + (ComputableTidilyInPolyTime.listIsEmpty' encS).comp hstk.tidy + have hhead : ComputableInPolyTime + (fun st : StackSearchState κ σ δ => st.stack.headD S.defaultNode) encSt encS := + ComputableTidilyInPolyTime.computableInPolyTime <| + (ComputableTidilyInPolyTime.headD S.defaultNode).comp hstk.tidy + have htail : ComputableInPolyTime (fun st : StackSearchState κ σ δ => st.stack.tail) + encSt (encList encS) := + ComputableTidilyInPolyTime.computableInPolyTime <| + (ComputableTidilyInPolyTime.listTail encS).comp hstk.tidy + have htopNode : ComputableInPolyTime S.topNode encSt (encStackNodeInput encK encS) := + computableInPolyTime_stackNodeInput_mk hctx hhead + have hleaf : ComputableInPolyTime (fun st => S.isLeaf (S.topNode st)) encSt encBool := + S.computableInPolyTime_isLeaf.comp htopNode + have htop : ComputableInPolyTime (fun st => S.leafInstance (S.topNode st)) encSt encB := + S.computableInPolyTime_leafInstance.comp htopNode + have hexpList : ComputableInPolyTime + (fun st : StackSearchState κ σ δ => S.expand (S.topNode st) ++ st.stack.tail) + encSt (encList encS) := + ComputableTidilyInPolyTime.computableInPolyTime <| + ComputableTidilyInPolyTime.listAppend' + (S.computableInPolyTime_expand.comp htopNode).tidy htail.tidy + have hexpand : ComputableInPolyTime + (fun st : StackSearchState κ σ δ => + StackSearchState.mk st.ctx (S.expand (S.topNode st) ++ st.stack.tail) st.acc) + encSt encSt := + computableInPolyTime_stackSearchState_mk hctx hexpList hacc + have hpSt : ComputableInPolyTime (fun p : StackSearchState κ σ δ × γ => p.1) + (encPair encSt encG) encSt := fst encSt encG + have hpG : ComputableInPolyTime (fun p : StackSearchState κ σ δ × γ => p.2) + (encPair encSt encG) encG := snd encSt encG + have hcombIn : ComputableInPolyTime + (fun p : StackSearchState κ σ δ × γ => StackCombineInput.mk p.1.ctx p.1.acc p.2) + (encPair encSt encG) (encStackCombineInput encK encD encG) := + computableInPolyTime_stackCombineInput_mk + (computableInPolyTime_stackSearchState_ctx hpSt) + (computableInPolyTime_stackSearchState_acc hpSt) hpG + have hrecord : ComputableInPolyTime + (fun p : StackSearchState κ σ δ × γ => + StackSearchState.mk p.1.ctx p.1.stack.tail (S.combine ⟨p.1.ctx, p.1.acc, p.2⟩)) + (encPair encSt encG) encSt := + computableInPolyTime_stackSearchState_mk + (computableInPolyTime_stackSearchState_ctx hpSt) + (htail.comp hpSt) (S.computableInPolyTime_combine.comp hcombIn) + obtain ⟨d, h⟩ := exists_computableInO_searchStep hdone hleaf htop hexpand hrecord hg + exact ⟨d, h.of_enc_eq fun _ => rfl⟩ + +private theorem topNode_encLength_le (S : StackAccumulationSpec encA encK encS encB encG encD) + (st : StackSearchState κ σ δ) : + (encStackNodeInput encK encS (S.topNode st)).length ≤ + 2 * (encStackSearchState encK encS encD st).length + (encS S.defaultNode).length + 2 := by + cases hstk : st.stack with + | nil => + have hctx_le : (encK st.ctx).length ≤ (encStackSearchState encK encS encD st).length := by + simp only [encStackSearchState_apply, length_encPair] + omega + simp only [topNode, hstk, List.headD_nil, encStackNodeInput_apply, length_encPair] + omega + | cons hd tl => + have hhd : (encS hd).length ≤ (encList encS (hd :: tl)).length := + length_le_encList_of_mem encS (List.mem_cons_self ..) + have hpair : 2 * (encK st.ctx).length + (encList encS (hd :: tl)).length ≤ + (encStackSearchState encK encS encD st).length := by + simp only [encStackSearchState_apply, hstk, length_encPair] + omega + simp only [topNode, hstk, List.headD_cons, encStackNodeInput_apply, length_encPair] + omega + +private theorem stack_exp_absorb {A_ov B_ov R_cnt leafMax Cp : ℝ} {K₀ K₁ M scale offset k e : ℕ} + {δ : ℝ} (hδ : 0 ≤ δ) {μ L leafLen : ℕ} {E : ℕ} + (hCp0 : 0 ≤ Cp) (hB0 : 0 ≤ B_ov) (hleaf0 : 0 ≤ leafMax) + (hA : A_ov ≤ Cp * ((L : ℝ) + 1) ^ E) + (hB : B_ov ≤ Cp * ((L : ℝ) + 1) ^ E) + (hR : R_cnt ≤ (K₀ * 2 ^ K₁ + 1) * 2 ^ ((1 / M : ℝ) * μ)) + (hleaf : leafMax ≤ + k * ((2 : ℝ) ^ (δ * ((scale * μ + offset : ℕ) : ℝ)) * ((leafLen : ℝ) + 1) ^ e) + (k + 1)) + (hll : ((leafLen : ℝ) + 1) ^ e ≤ Cp * ((L : ℝ) + 1) ^ E) : + A_ov + R_cnt * (B_ov + leafMax) ≤ + (Cp + (K₀ * 2 ^ K₁ + 1) * (Cp + k * 2 ^ (δ * offset) * Cp + (k + 1))) * + (2 ^ ((1 / M + scale * δ) * μ) * ((L : ℝ) + 1) ^ E) := by + set P : ℝ := ((L : ℝ) + 1) ^ E + set X : ℝ := 2 ^ ((1 / M : ℝ) * μ) + set Y : ℝ := 2 ^ ((scale * δ) * μ) + have hP1 : 1 ≤ P := one_le_pow₀ (le_add_of_nonneg_left (Nat.cast_nonneg _)) + have hX1 : 1 ≤ X := Real.one_le_rpow (by norm_num) (by positivity) + have hY1 : 1 ≤ Y := Real.one_le_rpow (by norm_num) (by positivity) + have hleaf' : leafMax ≤ k * 2 ^ (δ * offset) * Cp * Y * P + (k + 1) := by + have hexp : (2 : ℝ) ^ (δ * ((scale * μ + offset : ℕ) : ℝ)) = 2 ^ (δ * offset) * Y := by + dsimp only [Y] + rw [← Real.rpow_add (by norm_num)] + congr 1 + push_cast + ring + have hmul := mul_le_mul_of_nonneg_left hll + (show (0 : ℝ) ≤ k * ((2 : ℝ) ^ (δ * offset) * Y) from + mul_nonneg (Nat.cast_nonneg k) (mul_nonneg (Real.rpow_nonneg (by norm_num) _) + (by positivity))) + rw [hexp] at hleaf + have heq1 : (k : ℝ) * ((2 : ℝ) ^ (δ * offset) * Y * ((leafLen : ℝ) + 1) ^ e) = + k * ((2 : ℝ) ^ (δ * offset) * Y) * ((leafLen : ℝ) + 1) ^ e := by ring + have heq2 : (k : ℝ) * ((2 : ℝ) ^ (δ * offset) * Y) * (Cp * P) = + k * (2 : ℝ) ^ (δ * offset) * Cp * Y * P := by ring + linarith + have hXY : (2 : ℝ) ^ ((1 / M + scale * δ) * μ) = X * Y := by + dsimp only [X, Y] + rw [← Real.rpow_add (by norm_num)] + congr 1 + ring + have hYP1 : 1 ≤ Y * P := one_le_mul_of_one_le_of_one_le hY1 hP1 + have hround_sum : B_ov + leafMax ≤ (Cp + k * 2 ^ (δ * offset) * Cp + (k + 1)) * (Y * P) := by + have h₁ : Cp * P ≤ Cp * (Y * P) := + mul_le_mul_of_nonneg_left (le_mul_of_one_le_left (by positivity) hY1) hCp0 + have h₂ : ((k : ℝ) + 1) ≤ (k + 1) * (Y * P) := + le_mul_of_one_le_right (by positivity) hYP1 + linarith + have hprod : R_cnt * (B_ov + leafMax) ≤ + (K₀ * 2 ^ K₁ + 1) * (Cp + k * 2 ^ (δ * offset) * Cp + (k + 1)) * (X * Y * P) := by + have h₁ := mul_le_mul hR hround_sum (by linarith) (by positivity) + linarith + have hA_xyp : Cp * P ≤ Cp * (X * Y * P) := by + have hXY1 : 1 ≤ X * Y := one_le_mul_of_one_le_of_one_le hX1 hY1 + exact mul_le_mul_of_nonneg_left (le_mul_of_one_le_left (by positivity) hXY1) hCp0 + rw [hXY] + linarith + +private theorem rounds_succ_exp_le {rounds ν μA : α → ℕ} {K₀ K₁ M : ℕ} + (hrounds : ∀ a, rounds a ≤ K₀ * 2 ^ (ν a)) (hν : ∀ a, ν a ≤ μA a / M + K₁) (a : α) : + ((rounds a + 1 : ℕ) : ℝ) ≤ (K₀ * 2 ^ K₁ + 1) * 2 ^ ((1 / M : ℝ) * μA a) := by + have h₁ : rounds a ≤ K₀ * 2 ^ K₁ * 2 ^ (μA a / M) := by + calc rounds a ≤ K₀ * 2 ^ (ν a) := hrounds a + _ ≤ K₀ * 2 ^ (μA a / M + K₁) := + Nat.mul_le_mul_left K₀ (Nat.pow_le_pow_right two_pos (hν a)) + _ = K₀ * 2 ^ K₁ * 2 ^ (μA a / M) := by rw [pow_add]; ring + have h₂ : ((2 ^ (μA a / M) : ℕ) : ℝ) ≤ 2 ^ ((1 / M : ℝ) * μA a) := by + rw [Nat.cast_pow, Nat.cast_ofNat, ← Real.rpow_natCast, one_div_mul_eq_div] + exact Real.rpow_le_rpow_of_exponent_le (by norm_num) Nat.cast_div_le + have h₃ : (1 : ℝ) ≤ 2 ^ ((1 / M : ℝ) * μA a) := Real.one_le_rpow (by norm_num) (by positivity) + have h₄ : (rounds a : ℝ) ≤ (K₀ * 2 ^ K₁ : ℝ) * ((2 ^ (μA a / M) : ℕ) : ℝ) := by + exact_mod_cast h₁ + have h₅ := mul_le_mul_of_nonneg_left h₂ (by positivity : (0 : ℝ) ≤ K₀ * 2 ^ K₁) + rw [Nat.cast_succ] + linarith + +private theorem step_cost_le (S : StackAccumulationSpec encA encK encS encB encG encD) + {g : β → γ} {F : β → ℕ} {st : StackSearchState κ σ δ} {stateBound ansBound fBound d : ℕ} + (hst : (encStackSearchState encK encS encD st).length ≤ stateBound) + (hans : st.stack.isEmpty = false ∧ S.isLeaf (S.topNode st) = true → + (encG (g (S.leafInstance (S.topNode st)))).length ≤ ansBound) + (hf : st.stack.isEmpty = false ∧ S.isLeaf (S.topNode st) = true → + F (S.leafInstance (S.topNode st)) ≤ fBound) : + ((encStackSearchState encK encS encD st).length + 1) ^ d + + (if st.stack.isEmpty = false ∧ S.isLeaf (S.topNode st) = true then + F (S.leafInstance (S.topNode st)) + + ((encStackSearchState encK encS encD st).length + + (encG (g (S.leafInstance (S.topNode st)))).length + 1) ^ d + else 0) ≤ + ((stateBound + 1) ^ d + (stateBound + ansBound + 1) ^ d) + fBound := by + have hp1 := Nat.pow_le_pow_left (Nat.add_le_add_right hst 1) d + split_ifs with hact + · have ha_len := hans hact + have hf_le := hf hact + have hp2 := Nat.pow_le_pow_left (Nat.add_le_add_right (Nat.add_le_add hst ha_len) 1) d + omega + · omega + +private theorem exists_leafMax_exp_le (S : StackAccumulationSpec encA encK encS encB encG encD) + {g : β → γ} {Tg : β → ℕ} {μA : α → ℕ} {μB : β → ℕ} {stateBound : α → ℕ} + (hstatePoly : PolyBounded (fun a => (encA a).length) stateBound) + {scale offset k e : ℕ} {δ : ℝ} (hδ : 0 ≤ δ) + (hstate : ∀ a, ∀ i ≤ S.rounds a, + (encStackSearchState encK encS encD ((S.step g)^[i] (S.initState a))).length ≤ stateBound a) + (hmeas : ∀ a, ∀ i ≤ S.rounds a, + let st := (S.step g)^[i] (S.initState a) + st.stack.isEmpty = false ∧ S.isLeaf (S.topNode st) = true → + μB (S.leafInstance (S.topNode st)) ≤ scale * μA a + offset) + (hTg : ∀ b, (Tg b : ℝ) ≤ k * (2 ^ (δ * μB b) * ((encB b).length + 1) ^ e) + k) : + ∃ leafLen leafMax : α → ℕ, + PolyBounded (fun a => (encA a).length) leafLen ∧ + (∀ a, (leafMax a : ℝ) ≤ + k * ((2 : ℝ) ^ (δ * ((scale * μA a + offset : ℕ) : ℝ)) * ((leafLen a : ℝ) + 1) ^ e) + + (k + 1)) ∧ + (∀ a, ∀ i ≤ S.rounds a, + let st := (S.step g)^[i] (S.initState a) + st.stack.isEmpty = false ∧ S.isLeaf (S.topNode st) = true → + Tg (S.leafInstance (S.topNode st)) ≤ leafMax a) := by + obtain ⟨cl, dl, hleaf_len⟩ := S.computableInPolyTime_leafInstance.polyBounded_length.exists_le + let leafLen (a : α) : ℕ := + cl * (2 * stateBound a + (encS S.defaultNode).length + 3) ^ dl + let leafMax (a : α) : ℕ := + ⌈(k : ℝ) * (2 ^ (δ * ((scale * μA a + offset : ℕ) : ℝ)) * ((leafLen a : ℝ) + 1) ^ e) + k⌉₊ + have hleafPoly : PolyBounded (fun a => (encA a).length) leafLen := by + dsimp only [leafLen] + growth_poly + have hceil (a : α) : (leafMax a : ℝ) ≤ + k * ((2 : ℝ) ^ (δ * ((scale * μA a + offset : ℕ) : ℝ)) * ((leafLen a : ℝ) + 1) ^ e) + + (k + 1) := by + set X : ℝ := + (k : ℝ) * (2 ^ (δ * ((scale * μA a + offset : ℕ) : ℝ)) * ((leafLen a : ℝ) + 1) ^ e) + k + have hlt := Nat.ceil_lt_add_one (by positivity : 0 ≤ X) + dsimp only [leafMax, X] at hlt ⊢ + linarith + refine ⟨leafLen, leafMax, hleafPoly, hceil, fun a i hi hact => ?_⟩ + set st := (S.step g)^[i] (S.initState a) + set b := S.leafInstance (S.topNode st) + have hm : μB b ≤ scale * μA a + offset := hmeas a i hi hact + have hst : (encStackSearchState encK encS encD st).length ≤ stateBound a := hstate a i hi + have htn : (encStackNodeInput encK encS (S.topNode st)).length ≤ + 2 * stateBound a + (encS S.defaultNode).length + 2 := + (S.topNode_encLength_le st).trans (by omega) + have hblen : (encB b).length ≤ leafLen a := + (hleaf_len (S.topNode st)).trans (Nat.mul_le_mul_left cl (Nat.pow_le_pow_left (by omega) dl)) + have hexp : (2 : ℝ) ^ (δ * μB b) ≤ 2 ^ (δ * ((scale * μA a + offset : ℕ) : ℝ)) := + Real.rpow_le_rpow_of_exponent_le (by norm_num) + (mul_le_mul_of_nonneg_left (by exact_mod_cast hm) hδ) + have hpow : (((encB b).length : ℝ) + 1) ^ e ≤ ((leafLen a : ℝ) + 1) ^ e := by gcongr + refine Nat.cast_le.mp ((hTg b).trans ((?_ : _ ≤ _).trans (Nat.le_ceil _))) + gcongr + +/-- **Accumulated-time and polynomial-live-workspace transfer for `S.run g`.** +When the live encoded search state and leaf answers are polynomially bounded along `S.rounds a` +and `g` has polynomial workspace `Sg`, `S.run g` runs in **polynomial live workspace** +(`ComputableInPolySpace (S.run g) encA encD`) and within accumulated time +`O(poly(|a|) + (S.rounds a + 1) * (poly(|a|) + leafMax a))`, without materializing the leaf list. -/ +theorem exists_computableInO_run (S : StackAccumulationSpec encA encK encS encB encG encD) + {g : β → γ} {Tg Sg : β → ℕ} (hg : ComputableInO g encB encG Tg Sg) + (hSg : PolyBounded (fun b => (encB b).length) Sg) + {stateBound ansBound leafMax : α → ℕ} + (hstatePoly : PolyBounded (fun a => (encA a).length) stateBound) + (hansPoly : PolyBounded (fun a => (encA a).length) ansBound) + (hstate : ∀ a, ∀ i ≤ S.rounds a, + (encStackSearchState encK encS encD ((S.step g)^[i] (S.initState a))).length ≤ stateBound a) + (hans : ∀ a, ∀ i ≤ S.rounds a, + let st := (S.step g)^[i] (S.initState a) + st.stack.isEmpty = false ∧ S.isLeaf (S.topNode st) = true → + (encG (g (S.leafInstance (S.topNode st)))).length ≤ ansBound a) + (htime : ∀ a, ∀ i ≤ S.rounds a, + let st := (S.step g)^[i] (S.initState a) + st.stack.isEmpty = false ∧ S.isLeaf (S.topNode st) = true → + Tg (S.leafInstance (S.topNode st)) ≤ leafMax a) : + ∃ c e : ℕ, ∃ Space : α → ℕ, + PolyBounded (fun a => (encA a).length) Space ∧ + ComputableInO (S.run g) encA encD + (fun a => c * ((encA a).length + 1) ^ e + + (S.rounds a + 1) * (c * ((encA a).length + 1) ^ e + leafMax a)) + Space ∧ + ComputableInPolySpace (S.run g) encA encD := by + classical + rcases isEmpty_or_nonempty α with hα | hα + · have hz : ComputableInO (S.run g) encA encD + (fun a => 0 * ((encA a).length + 1) ^ 0 + + (S.rounds a + 1) * (0 * ((encA a).length + 1) ^ 0 + leafMax a)) + (fun _ => 0) := + ((ComputableInO.const (encIn := encA) (encMid := encBits) ([] : List Bool)).mono_le + (fun a => hα.elim a) (fun a => hα.elim a)).of_enc_eq fun a => hα.elim a + exact ⟨0, 0, fun _ => 0, .const 0, hz, + ComputableInPolySpace.of_inSpace (.const 0) (ComputableInSpace.of_inO hz)⟩ + obtain ⟨a₀⟩ := hα + let _ : Inhabited (StackSearchState κ σ δ) := ⟨S.initState a₀⟩ + let encSt := encStackSearchState encK encS encD + obtain ⟨d, hstep⟩ := S.exists_computableInO_step hg + have hinit_pt : ComputableInPolyTime S.initState encA encSt := + computableInPolyTime_stackSearchState_mk S.computableInPolyTime_initCtx + S.computableInPolyTime_initStack S.computableInPolyTime_initAcc + have hacc_pt : ComputableInPolyTime (fun st : StackSearchState κ σ δ => st.acc) encSt encD := + computableInPolyTime_stackSearchState_acc .id' + obtain ⟨dn, _, hn⟩ := S.computableInPolyTime_rounds.exists_degree + obtain ⟨di, _, hi⟩ := hinit_pt.exists_degree + obtain ⟨da, _, ha⟩ := hacc_pt.exists_degree + obtain ⟨cl, dl, hleaf_len⟩ := S.computableInPolyTime_leafInstance.polyBounded_length.exists_le + obtain ⟨cs, ds, hSg_le⟩ := hSg.exists_le + let leafLen (a : α) : ℕ := + cl * (2 * stateBound a + (encS S.defaultNode).length + 3) ^ dl + let sgBound (a : α) : ℕ := cs * (leafLen a + 1) ^ ds + let stepPoly (a : α) : ℕ := + (stateBound a + 1) ^ d + (stateBound a + ansBound a + 1) ^ d + have hround_t (a : α) (i : ℕ) (hi : i ≤ S.rounds a) : + ((encSt ((S.step g)^[i] (S.initState a))).length + 1) ^ d + + (if ((S.step g)^[i] (S.initState a)).stack.isEmpty = false ∧ + S.isLeaf (S.topNode ((S.step g)^[i] (S.initState a))) = true then + Tg (S.leafInstance (S.topNode ((S.step g)^[i] (S.initState a)))) + + ((encSt ((S.step g)^[i] (S.initState a))).length + + (encG (g (S.leafInstance (S.topNode ((S.step g)^[i] (S.initState a)))))).length + + 1) ^ d + else 0) ≤ stepPoly a + leafMax a := + S.step_cost_le (hstate a i hi) (hans a i hi) (htime a i hi) + have hround_s (a : α) (i : ℕ) (hi : i ≤ S.rounds a) : + ((encSt ((S.step g)^[i] (S.initState a))).length + 1) ^ d + + (if ((S.step g)^[i] (S.initState a)).stack.isEmpty = false ∧ + S.isLeaf (S.topNode ((S.step g)^[i] (S.initState a))) = true then + Sg (S.leafInstance (S.topNode ((S.step g)^[i] (S.initState a)))) + + ((encSt ((S.step g)^[i] (S.initState a))).length + + (encG (g (S.leafInstance (S.topNode ((S.step g)^[i] (S.initState a)))))).length + + 1) ^ d + else 0) ≤ stepPoly a + sgBound a := + S.step_cost_le (hstate a i hi) (hans a i hi) fun _ => by + have hst : (encStackSearchState encK encS encD + ((S.step g)^[i] (S.initState a))).length ≤ stateBound a := hstate a i hi + have htn : + (encStackNodeInput encK encS (S.topNode ((S.step g)^[i] (S.initState a)))).length ≤ + 2 * stateBound a + (encS S.defaultNode).length + 2 := + (S.topNode_encLength_le _).trans (by omega) + have hblen : (encB (S.leafInstance (S.topNode ((S.step g)^[i] (S.initState a))))).length ≤ + leafLen a := + (hleaf_len _).trans (Nat.mul_le_mul_left cl (Nat.pow_le_pow_left (by omega) dl)) + exact (hSg_le _).trans + (Nat.mul_le_mul_left cs (Nat.pow_le_pow_left (Nat.add_le_add_right hblen 1) ds)) + have hloop := ComputableInO.iterate hn.inO hi.inO hstep hround_t hround_s hstate + have hwhole := (ha.inO.comp hloop).of_enc_eq (g := S.run g) fun _ => rfl + let clockLen (a : α) : ℕ := (encNat (S.rounds a)).length + have hclkPoly : PolyBounded (fun a => (encA a).length) clockLen := + S.computableInPolyTime_rounds.polyBounded_length + have hOverhead : PolyBounded (fun a => (encA a).length) + (fun a => ((encA a).length + 1) ^ dn + ((encA a).length + 1) ^ di + + (stateBound a + 1) ^ da + stepPoly a + sgBound a + stateBound a + + (clockLen a + 1) ^ 2 + clockLen a) := by + dsimp only [stepPoly, sgBound, leafLen] + growth_poly + obtain ⟨c, e, hce⟩ := hOverhead.exists_le + let Space (a : α) : ℕ := c * ((encA a).length + 1) ^ e + have hSpacePoly : PolyBounded (fun a => (encA a).length) Space := by + dsimp only [Space] + growth_poly + have hcert : ComputableInO (S.run g) encA encD + (fun a => c * ((encA a).length + 1) ^ e + + (S.rounds a + 1) * (c * ((encA a).length + 1) ^ e + leafMax a)) Space := by + refine hwhole.mono_le (fun a => ?_) (fun a => ?_) + · have hfin : ((encSt ((S.step g)^[S.rounds a] (S.initState a))).length + 1) ^ da ≤ + (stateBound a + 1) ^ da := + Nat.pow_le_pow_left (Nat.add_le_add_right (hstate a (S.rounds a) le_rfl) 1) da + have h₁ := hce a + dsimp only [clockLen] at h₁ + rw [Nat.add_right_comm] + exact Nat.add_le_add (by omega) (Nat.mul_le_mul_left _ (by omega)) + · have hfin : ((encSt ((S.step g)^[S.rounds a] (S.initState a))).length + 1) ^ da ≤ + (stateBound a + 1) ^ da := + Nat.pow_le_pow_left (Nat.add_le_add_right (hstate a (S.rounds a) le_rfl) 1) da + have h₁ := hce a + dsimp only [Space, clockLen] at h₁ ⊢ + omega + exact ⟨c, e, Space, hSpacePoly, hcert, + ComputableInPolySpace.of_inSpace hSpacePoly (ComputableInSpace.of_inO hcert)⟩ + +/-- **Exponential-time decision transfer along a Boolean-OR `StackAccumulationSpec`.** +When `S.rounds a ≤ K₀ * 2 ^ (ν a)` with `ν a ≤ μA a / M + K₁` and every active leaf subinstance +satisfies `μB b ≤ scale * μA a + offset`, a decider for `B` within time +`2 ^ (δ * μB b) * poly(|b|)` transfers to `A` within time +`2 ^ ((1 / M + scale * δ) * μA a) * poly(|a|)`. -/ +theorem decidableInExpTime_of_stack + (S : StackAccumulationSpec encA encK encS encB encBool encBool) + {A : Set α} {B : Set β} {μA : α → ℕ} {μB : β → ℕ} + {ν : α → ℕ} {K₀ M K₁ scale offset : ℕ} + (hrounds : ∀ a, S.rounds a ≤ K₀ * 2 ^ (ν a)) + (hν : ∀ a, ν a ≤ μA a / M + K₁) + {stateBound : α → ℕ} (hstatePoly : PolyBounded (fun a => (encA a).length) stateBound) + (hAB : ∀ (g : β → Bool), (∀ b, b ∈ B ↔ g b = true) → + ∀ a, (a ∈ A ↔ S.run g a = true) ∧ + (∀ i ≤ S.rounds a, + (encStackSearchState encK encS encBool ((S.step g)^[i] (S.initState a))).length ≤ + stateBound a) ∧ + (∀ i ≤ S.rounds a, + let st := (S.step g)^[i] (S.initState a) + st.stack.isEmpty = false ∧ S.isLeaf (S.topNode st) = true → + μB (S.leafInstance (S.topNode st)) ≤ scale * μA a + offset)) + {δ : ℝ} (hδ : 0 ≤ δ) (hB : DecidableInExpTime B encB μB δ) : + DecidableInExpTime A encA μA (1 / M + scale * δ) := by + obtain ⟨e, h⟩ := hB + obtain ⟨g, t, k, hg, hgB, ht⟩ := h.exists_computableInO + have hspec := hAB g hgB + obtain ⟨leafLen, leafMax, hleafPoly, hleafMax_le, htime⟩ := + S.exists_leafMax_exp_le hstatePoly hδ (fun a => (hspec a).2.1) (fun a => (hspec a).2.2) ht + rcases isEmpty_or_nonempty α with hα | hα + · exact DecidableInExpTime.of_computableInO (.const false) + (fun a => hα.elim a) 1 0 (fun a => hα.elim a) + obtain ⟨a₀⟩ := hα + let _ : Inhabited (StackSearchState κ σ Bool) := ⟨S.initState a₀⟩ + let encSt := encStackSearchState encK encS encBool + obtain ⟨d, hstep⟩ := S.exists_computableInO_step hg + have hinit_pt : ComputableInPolyTime S.initState encA encSt := + computableInPolyTime_stackSearchState_mk S.computableInPolyTime_initCtx + S.computableInPolyTime_initStack S.computableInPolyTime_initAcc + have hacc_pt : ComputableInPolyTime (fun st : StackSearchState κ σ Bool => st.acc) + encSt encBool := + computableInPolyTime_stackSearchState_acc .id' + obtain ⟨dn, _, hn⟩ := S.computableInPolyTime_rounds.exists_degree + obtain ⟨di, _, hi⟩ := hinit_pt.exists_degree + obtain ⟨da, _, ha⟩ := hacc_pt.exists_degree + let stepPoly (a : α) : ℕ := (stateBound a + 1) ^ d + (stateBound a + 1 + 1) ^ d + have hround (a : α) (i : ℕ) (hi : i ≤ S.rounds a) : + ((encSt ((S.step g)^[i] (S.initState a))).length + 1) ^ d + + (if ((S.step g)^[i] (S.initState a)).stack.isEmpty = false ∧ + S.isLeaf (S.topNode ((S.step g)^[i] (S.initState a))) = true then + t (S.leafInstance (S.topNode ((S.step g)^[i] (S.initState a)))) + + ((encSt ((S.step g)^[i] (S.initState a))).length + + (encBool (g (S.leafInstance (S.topNode ((S.step g)^[i] (S.initState a)))))).length + + 1) ^ d + else 0) ≤ stepPoly a + leafMax a := + S.step_cost_le ((hspec a).2.1 i hi) (fun _ => by simp) (htime a i hi) + have hloop := ha.inO.comp (ComputableInO.iterate hn.inO hi.inO hstep hround hround + fun a i hi => (hspec a).2.1 i hi) + let clockLen (a : α) : ℕ := (encNat (S.rounds a)).length + have hclkPoly : PolyBounded (fun a => (encA a).length) clockLen := + S.computableInPolyTime_rounds.polyBounded_length + have hpoly : PolyBounded (fun a => (encA a).length) + (fun a => ((encA a).length + 1) ^ dn + ((encA a).length + 1) ^ di + + (stateBound a + 1) ^ da + (stepPoly a + stateBound a + (clockLen a + 1) ^ 2) + + (leafLen a + 1) ^ e) := by + dsimp only [stepPoly] + growth_poly + obtain ⟨Cp, E, hCp⟩ := hpoly.exists_le + set K : ℝ := Cp + (K₀ * 2 ^ K₁ + 1) * (Cp + k * 2 ^ (δ * offset) * Cp + (k + 1)) + refine DecidableInExpTime.of_computableInO hloop (fun a => (hspec a).1) ⌈K⌉₊ E fun a => ?_ + have hCp_a := hCp a + have hfin_da : ((encSt ((S.step g)^[S.rounds a] (S.initState a))).length + 1) ^ da ≤ + (stateBound a + 1) ^ da := + Nat.pow_le_pow_left (Nat.add_le_add_right ((hspec a).2.1 (S.rounds a) le_rfl) 1) da + have hA : ((((encA a).length + 1) ^ dn + ((encA a).length + 1) ^ di + + ((encSt ((S.step g)^[S.rounds a] (S.initState a))).length + 1) ^ da : ℕ) : ℝ) ≤ + Cp * (((encA a).length : ℝ) + 1) ^ E := by + exact_mod_cast (show ((encA a).length + 1) ^ dn + ((encA a).length + 1) ^ di + + ((encSt ((S.step g)^[S.rounds a] (S.initState a))).length + 1) ^ da ≤ + Cp * ((encA a).length + 1) ^ E by omega) + have hB_ov : ((stepPoly a + stateBound a + (clockLen a + 1) ^ 2 : ℕ) : ℝ) ≤ + Cp * (((encA a).length : ℝ) + 1) ^ E := by + exact_mod_cast (show stepPoly a + stateBound a + (clockLen a + 1) ^ 2 ≤ + Cp * ((encA a).length + 1) ^ E by omega) + have hll : ((leafLen a : ℝ) + 1) ^ e ≤ Cp * (((encA a).length : ℝ) + 1) ^ E := by + exact_mod_cast (show (leafLen a + 1) ^ e ≤ Cp * ((encA a).length + 1) ^ E by omega) + have habs := stack_exp_absorb hδ (Nat.cast_nonneg Cp) (Nat.cast_nonneg _) + (Nat.cast_nonneg _) hA hB_ov (rounds_succ_exp_le hrounds hν a) (hleafMax_le a) hll + have htot : (((((encA a).length + 1) ^ dn + ((encA a).length + 1) ^ di + + (S.rounds a + 1) * (stepPoly a + leafMax a + stateBound a + (clockLen a + 1) ^ 2) + + ((encSt ((S.step g)^[S.rounds a] (S.initState a))).length + 1) ^ da : ℕ) : ℝ)) ≤ + K * (2 ^ ((1 / M + scale * δ) * μA a) * (((encA a).length : ℝ) + 1) ^ E) := by + dsimp only [K, clockLen] at habs ⊢ + push_cast at habs ⊢ + linarith + exact htot.trans (mul_le_mul_of_nonneg_right (Nat.le_ceil K) (by positivity)) + +/-- **Subexponential-time decision transfer along a family of Boolean-OR stack reductions.** -/ +theorem decidableInSubexpTime_of_stack + {A : Set α} {B : Set β} {μA : α → ℕ} {μB : β → ℕ} {scale : ℕ} + (hfamily : ∀ M > 0, ∃ (S : StackAccumulationSpec encA encK encS encB encBool encBool) + (ν stateBound : α → ℕ) (K₀ K₁ offset : ℕ), + (∀ a, S.rounds a ≤ K₀ * 2 ^ (ν a)) ∧ + (∀ a, ν a ≤ μA a / M + K₁) ∧ + PolyBounded (fun a => (encA a).length) stateBound ∧ + ∀ (g : β → Bool), (∀ b, b ∈ B ↔ g b = true) → + ∀ a, (a ∈ A ↔ S.run g a = true) ∧ + (∀ i ≤ S.rounds a, + (encStackSearchState encK encS encBool ((S.step g)^[i] (S.initState a))).length ≤ + stateBound a) ∧ + (∀ i ≤ S.rounds a, + let st := (S.step g)^[i] (S.initState a) + st.stack.isEmpty = false ∧ S.isLeaf (S.topNode st) = true → + μB (S.leafInstance (S.topNode st)) ≤ scale * μA a + offset)) + (hB : DecidableInSubexpTime B encB μB) : + DecidableInSubexpTime A encA μA := by + intro ε hε + obtain ⟨M, hM⟩ := exists_nat_gt (2 / ε) + have hMpos : (0 : ℝ) < M := lt_trans (by positivity) hM + obtain ⟨S, ν, stateBound, K₀, K₁, offset, hrounds, hν, hstatePoly, hAB⟩ := + hfamily M (Nat.cast_pos.mp hMpos) + set δ : ℝ := ε / (2 * (scale + 1)) + have hδ : 0 < δ := by positivity + refine (S.decidableInExpTime_of_stack hrounds hν hstatePoly hAB hδ.le (hB δ hδ)).mono ?_ + have hMε : 1 / (M : ℝ) < ε / 2 := by + rw [div_lt_iff₀ hMpos] + rw [div_lt_iff₀ hε] at hM + linarith + have hcδ : (scale : ℝ) * δ ≤ ε / 2 := by + dsimp only [δ] + rw [mul_div_assoc', div_le_iff₀ (by positivity)] + nlinarith + linarith + +/-- **Capped summed-counting transfer along `StackAccumulationSpec` with polynomial live +workspace.** +Given a `CappedNatAcc`-accumulating stack specification `S` whose final `(S.run countB a).total` +equals `countA a`, with `S.rounds a ≤ K₀ * 2 ^ (ν a)`, `ν a ≤ μA a / M + K₁`, leaf measure +`μB b ≤ scale * μA a + offset`, and leaf counter `ComputableInO countB encB encNat Tg Sg` with +`PolyBounded length Sg`, `countA` is computable in **polynomial live workspace** AND time +`O(2 ^ ((1 / M + scale * δ) * μA a) * (|a| + 1) ^ E)`. -/ +theorem exists_computableInO_cappedSum_of_stack + (S : StackAccumulationSpec encA encK encS encB encNat encCappedNatAcc) + {countA : α → ℕ} {countB : β → ℕ} {μA : α → ℕ} {μB : β → ℕ} + {ν stateBound ansBound : α → ℕ} {K₀ M K₁ scale offset : ℕ} + (hrounds : ∀ a, S.rounds a ≤ K₀ * 2 ^ (ν a)) + (hν : ∀ a, ν a ≤ μA a / M + K₁) + (hstatePoly : PolyBounded (fun a => (encA a).length) stateBound) + (hansPoly : PolyBounded (fun a => (encA a).length) ansBound) + (hcorrect : ∀ a, (S.run countB a).total = countA a) + (hstate : ∀ a, ∀ i ≤ S.rounds a, + (encStackSearchState encK encS encCappedNatAcc ((S.step countB)^[i] (S.initState a))).length ≤ + stateBound a) + (hans : ∀ a, ∀ i ≤ S.rounds a, + let st := (S.step countB)^[i] (S.initState a) + st.stack.isEmpty = false ∧ S.isLeaf (S.topNode st) = true → + (encNat (countB (S.leafInstance (S.topNode st)))).length ≤ ansBound a) + (hmeas : ∀ a, ∀ i ≤ S.rounds a, + let st := (S.step countB)^[i] (S.initState a) + st.stack.isEmpty = false ∧ S.isLeaf (S.topNode st) = true → + μB (S.leafInstance (S.topNode st)) ≤ scale * μA a + offset) + {Tg Sg : β → ℕ} (hg : ComputableInO countB encB encNat Tg Sg) + (hSg : PolyBounded (fun b => (encB b).length) Sg) + {δ : ℝ} (hδ : 0 ≤ δ) {k e : ℕ} + (hTg : ∀ b, (Tg b : ℝ) ≤ k * (2 ^ (δ * μB b) * ((encB b).length + 1) ^ e) + k) : + ∃ T Space : α → ℕ, ∃ C₀ E : ℕ, + PolyBounded (fun a => (encA a).length) Space ∧ + ComputableInO countA encA encNat T Space ∧ + ComputableInPolySpace countA encA encNat ∧ + ∀ a, (T a : ℝ) ≤ + C₀ * (2 ^ ((1 / M + scale * δ) * μA a) * (((encA a).length : ℝ) + 1) ^ E) + C₀ := by + obtain ⟨leafLen, leafMax, hleafPoly, hleafMax_le, htime⟩ := + S.exists_leafMax_exp_le hstatePoly hδ hstate hmeas hTg + obtain ⟨cs, es, Space₀, hSpace₀, hrun, _⟩ := + S.exists_computableInO_run hg hSg hstatePoly hansPoly hstate hans htime + obtain ⟨dtot, _, htot_pt⟩ := (encCappedNatAcc_total_polyTime + (ComputableInPolyTime.id' (encIn := encCappedNatAcc))).exists_degree + have hout := (htot_pt.inO.comp hrun).of_enc_eq (encC := encNat) (g := countA) fun a => by + simp only [Function.comp_apply, hcorrect a] + have hrun_len (a : α) : (encCappedNatAcc (S.run countB a)).length ≤ stateBound a := by + have hst := hstate a (S.rounds a) le_rfl + have hle : (encCappedNatAcc ((S.step countB)^[S.rounds a] (S.initState a)).acc).length ≤ + (encStackSearchState encK encS encCappedNatAcc + ((S.step countB)^[S.rounds a] (S.initState a))).length := by + simp only [encStackSearchState_apply, length_encPair] + omega + exact hle.trans hst + let Space (a : α) : ℕ := Space₀ a + ((encCappedNatAcc (S.run countB a)).length + 1) ^ dtot + have hSpaceUpper : PolyBounded (fun a => (encA a).length) + (fun a => Space₀ a + (stateBound a + 1) ^ dtot) := by growth_poly + have hSpacePoly : PolyBounded (fun a => (encA a).length) Space := + hSpaceUpper.mono fun a => + Nat.add_le_add_left (Nat.pow_le_pow_left (Nat.add_le_add_right (hrun_len a) 1) dtot) _ + have hps : ComputableInPolySpace countA encA encNat := + ComputableInPolySpace.of_inSpace hSpacePoly (ComputableInSpace.of_inO hout) + have hpoly : PolyBounded (fun a => (encA a).length) + (fun a => cs * ((encA a).length + 1) ^ es + (stateBound a + 1) ^ dtot + + (leafLen a + 1) ^ e) := by growth_poly + obtain ⟨Cp, E, hCp⟩ := hpoly.exists_le + set K : ℝ := Cp + (K₀ * 2 ^ K₁ + 1) * (Cp + k * 2 ^ (δ * offset) * Cp + (k + 1)) + refine ⟨_, Space, ⌈K⌉₊, E, hSpacePoly, hout, hps, fun a => ?_⟩ + have hCp_a := hCp a + have hpost_dtot := Nat.pow_le_pow_left (Nat.add_le_add_right (hrun_len a) 1) dtot + have hA : ((cs * ((encA a).length + 1) ^ es + + ((encCappedNatAcc (S.run countB a)).length + 1) ^ dtot : ℕ) : ℝ) ≤ + Cp * (((encA a).length : ℝ) + 1) ^ E := by + exact_mod_cast (show cs * ((encA a).length + 1) ^ es + + ((encCappedNatAcc (S.run countB a)).length + 1) ^ dtot ≤ + Cp * ((encA a).length + 1) ^ E by omega) + have hB_ov : ((cs * ((encA a).length + 1) ^ es : ℕ) : ℝ) ≤ + Cp * (((encA a).length : ℝ) + 1) ^ E := by + exact_mod_cast (show cs * ((encA a).length + 1) ^ es ≤ + Cp * ((encA a).length + 1) ^ E by omega) + have hll : ((leafLen a : ℝ) + 1) ^ e ≤ Cp * (((encA a).length : ℝ) + 1) ^ E := by + exact_mod_cast (show (leafLen a + 1) ^ e ≤ Cp * ((encA a).length + 1) ^ E by omega) + have habs := stack_exp_absorb hδ (Nat.cast_nonneg Cp) (Nat.cast_nonneg _) (Nat.cast_nonneg _) + hA hB_ov (rounds_succ_exp_le hrounds hν a) (hleafMax_le a) hll + have htot : ((cs * ((encA a).length + 1) ^ es + + (S.rounds a + 1) * (cs * ((encA a).length + 1) ^ es + leafMax a) + + ((encCappedNatAcc (S.run countB a)).length + 1) ^ dtot : ℕ) : ℝ) ≤ + K * (2 ^ ((1 / M + scale * δ) * μA a) * (((encA a).length : ℝ) + 1) ^ E) := by + dsimp only [K] at habs ⊢ + push_cast at habs ⊢ + linarith + exact (htot.trans (mul_le_mul_of_nonneg_right (Nat.le_ceil K) (by positivity))).trans + (le_add_of_nonneg_right (Nat.cast_nonneg _)) + +/-! ### Bridge to `BinaryBranching` and disjoint sparsification -/ + +/-- When `S` expands inner states to the two children `[T.next s false, T.next s true]` of a +`BinaryBranching` rule `T`, iterating `S.step g` agrees at every step with `T.searchStep`. -/ +theorem iterate_step_eq_binaryBranching + (S : StackAccumulationSpec encA encK encS encB encG encD) + (g : β → γ) (c : κ) (T : BinaryBranching σ) + (hleaf : ∀ s, S.isLeaf ⟨c, s⟩ = true ↔ T.IsLeaf s) + (hexp : ∀ s, ¬ T.IsLeaf s → S.expand ⟨c, s⟩ = [T.next s false, T.next s true]) + (n : ℕ) (stk : List σ) (ac : δ) : + (S.step g)^[n] ⟨c, stk, ac⟩ = + let p := (T.searchStep (fun d s => S.combine ⟨c, d, g (S.leafInstance ⟨c, s⟩)⟩))^[n] (stk, ac) + ⟨c, p.1, p.2⟩ := by + induction n generalizing stk ac with + | zero => rfl + | succ n ih => + have hone : S.step g ⟨c, stk, ac⟩ = + let p := T.searchStep (fun d s => S.combine ⟨c, d, g (S.leafInstance ⟨c, s⟩)⟩) (stk, ac) + ⟨c, p.1, p.2⟩ := by + cases stk with + | nil => rfl + | cons s rest => + by_cases hs : T.IsLeaf s + · have hs' : S.isLeaf ⟨c, s⟩ = true := (hleaf s).mpr hs + simp [step, topNode, BinaryBranching.searchStep, hs, hs'] + · have hs' : S.isLeaf ⟨c, s⟩ = false := by + simpa using fun h => hs ((hleaf s).mp h) + simp [step, topNode, BinaryBranching.searchStep, hs, hs', hexp s hs] + rw [Function.iterate_succ_apply, Function.iterate_succ_apply, hone] + exact ih _ _ + +/-- **Leaf-word fold theorem (`BinaryBranching` / sparsification bridge).** +For a terminating `BinaryBranching` rule `T` on input `a` starting at `[root]` with leaf depth at +most `h` and `2 * L.length ≤ S.rounds a` on the duplicate-free list `L` of leaf words, `S.run g a` +equals the fold over all leaf states `L.map (T.walk root)` while every intermediate stack has +length at most `h + 1` and holds only tree nodes of depth at most `h`. -/ +theorem run_eq_foldl_leafWords + (S : StackAccumulationSpec encA encK encS encB encG encD) + (g : β → γ) (a : α) (T : BinaryBranching σ) (hT : T.Terminating) + {root : σ} (hinit : S.initStack a = [root]) + (hleaf : ∀ s, S.isLeaf ⟨S.initCtx a, s⟩ = true ↔ T.IsLeaf s) + (hexp : ∀ s, ¬ T.IsLeaf s → + S.expand ⟨S.initCtx a, s⟩ = [T.next s false, T.next s true]) + {h : ℕ} (hh : ∀ w, T.IsLeafWord root w → w.length ≤ h) + (hrounds : ∀ (L : List (List Bool)), L.Nodup → (∀ w, w ∈ L ↔ T.IsLeafWord root w) → + 2 * L.length ≤ S.rounds a + 1) : + ∃ L : List (List Bool), L.Nodup ∧ (∀ w, w ∈ L ↔ T.IsLeafWord root w) ∧ + S.run g a = (L.map (T.walk root)).foldl + (fun d s => S.combine ⟨S.initCtx a, d, g (S.leafInstance ⟨S.initCtx a, s⟩)⟩) + (S.initAcc a) ∧ + ∀ i ≤ S.rounds a, + let st := (S.step g)^[i] (S.initState a) + st.stack.length ≤ h + 1 ∧ + (∀ t ∈ st.stack, ∃ w, T.IsNodeWord root w ∧ w.length ≤ h ∧ T.walk root w = t) ∧ + ∃ L', L' <+: L ∧ st.acc = (L'.map (T.walk root)).foldl + (fun d s => S.combine ⟨S.initCtx a, d, g (S.leafInstance ⟨S.initCtx a, s⟩)⟩) + (S.initAcc a) := by + let f := fun (d : δ) (s : σ) => + S.combine ⟨S.initCtx a, d, g (S.leafInstance ⟨S.initCtx a, s⟩)⟩ + obtain ⟨L, hnd, hL, N, hN, hsearch⟩ := T.exists_iterate_searchStep hT f root hh + have hNR : N ≤ S.rounds a := by + have := hrounds L hnd hL + omega + obtain ⟨hfin, hpref⟩ := hsearch [] (S.initAcc a) + have hfix : ∀ k, (T.searchStep f)^[k] ([], (L.map (T.walk root)).foldl f (S.initAcc a)) = + ([], (L.map (T.walk root)).foldl f (S.initAcc a)) := + Function.iterate_fixed (by rfl) + have hafter (m : ℕ) (hm : N ≤ m) : + (T.searchStep f)^[m] ([root], S.initAcc a) = + ([], (L.map (T.walk root)).foldl f (S.initAcc a)) := by + rw [show m = (m - N) + N by omega, Function.iterate_add_apply, hfin, hfix] + refine ⟨L, hnd, hL, ?_, fun i hi => ?_⟩ + · simp only [run, initState, hinit] + rw [S.iterate_step_eq_binaryBranching g (S.initCtx a) T hleaf hexp (S.rounds a) [root] + (S.initAcc a), hafter (S.rounds a) hNR] + · dsimp only [initState] + rw [hinit, S.iterate_step_eq_binaryBranching g (S.initCtx a) T hleaf hexp i [root] + (S.initAcc a)] + by_cases hiN : i ≤ N + · obtain ⟨stk, L', hL', heq, hlen, hmem⟩ := hpref i hiN + rw [List.append_nil] at heq + rw [heq] + exact ⟨hlen, hmem, L', hL', rfl⟩ + · rw [hafter i (by omega)] + exact ⟨Nat.zero_le _, fun _ ht => by simp at ht, L, List.prefix_rfl, rfl⟩ + +/-- **Exact additive root recovery for capped disjoint-branching sums.** +When `val : σ → ℕ` is additive across the children of every inner state (`val t = val (next false) + +val (next true)`), `g` computes `val` on leaves, and `val root ≤ cap`, a `CappedNatAcc` stack +traversal recovers `val root` exactly. -/ +theorem run_cappedSum_eq_root + (S : StackAccumulationSpec encA encK encS encB encNat encCappedNatAcc) + (g : β → ℕ) (a : α) (T : BinaryBranching σ) (hT : T.Terminating) + {root : σ} {cap : ℕ} + (hinit : S.initStack a = [root]) + (hinitAcc : S.initAcc a = CappedNatAcc.init cap) + (hcombine : ∀ d v, S.combine ⟨S.initCtx a, d, v⟩ = d.add v) + (hleaf : ∀ s, S.isLeaf ⟨S.initCtx a, s⟩ = true ↔ T.IsLeaf s) + (hexp : ∀ s, ¬ T.IsLeaf s → + S.expand ⟨S.initCtx a, s⟩ = [T.next s false, T.next s true]) + {h : ℕ} (hh : ∀ w, T.IsLeafWord root w → w.length ≤ h) + (hrounds : ∀ (L : List (List Bool)), L.Nodup → (∀ w, w ∈ L ↔ T.IsLeafWord root w) → + 2 * L.length ≤ S.rounds a + 1) + {val : σ → ℕ} + (hadd : ∀ t, ¬ T.IsLeaf t → val t = val (T.next t false) + val (T.next t true)) + (hval_leaf : ∀ t, T.IsLeaf t → g (S.leafInstance ⟨S.initCtx a, t⟩) = val t) + (hcap : val root ≤ cap) : + (S.run g a).total = val root := by + classical + obtain ⟨L, hnd, hL, hrun_eq, _⟩ := + S.run_eq_foldl_leafWords g a T hT hinit hleaf hexp hh hrounds + have hcomb_eq : (fun (d : CappedNatAcc) (s : σ) => + S.combine ⟨S.initCtx a, d, g (S.leafInstance ⟨S.initCtx a, s⟩)⟩) = + fun d s => d.add (g (S.leafInstance ⟨S.initCtx a, s⟩)) := by + funext d s + exact hcombine d _ + rw [hrun_eq, hinitAcc, hcomb_eq, CappedNatAcc.foldl_add_init_total] + have hsum_eq : ((L.map (T.walk root)).map (fun s => g (S.leafInstance ⟨S.initCtx a, s⟩))).sum = + val root := by + rw [List.map_map] + have hcongr : List.map ((fun s => g (S.leafInstance ⟨S.initCtx a, s⟩)) ∘ T.walk root) L = + L.map (fun w => val (T.walk root w)) := + List.map_congr_left fun w hw => hval_leaf _ ((hL w).mp hw).isLeaf_walk + rw [hcongr, ← List.sum_toFinset _ hnd] + exact T.sum_leafWords_eq hT hadd root fun w => by rw [List.mem_toFinset, hL] + rw [hsum_eq, Nat.min_eq_right hcap] + +end StackAccumulationSpec + +end Cslib.Complexity diff --git a/CslibFrontier/Computability/Complexity/Reduction/BoundedOracle.lean b/CslibFrontier/Computability/Complexity/Reduction/BoundedOracle.lean new file mode 100644 index 0000000000..3f0a04190f --- /dev/null +++ b/CslibFrontier/Computability/Complexity/Reduction/BoundedOracle.lean @@ -0,0 +1,1876 @@ +/- +Copyright (c) 2026 Samuel Schlesinger. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Samuel Schlesinger +-/ + +module +-- upstream: candidate + +public import CslibFrontier.Computability.Complexity.Classes.Oracle.BoundedQuery +public import CslibFrontier.Computability.Complexity.Classes.Oracle.Deterministic +public import CslibFrontier.Computability.Complexity.Classes.Oracle.Space +public import CslibFrontier.Computability.Complexity.FineGrained +public import CslibFrontier.Computability.Complexity.FineGrained.DisjointInstances +public import CslibFrontier.Computability.Complexity.FineGrained.SearchStep +public import CslibFrontier.Computability.Complexity.Reduction.Turing +public import CslibFrontier.Computability.Machines.Turing.MultiTape.Complexity.PolySpace.Plain +public import CslibFrontier.Computability.Machines.Turing.MultiTape.Encodings.Decoder.Basic +public import CslibFrontier.Computability.Machines.Turing.MultiTape.Encodings.Structure +public import CslibFrontier.Computability.Machines.Turing.MultiTape.Probabilistic.Replay.Simulation +import CslibFrontier.Computability.Machines.Turing.MultiTape.Complexity.BigO.Plain +import CslibFrontier.Computability.Machines.Turing.MultiTape.Complexity.PolyTime.Basic +import CslibFrontier.Computability.Machines.Turing.MultiTape.Complexity.PolyTime.BitString +import CslibFrontier.Computability.Machines.Turing.MultiTape.Complexity.PolyTime.Configuration +import CslibFrontier.Computability.Machines.Turing.MultiTape.Complexity.PolyTime.Finite +import CslibFrontier.Computability.Machines.Turing.MultiTape.Complexity.PolyTime.Iteration +import CslibFrontier.Computability.Machines.Turing.MultiTape.Complexity.PolyTime.List +import CslibFrontier.Computability.Machines.Turing.MultiTape.Complexity.PolyTime.Nat +import CslibFrontier.Computability.Machines.Turing.MultiTape.Complexity.PolyTime.Nat.Binary +import CslibFrontier.Computability.Machines.Turing.MultiTape.Internal.OCombinators +import CslibFrontier.Computability.Machines.Turing.MultiTape.Internal.OCountedIteration +import CslibFrontier.Computability.Machines.Turing.MultiTape.ResourceBounds.Polynomial.Automation +import CslibFrontier.Computability.Probabilistic.Oracle.Composition +import CslibFrontier.Computability.Probabilistic.Oracle.Substitution +import CslibFrontier.Computability.Probabilistic.QueryBounds + +/-! +# Oracle reductions with explicit query and answer lengths + +`Cslib.Complexity.PolyTimeTuringReducible` +(`CslibFrontier/Computability/Complexity/Reduction/Turing.lean`) and +`Cslib.Complexity.ComputableInPolyTimeWithOracle` +(`CslibFrontier/Computability/Complexity/Classes/Oracle.lean`) quantify over adaptive +deterministic `WordQueryComp` programs certified by `IsOraclePPTOn` against one-bit language +oracles. Fine-grained and exact exponential complexity require explicit quantitative accounting of +the oracle interaction across both decision and multi-bit function oracles: + +* `Cslib.Complexity.OracleCallBound`: an `enc_structure`-backed record tracking four explicit + quantities on each input `a`: + * `qcount`: number of oracle queries issued along the run; + * `qlen`: maximum bit-length of any single query word issued along the run; + * `totalQlen`: total bit-length `∑ q, |q|` summed across all queries issued along the run; + * `alen`: maximum bit-length of any oracle answer returned along the run. +* `Cslib.Complexity.BoundedOracleProgram`: a `#4391` `structure` packaging a deterministic adaptive + `WordQueryComp` program, its `IsOraclePPTOn` certificate, an explicit `OracleCallBound` profile + respected against `oracle : List Bool → List Bool`, and a polynomial-time unary answer-length + allowance `alenCap` enabling open handler substitution. +* `Cslib.Complexity.BoundedOracleReduction`: the specialization to typed decision problems + `(A, encA)` and `(B, encB)` against `languageOracle (encB '' B)` (`alen ≤ 1`). + +In addition to identity, zero-query polynomial-time lifts, single-query many-one/function lifts, +and bridges to `PolyTimeTuringReducible` and `PWithOracleQueries`, this module extends +`Turing.MultiTapePTM` simulation from one-bit `receiveBit` to arbitrary word replies `receiveWord`, +proving: + +1. **Composition (`BoundedOracleProgram.comp`, `BoundedOracleReduction.trans`):** explicit + worst-case composition via `wordMax` and sharper linear `totalQlen` composition when the inner + total query length is affine in the outer query length. +2. **Polynomial-time and polynomial-space multi-bit oracle transfer + (`BoundedOracleProgram.computableInPolyTime`, + `BoundedOracleProgram.exists_computableInO_polySpace`):** + simulator workspace is bounded in terms of input length, clock, answer-length cap, and simulated + oracle workspace — never as a polynomial in simulated oracle running time. +3. **Parameterized exponential and subexponential time transfer + (`BoundedOracleReduction.decidableInExpTime`, `BoundedOracleReduction.decidableInSubexpTime`):** + guarding oracle calls by a polynomial-time validity/length predicate that holds along + `queriesWith` transfers `2 ^ (δ * μB)` deciders to `2 ^ (scale * δ * μA)` with polynomial + overhead absorbing query count and construction cost. + +## Main definitions + +* `Cslib.Complexity.OracleCallBound`, `Cslib.Complexity.OracleCallBound.Respects`: explicit + `(qcount, qlen, totalQlen, alen)` call budget and run satisfaction predicate. +* `Turing.MultiTapePTM.receiveWord`: multi-bit reply installation on `FiniteConfig`. +* `Cslib.Complexity.BoundedOracleProgram`: multi-bit functional oracle program with explicit query + and answer length accounting. +* `Cslib.Complexity.BoundedOracleReduction`: language oracle reduction with explicit query and + answer length accounting. + +## Main results + +* `Turing.MultiTapePTM.computableInPolyTime_run_word`, + `Turing.MultiTapePTM.exists_computableInO_run_word`: multi-bit clocked oracle machine simulation + in polynomial time and in polynomial workspace. +* `Cslib.Complexity.BoundedOracleProgram.id`, `.ofPolyTime`, `.ofSingleQuery`, `.comp`, + `.compAffine`, `.totalQueryLength_comp_affine`, `.computableInPolyTime`, + `.exists_computableInO_polySpace`, `.computableInPolySpace`. +* `Cslib.Complexity.BoundedOracleReduction.refl`, `.ofPolyTime`, `.ofSizeSensitive`, + `.transDecoded`, `.trans`, `.polyTimeTuringReducible`, `.mem_PWithOracleQueries`, + `.ofPWithOracleQueries`, `.mem_P`, `.mem_PSPACE`, `.decidableInExpTime`, + `.decidableInSubexpTime`. + +## References + +* [R. E. Ladner, N. A. Lynch, A. L. Selman, *A comparison of polynomial time + reducibilities*][LadnerLynchSelman1975] +* [S. Arora, B. Barak, *Computational Complexity: A Modern Approach*][AroraBarak09], Section 3.4 +* [R. Impagliazzo, R. Paturi, F. Zane, *Which problems have strongly exponential + complexity?*][ImpagliazzoPaturiZane2001] +-/ + +public section + +/-! ### Multi-bit oracle simulation on `Turing.MultiTapePTM` -/ + +namespace Turing.MultiTapePTM + +open Cslib Cslib.Complexity MultiTapeMachine MultiTapeTM + +variable {k : ℕ} {Control Operation : Type} [DecidableEq Operation] + (machine : MultiTapePTM k Bool Control Operation) + +/-- Install a multi-bit word reply to the pending query on `p.1`; leave `p.1` unchanged when no +query is pending. -/ +@[expose] +def receiveWord (p : FiniteConfig k Bool Control Operation × List Bool) : + FiniteConfig k Bool Control Operation := + match machine.pendingQuery p.1 with + | some (op, next) => p.1.receive op next p.2 + | none => p.1 + +/-- Against any word oracle `oracle : List Bool → List Bool`, one `answerStep` either installs +`oracle (machine.pendingRequest cfg)` via `receiveWord` or executes `localStep`. -/ +theorem answerStep_word (oracle : List Bool → List Bool) + (cfg : FiniteConfig k Bool Control Operation) : + machine.answerStep (fun q => oracle q.2) cfg = + if (machine.pendingQuery cfg).isSome then + machine.receiveWord (cfg, oracle (machine.pendingRequest cfg)) + else machine.localStep cfg := by + unfold answerStep receiveWord pendingRequest localStep pendingQuery + cases cfg.tapes.state with + | none => rfl + | some control => + simp only [Option.map_some] + cases machine.tr control cfg.tapes.inputSymbol cfg.tapes.workTapeSymbols cfg.answerSymbols + false <;> rfl + +/-- When every reply to a request of length at most `steps` has length at most `answerSize`, one +`answerStep` advances `FiniteConfig.SpaceBound` from `steps` to `steps + 1` with the same +`answerSize`. -/ +theorem spaceBound_answerStep_word (oracle : List Bool → List Bool) + {inputSize steps answerSize : ℕ} {cfg : FiniteConfig k Bool Control Operation} + (h : FiniteConfig.SpaceBound inputSize steps answerSize cfg) + (hans : ∀ w, w.length ≤ steps → (oracle w).length ≤ answerSize) : + FiniteConfig.SpaceBound inputSize (steps + 1) answerSize + (machine.answerStep (fun q => oracle q.2) cfg) := by + unfold answerStep + split + · exact h.mono le_rfl (Nat.le_succ _) le_rfl + · split + · exact h.step _ _ _ + · exact h.receive _ _ _ (hans _ (h.query _)) + +section FiniteControl + +variable [Finite Control] [Fintype Operation] + +theorem receiveWord_pt : ComputableInPolyTime machine.receiveWord + (encPair encFiniteConfig encBits) encFiniteConfig := by + refine .of_tidy <| ComputableTidilyInPolyTime.finite_cases + (tag := fun p : FiniteConfig k Bool Control Operation × List Bool => machine.pendingQuery p.1) + (branch := fun q (p : FiniteConfig k Bool Control Operation × List Bool) => match q with + | some (op, next) => p.1.receive op next p.2 + | none => p.1) + (machine.pendingQuery_pt.tidy.comp + (ComputableTidilyInPolyTime.fst encFiniteConfig encBits)) ?_ + rintro (_ | ⟨op, next⟩) + · exact ComputableTidilyInPolyTime.fst _ _ + · exact ComputableTidilyInPolyTime.finiteConfig_receive + (ComputableTidilyInPolyTime.fst encFiniteConfig encBits) + (ComputableTidilyInPolyTime.snd encFiniteConfig encBits) op next + +/-- **Independent time and space of one multi-bit oracle instruction.** +Charges `Tg` and `Sg` only when `(machine.pendingQuery cfg).isSome = true`. -/ +theorem answerStep_word_inO {oracle : List Bool → List Bool} {Tg Sg : List Bool → ℕ} + (horacle : ComputableInO oracle encBits encBits Tg Sg) : + ∃ d : ℕ, ComputableInO (machine.answerStep fun q => oracle q.2) + encFiniteConfig encFiniteConfig + (fun cfg => ((encFiniteConfig cfg).length + 1) ^ d + + if (machine.pendingQuery cfg).isSome = true then + Tg (machine.pendingRequest cfg) + + ((encFiniteConfig cfg).length + + (oracle (machine.pendingRequest cfg)).length + 1) ^ d + else 0) + (fun cfg => ((encFiniteConfig cfg).length + 1) ^ d + + if (machine.pendingQuery cfg).isSome = true then + Sg (machine.pendingRequest cfg) + + ((encFiniteConfig cfg).length + + (oracle (machine.pendingRequest cfg)).length + 1) ^ d + else 0) := by + have hdone : ComputableInPolyTime (fun _ : FiniteConfig k Bool Control Operation => false) + encFiniteConfig encBool := .const false + have hleaf : ComputableInPolyTime (fun cfg => (machine.pendingQuery cfg).isSome) + encFiniteConfig encBool := + (ComputableInPolyTime.of_finite Option.isSome).comp machine.pendingQuery_pt + obtain ⟨d, h⟩ := exists_computableInO_searchStep hdone hleaf machine.pendingRequest_pt + machine.localStep_pt machine.receiveWord_pt horacle + refine ⟨d, (h.mono_le (fun cfg => ?_) (fun cfg => ?_)).of_enc_eq fun cfg => ?_⟩ + · simp only [true_and, encBits_apply] + exact le_rfl + · simp only [true_and, encBits_apply] + exact le_rfl + · simp only [Bool.false_eq_true, ite_false] + rw [machine.answerStep_word] + +theorem computableInPolyTime_answerStep_word {oracle : List Bool → List Bool} + (horacle : ComputableInPolyTime oracle encBits encBits) : + ComputableInPolyTime (machine.answerStep fun q => oracle q.2) + encFiniteConfig encFiniteConfig := by + have hcond : ComputableTidilyInPolyTime (fun cfg => (machine.pendingQuery cfg).isSome) + encFiniteConfig encBool := + (ComputableTidilyInPolyTime.of_finite Option.isSome).comp machine.pendingQuery_pt.tidy + have h := ComputableTidilyInPolyTime.cond hcond + (machine.receiveWord_pt.tidy.comp + (ComputableTidilyInPolyTime.id'.prod (horacle.tidy.comp machine.pendingRequest_pt.tidy))) + machine.localStep_pt.tidy + exact (h.of_enc_eq fun cfg => by rw [machine.answerStep_word]; rfl).computableInPolyTime + +omit [Fintype Operation] in +/-- **A clocked multi-bit oracle run against a polynomial-time word oracle is polynomial-time.** -/ +theorem computableInPolyTime_run_word [Finite Operation] {α : Type} {input : α ↪ List Bool} + {oracle : List Bool → List Bool} (horacle : ComputableInPolyTime oracle encBits encBits) + (c d : ℕ) : + ComputableInPolyTime (fun a => OracleComp.interpret (m := Id) (fun q => oracle q.2) + (machine.run (pure false) (fun op word => OracleComp.query (op, word)) + (c * ((input a).length + 1) ^ d) (input a))) input encBits := by + refine .of_tidy ?_ + classical + let _ := Fintype.ofFinite Operation + obtain ⟨cf, hcf⟩ := length_encFiniteConfig_le (k := k) (State := Control) (Oracle := Operation) + obtain ⟨co, do', ho_len⟩ := horacle.polyBounded_length.exists_le + let clk (a : α) : ℕ := c * ((input a).length + 1) ^ d + let ansMax (a : α) : ℕ := co * (clk a + 1) ^ do' + have hcount : ComputableTidilyInPolyTime clk input encUnary := + ((ComputableTidilyInPolyTime.unary_eval (Polynomial.C c * (Polynomial.X + 1) ^ d)).comp + (ComputableTidilyInPolyTime.encoding_length input)).of_enc_eq fun _ => by simp [clk] + have hinit : ComputableTidilyInPolyTime + (fun a => FiniteConfig.init (k := k) (Oracle := Operation) machine.initial (input a)) + input encFiniteConfig := + ComputableTidilyInPolyTime.finiteConfig_init (by fun_prop) _ + have hspace (a : α) {i : ℕ} (hi : i ≤ clk a) : + FiniteConfig.SpaceBound (input a).length i (ansMax a) + ((machine.answerStep fun q => oracle q.2)^[i] + (FiniteConfig.init machine.initial (input a))) := by + induction i with + | zero => exact (FiniteConfig.spaceBound_init _ _ 0).mono le_rfl le_rfl (Nat.zero_le _) + | succ i ih => + rw [Function.iterate_succ_apply'] + refine machine.spaceBound_answerStep_word oracle (ih (Nat.le_of_succ_le hi)) fun w hw => ?_ + have hw' : w.length ≤ clk a := hw.trans (Nat.le_of_succ_le hi) + exact (ho_len w).trans (Nat.mul_le_mul_left co + (Nat.pow_le_pow_left (Nat.add_le_add_right hw' 1) do')) + have hbound : PolyBounded (fun a => (input a).length) + (fun a => cf * ((input a).length + clk a + ansMax a + 1)) := by + dsimp only [clk, ansMax] + growth_poly + have hit := ComputableTidilyInPolyTime.iterate hcount hinit + (machine.computableInPolyTime_answerStep_word horacle).tidy hbound fun a i hi => + (hcf _ _ _ _ (hspace a hi)).trans (Nat.mul_le_mul_left cf (by omega)) + have hout : ComputableTidilyInPolyTime + (fun cfg : FiniteConfig k Bool Control Operation => cfg.tapes.output) + encFiniteConfig encBits := by fun_prop + exact (hout.comp hit).of_enc_eq fun a => by rw [machine.interpret_run_pure_false]; rfl + +omit [Fintype Operation] in +/-- **A clocked multi-bit oracle run against a polynomial-space word oracle runs in polynomial +workspace**, with explicit time `O(poly(|a|) + (clock a + 1) * (poly(|a|) + wordMax Tg (clock a)))` +charging `Tg` only up to the clock and bounding space solely by input, simulated space, and +counters (never by simulated time `Tg`). -/ +theorem exists_computableInO_run_word [Finite Operation] {α : Type} {input : α ↪ List Bool} + {oracle : List Bool → List Bool} {Tg Sg : List Bool → ℕ} + (horacle : ComputableInO oracle encBits encBits Tg Sg) + (hSg : PolyBounded List.length Sg) (c d : ℕ) : + ∃ (c₀ e₀ : ℕ) (S : α → ℕ), + PolyBounded (fun a => (input a).length) S ∧ + ComputableInO (fun a => OracleComp.interpret (m := Id) (fun q => oracle q.2) + (machine.run (pure false) (fun op word => OracleComp.query (op, word)) + (c * ((input a).length + 1) ^ d) (input a))) input encBits + (fun a => c₀ * ((input a).length + 1) ^ e₀ + + (c * ((input a).length + 1) ^ d + 1) * + (c₀ * ((input a).length + 1) ^ e₀ + wordMax Tg (c * ((input a).length + 1) ^ d))) + S := by + classical + let _ := Fintype.ofFinite Operation + let _ : Inhabited (FiniteConfig k Bool Control Operation) := + ⟨FiniteConfig.init machine.initial []⟩ + obtain ⟨e, hstep⟩ := machine.answerStep_word_inO horacle + obtain ⟨cg, dg, hSg_le⟩ := hSg.exists_le + obtain ⟨kg, ho_len⟩ := horacle.length_le + obtain ⟨cf, hcf⟩ := length_encFiniteConfig_le (k := k) (State := Control) (Oracle := Operation) + let clk (a : α) : ℕ := c * ((input a).length + 1) ^ d + let sgMax (a : α) : ℕ := cg * (clk a + 1) ^ dg + let ansMax (a : α) : ℕ := kg * (sgMax a + 1) + have hans_le (a : α) {w : List Bool} (hw : w.length ≤ clk a) : + (oracle w).length ≤ ansMax a := by + have hsg : Sg w ≤ sgMax a := + (hSg_le w).trans (Nat.mul_le_mul_left cg + (Nat.pow_le_pow_left (Nat.add_le_add_right hw 1) dg)) + exact (ho_len w).trans (Nat.mul_le_mul_left kg (Nat.add_le_add_right hsg 1)) + have hn : ComputableTidilyInPolyTime clk input encNat := by + have hlen : ComputableTidilyInPolyTime (fun a => (input a).length) input encUnary := by + fun_prop + exact (ComputableTidilyInPolyTime.unary_to_binary.comp + ((ComputableTidilyInPolyTime.unary_eval (Polynomial.C c * (Polynomial.X + 1) ^ d)).comp + hlen)).of_enc_eq fun _ => by simp [clk] + obtain ⟨dn, _, hn⟩ := hn.exists_degree + have hinit : ComputableTidilyInPolyTime + (fun a => FiniteConfig.init (k := k) (Oracle := Operation) machine.initial (input a)) + input encFiniteConfig := + ComputableTidilyInPolyTime.finiteConfig_init (by fun_prop) _ + obtain ⟨di, _, hinit⟩ := hinit.exists_degree + have hout : ComputableTidilyInPolyTime + (fun cfg : FiniteConfig k Bool Control Operation => cfg.tapes.output) + encFiniteConfig encBits := by fun_prop + obtain ⟨do', _, hout⟩ := hout.exists_degree + let step := machine.answerStep fun q => oracle q.2 + have hspace (a : α) {i : ℕ} (hi : i ≤ clk a) : + FiniteConfig.SpaceBound (input a).length i (ansMax a) + (step^[i] (FiniteConfig.init machine.initial (input a))) := by + induction i with + | zero => exact (FiniteConfig.spaceBound_init _ _ 0).mono le_rfl le_rfl (Nat.zero_le _) + | succ i ih => + rw [Function.iterate_succ_apply'] + exact machine.spaceBound_answerStep_word oracle (ih (Nat.le_of_succ_le hi)) + fun w hw => hans_le a (hw.trans (Nat.le_of_succ_le hi)) + let B (a : α) : ℕ := cf * ((input a).length + clk a + ansMax a + 1) + have hlen (a : α) {i : ℕ} (hi : i ≤ clk a) : + (encFiniteConfig (step^[i] (FiniteConfig.init machine.initial (input a)))).length ≤ B a := + (hcf _ _ _ _ (hspace a hi)).trans (Nat.mul_le_mul_left cf (by omega)) + have hreq (a : α) {i : ℕ} (hi : i ≤ clk a) : + (machine.pendingRequest (step^[i] (FiniteConfig.init machine.initial (input a)))).length ≤ + clk a := + (machine.length_pendingRequest_le (hspace a hi)).trans hi + let stepPoly (a : α) : ℕ := (B a + 1) ^ e + (B a + ansMax a + 1) ^ e + have hit := ComputableInO.iterate hn.inO.computableInO hinit.inO.computableInO hstep + (R := fun a => stepPoly a + wordMax Tg (clk a)) + (Q := fun a => stepPoly a + sgMax a) (B := B) + (fun a i hi => by + have hl := hlen a hi + have hr := hreq a hi + have hp1 := Nat.pow_le_pow_left (Nat.add_le_add_right hl 1) e + split_ifs + · have ha := hans_le a hr + have hp2 := Nat.pow_le_pow_left (Nat.add_le_add_right (Nat.add_le_add hl ha) 1) e + have htm := le_wordMax Tg hr + dsimp only [step, stepPoly] at hl hr hp1 ha hp2 htm ⊢ + omega + · dsimp only [step, stepPoly] at hl hr hp1 ⊢ + omega) + (fun a i hi => by + have hl := hlen a hi + have hr := hreq a hi + have hp1 := Nat.pow_le_pow_left (Nat.add_le_add_right hl 1) e + split_ifs + · have ha := hans_le a hr + have hp2 := Nat.pow_le_pow_left (Nat.add_le_add_right (Nat.add_le_add hl ha) 1) e + have hsm : Sg (machine.pendingRequest + (step^[i] (FiniteConfig.init machine.initial (input a)))) ≤ sgMax a := + (hSg_le _).trans (Nat.mul_le_mul_left cg + (Nat.pow_le_pow_left (Nat.add_le_add_right hr 1) dg)) + dsimp only [step, stepPoly] at hl hr hp1 ha hp2 hsm ⊢ + omega + · dsimp only [step, stepPoly] at hl hr hp1 ⊢ + omega) + (fun a _ hi => hlen a hi) + have hwhole := (hout.inO.computableInO.comp hit).of_enc_eq + (g := fun a => OracleComp.interpret (m := Id) (fun q => oracle q.2) + (machine.run (pure false) (fun op word => OracleComp.query (op, word)) + (clk a) (input a))) + fun a => by rw [machine.interpret_run_pure_false]; rfl + let clockLen (a : α) : ℕ := (encNat (clk a)).length + have hclkLen (a : α) : clockLen a ≤ clk a + 1 := by + dsimp only [clockLen] + rw [encNat_apply, Nat.size_eq_bits_len] + exact (Nat.size_le.mpr Nat.lt_two_pow_self).trans (Nat.le_succ _) + have hOverhead : PolyBounded (fun a => (input a).length) + (fun a => ((input a).length + 1) ^ dn + ((input a).length + 1) ^ di + + (B a + 1) ^ do' + stepPoly a + sgMax a + B a + (clk a + 1 + 1) ^ 2 + (clk a + 1)) := by + dsimp only [stepPoly, B, ansMax, sgMax, clk] + growth_poly + obtain ⟨c₀, e₀, hc₀⟩ := hOverhead.exists_le + let S (a : α) : ℕ := c₀ * ((input a).length + 1) ^ e₀ + have hSPoly : PolyBounded (fun a => (input a).length) S := by + dsimp only [S] + growth_poly + refine ⟨c₀, e₀, S, hSPoly, hwhole.mono_le (fun a => ?_) (fun a => ?_)⟩ + · have hfin := Nat.pow_le_pow_left (Nat.add_le_add_right (hlen a le_rfl) 1) do' + have hcl2 := Nat.pow_le_pow_left (Nat.add_le_add_right (hclkLen a) 1) 2 + have h₁ := hc₀ a + dsimp only [step, clk, clockLen] at hfin hcl2 h₁ ⊢ + rw [Nat.add_right_comm] + exact Nat.add_le_add (by omega) (Nat.mul_le_mul_left _ (by omega)) + · have hfin := Nat.pow_le_pow_left (Nat.add_le_add_right (hlen a le_rfl) 1) do' + have hcl := hclkLen a + have h₁ := hc₀ a + dsimp only [step, S, clk, clockLen] at hfin hcl h₁ ⊢ + omega + +end FiniteControl + +end Turing.MultiTapePTM + +/-! ### `OracleCallBound`, `BoundedOracleProgram`, and `BoundedOracleReduction` -/ + +namespace Cslib.Complexity + +open Probability _root_.Turing _root_.Turing.MultiTapeTM + +@[expose] section +/-- Explicit quantitative profile of an oracle call budget on a single input: +`qcount` queries, each of bit-length at most `qlen`, with total bit-length at most `totalQlen`, +and each answer of bit-length at most `alen`. -/ +@[ext] +structure OracleCallBound where + /-- Maximum number of oracle queries issued along the run. -/ + qcount : ℕ + /-- Maximum bit-length of any single query word issued along the run. -/ + qlen : ℕ + /-- Maximum sum of bit-lengths of all query words issued along the run. -/ + totalQlen : ℕ + /-- Maximum bit-length of any oracle answer read along the run. -/ + alen : ℕ + deriving DecidableEq, Repr +end + +/-- Framed binary encoding of `OracleCallBound`. -/ +enc_structure encOracleCallBound : OracleCallBound where + qcount : encNat, qlen : encNat, totalQlen : encNat, alen : encNat + +namespace OracleCallBound + +/-- Zero-query profile `(0, 0, 0, 0)`. -/ +@[expose] def zero : OracleCallBound := ⟨0, 0, 0, 0⟩ + +/-- Single-query profile `(1, ql, ql, al)` for a query of length `≤ ql` and reply of length `≤ al`. +-/ +@[expose] def single (ql al : ℕ) : OracleCallBound := ⟨1, ql, ql, al⟩ + +/-- Coordinatewise dominance between `OracleCallBound` profiles. -/ +@[expose] def Le (b₁ b₂ : OracleCallBound) : Prop := + b₁.qcount ≤ b₂.qcount ∧ b₁.qlen ≤ b₂.qlen ∧ b₁.totalQlen ≤ b₂.totalQlen ∧ b₁.alen ≤ b₂.alen + +/-- `prog` **respects** `b` against the word oracle `oracle : List Bool → List Bool`: along the +deterministic run `queriesWith (fun q => oracle q.2) prog`, query count is `≤ b.qcount`, each query +has length `≤ b.qlen`, total query length is `≤ b.totalQlen`, and each reply has length `≤ b.alen`. +-/ +@[expose] +def Respects {β : Type} (oracle : List Bool → List Bool) (prog : WordQueryComp Unit β) + (b : OracleCallBound) : Prop := + let qs := OracleComp.queriesWith (fun q => oracle q.2) prog + qs.length ≤ b.qcount ∧ + (∀ q ∈ qs, q.2.length ≤ b.qlen) ∧ + (qs.map fun q => q.2.length).sum ≤ b.totalQlen ∧ + (∀ q ∈ qs, (oracle q.2).length ≤ b.alen) + +theorem Respects.mono {β : Type} {oracle : List Bool → List Bool} {prog : WordQueryComp Unit β} + {b₁ b₂ : OracleCallBound} (h : Respects oracle prog b₁) (hle : b₁.Le b₂) : + Respects oracle prog b₂ := by + rcases h with ⟨hqc, hql, htql, hal⟩ + rcases hle with ⟨hlqc, hlql, hltql, hlal⟩ + exact ⟨hqc.trans hlqc, fun q hq => (hql q hq).trans hlql, + htql.trans hltql, fun q hq => (hal q hq).trans hlal⟩ + +theorem respects_pure {β : Type} (oracle : List Bool → List Bool) (x : β) (b : OracleCallBound) : + Respects oracle (pure x) b := by + simp [Respects] + +theorem respects_map {β γ : Type} (oracle : List Bool → List Bool) (f : β → γ) + (prog : WordQueryComp Unit β) (b : OracleCallBound) : + Respects oracle (f <$> prog) b ↔ Respects oracle prog b := by + simp [Respects, OracleComp.queriesWith_map] + +/-- Composed call bound when an outer run with bound `b₁` answers each query `w` (`|w| ≤ b₁.qlen`) +using an inner oracle program with profile `b₂ w`. -/ +@[expose] +noncomputable def comp (b₁ : OracleCallBound) (b₂ : List Bool → OracleCallBound) : + OracleCallBound where + qcount := b₁.qcount * wordMax (fun w => (b₂ w).qcount) b₁.qlen + qlen := wordMax (fun w => (b₂ w).qlen) b₁.qlen + totalQlen := b₁.qcount * wordMax (fun w => (b₂ w).totalQlen) b₁.qlen + alen := wordMax (fun w => (b₂ w).alen) b₁.qlen + +end OracleCallBound + +/-- Auxiliary structural lemma for substituting a deterministic word-query handler `G` into an +outer `WordQueryComp` program `prog`. -/ +private theorem interpret_and_queriesWith_subst {β : Type} + (oracle₁ oracle₂ : List Bool → List Bool) + (G : Unit × List Bool → WordQueryComp Unit (List Bool)) + (prog : WordQueryComp Unit β) + (hG : ∀ q ∈ OracleComp.queriesWith (fun q => oracle₁ q.2) prog, + OracleComp.interpret (m := Id) (fun q' => oracle₂ q'.2) (G q) = oracle₁ q.2) : + OracleComp.interpret (m := Id) (fun q' => oracle₂ q'.2) (OracleComp.interpret G prog) = + OracleComp.interpret (m := Id) (fun q => oracle₁ q.2) prog ∧ + OracleComp.queriesWith (fun q' => oracle₂ q'.2) (OracleComp.interpret G prog) = + (OracleComp.queriesWith (fun q => oracle₁ q.2) prog).flatMap fun q => + OracleComp.queriesWith (fun q' => oracle₂ q'.2) (G q) := by + induction prog using PFunctor.FreeM.induction with + | pure x => exact ⟨rfl, rfl⟩ + | lift_bind q cont ih => + change OracleComp.interpret (m := Id) (fun q' => oracle₂ q'.2) + (OracleComp.interpret G (OracleComp.query q >>= cont)) = + OracleComp.interpret (m := Id) (fun q => oracle₁ q.2) (OracleComp.query q >>= cont) ∧ + OracleComp.queriesWith (fun q' => oracle₂ q'.2) + (OracleComp.interpret G (OracleComp.query q >>= cont)) = + (OracleComp.queriesWith (fun q => oracle₁ q.2) (OracleComp.query q >>= cont)).flatMap _ + rw [OracleComp.interpret_bind, OracleComp.interpret_query, OracleComp.interpret_bind, + OracleComp.queriesWith_bind, OracleComp.queriesWith_query_bind, List.flatMap_cons] + have hq : OracleComp.interpret (m := Id) (fun q' => oracle₂ q'.2) (G q) = oracle₁ q.2 := + hG q (List.mem_cons_self ..) + rw [hq] + obtain ⟨heval, hqs⟩ := ih (oracle₁ q.2) fun q' hq' => hG q' (List.mem_cons_of_mem _ hq') + exact ⟨heval, congrArg (_ ++ ·) hqs⟩ + +private theorem forall_queriesWith_of_probQueriesSatisfy {β : Type} + {p : Unit × List Bool → Prop} (answer : Unit × List Bool → List Bool) + (prog : WordQueryComp Unit β) + (h : (OracleComp.interpret ProbOracleComp.query prog).QueriesSatisfy p) : + ∀ q ∈ OracleComp.queriesWith answer prog, p q := by + induction prog using PFunctor.FreeM.induction with + | pure _ => simp + | lift_bind q cont ih => + change (OracleComp.interpret ProbOracleComp.query + (OracleComp.query q >>= cont)).QueriesSatisfy p at h + rw [OracleComp.interpret_bind, OracleComp.interpret_query, ProbOracleComp.query] at h + obtain ⟨hpq, hcont⟩ := OracleComp.QueriesSatisfy.liftBind_iff.mp h + intro q' hq' + change q' ∈ OracleComp.queriesWith answer (OracleComp.query q >>= cont) at hq' + rw [OracleComp.queriesWith_query_bind, List.mem_cons] at hq' + rcases hq' with rfl | hq' + · exact hpq + · exact ih (answer q) (hcont (answer q)) q' hq' + +/-- **Deterministic adaptive oracle program with explicit query and answer length bounds.** +Packages a `WordQueryComp` program computing `f : α → β` relative to `oracle : List Bool → List +Bool`, certified by `IsOraclePPTOn`, together with an explicit `OracleCallBound` profile `bound a` +and a polynomial-time unary reply-length allowance `alenCap a` (`(bound a).alen ≤ alenCap a`) used +when composing open oracle handlers. -/ +structure BoundedOracleProgram {α β : Type} (encA : α ↪ List Bool) (encB : β ↪ List Bool) + (oracle : List Bool → List Bool) (f : α → β) where + /-- Deterministic adaptive word-query program. -/ + program : α → WordQueryComp Unit β + /-- Explicit `(qcount, qlen, totalQlen, alen)` profile on each input. -/ + bound : α → OracleCallBound + /-- Polynomial-time unary upper allowance on reply lengths along the run. -/ + alenCap : α → ℕ + /-- Strict oracle-PPT machine realization across all stateful handlers. -/ + isOraclePPTOn : + IsOraclePPTOn encA encB (fun a => OracleComp.interpret ProbOracleComp.query (program a)) + /-- Polynomial-time certificate for `alenCap` in unary. -/ + computableInPolyTime_alenCap : ComputableInPolyTime alenCap encA encUnary + /-- Functional correctness against `oracle`. -/ + eval_eq : ∀ a, OracleComp.interpret (m := Id) (fun q => oracle q.2) (program a) = f a + /-- Every run respects `bound a`. -/ + respects_bound : ∀ a, OracleCallBound.Respects oracle (program a) (bound a) + /-- `alenCap a` dominates `(bound a).alen`. -/ + alen_le_alenCap : ∀ a, (bound a).alen ≤ alenCap a + +namespace BoundedOracleProgram + +variable {α β γ : Type} {encA : α ↪ List Bool} {encB : β ↪ List Bool} {encC : γ ↪ List Bool} + +/-- Number of queries budgeted on `a`. -/ +@[expose] def qcount {oracle : List Bool → List Bool} {f : α → β} + (R : BoundedOracleProgram encA encB oracle f) (a : α) : ℕ := (R.bound a).qcount + +/-- Per-query length budgeted on `a`. -/ +@[expose] def qlen {oracle : List Bool → List Bool} {f : α → β} + (R : BoundedOracleProgram encA encB oracle f) (a : α) : ℕ := (R.bound a).qlen + +/-- Total query length budgeted on `a`. -/ +@[expose] def totalQlen {oracle : List Bool → List Bool} {f : α → β} + (R : BoundedOracleProgram encA encB oracle f) (a : α) : ℕ := (R.bound a).totalQlen + +/-- Per-answer length budgeted on `a`. -/ +@[expose] def alen {oracle : List Bool → List Bool} {f : α → β} + (R : BoundedOracleProgram encA encB oracle f) (a : α) : ℕ := (R.bound a).alen + +/-- Weaken the `OracleCallBound` profile of `R` to any coordinatewise larger `bound'`. -/ +@[expose] +def mono {oracle : List Bool → List Bool} {f : α → β} + (R : BoundedOracleProgram encA encB oracle f) + {bound' : α → OracleCallBound} {alenCap' : α → ℕ} + (hbound : ∀ a, (R.bound a).Le (bound' a)) + (hcap_pt : ComputableInPolyTime alenCap' encA encUnary) + (hcap_le : ∀ a, (bound' a).alen ≤ alenCap' a) : + BoundedOracleProgram encA encB oracle f where + program := R.program + bound := bound' + alenCap := alenCap' + isOraclePPTOn := R.isOraclePPTOn + computableInPolyTime_alenCap := hcap_pt + eval_eq := R.eval_eq + respects_bound a := (R.respects_bound a).mono (hbound a) + alen_le_alenCap := hcap_le + +/-- A plain polynomial-time function `f : α → β` lifts to a `0`-query `BoundedOracleProgram` with +`OracleCallBound.zero` relative to every word oracle. -/ +@[expose] +def ofPolyTime {f : α → β} (hf : ComputableInPolyTime f encA encB) + (oracle : List Bool → List Bool) : + BoundedOracleProgram encA encB oracle f where + program a := pure (f a) + bound _ := OracleCallBound.zero + alenCap _ := 0 + isOraclePPTOn := hf.isOraclePPTOn + computableInPolyTime_alenCap := .const 0 + eval_eq _ := rfl + respects_bound _ := OracleCallBound.respects_pure oracle _ _ + alen_le_alenCap _ := le_rfl + +/-- Polynomial-time postprocessing `g : β → γ` preserves `bound` and `alenCap`. -/ +@[expose] +def map {oracle : List Bool → List Bool} {f : α → β} {g : β → γ} + (R : BoundedOracleProgram encA encB oracle f) + (hg : ComputableInPolyTime g encB encC) : + BoundedOracleProgram encA encC oracle (g ∘ f) where + program a := g <$> R.program a + bound := R.bound + alenCap := R.alenCap + isOraclePPTOn := by + simpa only [OracleComp.interpret_map] using R.isOraclePPTOn.map' hg + computableInPolyTime_alenCap := R.computableInPolyTime_alenCap + eval_eq a := by + rw [OracleComp.interpret_map, R.eval_eq a] + rfl + respects_bound a := (OracleCallBound.respects_map oracle g (R.program a) (R.bound a)).mpr + (R.respects_bound a) + alen_le_alenCap := R.alen_le_alenCap + +/-- Polynomial-time preprocessing `p : γ → α` pulls back `bound` and `alenCap` along `p`. -/ +@[expose] +def preprocess {oracle : List Bool → List Bool} {f : α → β} {p : γ → α} + (R : BoundedOracleProgram encA encB oracle f) + (hp : ComputableInPolyTime p encC encA) : + BoundedOracleProgram encC encB oracle (f ∘ p) where + program c := R.program (p c) + bound c := R.bound (p c) + alenCap c := R.alenCap (p c) + isOraclePPTOn := R.isOraclePPTOn.preprocess' hp + computableInPolyTime_alenCap := R.computableInPolyTime_alenCap.comp hp + eval_eq c := R.eval_eq (p c) + respects_bound c := R.respects_bound (p c) + alen_le_alenCap c := R.alen_le_alenCap (p c) + +/-- **Single-query oracle call** with explicit request generator `req : α → List Bool`, unary +answer-length cap `alenCap : α → ℕ`, and polynomial-time reply decoder `decode : α × List Bool → +β`. Issues `1` query of length `(req a).length` and reads at most `alenCap a` reply bits. -/ +@[expose] +def ofSingleQuery {oracle : List Bool → List Bool} {req : α → List Bool} {alenCap : α → ℕ} + {decode : α × List Bool → β} + (hreq : ComputableInPolyTime req encA encBits) + (halen : ComputableInPolyTime alenCap encA encUnary) + (hdec : ComputableInPolyTime decode (encPair encA encBits) encB) + (hle : ∀ a, (oracle (req a)).length ≤ alenCap a) : + BoundedOracleProgram encA encB oracle (fun a => decode (a, oracle (req a))) where + program a := (fun reply => decode (a, reply)) <$> + (List.take (alenCap a) <$> OracleComp.query ((), req a)) + bound a := OracleCallBound.single (req a).length (oracle (req a)).length + alenCap := alenCap + isOraclePPTOn := by + have hq := IsOraclePPTOn.query_take' () hreq halen + simpa only [OracleComp.interpret_map, OracleComp.interpret_query, Functor.map_map] using + hq.map_with' (f := fun a reply => decode (a, reply)) hdec + computableInPolyTime_alenCap := halen + eval_eq a := by + simp only [OracleComp.interpret_map, Functor.map_map] + change decode (a, (oracle (req a)).take (alenCap a)) = decode (a, oracle (req a)) + rw [List.take_of_length_le (hle a)] + respects_bound a := by + simp [OracleCallBound.Respects, OracleCallBound.single, OracleComp.queriesWith_map] + alen_le_alenCap a := hle a + +/-- **Identity word-oracle program** on `List Bool` given a polynomial-time unary bound `alenCap` +on `(oracle w).length`: makes `1` query `w` of length `w.length` and returns `oracle w`. -/ +@[expose] +def id {oracle : List Bool → List Bool} {alenCap : List Bool → ℕ} + (halen : ComputableInPolyTime alenCap encBits encUnary) + (hle : ∀ w, (oracle w).length ≤ alenCap w) : + BoundedOracleProgram encBits encBits oracle oracle := + ofSingleQuery (req := _root_.id) (alenCap := alenCap) (decode := Prod.snd) + .id' halen (.snd encBits encBits) hle + +private theorem list_sum_affine_le {ι : Type} (f g : ι → ℕ) (scale offset : ℕ) : + ∀ (l : List ι), (∀ x ∈ l, f x ≤ scale * g x + offset) → + (l.map f).sum ≤ scale * (l.map g).sum + offset * l.length + | [], _ => by simp + | x :: xs, h => by + have hx := h x List.mem_cons_self + have hxs := list_sum_affine_le f g scale offset xs + fun y hy => h y (List.mem_cons_of_mem x hy) + simp only [List.map_cons, List.sum_cons, List.length_cons, Nat.mul_add, Nat.mul_one] + omega + +/-- Polynomial reply-length allowance for `BoundedOracleProgram.comp`. -/ +noncomputable def compCapPoly {oracle₁ oracle₂ : List Bool → List Bool} {f : α → β} + (R₁ : BoundedOracleProgram encA encB oracle₁ f) + (R₂ : BoundedOracleProgram encBits encBits oracle₂ oracle₁) : Polynomial ℕ := + let hqb := IsOraclePPTOn.query_bounds R₁.isOraclePPTOn + let c₁ := Classical.choose hqb + let d₁ := Classical.choose (Classical.choose_spec hqb) + let hcap₂ : PolyBounded List.length R₂.alenCap := by + simpa only [encUnary_apply, List.length_replicate, encBits_apply] using + R₂.computableInPolyTime_alenCap.polyBounded_length + let hex₂ := hcap₂.exists_le + let c₂ := Classical.choose hex₂ + let d₂ := Classical.choose (Classical.choose_spec hex₂) + Polynomial.C c₂ * (Polynomial.C c₁ * (Polynomial.X + 1) ^ d₁ + 1) ^ d₂ + +/-- **Composition of `BoundedOracleProgram`s with explicit query and answer length accounting.** +Substitutes `R₂ : BoundedOracleProgram encBits encBits oracle₂ oracle₁` for each query of +`R₁ : BoundedOracleProgram encA encB oracle₁ f`, truncating replies to `R₁.alenCap a` so open +machine realization (`IsOraclePPTOn.interpret_preprocess_open'`) holds against every stateful +external oracle while `OracleCallBound.comp` records the composed `(qcount, qlen, totalQlen, alen)` +budget (with `alen` additionally capped by the polynomial machine reply bound). -/ +@[expose] +noncomputable def comp {oracle₁ oracle₂ : List Bool → List Bool} {f : α → β} + (R₁ : BoundedOracleProgram encA encB oracle₁ f) + (R₂ : BoundedOracleProgram encBits encBits oracle₂ oracle₁) : + BoundedOracleProgram encA encB oracle₂ f where + program a := OracleComp.interpret + (fun q : Unit × List Bool => List.take (R₁.alenCap a) <$> R₂.program q.2) (R₁.program a) + bound a := + let bc := (R₁.bound a).comp R₂.bound + { bc with alen := min bc.alen ((compCapPoly R₁ R₂).eval (encA a).length) } + alenCap a := (compCapPoly R₁ R₂).eval (encA a).length + isOraclePPTOn := by + let G (a : α) (q : Unit × List Bool) : WordQueryComp Unit (List Bool) := + List.take (R₁.alenCap a) <$> R₂.program q.2 + let EIn := encPair encA (encPair (encFinEnum Unit) encBits) + have hR₂_lift : IsOraclePPTOn EIn encBits + (fun ⟨_, _, w⟩ => OracleComp.interpret ProbOracleComp.query (R₂.program w)) := + R₂.isOraclePPTOn.preprocess' (input := EIn) + (prepare := fun ⟨_, _, w⟩ => w) (by dsimp only [EIn]; fun_prop) + have htake_pt : ComputableInPolyTime + (fun ⟨⟨a, _, _⟩, reply⟩ => reply.take (R₁.alenCap a)) + (encPair EIn encBits) encBits := by + have hfstE : ComputableInPolyTime + (fun ⟨⟨a, _, _⟩, _⟩ => a) (encPair EIn encBits) encA := by + dsimp only [EIn]; fun_prop + have hsndB : ComputableInPolyTime + (fun ⟨_, reply⟩ => reply) (encPair EIn encBits) encBits := + ComputableInPolyTime.snd EIn encBits + exact (ComputableTidilyInPolyTime.bitsTake.comp + (hsndB.tidy.prod (R₁.computableInPolyTime_alenCap.comp hfstE).tidy)).computableInPolyTime + have hhandler : IsOraclePPTOn EIn encBits + (fun p : α × (Unit × List Bool) => + OracleComp.interpret ProbOracleComp.query (G p.1 p.2)) := by + simpa only [G, OracleComp.interpret_map] using + hR₂_lift.map_with' (f := fun ⟨a, _⟩ reply => reply.take (R₁.alenCap a)) htake_pt + have hresources : ComputableInPolyTime (fun p : α × List Bool => R₁.alenCap p.1) + (encPair encA encBits) encUnary := + R₁.computableInPolyTime_alenCap.comp (ComputableInPolyTime.fst encA encBits) + have hsub := R₁.isOraclePPTOn.interpret_preprocess_open' + (operationEncoding := encFinEnum Unit) + (handler := fun a q => OracleComp.interpret ProbOracleComp.query (G a q)) + (prepare := _root_.id) (resources := fun a _ => R₁.alenCap a) + .id' hhandler hresources fun a q reply hreply => by + dsimp only [G] at hreply + rw [OracleComp.interpret_map] at hreply + obtain ⟨raw, -, rfl⟩ := OracleComp.mem_supportWith_map_iff.mp hreply + exact List.length_take_le _ _ + convert hsub using 1 + funext a + rw [OracleComp.interpret_interpret, OracleComp.interpret_interpret] + congr 1 + funext q + simp only [ProbOracleComp.interpret_query] + rfl + computableInPolyTime_alenCap := by + exact ((ComputableInPolyTime.unary_eval (compCapPoly R₁ R₂)).comp + (ComputableInPolyTime.encoding_length encA)).of_enc_eq fun _ => rfl + eval_eq a := by + let G (q : Unit × List Bool) : WordQueryComp Unit (List Bool) := + List.take (R₁.alenCap a) <$> R₂.program q.2 + rcases R₁.respects_bound a with ⟨_, _, _, hal₁⟩ + have hG (q : Unit × List Bool) + (hq : q ∈ OracleComp.queriesWith (fun q => oracle₁ q.2) (R₁.program a)) : + OracleComp.interpret (m := Id) (fun q' => oracle₂ q'.2) (G q) = oracle₁ q.2 := by + dsimp only [G] + rw [OracleComp.interpret_map, R₂.eval_eq q.2] + exact List.take_of_length_le ((hal₁ q hq).trans (R₁.alen_le_alenCap a)) + exact (interpret_and_queriesWith_subst oracle₁ oracle₂ G (R₁.program a) hG).1.trans + (R₁.eval_eq a) + respects_bound a := by + let hqb := IsOraclePPTOn.query_bounds R₁.isOraclePPTOn + let c₁ := Classical.choose hqb + let hc₁ := Classical.choose_spec hqb + let d₁ := Classical.choose hc₁ + have hqb₁ : ∀ x, (OracleComp.interpret ProbOracleComp.query (R₁.program x)).IsQueryBounded + (c₁ * ((encA x).length + 1) ^ d₁) ∧ + (OracleComp.interpret ProbOracleComp.query (R₁.program x)).QueriesSatisfy + (fun request => request.2.length ≤ c₁ * ((encA x).length + 1) ^ d₁) := + Classical.choose_spec hc₁ + have hcap₂_poly : PolyBounded List.length R₂.alenCap := by + simpa only [encUnary_apply, List.length_replicate, encBits_apply] using + R₂.computableInPolyTime_alenCap.polyBounded_length + let hex₂ := hcap₂_poly.exists_le + let c₂ := Classical.choose hex₂ + let hc₂ := Classical.choose_spec hex₂ + let d₂ := Classical.choose hc₂ + have hcap₂_le : ∀ w : List Bool, R₂.alenCap w ≤ c₂ * (w.length + 1) ^ d₂ := + Classical.choose_spec hc₂ + let G (q : Unit × List Bool) : WordQueryComp Unit (List Bool) := + List.take (R₁.alenCap a) <$> R₂.program q.2 + rcases R₁.respects_bound a with ⟨hqc₁, hql₁, _, hal₁⟩ + have hG (q : Unit × List Bool) + (hq : q ∈ OracleComp.queriesWith (fun q => oracle₁ q.2) (R₁.program a)) : + OracleComp.interpret (m := Id) (fun q' => oracle₂ q'.2) (G q) = oracle₁ q.2 := by + dsimp only [G] + rw [OracleComp.interpret_map, R₂.eval_eq q.2] + exact List.take_of_length_le ((hal₁ q hq).trans (R₁.alen_le_alenCap a)) + have hqs := (interpret_and_queriesWith_subst oracle₁ oracle₂ G (R₁.program a) hG).2 + dsimp only [OracleCallBound.Respects, OracleCallBound.comp] + change (OracleComp.queriesWith (fun q' => oracle₂ q'.2) + (OracleComp.interpret G (R₁.program a))).length ≤ _ ∧ _ + rw [hqs] + set qs₁ := OracleComp.queriesWith (fun q => oracle₁ q.2) (R₁.program a) + have hinner_qs (q : Unit × List Bool) : + OracleComp.queriesWith (fun q' => oracle₂ q'.2) (G q) = + OracleComp.queriesWith (fun q' => oracle₂ q'.2) (R₂.program q.2) := by + dsimp only [G] + exact OracleComp.queriesWith_map _ _ _ + refine ⟨?_, ?_, ?_, ?_⟩ + · rw [List.length_flatMap] + have hsum_le : (qs₁.map fun q => + (OracleComp.queriesWith (fun q' => oracle₂ q'.2) (G q)).length).sum ≤ + qs₁.length * wordMax (fun w => (R₂.bound w).qcount) (R₁.bound a).qlen := by + have hmem : ∀ x ∈ qs₁.map (fun q => + (OracleComp.queriesWith (fun q' => oracle₂ q'.2) (G q)).length), + x ≤ wordMax (fun w => (R₂.bound w).qcount) (R₁.bound a).qlen := by + intro x hx + obtain ⟨q, hq, rfl⟩ := List.mem_map.mp hx + rw [hinner_qs] + rcases R₂.respects_bound q.2 with ⟨hqc₂, _, _, _⟩ + exact hqc₂.trans (le_wordMax (fun w => (R₂.bound w).qcount) (hql₁ q hq)) + simpa only [List.length_map, smul_eq_mul] using List.sum_le_length_nsmul _ _ hmem + exact hsum_le.trans (Nat.mul_le_mul_right _ hqc₁) + · intro q' hq' + obtain ⟨q, hq, hq'_mem⟩ := List.mem_flatMap.mp hq' + rw [hinner_qs] at hq'_mem + rcases R₂.respects_bound q.2 with ⟨_, hql₂, _, _⟩ + exact (hql₂ q' hq'_mem).trans + (le_wordMax (fun w => (R₂.bound w).qlen) (hql₁ q hq)) + · rw [List.map_flatMap, List.flatMap_def, List.sum_flatten, List.map_map] + have hsum_le : (qs₁.map + ((fun l : List ℕ => l.sum) ∘ fun q => + (OracleComp.queriesWith (fun q' => oracle₂ q'.2) (G q)).map + (fun q' => q'.2.length))).sum ≤ + qs₁.length * wordMax (fun w => (R₂.bound w).totalQlen) (R₁.bound a).qlen := by + have hmem : ∀ x ∈ qs₁.map + ((fun l : List ℕ => l.sum) ∘ fun q => + (OracleComp.queriesWith (fun q' => oracle₂ q'.2) (G q)).map + (fun q' => q'.2.length)), + x ≤ wordMax (fun w => (R₂.bound w).totalQlen) (R₁.bound a).qlen := by + intro x hx + obtain ⟨q, hq, rfl⟩ := List.mem_map.mp hx + simp only [Function.comp_apply, hinner_qs] + rcases R₂.respects_bound q.2 with ⟨_, _, htql₂, _⟩ + exact htql₂.trans (le_wordMax (fun w => (R₂.bound w).totalQlen) (hql₁ q hq)) + simpa only [List.length_map, smul_eq_mul] using List.sum_le_length_nsmul _ _ hmem + exact hsum_le.trans (Nat.mul_le_mul_right _ hqc₁) + · intro q' hq' + obtain ⟨q, hq, hq'_mem⟩ := List.mem_flatMap.mp hq' + rw [hinner_qs] at hq'_mem + rcases R₂.respects_bound q.2 with ⟨_, _, _, hal₂⟩ + refine le_min + ((hal₂ q' hq'_mem).trans (le_wordMax (fun w => (R₂.bound w).alen) (hql₁ q hq))) ?_ + have hq_clk : q.2.length ≤ c₁ * ((encA a).length + 1) ^ d₁ := + forall_queriesWith_of_probQueriesSatisfy (fun q => oracle₁ q.2) (R₁.program a) + (hqb₁ a).2 q hq + have hcap_eval : (compCapPoly R₁ R₂).eval (encA a).length = + c₂ * (c₁ * ((encA a).length + 1) ^ d₁ + 1) ^ d₂ := by + dsimp only [compCapPoly, c₁, d₁, c₂, d₂, hc₁, hc₂, hqb, hex₂] + simp + rw [hcap_eval] + exact ((hal₂ q' hq'_mem).trans (R₂.alen_le_alenCap q.2)).trans + ((hcap₂_le q.2).trans + (Nat.mul_le_mul_left c₂ (Nat.pow_le_pow_left (Nat.add_le_add_right hq_clk 1) d₂))) + alen_le_alenCap _ := Nat.min_le_right _ _ + +@[simp] +theorem qcount_comp {oracle₁ oracle₂ : List Bool → List Bool} {f : α → β} + (R₁ : BoundedOracleProgram encA encB oracle₁ f) + (R₂ : BoundedOracleProgram encBits encBits oracle₂ oracle₁) (a : α) : + (R₁.comp R₂).qcount a = R₁.qcount a * wordMax R₂.qcount (R₁.qlen a) := rfl + +@[simp] +theorem qlen_comp {oracle₁ oracle₂ : List Bool → List Bool} {f : α → β} + (R₁ : BoundedOracleProgram encA encB oracle₁ f) + (R₂ : BoundedOracleProgram encBits encBits oracle₂ oracle₁) (a : α) : + (R₁.comp R₂).qlen a = wordMax R₂.qlen (R₁.qlen a) := rfl + +@[simp] +theorem totalQlen_comp {oracle₁ oracle₂ : List Bool → List Bool} {f : α → β} + (R₁ : BoundedOracleProgram encA encB oracle₁ f) + (R₂ : BoundedOracleProgram encBits encBits oracle₂ oracle₁) (a : α) : + (R₁.comp R₂).totalQlen a = R₁.qcount a * wordMax R₂.totalQlen (R₁.qlen a) := rfl + +theorem alen_comp_le {oracle₁ oracle₂ : List Bool → List Bool} {f : α → β} + (R₁ : BoundedOracleProgram encA encB oracle₁ f) + (R₂ : BoundedOracleProgram encBits encBits oracle₂ oracle₁) (a : α) : + (R₁.comp R₂).alen a ≤ wordMax R₂.alen (R₁.qlen a) := + Nat.min_le_left _ _ + +/-- **Sharper affine `totalQlen` bound under composition:** when `R₂.totalQlen w ≤ scale * |w| + +offset`, the actual sum of inner query lengths along `(R₁.comp R₂).program a` is bounded by +`scale * R₁.totalQlen a + offset * R₁.qcount a`, preserving total-query-length sparsity rather than +multiplying `qcount * qlen`. -/ +theorem totalQueryLength_comp_affine {oracle₁ oracle₂ : List Bool → List Bool} {f : α → β} + (R₁ : BoundedOracleProgram encA encB oracle₁ f) + (R₂ : BoundedOracleProgram encBits encBits oracle₂ oracle₁) + {scale offset : ℕ} (haff : ∀ w, R₂.totalQlen w ≤ scale * w.length + offset) (a : α) : + ((OracleComp.queriesWith (fun q' => oracle₂ q'.2) ((R₁.comp R₂).program a)).map + fun q' => q'.2.length).sum ≤ + scale * R₁.totalQlen a + offset * R₁.qcount a := by + rcases R₁.respects_bound a with ⟨hqc₁, _, htql₁, hal₁⟩ + let G (q : Unit × List Bool) : WordQueryComp Unit (List Bool) := + List.take (R₁.alenCap a) <$> R₂.program q.2 + have hG (q : Unit × List Bool) + (hq : q ∈ OracleComp.queriesWith (fun q => oracle₁ q.2) (R₁.program a)) : + OracleComp.interpret (m := Id) (fun q' => oracle₂ q'.2) (G q) = oracle₁ q.2 := by + dsimp only [G] + rw [OracleComp.interpret_map, R₂.eval_eq q.2] + exact List.take_of_length_le ((hal₁ q hq).trans (R₁.alen_le_alenCap a)) + have hqs : OracleComp.queriesWith (fun q' => oracle₂ q'.2) ((R₁.comp R₂).program a) = + (OracleComp.queriesWith (fun q => oracle₁ q.2) (R₁.program a)).flatMap fun q => + OracleComp.queriesWith (fun q' => oracle₂ q'.2) (G q) := + (interpret_and_queriesWith_subst oracle₁ oracle₂ G (R₁.program a) hG).2 + rw [hqs, List.map_flatMap, List.flatMap_def, List.sum_flatten, List.map_map] + set qs₁ := OracleComp.queriesWith (fun q => oracle₁ q.2) (R₁.program a) + have hstep := list_sum_affine_le + (fun q : Unit × List Bool => + ((OracleComp.queriesWith (fun q' => oracle₂ q'.2) (G q)).map fun q' => q'.2.length).sum) + (fun q => q.2.length) scale offset qs₁ fun q _ => by + dsimp only [G] + rw [OracleComp.queriesWith_map] + rcases R₂.respects_bound q.2 with ⟨_, _, htql₂, _⟩ + exact htql₂.trans (haff q.2) + have hmul₁ : scale * (qs₁.map fun q => q.2.length).sum ≤ scale * R₁.totalQlen a := + Nat.mul_le_mul_left scale htql₁ + have hmul₂ : offset * qs₁.length ≤ offset * R₁.qcount a := + Nat.mul_le_mul_left offset hqc₁ + simpa only [Function.comp_def] using hstep.trans (Nat.add_le_add hmul₁ hmul₂) + +/-- Composed `BoundedOracleProgram` refining `comp` with the sharper linear `totalQlen` budget +`scale * R₁.totalQlen a + offset * R₁.qcount a` when `R₂.totalQlen` is affine in query length. -/ +@[expose] +noncomputable def compAffine {oracle₁ oracle₂ : List Bool → List Bool} {f : α → β} + (R₁ : BoundedOracleProgram encA encB oracle₁ f) + (R₂ : BoundedOracleProgram encBits encBits oracle₂ oracle₁) + {scale offset : ℕ} (haff : ∀ w, R₂.totalQlen w ≤ scale * w.length + offset) : + BoundedOracleProgram encA encB oracle₂ f := by + let C := R₁.comp R₂ + exact + { program := C.program + bound := fun a => + { C.bound a with totalQlen := scale * R₁.totalQlen a + offset * R₁.qcount a } + alenCap := C.alenCap + isOraclePPTOn := C.isOraclePPTOn + computableInPolyTime_alenCap := C.computableInPolyTime_alenCap + eval_eq := C.eval_eq + respects_bound := fun a => by + rcases C.respects_bound a with ⟨hqc, hql, _, hal⟩ + exact ⟨hqc, hql, totalQueryLength_comp_affine R₁ R₂ haff a, hal⟩ + alen_le_alenCap := C.alen_le_alenCap } + +/-- **Polynomial-time transfer for multi-bit word oracles:** if `oracle : List Bool → List Bool` is +computable in polynomial time, any `BoundedOracleProgram` relative to `oracle` is computable in +polynomial time. -/ +theorem computableInPolyTime {oracle : List Bool → List Bool} {f : α → β} + (R : BoundedOracleProgram encA encB oracle f) + (horacle : ComputableInPolyTime oracle encBits encBits) : + ComputableInPolyTime f encA encB := by + obtain ⟨_, _, machine, c, d, hrun⟩ := R.isOraclePPTOn.exists_fin_run_pure_false + refine (machine.computableInPolyTime_run_word (input := encA) horacle c d).of_enc_eq fun a => ?_ + rw [← R.eval_eq a, ← hrun a (fun q => oracle q.2)] + rfl + +/-- **Explicit `ComputableInO` transfer in polynomial workspace for multi-bit word oracles:** +simulating `R` against `ComputableInO oracle encBits encBits Tg Sg` uses **polynomial workspace** +(depending only on input length, machine clock, answer-length growth, and `Sg` — never on `Tg`) +and charges `Tg` at most once per step up to the polynomial clock. -/ +theorem exists_computableInO_polySpace {oracle : List Bool → List Bool} {f : α → β} + {Tg Sg : List Bool → ℕ} + (R : BoundedOracleProgram encA encB oracle f) + (horacle : ComputableInO oracle encBits encBits Tg Sg) + (hSg : PolyBounded List.length Sg) : + ∃ (c₀ e₀ : ℕ) (S : α → ℕ), PolyBounded (fun a => (encA a).length) S ∧ + ∃ c₁ d₁ : ℕ, + ComputableInO f encA encB + (fun a => c₀ * ((encA a).length + 1) ^ e₀ + + (c₁ * ((encA a).length + 1) ^ d₁ + 1) * + (c₀ * ((encA a).length + 1) ^ e₀ + + wordMax Tg (c₁ * ((encA a).length + 1) ^ d₁))) + S := by + obtain ⟨_, _, machine, c₁, d₁, hrun⟩ := R.isOraclePPTOn.exists_fin_run_pure_false + obtain ⟨c₀, e₀, S, hSPoly, hcomp⟩ := + machine.exists_computableInO_run_word (input := encA) horacle hSg c₁ d₁ + refine ⟨c₀, e₀, S, hSPoly, c₁, d₁, hcomp.of_enc_eq fun a => ?_⟩ + rw [← R.eval_eq a, ← hrun a (fun q => oracle q.2)] + rfl + +/-- **Polynomial-space transfer for multi-bit word oracles:** if `oracle : List Bool → List Bool` is +computable in polynomial space, any `BoundedOracleProgram` relative to `oracle` is computable in +polynomial space. -/ +theorem computableInPolySpace {oracle : List Bool → List Bool} {f : α → β} + (R : BoundedOracleProgram encA encB oracle f) + (horacle : ComputableInPolySpace oracle encBits encBits) : + ComputableInPolySpace f encA encB := by + obtain ⟨t, s, hs, hc, hl⟩ := horacle + have hO : ComputableInO oracle encBits encBits t (fun w => s w.length) := + (hc.computableTidilyInO hl).computableInO + have hsPoly : PolyBounded List.length (fun w : List Bool => s w.length) := + .of_polynomiallyBounded List.length hs + obtain ⟨_, _, S, hSPoly, _, _, c, htm, hout⟩ := R.exists_computableInO_polySpace hO hsPoly + exact ComputableInPolySpace.of_inSpace hSPoly ⟨_, c, htm, hout⟩ + +end BoundedOracleProgram + +/-! ### `BoundedOracleReduction`: language oracle reductions with explicit call profiles -/ + +/-- Word-oracle adapter for a typed decision problem `(B, encB)`: maps `w : List Bool` to +`[decide (w ∈ encB '' B)]`, matching `languageOracle (encB '' B) ((), w)`. -/ +@[expose] +noncomputable def encodedDecisionOracle {β : Type} (encB : β ↪ List Bool) (B : Set β) + (w : List Bool) : List Bool := + languageOracle (encB '' B) ((), w) + +@[simp] +theorem length_encodedDecisionOracle {β : Type} (encB : β ↪ List Bool) (B : Set β) + (w : List Bool) : (encodedDecisionOracle encB B w).length = 1 := by + simp [encodedDecisionOracle, languageOracle] + +/-- **Deterministic adaptive oracle reduction between decision problems `(A, encA)` and `(B, encB)` +with explicit `(qcount, qlen, totalQlen, alen)` call accounting.** -/ +structure BoundedOracleReduction {α β : Type} (encA : α ↪ List Bool) (encB : β ↪ List Bool) + (A : Set α) (B : Set β) where + /-- Deterministic adaptive word-query decider program. -/ + program : α → WordQueryComp Unit Bool + /-- Explicit `(qcount, qlen, totalQlen, alen)` call profile on each input. -/ + bound : α → OracleCallBound + /-- Strict oracle-PPT machine realization across all stateful handlers. -/ + isOraclePPTOn : + IsOraclePPTOn encA encBool (fun a => OracleComp.interpret ProbOracleComp.query (program a)) + /-- Decision correctness relative to `encB '' B`. -/ + decides : ∀ a, + a ∈ A ↔ OracleComp.interpret (m := Id) (languageOracle (encB '' B)) (program a) = true + /-- Every run against `encB '' B` respects `bound a`. -/ + respects_bound : ∀ a, + OracleCallBound.Respects (encodedDecisionOracle encB B) (program a) (bound a) + +namespace BoundedOracleReduction + +variable {α β γ : Type} {encA : α ↪ List Bool} {encB : β ↪ List Bool} {encC : γ ↪ List Bool} + +/-- Number of oracle queries budgeted on `a`. -/ +@[expose] def qcount {A : Set α} {B : Set β} + (R : BoundedOracleReduction encA encB A B) (a : α) : ℕ := (R.bound a).qcount + +/-- Per-query length budgeted on `a`. -/ +@[expose] def qlen {A : Set α} {B : Set β} + (R : BoundedOracleReduction encA encB A B) (a : α) : ℕ := (R.bound a).qlen + +/-- Total query length budgeted on `a`. -/ +@[expose] def totalQlen {A : Set α} {B : Set β} + (R : BoundedOracleReduction encA encB A B) (a : α) : ℕ := (R.bound a).totalQlen + +/-- Per-answer length budgeted on `a`. -/ +@[expose] def alen {A : Set α} {B : Set β} + (R : BoundedOracleReduction encA encB A B) (a : α) : ℕ := (R.bound a).alen + +/-- Weaken the call bound of a `BoundedOracleReduction` to any coordinatewise larger profile. -/ +@[expose] +def mono {A : Set α} {B : Set β} (R : BoundedOracleReduction encA encB A B) + {bound' : α → OracleCallBound} (h : ∀ a, (R.bound a).Le (bound' a)) : + BoundedOracleReduction encA encB A B where + program := R.program + bound := bound' + isOraclePPTOn := R.isOraclePPTOn + decides := R.decides + respects_bound a := (R.respects_bound a).mono (h a) + +/-- Build a `BoundedOracleReduction` from a `BoundedOracleProgram` computing a decider `f` for `A` +against `encodedDecisionOracle encB B`. -/ +@[expose] +def ofProgram {A : Set α} {B : Set β} {f : α → Bool} + (P : BoundedOracleProgram encA encBool (encodedDecisionOracle encB B) f) + (hf : ∀ a, a ∈ A ↔ f a = true) : + BoundedOracleReduction encA encB A B where + program := P.program + bound := P.bound + isOraclePPTOn := P.isOraclePPTOn + decides a := by + rw [hf a] + have heq : (fun q : Unit × List Bool => encodedDecisionOracle encB B q.2) = + languageOracle (encB '' B) := rfl + rw [← P.eval_eq a, heq] + respects_bound := P.respects_bound + +open Classical in +/-- View a `BoundedOracleReduction` as a `BoundedOracleProgram` computing `fun a => decide (a ∈ A)` +with unary answer-length cap `1`. -/ +@[expose] +noncomputable def toProgram {A : Set α} {B : Set β} + (R : BoundedOracleReduction encA encB A B) : + BoundedOracleProgram encA encBool (encodedDecisionOracle encB B) + (fun a => decide (a ∈ A)) where + program := R.program + bound a := { R.bound a with alen := min (R.bound a).alen 1 } + alenCap _ := 1 + isOraclePPTOn := R.isOraclePPTOn + computableInPolyTime_alenCap := .const 1 + eval_eq a := by + have heq : (fun q : Unit × List Bool => encodedDecisionOracle encB B q.2) = + languageOracle (encB '' B) := rfl + rw [heq] + exact Bool.eq_iff_iff.mpr ⟨fun h => decide_eq_true ((R.decides a).mpr h), + fun h => (R.decides a).mp (of_decide_eq_true h)⟩ + respects_bound a := by + rcases R.respects_bound a with ⟨hqc, hql, htql, hal⟩ + refine ⟨hqc, hql, htql, fun q hq => le_min (hal q hq) ?_⟩ + simp only [length_encodedDecisionOracle, le_refl] + alen_le_alenCap _ := Nat.min_le_right _ _ + +/-- A problem in `P` has a `0`-query `BoundedOracleReduction` to every problem `B`. -/ +@[expose] +noncomputable def ofPolyTime {A : Set α} (B : Set β) {f : α → Bool} + (hf : ComputableInPolyTime f encA encBool) (hA : ∀ a, a ∈ A ↔ f a = true) : + BoundedOracleReduction encA encB A B := + ofProgram (BoundedOracleProgram.ofPolyTime hf (encodedDecisionOracle encB B)) hA + +/-- **Single-query lift from `SizeSensitiveReduction`:** a many-one `SizeSensitiveReduction` lifts +to a `1`-query `BoundedOracleReduction` with `qlen = totalQlen = |encB (R.toFun a)|` and `alen = 1`. +-/ +@[expose] +noncomputable def ofSizeSensitive {A : Set α} {B : Set β} {μA : α → ℕ} {μB : β → ℕ} + (R : SizeSensitiveReduction encA encB μA μB) + (hAB : ∀ a, a ∈ A ↔ R.toFun a ∈ B) : + BoundedOracleReduction encA encB A B := by + let req (a : α) : List Bool := encB (R.toFun a) + have hreq : ComputableInPolyTime req encA encBits := + R.computableInPolyTime_toFun.of_enc_eq fun _ => rfl + have hdec : ComputableInPolyTime + (fun p : α × List Bool => p.2.headD false) (encPair encA encBits) encBool := + Decoder.bool.computableInPolyTime.comp (ComputableInPolyTime.snd encA encBits) + let P := BoundedOracleProgram.ofSingleQuery (oracle := encodedDecisionOracle encB B) + (req := req) (alenCap := fun _ => 1) (decode := fun p => p.2.headD false) + hreq (.const 1) hdec (fun a => by simp only [length_encodedDecisionOracle, le_refl]) + refine ofProgram P fun a => ?_ + dsimp only [req, encodedDecisionOracle, languageOracle] + simp only [List.headD_cons, decide_eq_true_eq, encB.injective.mem_set_image] + exact hAB a + +/-- **Identity / reflexivity (`refl`)** of `BoundedOracleReduction`: `1` query of length `|encA a|` +and `1`-bit reply. -/ +@[expose] +noncomputable def refl (encA : α ↪ List Bool) (A : Set α) : + BoundedOracleReduction encA encA A A := + ofSizeSensitive (SizeSensitiveReduction.refl encA (fun _ => 0)) (fun _ => Iff.rfl) + +/-- Complement the source language `Aᶜ` without changing the `OracleCallBound` profile. -/ +@[expose] +def complLeft {A : Set α} {B : Set β} (R : BoundedOracleReduction encA encB A B) : + BoundedOracleReduction encA encB Aᶜ B where + program a := Bool.not <$> R.program a + bound := R.bound + isOraclePPTOn := by + have hnot : ComputableInPolyTime Bool.not encBool encBool := + ComputableTidilyInPolyTime.bool_not.computableInPolyTime + simpa only [OracleComp.interpret_map] using R.isOraclePPTOn.map' hnot + decides a := by + rw [Set.mem_compl_iff, R.decides a, OracleComp.interpret_map] + change ¬(_ = true) ↔ (!(OracleComp.interpret (m := Id) _ (R.program a))) = true + cases OracleComp.interpret (m := Id) (languageOracle (encB '' B)) (R.program a) <;> simp + respects_bound a := + (OracleCallBound.respects_map (encodedDecisionOracle encB B) Bool.not (R.program a) + (R.bound a)).mpr (R.respects_bound a) + +/-- Every language's complement reduces to the language itself via `1` query (`Aᶜ ≤ B` for `B = A`). +-/ +@[expose] +noncomputable def complSelf (encA : α ↪ List Bool) (A : Set α) : + BoundedOracleReduction encA encA Aᶜ A := + (refl encA A).complLeft + +/-- Lift a typed `BoundedOracleReduction encB encC B C` to a word-level `BoundedOracleProgram` +answering `encodedDecisionOracle encB B` via a total polynomial-time `D : Decoder encB`: +non-canonical words (`encB (D.decode w) ≠ w`) are rejected in `0` queries, while canonical +encodings run `R₂`. -/ +@[expose] +noncomputable def toDecodedWordProgram {B : Set β} {C : Set γ} + (D : Decoder encB) (R₂ : BoundedOracleReduction encB encC B C) : + BoundedOracleProgram encBits encBits + (encodedDecisionOracle encC C) (encodedDecisionOracle encB B) := by + classical + let isCan (w : List Bool) : Bool := decide (encB (D.decode w) = w) + have hreenc : ComputableInPolyTime (fun b : β => (encB b : List Bool)) encB encBits := + ComputableInPolyTime.id'.of_enc_eq fun _ => rfl + have hisCan : ComputableInPolyTime isCan encBits encBool := + ((hreenc.comp D.computableInPolyTime).tidy.decide_eq' .id').computableInPolyTime + have hsingleton : ComputableInPolyTime (fun b : Bool => [b]) encBool encBits := + ComputableInPolyTime.id'.of_enc_eq fun b => (encBool_apply b).symm + let yesProg (w : List Bool) : WordQueryComp Unit (List Bool) := + (fun b => [b]) <$> R₂.program (D.decode w) + have hyes_ppt : IsOraclePPTOn encBits encBits + (fun w => OracleComp.interpret ProbOracleComp.query (yesProg w)) := by + have hpre := R₂.isOraclePPTOn.preprocess' D.computableInPolyTime + simpa only [yesProg, OracleComp.interpret_map] using hpre.map' hsingleton + have hno_ppt : IsOraclePPTOn encBits encBits + (fun _ : List Bool => + OracleComp.interpret (spec := fun _ : Unit × List Bool => List Bool) + ProbOracleComp.query (pure [false])) := by + simpa only [OracleComp.interpret_pure] using + (ComputableInPolyTime.const (encIn := encBits) (encOut := encBits) [false]).isOraclePPTOn + refine + { program := fun w => if isCan w then yesProg w else pure [false] + bound := fun w => + if isCan w then { R₂.bound (D.decode w) with alen := 1 } else OracleCallBound.zero + alenCap := fun _ => 1 + isOraclePPTOn := by + refine (IsOraclePPTOn.cond' hisCan hyes_ppt hno_ppt).congr fun w _ _ _ => ?_ + by_cases hc : isCan w = true <;> simp [hc] + computableInPolyTime_alenCap := .const 1 + eval_eq := fun w => ?_ + respects_bound := fun w => ?_ + alen_le_alenCap := fun w => by split_ifs <;> simp [OracleCallBound.zero] } + · by_cases hc : isCan w = true + · simp only [hc, ↓reduceIte, yesProg, OracleComp.interpret_map, encodedDecisionOracle] + have hcan : encB (D.decode w) = w := of_decide_eq_true hc + have hmem : w ∈ encB '' B ↔ D.decode w ∈ B := by + conv_lhs => rw [← hcan] + exact encB.injective.mem_set_image + have heq : (fun q : Unit × List Bool => languageOracle (encC '' C) ((), q.2)) = + languageOracle (encC '' C) := rfl + rw [heq] + change [OracleComp.interpret (m := Id) (languageOracle (encC '' C)) + (R₂.program (D.decode w))] = [decide (w ∈ encB '' B)] + congr 1 + exact Bool.eq_iff_iff.mpr ⟨fun h => decide_eq_true (hmem.mpr ((R₂.decides _).mpr h)), + fun h => (R₂.decides _).mp (hmem.mp (of_decide_eq_true h))⟩ + · have hnc : isCan w = false := Bool.eq_false_iff.mpr hc + simp only [hnc, Bool.false_eq_true, ↓reduceIte, encodedDecisionOracle, languageOracle] + have hnotmem : w ∉ encB '' B := by + rintro ⟨b, _, rfl⟩ + have : isCan (encB b) = true := by simp [isCan, D.decode_enc] + rw [this] at hnc + exact Bool.noConfusion hnc + simp only [OracleComp.interpret_pure, hnotmem, decide_false] + rfl + · by_cases hc : isCan w = true + · simp only [hc, ↓reduceIte] + have hresp : OracleCallBound.Respects (encodedDecisionOracle encC C) (yesProg w) + (R₂.bound (D.decode w)) := + (OracleCallBound.respects_map (encodedDecisionOracle encC C) (fun b => [b]) + (R₂.program (D.decode w)) (R₂.bound (D.decode w))).mpr + (R₂.respects_bound (D.decode w)) + rcases hresp with ⟨hqc, hql, htql, _⟩ + refine ⟨hqc, hql, htql, fun q _ => ?_⟩ + simp only [length_encodedDecisionOracle, le_refl] + · have hnc : isCan w = false := Bool.eq_false_iff.mpr hc + simp only [hnc, Bool.false_eq_true, ↓reduceIte] + exact OracleCallBound.respects_pure _ _ _ + +/-- **Transitivity (`transDecoded`) across any typed intermediate language `(B, encB)` equipped +with `D : Decoder encB`,** tracking explicit `(qcount, qlen, totalQlen, alen)` composition. -/ +@[expose] +noncomputable def transDecoded {A : Set α} {B : Set β} {C : Set γ} + (D : Decoder encB) + (R₁ : BoundedOracleReduction encA encB A B) + (R₂ : BoundedOracleReduction encB encC B C) : + BoundedOracleReduction encA encC A C := + ofProgram (R₁.toProgram.comp (R₂.toDecodedWordProgram D)) (fun _ => by simp) + +/-- **Transitivity (`trans`) across word-encoded intermediate languages `(B, encBits)`.** -/ +@[expose] +noncomputable def trans {A : Set α} {B : Set (List Bool)} {C : Set γ} + (R₁ : BoundedOracleReduction encA encBits A B) + (R₂ : BoundedOracleReduction encBits encC B C) : + BoundedOracleReduction encA encC A C := + R₁.transDecoded Decoder.bits R₂ + +/-! ### Bridges to `PolyTimeTuringReducible`, `PWithOracleQueries`, `P`, and `PSPACE` -/ + +/-- Every `BoundedOracleReduction` witnesses `PolyTimeTuringReducible` (`A ≤ᵖ_T B`). -/ +theorem polyTimeTuringReducible {A : Set α} {B : Set β} + (R : BoundedOracleReduction encA encB A B) : + PolyTimeTuringReducible encA encB A B := by + classical + exact ⟨fun a => decide (a ∈ A), + ⟨R.program, R.isOraclePPTOn, fun a => R.toProgram.eval_eq a⟩, + fun _ => by simp⟩ + +/-- If `R.qcount a ≤ r (encA a).length` for all `a`, then `R` places `A` in +`PWithOracleQueries (encB '' B) r encA`. -/ +theorem mem_PWithOracleQueries {A : Set α} {B : Set β} + (R : BoundedOracleReduction encA encB A B) {r : ℕ → ℕ} + (hr : ∀ a, R.qcount a ≤ r (encA a).length) : + A ∈ PWithOracleQueries (encB '' B) r encA := by + classical + refine ⟨fun a => decide (a ∈ A), ⟨R.program, R.isOraclePPTOn, fun a => ⟨?_, ?_⟩⟩, + fun _ => by simp⟩ + · exact R.toProgram.eval_eq a + · rcases R.respects_bound a with ⟨hqc, _, _, _⟩ + have heq : (fun q : Unit × List Bool => encodedDecisionOracle encB B q.2) = + languageOracle (encB '' B) := rfl + rw [← heq] + exact hqc.trans (hr a) + +/-- Conversely, any membership witness `A ∈ PWithOracleQueries (encB '' B) r encA` yields a +`BoundedOracleReduction encA encB A B` with `qcount a = r |encA a|`, polynomial `qlen`, +`totalQlen = qcount * qlen`, and `alen = 1`. -/ +noncomputable def ofPWithOracleQueries {A : Set α} {B : Set β} {r : ℕ → ℕ} + (h : A ∈ PWithOracleQueries (encB '' B) r encA) : + BoundedOracleReduction encA encB A B := by + classical + let f := Classical.choose h + have hf_spec := Classical.choose_spec h + let prog := Classical.choose hf_spec.1 + have hprog := Classical.choose_spec hf_spec.1 + let hqb_ex := IsOraclePPTOn.query_bounds hprog.1 + let c := Classical.choose hqb_ex + let hc := Classical.choose_spec hqb_ex + let d := Classical.choose hc + have hqb : ∀ a, (OracleComp.interpret ProbOracleComp.query (prog a)).IsQueryBounded + (c * ((encA a).length + 1) ^ d) ∧ + (OracleComp.interpret ProbOracleComp.query (prog a)).QueriesSatisfy + (fun request => request.2.length ≤ c * ((encA a).length + 1) ^ d) := + Classical.choose_spec hc + let ql (a : α) : ℕ := c * ((encA a).length + 1) ^ d + refine + { program := prog + bound := fun a => + { qcount := r (encA a).length + qlen := ql a + totalQlen := r (encA a).length * ql a + alen := 1 } + isOraclePPTOn := hprog.1 + decides := fun a => by rw [hf_spec.2 a, (hprog.2 a).1] + respects_bound := fun a => ?_ } + have heq : (fun q : Unit × List Bool => encodedDecisionOracle encB B q.2) = + languageOracle (encB '' B) := rfl + dsimp only [OracleCallBound.Respects] + have hqc : (OracleComp.queriesWith (fun q => encodedDecisionOracle encB B q.2) + (prog a)).length ≤ r (encA a).length := by + rw [heq] + exact (hprog.2 a).2 + have hql : ∀ q ∈ OracleComp.queriesWith (fun q => encodedDecisionOracle encB B q.2) (prog a), + q.2.length ≤ ql a := + forall_queriesWith_of_probQueriesSatisfy _ (prog a) (hqb a).2 + refine ⟨hqc, hql, ?_, fun q _ => by simp only [length_encodedDecisionOracle, le_refl]⟩ + set qs := OracleComp.queriesWith (fun q => encodedDecisionOracle encB B q.2) (prog a) + have hsum : (qs.map fun q => q.2.length).sum ≤ qs.length * ql a := by + have hmem : ∀ x ∈ qs.map (fun q => q.2.length), x ≤ ql a := by + intro x hx + obtain ⟨q, hq, rfl⟩ := List.mem_map.mp hx + exact hql q hq + simpa only [List.length_map, smul_eq_mul] using List.sum_le_length_nsmul _ _ hmem + exact hsum.trans (Nat.mul_le_mul_right (ql a) hqc) + +/-- **Polynomial-time transfer (`mem_P`)** across `BoundedOracleReduction` when `D : Decoder encB` +and `B ∈ P encB`. -/ +theorem mem_P {A : Set α} {B : Set β} (D : Decoder encB) + (R : BoundedOracleReduction encA encB A B) (hB : B ∈ P encB) : + A ∈ P encA := by + classical + obtain ⟨g, hg, hgB⟩ := hB + let R_P : BoundedOracleReduction encB encBits B ∅ := ofPolyTime ∅ hg hgB + let R_comp := R.transDecoded D R_P + have horacle : ComputableInPolyTime (encodedDecisionOracle encBits ∅) encBits encBits := + (ComputableInPolyTime.const (encIn := encBits) (encOut := encBits) [false]).of_enc_eq + fun w => by simp [encodedDecisionOracle, languageOracle] + exact ⟨_, R_comp.toProgram.computableInPolyTime horacle, fun _ => by simp⟩ + +/-- **Polynomial-space transfer (`mem_PSPACE`)** across `BoundedOracleReduction` when +`D : Decoder encB` and `B ∈ PSPACE encB`. -/ +theorem mem_PSPACE {A : Set α} {B : Set β} (D : Decoder encB) + (R : BoundedOracleReduction encA encB A B) (hB : B ∈ PSPACE encB) : + A ∈ PSPACE encA := by + classical + obtain ⟨T, S, hS, g, hg, hgB⟩ := exists_computableInO_of_mem_PSPACE hB + let isCan (w : List Bool) : Bool := decide (encB (D.decode w) = w) + have hreenc : ComputableInPolyTime (fun b : β => (encB b : List Bool)) encB encBits := + ComputableInPolyTime.id'.of_enc_eq fun _ => rfl + have hisCan : ComputableInPolyTime isCan encBits encBool := + ((hreenc.comp D.computableInPolyTime).tidy.decide_eq' .id').computableInPolyTime + have hg_ps : ComputableInPolySpace g encB encBool := by + obtain ⟨c, htm, hout⟩ := hg + exact ComputableInPolySpace.of_inSpace hS ⟨_, c, htm, hout⟩ + have hdecB_ps : ComputableInPolySpace (fun w : List Bool => + if isCan w then g (D.decode w) else false) encBits encBool := + ComputableInPolySpace.ite (ComputableInPolySpace.of_polyTime hisCan) + (hg_ps.comp (ComputableInPolySpace.of_polyTime D.computableInPolyTime)) + (ComputableInPolySpace.of_polyTime (.const false)) + have hsingleton : ComputableInPolySpace (fun b : Bool => [b]) encBool encBits := + ComputableInPolySpace.of_polyTime (ComputableInPolyTime.id'.of_enc_eq fun b => + (encBool_apply b).symm) + have horacle_eq : encodedDecisionOracle encB B = + fun w => [if isCan w then g (D.decode w) else false] := by + funext w + simp only [encodedDecisionOracle, languageOracle] + congr 1 + by_cases hc : isCan w = true + · simp only [hc, ↓reduceIte] + have hcan : encB (D.decode w) = w := of_decide_eq_true hc + have hmem : w ∈ encB '' B ↔ D.decode w ∈ B := by + conv_lhs => rw [← hcan] + exact encB.injective.mem_set_image + exact Bool.eq_iff_iff.mpr ⟨fun h => (hgB _).mp (hmem.mp (of_decide_eq_true h)), + fun h => decide_eq_true (hmem.mpr ((hgB _).mpr h))⟩ + · have hnc : isCan w = false := Bool.eq_false_iff.mpr hc + simp only [hnc, Bool.false_eq_true, ↓reduceIte] + have hnotmem : w ∉ encB '' B := by + rintro ⟨b, _, rfl⟩ + have : isCan (encB b) = true := by simp [isCan, D.decode_enc] + rw [this] at hnc + exact Bool.noConfusion hnc + simp [hnotmem] + have horacle : ComputableInPolySpace (encodedDecisionOracle encB B) encBits encBits := by + rw [horacle_eq] + exact hsingleton.comp hdecB_ps + have hf_ps := R.toProgram.computableInPolySpace horacle + exact ⟨_, hf_ps, fun _ => by simp⟩ + +/-! ### Parameterized exponential and subexponential oracle transfer -/ + +/-- Internal simulator state pairing a fixed parameter budget `budget = scale * μA a + offset` +with the live `FiniteConfig` of the deterministic oracle machine. -/ +private structure GuardedOracleState (k m : ℕ) where + budget : ℕ + cfg : Turing.MultiTapeMachine.FiniteConfig k Bool (Fin m) Unit + +private noncomputable def encGuardedOracleState {k m : ℕ} : + GuardedOracleState k m ↪ List Bool where + toFun s := encPair encNat encFiniteConfig (s.budget, s.cfg) + inj' s₁ s₂ h := by + have hp := (encPair encNat encFiniteConfig).injective h + cases s₁; cases s₂ + cases hp + rfl + +@[simp] +private theorem encGuardedOracleState_apply {k m : ℕ} (s : GuardedOracleState k m) : + encGuardedOracleState s = encPair encNat encFiniteConfig (s.budget, s.cfg) := rfl + +private theorem guardedOracleState_parts {k m : ℕ} : + ComputableInPolyTime (fun s : GuardedOracleState k m => (s.budget, s.cfg)) + encGuardedOracleState (encPair encNat encFiniteConfig) := + (ComputableInPolyTime.id' (encIn := encGuardedOracleState)).of_enc_eq fun _ => rfl + +private theorem computableInPolyTime_guardedBudget {k m : ℕ} : + ComputableInPolyTime (GuardedOracleState.budget (k := k) (m := m)) + encGuardedOracleState encNat := + guardedOracleState_parts.fst' + +private theorem computableInPolyTime_guardedCfg {k m : ℕ} : + ComputableInPolyTime (GuardedOracleState.cfg (k := k) (m := m)) + encGuardedOracleState encFiniteConfig := + guardedOracleState_parts.snd' + +private theorem computableInPolyTime_guardedMk {k m : ℕ} {ι : Type} {encI : ι ↪ List Bool} + {fb : ι → ℕ} {fc : ι → Turing.MultiTapeMachine.FiniteConfig k Bool (Fin m) Unit} + (hb : ComputableInPolyTime fb encI encNat) + (hc : ComputableInPolyTime fc encI encFiniteConfig) : + ComputableInPolyTime (fun x => GuardedOracleState.mk (fb x) (fc x)) + encI encGuardedOracleState := + (hb.prod hc).of_enc_eq fun _ => rfl + +/-- **Parameterized exponential-time transfer across `BoundedOracleReduction`:** +when `D : Decoder encB` decodes canonical `encB`-words in polynomial time, `μA` and `μB` are +polynomial-time computable, and every query `q` issued by `R.program a` against `encB '' B` +with `encB b = q.2` satisfies `μB b ≤ scale * μA a + offset`, any `2 ^ (δ * μB b) * poly(|b|)` +decider for `B` transfers to a `2 ^ ((scale * δ) * μA a) * poly(|a|)` decider for `A` — with +polynomial overhead absorbing both query count and query construction cost. -/ +theorem decidableInExpTime {A : Set α} {B : Set β} {μA : α → ℕ} {μB : β → ℕ} + (D : Decoder encB) + (R : BoundedOracleReduction encA encB A B) + {scale offset : ℕ} + (hμA : ComputableInPolyTime μA encA encNat) + (hμB : ComputableInPolyTime μB encB encNat) + (hparam : ∀ a q, + q ∈ OracleComp.queriesWith (languageOracle (encB '' B)) (R.program a) → + ∀ b, encB b = q.2 → μB b ≤ scale * μA a + offset) + {δ : ℝ} (hδ : 0 ≤ δ) (hB : DecidableInExpTime B encB μB δ) : + DecidableInExpTime A encA μA (scale * δ) := by + classical + obtain ⟨e, h⟩ := hB + obtain ⟨g, t, k_cost, hg, hgB, ht⟩ := h.exists_computableInO + obtain ⟨k_tm, m_tm, machine, c_clk, d_clk, hrun⟩ := R.isOraclePPTOn.exists_fin_run_pure_false + let _ : Inhabited β := ⟨D.decode []⟩ + let _ : Inhabited (GuardedOracleState k_tm m_tm) := + ⟨⟨0, Turing.MultiTapeMachine.FiniteConfig.init machine.initial []⟩⟩ + let isCan (w : List Bool) : Bool := decide (encB (D.decode w) = w) + have hreenc : ComputableInPolyTime (fun b : β => (encB b : List Bool)) encB encBits := + ComputableInPolyTime.id'.of_enc_eq fun _ => rfl + have hisCan : ComputableInPolyTime isCan encBits encBool := + ((hreenc.comp D.computableInPolyTime).tidy.decide_eq' .id').computableInPolyTime + let guardAns (K : ℕ) (w : List Bool) : Bool := + if isCan w && decide (μB (D.decode w) ≤ K) then g (D.decode w) else false + let stepGuard (s : GuardedOracleState k_tm m_tm) : GuardedOracleState k_tm m_tm := + ⟨s.budget, machine.answerStep (fun q => [guardAns s.budget q.2]) s.cfg⟩ + let isActive (s : GuardedOracleState k_tm m_tm) : Bool := + (machine.pendingQuery s.cfg).isSome && + (isCan (machine.pendingRequest s.cfg) && + decide (μB (D.decode (machine.pendingRequest s.cfg)) ≤ s.budget)) + let subinst (s : GuardedOracleState k_tm m_tm) : β := + D.decode (machine.pendingRequest s.cfg) + let localStep (s : GuardedOracleState k_tm m_tm) : GuardedOracleState k_tm m_tm := + ⟨s.budget, machine.answerStep (fun _ => [false]) s.cfg⟩ + let combine (p : GuardedOracleState k_tm m_tm × Bool) : GuardedOracleState k_tm m_tm := + ⟨p.1.budget, machine.receiveWord (p.1.cfg, [p.2])⟩ + have hstep_eq (s : GuardedOracleState k_tm m_tm) : + stepGuard s = + (if false then s else if isActive s then combine (s, g (subinst s)) else localStep s) := by + rcases s with ⟨K, cfg⟩ + dsimp only [stepGuard, isActive, subinst, combine, localStep] + rw [machine.answerStep_word (fun w => [guardAns K w]) cfg, + machine.answerStep_word (fun _ => [false]) cfg] + by_cases hpq : (machine.pendingQuery cfg).isSome = true + · simp only [hpq, ↓reduceIte, Bool.true_and, Bool.false_eq_true, guardAns] + by_cases hc : (isCan (machine.pendingRequest cfg) && + decide (μB (D.decode (machine.pendingRequest cfg)) ≤ K)) = true + · simp only [hc, ↓reduceIte] + · have hnc : (isCan (machine.pendingRequest cfg) && + decide (μB (D.decode (machine.pendingRequest cfg)) ≤ K)) = false := + Bool.eq_false_iff.mpr hc + simp only [hnc, Bool.false_eq_true, ↓reduceIte] + · have hnpq : (machine.pendingQuery cfg).isSome = false := Bool.eq_false_iff.mpr hpq + simp only [hnpq, Bool.false_eq_true, Bool.false_and, ↓reduceIte] + -- Polynomial-time certificates for all local pieces of `stepGuard`. + have hcfg_pt := computableInPolyTime_guardedCfg (k := k_tm) (m := m_tm) + have hbud_pt := computableInPolyTime_guardedBudget (k := k_tm) (m := m_tm) + have hpend_pt : ComputableInPolyTime + (fun s : GuardedOracleState k_tm m_tm => machine.pendingRequest s.cfg) + encGuardedOracleState encBits := + machine.pendingRequest_pt.comp hcfg_pt + have hsubinst_pt : ComputableInPolyTime subinst encGuardedOracleState encB := + D.computableInPolyTime.comp hpend_pt + have hisSome_pt : ComputableInPolyTime + (fun s : GuardedOracleState k_tm m_tm => (machine.pendingQuery s.cfg).isSome) + encGuardedOracleState encBool := + ((ComputableInPolyTime.of_finite Option.isSome).comp machine.pendingQuery_pt).comp hcfg_pt + have hle_pt : ComputableInPolyTime + (fun s : GuardedOracleState k_tm m_tm => decide (μB (subinst s) ≤ s.budget)) + encGuardedOracleState encBool := + ((hμB.comp hsubinst_pt).tidy.binary_le' hbud_pt.tidy).computableInPolyTime + have hisActive_pt : ComputableInPolyTime isActive encGuardedOracleState encBool := by + have hand2 := ComputableTidilyInPolyTime.bool_and.comp + (((hisCan.comp hpend_pt).tidy).prod hle_pt.tidy) + exact (ComputableTidilyInPolyTime.bool_and.comp + (hisSome_pt.tidy.prod hand2)).computableInPolyTime + have hlocal_pt : ComputableInPolyTime localStep encGuardedOracleState encGuardedOracleState := + computableInPolyTime_guardedMk hbud_pt + ((machine.computableInPolyTime_answerStep_word (.const [false])).comp hcfg_pt) + have hcombine_pt : ComputableInPolyTime combine + (encPair encGuardedOracleState encBool) encGuardedOracleState := by + have hp1 : ComputableInPolyTime (fun p : GuardedOracleState k_tm m_tm × Bool => p.1) + (encPair encGuardedOracleState encBool) encGuardedOracleState := .fst _ _ + have hp2_word : ComputableInPolyTime (fun p : GuardedOracleState k_tm m_tm × Bool => [p.2]) + (encPair encGuardedOracleState encBool) encBits := + (ComputableInPolyTime.snd encGuardedOracleState encBool).of_enc_eq (encD := encBits) + fun p => (encBool_apply p.2).symm + exact computableInPolyTime_guardedMk (hbud_pt.comp hp1) + (machine.receiveWord_pt.comp ((hcfg_pt.comp hp1).prod hp2_word)) + obtain ⟨d_step, hstep_inO⟩ := exists_computableInO_searchStep + (done := fun _ : GuardedOracleState k_tm m_tm => false) + (.const false) hisActive_pt hsubinst_pt hlocal_pt hcombine_pt hg + have hstep : ComputableInO stepGuard encGuardedOracleState encGuardedOracleState + (fun s => ((encGuardedOracleState s).length + 1) ^ d_step + + if isActive s then + t (subinst s) + + ((encGuardedOracleState s).length + (encBool (g (subinst s))).length + 1) ^ d_step + else 0) + (fun s => ((encGuardedOracleState s).length + 1) ^ d_step + + if isActive s then + t (subinst s) + + ((encGuardedOracleState s).length + (encBool (g (subinst s))).length + 1) ^ d_step + else 0) := by + refine (hstep_inO.mono_le (fun _ => ?_) (fun _ => ?_)).of_enc_eq fun s => ?_ + · simp only [true_and] + exact le_rfl + · simp only [true_and] + exact le_rfl + · rw [hstep_eq s] + -- Initial state, iteration count, and final decision bit. + let K (a : α) : ℕ := scale * μA a + offset + let clk (a : α) : ℕ := c_clk * ((encA a).length + 1) ^ d_clk + let initSt (a : α) : GuardedOracleState k_tm m_tm := + ⟨K a, Turing.MultiTapeMachine.FiniteConfig.init machine.initial (encA a)⟩ + have hK_pt : ComputableInPolyTime K encA encNat := by + have hsc : ComputableTidilyInPolyTime (fun _ : α => scale) encA encNat := .const scale + have hof : ComputableTidilyInPolyTime (fun _ : α => offset) encA encNat := .const offset + exact ((hsc.binary_mul' hμA.tidy).binary_add' hof).computableInPolyTime + have hinit_cfg_pt : ComputableInPolyTime + (fun a : α => + Turing.MultiTapeMachine.FiniteConfig.init (k := k_tm) (Oracle := Unit) + machine.initial (encA a)) + encA encFiniteConfig := + (ComputableTidilyInPolyTime.finiteConfig_init (by fun_prop) _).computableInPolyTime + have hinit_pt : ComputableInPolyTime initSt encA encGuardedOracleState := + computableInPolyTime_guardedMk hK_pt hinit_cfg_pt + let pClk : Polynomial ℕ := Polynomial.C c_clk * (Polynomial.X + 1) ^ d_clk + have hclk_pt : ComputableInPolyTime clk encA encNat := + ComputableTidilyInPolyTime.computableInPolyTime <| + ((ComputableTidilyInPolyTime.unary_to_binary.comp + ((ComputableTidilyInPolyTime.unary_eval pClk).comp + (ComputableTidilyInPolyTime.encoding_length encA)))).of_enc_eq + fun a => by simp [clk, pClk] + have hout_raw : ComputableTidilyInPolyTime + (fun cfg : Turing.MultiTapeMachine.FiniteConfig k_tm Bool (Fin m_tm) Unit => + cfg.tapes.output) + encFiniteConfig encBits := by fun_prop + have hout_pt : ComputableInPolyTime + (fun s : GuardedOracleState k_tm m_tm => s.cfg.tapes.output.headD false) + encGuardedOracleState encBool := + Decoder.bool.computableInPolyTime.comp (hout_raw.computableInPolyTime.comp hcfg_pt) + -- Track `stepGuard^[i] (initSt a)` and its `FiniteConfig.SpaceBound`. + have hiter_eq (a : α) (i : ℕ) : + stepGuard^[i] (initSt a) = + ⟨K a, (machine.answerStep (fun q => [guardAns (K a) q.2]))^[i] + (Turing.MultiTapeMachine.FiniteConfig.init machine.initial (encA a))⟩ := by + induction i with + | zero => rfl + | succ i ih => rw [Function.iterate_succ_apply', Function.iterate_succ_apply', ih] + have hspace (a : α) {i : ℕ} (hi : i ≤ clk a) : + Turing.MultiTapeMachine.FiniteConfig.SpaceBound (encA a).length i 1 + ((machine.answerStep (fun q => [guardAns (K a) q.2]))^[i] + (Turing.MultiTapeMachine.FiniteConfig.init machine.initial (encA a))) := by + induction i with + | zero => + exact (Turing.MultiTapeMachine.FiniteConfig.spaceBound_init _ _ 0).mono + le_rfl le_rfl (Nat.zero_le _) + | succ i ih => + rw [Function.iterate_succ_apply'] + exact machine.spaceBound_answerStep_word (fun w => [guardAns (K a) w]) + (ih (Nat.le_of_succ_le hi)) fun _ _ => le_rfl + obtain ⟨cf, hcf⟩ := + length_encFiniteConfig_le (k := k_tm) (State := Fin m_tm) (Oracle := Unit) + obtain ⟨cK, dK, hK_len⟩ := hK_pt.polyBounded_length.exists_le + let stateBound (a : α) : ℕ := + 2 * (cK * ((encA a).length + 1) ^ dK) + 1 + + cf * ((encA a).length + clk a + 2) + have hstate (a : α) (i : ℕ) (hi : i ≤ clk a) : + (encGuardedOracleState (stepGuard^[i] (initSt a))).length ≤ stateBound a := by + rw [hiter_eq] + have hcfg_len : (encFiniteConfig + ((machine.answerStep (fun q => [guardAns (K a) q.2]))^[i] + (Turing.MultiTapeMachine.FiniteConfig.init machine.initial (encA a)))).length ≤ + cf * ((encA a).length + clk a + 2) := + (hcf _ _ _ _ (hspace a hi)).trans (Nat.mul_le_mul_left cf (by omega)) + have hk_len := hK_len a + simp only [encGuardedOracleState_apply, length_encPair] + dsimp only [stateBound] + omega + -- Bound `t (subinst st)` on every active step using `isCan` and `μB ≤ K a`. + let leafMax (a : α) : ℕ := + ⌈(k_cost : ℝ) * (2 ^ (δ * (K a : ℝ)) * ((clk a : ℝ) + 1) ^ e) + k_cost⌉₊ + have htime (a : α) (i : ℕ) (hi : i ≤ clk a) : + isActive (stepGuard^[i] (initSt a)) = true → + t (subinst (stepGuard^[i] (initSt a))) ≤ leafMax a := by + intro hact + set st := stepGuard^[i] (initSt a) + have hst_eq : st = ⟨K a, (machine.answerStep (fun q => [guardAns (K a) q.2]))^[i] + (Turing.MultiTapeMachine.FiniteConfig.init machine.initial (encA a))⟩ := hiter_eq a i + dsimp only [isActive] at hact + rcases Bool.and_eq_true_iff.mp hact with ⟨_, hrest⟩ + rcases Bool.and_eq_true_iff.mp hrest with ⟨hcan_b, hle_b⟩ + have hcan : encB (subinst st) = machine.pendingRequest st.cfg := of_decide_eq_true hcan_b + have hμ_le : μB (subinst st) ≤ K a := by + have hle' : μB (subinst st) ≤ st.budget := of_decide_eq_true hle_b + simpa only [hst_eq] using hle' + have hreq_len : (encB (subinst st)).length ≤ clk a := by + rw [hcan, hst_eq] + exact (machine.length_pendingRequest_le (hspace a hi)).trans hi + have hexp : (2 : ℝ) ^ (δ * μB (subinst st)) ≤ 2 ^ (δ * (K a : ℝ)) := + Real.rpow_le_rpow_of_exponent_le (by norm_num) + (mul_le_mul_of_nonneg_left (by exact_mod_cast hμ_le) hδ) + have hpow : (((encB (subinst st)).length : ℝ) + 1) ^ e ≤ ((clk a : ℝ) + 1) ^ e := by gcongr + refine Nat.cast_le.mp ((ht (subinst st)).trans ((?_ : _ ≤ _).trans (Nat.le_ceil _))) + gcongr + -- Assemble the `ComputableInO.iterate` decider and absorb polynomial overhead. + obtain ⟨dn, _, hn⟩ := hclk_pt.exists_degree + obtain ⟨di, _, hi_deg⟩ := hinit_pt.exists_degree + obtain ⟨da, _, ha_deg⟩ := hout_pt.exists_degree + let stepPoly (a : α) : ℕ := (stateBound a + 1) ^ d_step + (stateBound a + 2) ^ d_step + have hround (a : α) (i : ℕ) (hi : i ≤ clk a) : + ((encGuardedOracleState (stepGuard^[i] (initSt a))).length + 1) ^ d_step + + (if isActive (stepGuard^[i] (initSt a)) then + t (subinst (stepGuard^[i] (initSt a))) + + ((encGuardedOracleState (stepGuard^[i] (initSt a))).length + + (encBool (g (subinst (stepGuard^[i] (initSt a))))).length + 1) ^ d_step + else 0) ≤ stepPoly a + leafMax a := by + set st := stepGuard^[i] (initSt a) + have hst : (encGuardedOracleState st).length ≤ stateBound a := hstate a i hi + have hp1 := Nat.pow_le_pow_left (Nat.add_le_add_right hst 1) d_step + split_ifs with hact + · have ht_le : t (subinst st) ≤ leafMax a := htime a i hi hact + have hp2 : ((encGuardedOracleState st).length + + (encBool (g (subinst st))).length + 1) ^ d_step ≤ + (stateBound a + 2) ^ d_step := by + simp only [encBool_apply, List.length_singleton] + exact Nat.pow_le_pow_left (by omega) d_step + dsimp only [stepPoly] + omega + · dsimp only [stepPoly] + omega + have hloop := ha_deg.inO.comp (ComputableInO.iterate hn.inO hi_deg.inO hstep hround hround + fun a i hi => hstate a i hi) + have hdecides_loop (a : α) : + a ∈ A ↔ (stepGuard^[clk a] (initSt a)).cfg.tapes.output.headD false = true := by + let ans_a : Unit × List Bool → List Bool := fun q => [guardAns (K a) q.2] + have hcongr : OracleComp.interpret (m := Id) ans_a (R.program a) = + OracleComp.interpret (m := Id) (languageOracle (encB '' B)) (R.program a) := by + refine (OracleComp.interpret_id_congr (languageOracle (encB '' B)) ans_a + (R.program a) ?_).1 + intro q hq + dsimp only [ans_a, languageOracle] + congr 1 + by_cases hmem : q.2 ∈ encB '' B + · rcases hmem with ⟨b, hbB, hb_eq⟩ + have hdec_b : D.decode q.2 = b := by rw [← hb_eq, D.decode_enc] + have hcan_q : isCan q.2 = true := by simp [isCan, hdec_b, hb_eq] + have hμ_q : μB b ≤ K a := hparam a q hq b hb_eq + have hle_q : decide (μB b ≤ K a) = true := decide_eq_true hμ_q + simp only [guardAns, hcan_q, hdec_b, hle_q, Bool.and_self, ↓reduceIte] + have hmem' : q.2 ∈ encB '' B := ⟨b, hbB, hb_eq⟩ + simp only [hmem', decide_true] + exact (hgB b).mp hbB + · simp only [hmem, decide_false] + by_cases hcond : (isCan q.2 && decide (μB (D.decode q.2) ≤ K a)) = true + · simp only [guardAns, hcond, ↓reduceIte] + rcases Bool.and_eq_true_iff.mp hcond with ⟨hcan_q, _⟩ + have hcan_eq : encB (D.decode q.2) = q.2 := of_decide_eq_true hcan_q + have hnotB : D.decode q.2 ∉ B := fun hb => hmem ⟨D.decode q.2, hb, hcan_eq⟩ + exact Bool.eq_false_iff.mpr fun hgb => hnotB ((hgB _).mpr hgb) + · have hnc : (isCan q.2 && decide (μB (D.decode q.2) ≤ K a)) = false := + Bool.eq_false_iff.mpr hcond + simp only [guardAns, hnc, Bool.false_eq_true, ↓reduceIte] + have hm_out : ((machine.answerStep ans_a)^[clk a] + (Turing.MultiTapeMachine.FiniteConfig.init machine.initial (encA a))).tapes.output = + encBool (OracleComp.interpret (m := Id) (languageOracle (encB '' B)) (R.program a)) := by + rw [← hcongr, ← hrun a ans_a, ← machine.interpret_run_pure_false] + rw [hiter_eq a (clk a)] + dsimp only + change a ∈ A ↔ (((machine.answerStep ans_a)^[clk a] + (Turing.MultiTapeMachine.FiniteConfig.init machine.initial (encA a))).tapes.output).headD + false = true + rw [hm_out, encBool_apply, List.headD_cons] + exact R.decides a + let clockLen (a : α) : ℕ := (encNat (clk a)).length + have hclkLen (a : α) : clockLen a ≤ clk a + 1 := by + dsimp only [clockLen] + rw [encNat_apply, Nat.size_eq_bits_len] + exact (Nat.size_le.mpr Nat.lt_two_pow_self).trans (Nat.le_succ _) + have hpoly : PolyBounded (fun a => (encA a).length) + (fun a => ((encA a).length + 1) ^ dn + ((encA a).length + 1) ^ di + + (stateBound a + 1) ^ da + + (clk a + 1) * (stepPoly a + stateBound a + (clk a + 1 + 1) ^ 2 + + (clk a + 1) ^ e + 1)) := by + dsimp only [stepPoly, stateBound, clk] + growth_poly + obtain ⟨Cp, E, hCp⟩ := hpoly.exists_le + set C_big : ℝ := Cp + Cp * (k_cost * 2 ^ (δ * offset) + (k_cost + 1)) + refine DecidableInExpTime.of_computableInO hloop hdecides_loop ⌈C_big⌉₊ E fun a => ?_ + have hCp_a := hCp a + have hfin_da : ((encGuardedOracleState (stepGuard^[clk a] (initSt a))).length + 1) ^ da ≤ + (stateBound a + 1) ^ da := + Nat.pow_le_pow_left (Nat.add_le_add_right (hstate a (clk a) le_rfl) 1) da + have hcl2 := Nat.pow_le_pow_left (Nat.add_le_add_right (hclkLen a) 1) 2 + set P : ℝ := (((encA a).length : ℝ) + 1) ^ E + set Y : ℝ := (2 : ℝ) ^ ((scale * δ) * μA a) + have hP1 : 1 ≤ P := one_le_pow₀ (le_add_of_nonneg_left (Nat.cast_nonneg _)) + have hY1 : 1 ≤ Y := Real.one_le_rpow (by norm_num) (by positivity) + have hleaf_bound : (leafMax a : ℝ) ≤ + (k_cost * 2 ^ (δ * offset)) * Y * (((clk a : ℝ) + 1) ^ e) + (k_cost + 1) := by + have hceil : (leafMax a : ℝ) < + (k_cost : ℝ) * (2 ^ (δ * (K a : ℝ)) * ((clk a : ℝ) + 1) ^ e) + k_cost + 1 := + Nat.ceil_lt_add_one (by positivity) + have hexp_split : (2 : ℝ) ^ (δ * (K a : ℝ)) = 2 ^ (δ * offset) * Y := by + dsimp only [K, Y] + push_cast + rw [← Real.rpow_add (by norm_num : (0 : ℝ) < 2)] + congr 1 + ring + rw [hexp_split] at hceil + linarith + have hbase_le : (((encA a).length + 1) ^ dn + ((encA a).length + 1) ^ di + + ((encGuardedOracleState (stepGuard^[clk a] (initSt a))).length + 1) ^ da + + (clk a + 1) * (stepPoly a + stateBound a + (clockLen a + 1) ^ 2) : ℝ) ≤ Cp * P := by + have hnat : ((encA a).length + 1) ^ dn + ((encA a).length + 1) ^ di + + ((encGuardedOracleState (stepGuard^[clk a] (initSt a))).length + 1) ^ da + + (clk a + 1) * (stepPoly a + stateBound a + (clockLen a + 1) ^ 2) ≤ + Cp * ((encA a).length + 1) ^ E := by + have hmul_le : (clk a + 1) * (stepPoly a + stateBound a + (clockLen a + 1) ^ 2) ≤ + (clk a + 1) * (stepPoly a + stateBound a + (clk a + 1 + 1) ^ 2 + + (clk a + 1) ^ e + 1) := + Nat.mul_le_mul_left _ (by omega) + omega + dsimp only [P] + exact_mod_cast hnat + have hclk_pow_le : ((clk a : ℝ) + 1) * (((clk a : ℝ) + 1) ^ e) ≤ Cp * P := by + have hnat : (clk a + 1) * ((clk a + 1) ^ e) ≤ Cp * ((encA a).length + 1) ^ E := by + have hmul_le : (clk a + 1) * ((clk a + 1) ^ e) ≤ + (clk a + 1) * (stepPoly a + stateBound a + (clk a + 1 + 1) ^ 2 + + (clk a + 1) ^ e + 1) := + Nat.mul_le_mul_left _ (by omega) + omega + dsimp only [P] + exact_mod_cast hnat + have hclk_le : ((clk a : ℝ) + 1) ≤ Cp * P := by + have hnat : clk a + 1 ≤ Cp * ((encA a).length + 1) ^ E := by + have hmul_le : (clk a + 1) * 1 ≤ + (clk a + 1) * (stepPoly a + stateBound a + (clk a + 1 + 1) ^ 2 + + (clk a + 1) ^ e + 1) := + Nat.mul_le_mul_left _ (by omega) + omega + dsimp only [P] + exact_mod_cast hnat + have htot : (((((encA a).length + 1) ^ dn + ((encA a).length + 1) ^ di + + (clk a + 1) * (stepPoly a + leafMax a + stateBound a + (clockLen a + 1) ^ 2) + + ((encGuardedOracleState (stepGuard^[clk a] (initSt a))).length + 1) ^ da : ℕ) : ℝ)) ≤ + C_big * (Y * P) := by + have hmul_leaf : ((clk a : ℝ) + 1) * (leafMax a : ℝ) ≤ + Cp * (k_cost * 2 ^ (δ * offset)) * (Y * P) + Cp * (k_cost + 1) * P := by + have h1 : ((clk a : ℝ) + 1) * (leafMax a : ℝ) ≤ + ((clk a : ℝ) + 1) * + ((k_cost * 2 ^ (δ * offset)) * Y * (((clk a : ℝ) + 1) ^ e) + (k_cost + 1)) := + mul_le_mul_of_nonneg_left hleaf_bound (by positivity) + have h2 : (k_cost * 2 ^ (δ * offset)) * Y * (((clk a : ℝ) + 1) * (((clk a : ℝ) + 1) ^ e)) ≤ + (k_cost * 2 ^ (δ * offset)) * Y * (Cp * P) := + mul_le_mul_of_nonneg_left hclk_pow_le (by positivity) + have h3 : (k_cost + 1 : ℝ) * ((clk a : ℝ) + 1) ≤ (k_cost + 1 : ℝ) * (Cp * P) := + mul_le_mul_of_nonneg_left hclk_le (by positivity) + linarith + have hYP : P ≤ Y * P := le_mul_of_one_le_left (by positivity) hY1 + have hbase_YP : (Cp : ℝ) * P ≤ Cp * (Y * P) := mul_le_mul_of_nonneg_left hYP (by positivity) + have hk_YP : Cp * (k_cost + 1 : ℝ) * P ≤ Cp * (k_cost + 1 : ℝ) * (Y * P) := + mul_le_mul_of_nonneg_left hYP (by positivity) + dsimp only [C_big, clockLen] at hbase_le hmul_leaf ⊢ + push_cast at hbase_le ⊢ + linarith + exact htot.trans (mul_le_mul_of_nonneg_right (Nat.le_ceil C_big) (by positivity)) + +/-- **Parameterized subexponential-time transfer across `BoundedOracleReduction`.** -/ +theorem decidableInSubexpTime {A : Set α} {B : Set β} {μA : α → ℕ} {μB : β → ℕ} + (D : Decoder encB) + (R : BoundedOracleReduction encA encB A B) + {scale offset : ℕ} + (hμA : ComputableInPolyTime μA encA encNat) + (hμB : ComputableInPolyTime μB encB encNat) + (hparam : ∀ a q, + q ∈ OracleComp.queriesWith (languageOracle (encB '' B)) (R.program a) → + ∀ b, encB b = q.2 → μB b ≤ scale * μA a + offset) + (hB : DecidableInSubexpTime B encB μB) : + DecidableInSubexpTime A encA μA := by + intro ε hε + set δ : ℝ := ε / (scale + 1) + have hδ : 0 < δ := by positivity + refine (R.decidableInExpTime D hμA hμB hparam hδ.le (hB δ hδ)).mono ?_ + dsimp only [δ] + rw [mul_div_assoc', div_le_iff₀ (by positivity)] + nlinarith + +end BoundedOracleReduction + +end Cslib.Complexity diff --git a/CslibFrontierTests/DisjointInstancesAndOracleReduction.lean b/CslibFrontierTests/DisjointInstancesAndOracleReduction.lean new file mode 100644 index 0000000000..1f9d4b69d1 --- /dev/null +++ b/CslibFrontierTests/DisjointInstancesAndOracleReduction.lean @@ -0,0 +1,496 @@ +/- +Copyright (c) 2026 Samuel Schlesinger. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Samuel Schlesinger +-/ + +module +-- upstream: local-only (test driver) + +public import CslibFrontier.Computability.Complexity.FineGrained.DisjointInstances +public import CslibFrontier.Computability.Complexity.Reduction.BoundedOracle +import CslibFrontier.Computability.Machines.Turing.MultiTape.Complexity.PolyTime.BitString +import CslibFrontier.Computability.Machines.Turing.MultiTape.Complexity.PolyTime.List +import CslibFrontier.Computability.Machines.Turing.MultiTape.Complexity.PolyTime.Nat +import CslibFrontier.Computability.Machines.Turing.MultiTape.Complexity.PolyTime.Nat.Binary + +/-! +# Worked clients for `DisjointInstances` and `BoundedOracle` + +Kernel-checked strict-`module` examples (with no `import all`, `sorry`, `axiom`, or +`native_decide`) exercising: + +1. `SizeSensitiveReduction`: non-identity linear-parameter bit-duplication map, composition + multiplying scales, exponential/subexponential transfer, and polynomial-space preservation. +2. `InstanceBatch`, `CNFInstanceBatch` (`encCNFInstanceBatch`), `CappedNatAcc` (`encCappedNatAcc`), + and `DisjointBatchReduction`: empty, singleton, and multi-element batches, exact below-cap sums + versus clamped above-cap sums, disjoint CNF variable-measure aggregation, OR decision transfer, + and capped summed-counting transfer in polynomial live workspace. +3. `StackAccumulationSpec` and `BinaryBranching`: concrete depth-bounded binary branching tree + accumulating exact leaf counts `2 ^ d` via `CappedNatAcc` without materializing the leaf list. +4. `OracleCallBound` (`encOracleCallBound`), `BoundedOracleProgram` (on a genuine multi-bit word + oracle returning `w ++ [true]`), and `BoundedOracleReduction`: zero-query, single-query, + composed, and affine-total-length call profiles, bridges to `PolyTimeTuringReducible` and + `PWithOracleQueries`, and polynomial-time, polynomial-space, and parameterized exponential / + subexponential transfer. +-/ + +public section + +namespace CslibFrontierTests.DisjointInstancesAndOracleReduction + +open Cslib Cslib.Complexity Cslib.Logic.PL _root_.Turing _root_.Turing.MultiTapeTM + +/-! ### 1. `SizeSensitiveReduction` -/ + +/-- Concrete size-sensitive reduction duplicating a bit word (`|w ++ w| = 2 * |w|`). -/ +def dupBitsReduction : SizeSensitiveReduction encBits encBits List.length List.length where + toFun w := w ++ w + scale := 2 + offset := 0 + computableInPolyTime_toFun := + (ComputableTidilyInPolyTime.bitsAppend .id' .id').computableInPolyTime + measure_le w := by + simp only [List.length_append] + omega + +/-- Composing `dupBitsReduction` with itself produces scale `2 * 2 = 4` and maps `[true, false]` +to a word of length `8`. -/ +example : + (dupBitsReduction.trans dupBitsReduction).scale = 4 ∧ + (dupBitsReduction.trans dupBitsReduction).offset = 0 ∧ + ((dupBitsReduction.trans dupBitsReduction).toFun [true, false]).length = 8 ∧ + (SizeSensitiveReduction.refl encBits List.length).toFun [true] = [true] := by + refine ⟨rfl, by simp [SizeSensitiveReduction.trans, dupBitsReduction], ?_, rfl⟩ + decide + +/-- Exponential and polynomial-space transfer along `dupBitsReduction` on the nonempty-word +language (`w ≠ [] ↔ w ++ w ≠ []`). -/ +example {δ : ℝ} (hδ : 0 ≤ δ) + (hExp : DecidableInExpTime {w : List Bool | w ≠ []} encBits List.length δ) + (hPS : ComputableInPolySpace List.reverse encBits encBits) : + DecidableInExpTime {w : List Bool | w ≠ []} encBits List.length (2 * δ) ∧ + ComputableInPolySpace (fun w => (w ++ w).reverse) encBits encBits := by + have hiff (w : List Bool) : w ∈ {u : List Bool | u ≠ []} ↔ + dupBitsReduction.toFun w ∈ {u : List Bool | u ≠ []} := by + cases w <;> simp [dupBitsReduction] + have hexp' := dupBitsReduction.decidableInExpTime hiff hδ hExp + simp only [dupBitsReduction, Nat.cast_ofNat] at hexp' + exact ⟨hexp', dupBitsReduction.computableInPolySpace_comp hPS⟩ + +/-! ### 2. `InstanceBatch`, `CNFInstanceBatch`, `CappedNatAcc`, and `DisjointBatchReduction` -/ + +/-- `InstanceBatch`: empty, singleton, and multi-element `sumMeasure` and `maxMeasure` checks. -/ +example : + (InstanceBatch.nil : InstanceBatch (List Bool)).sumMeasure List.length = 0 ∧ + (InstanceBatch.nil : InstanceBatch (List Bool)).maxMeasure List.length = 0 ∧ + (InstanceBatch.singleton [true, false, true]).sumMeasure List.length = 3 ∧ + (⟨[[true], [false, true], [true, true, false]]⟩ : + InstanceBatch (List Bool)).sumMeasure List.length = 6 ∧ + (⟨[[true], [false, true], [true, true, false]]⟩ : + InstanceBatch (List Bool)).maxMeasure List.length = 3 := by + decide + +/-- `CappedNatAcc` (`encCappedNatAcc`): exact folding below cap (`2 + 3 + 4 = 9 ≤ 10`), clamping +above cap (`6 + 7 ↦ 10`), and polynomial-time `enc_structure` projections. -/ +example : + (((CappedNatAcc.init 10).add 2).add 3).add 4 = ⟨10, 9⟩ ∧ + (((CappedNatAcc.init 10).add 6).add 7) = ⟨10, 10⟩ ∧ + ([2, 3, 4].foldl CappedNatAcc.add (CappedNatAcc.init 10)).total = 9 ∧ + ([6, 7].foldl CappedNatAcc.add (CappedNatAcc.init 10)).total = 10 ∧ + ComputableInPolyTime CappedNatAcc.total encCappedNatAcc encNat ∧ + ComputableInPolyTime CappedNatAcc.cap encCappedNatAcc encNat := by + refine ⟨rfl, rfl, by decide, by decide, + encCappedNatAcc_total_polyTime .id', encCappedNatAcc_cap_polyTime .id'⟩ + +/-- `CNFInstanceBatch` (`encCNFInstanceBatch`): empty batch vs disjoint variable-splitting batch +`[[[(0, true)]], [[(0, false)]]]` over `2` declared variables. -/ +def emptyCNFBatch : CNFInstanceBatch := ⟨2, []⟩ +def singletonCNFBatch : CNFInstanceBatch := ⟨2, [[[(0, true)]]]⟩ +def splitCNFBatch : CNFInstanceBatch := ⟨2, [[[(0, true)]], [[(0, false)]]]⟩ + +example : + emptyCNFBatch.sumNumVars = 0 ∧ + singletonCNFBatch.sumNumVars = 1 ∧ + splitCNFBatch.sumNumVars = 2 ∧ + ComputableInPolyTime CNFInstanceBatch.declaredVars encCNFInstanceBatch encUnary ∧ + ComputableInPolyTime CNFInstanceBatch.formulas encCNFInstanceBatch (encList encCNF) := by + refine ⟨by decide, by decide, by decide, + encCNFInstanceBatch_declaredVars_polyTime .id', + encCNFInstanceBatch_formulas_polyTime .id'⟩ + +/-- Concrete 2-way word-splitting `DisjointBatchReduction` (`w ↦ [w.take 1, w.drop 1]`) whose +summed subinstance length equals `|w|` (`scale = 1`, `offset = 0`). -/ +def splitWordBatchReduction : + DisjointBatchReduction encBits encBits List.length List.length where + toBatch w := ⟨[w.take 1, w.drop 1]⟩ + scale := 1 + offset := 0 + computableInPolyTime_toBatch := by + have htake : ComputableTidilyInPolyTime (fun w : List Bool => w.take 1) encBits encBits := + ComputableTidilyInPolyTime.bitsTake.comp + (ComputableTidilyInPolyTime.id'.prod (.const 1)) + have hdrop : ComputableTidilyInPolyTime (fun w : List Bool => w.drop 1) encBits encBits := + ComputableTidilyInPolyTime.bitsDropWithInput .id' (.const 1) + have hlist : ComputableInPolyTime (fun w : List Bool => [w.take 1, w.drop 1]) + encBits (encList encBits) := + (ComputableTidilyInPolyTime.cons' htake + (ComputableTidilyInPolyTime.cons' hdrop (.const []))).computableInPolyTime + exact computableInPolyTime_instanceBatch_mk hlist + sumMeasure_le w := by + simp only [InstanceBatch.sumMeasure, List.map_cons, List.map_nil, List.sum_cons, + List.sum_nil, Nat.add_zero, one_mul] + have h := congrArg List.length (List.take_append_drop 1 w) + rw [List.length_append] at h + omega + +/-- Empty, singleton, and multi-bit behavior of `splitWordBatchReduction`, plus OR exponential +transfer (`{w | true ∈ w}`). -/ +example {δ : ℝ} (hδ : 0 ≤ δ) + (hExp : DecidableInExpTime {w : List Bool | true ∈ w} encBits List.length δ) : + (splitWordBatchReduction.toBatch []).sumMeasure List.length = 0 ∧ + (splitWordBatchReduction.toBatch [true]).sumMeasure List.length = 1 ∧ + (splitWordBatchReduction.toBatch [false, true, false]).sumMeasure List.length = 3 ∧ + DecidableInExpTime {w : List Bool | true ∈ w} encBits List.length δ := by + refine ⟨by decide, by decide, by decide, ?_⟩ + have hor : ∀ w : List Bool, + w ∈ {u : List Bool | true ∈ u} ↔ + ∃ sub ∈ (splitWordBatchReduction.toBatch w).items, + sub ∈ {u : List Bool | true ∈ u} := by + intro w + change (true ∈ w) ↔ + ∃ sub ∈ (splitWordBatchReduction.toBatch w).items, true ∈ sub + simp only [splitWordBatchReduction, List.mem_cons, + List.not_mem_nil, or_false] + conv_lhs => rw [← List.take_append_drop 1 w, List.mem_append] + constructor + · rintro (h | h) + · exact ⟨w.take 1, Or.inl rfl, h⟩ + · exact ⟨w.drop 1, Or.inr rfl, h⟩ + · rintro ⟨sub, rfl | rfl, h⟩ + · exact Or.inl h + · exact Or.inr h + have htr := splitWordBatchReduction.decidableInExpTime_or hor hδ hExp + simpa only [splitWordBatchReduction, Nat.cast_one, one_mul] using htr + +/-! ### 3. `StackAccumulationSpec` and `BinaryBranching` -/ + +/-- Complete binary branching tree of height `n` on countdown depth `s : ℕ`: `0` is a leaf, and +`s + 1` branches to `(s, s)`. -/ +@[expose] +def countdownBranching : BinaryBranching ℕ where + IsLeaf s := s = 0 + next s _ := s - 1 + +theorem countdownBranching_terminating : countdownBranching.Terminating := + BinaryBranching.Terminating.of_lt (T := countdownBranching) id fun s hs _ => by + change ¬(s = 0) at hs + change s - 1 < s + omega + +/-- Concrete `StackAccumulationSpec` traversing `countdownBranching` from depth `n` (given in +unary so `rounds n = 2 * 2 ^ n` has linear binary length) and summing `1` at every leaf into a +`CappedNatAcc` with cap `2 ^ n`. -/ +@[expose] +def countdownStackSpec : + StackAccumulationSpec encUnary (encFinEnum Unit) encNat encNat encNat encCappedNatAcc where + defaultNode := 0 + initCtx _ := () + initStack n := [n] + initAcc n := CappedNatAcc.init (2 ^ n) + rounds n := 2 * 2 ^ n + isLeaf p := decide (p.node = 0) + leafInstance p := p.node + expand p := [p.node - 1, p.node - 1] + combine p := p.acc.add p.leafVal + computableInPolyTime_initCtx := .const () + computableInPolyTime_initStack := by + exact (ComputableTidilyInPolyTime.cons' ComputableTidilyInPolyTime.unary_to_binary + (.const [])).computableInPolyTime + computableInPolyTime_initAcc := by + exact CappedNatAcc.computableInPolyTime_init + ComputableTidilyInPolyTime.binary_two_pow.computableInPolyTime + computableInPolyTime_rounds := by + have hpow := ComputableTidilyInPolyTime.binary_two_pow + exact ((ComputableTidilyInPolyTime.const 2).binary_mul' hpow).computableInPolyTime + computableInPolyTime_isLeaf := by + have hnd := computableInPolyTime_stackNodeInput_node + (encK := encFinEnum Unit) (encS := encNat) .id' + exact (hnd.tidy.decide_eq' (.const 0)).computableInPolyTime + computableInPolyTime_leafInstance := + computableInPolyTime_stackNodeInput_node (encK := encFinEnum Unit) (encS := encNat) .id' + computableInPolyTime_expand := by + have hnd := computableInPolyTime_stackNodeInput_node + (encK := encFinEnum Unit) (encS := encNat) .id' + have hsub := hnd.tidy.binary_sub' (.const 1) + exact (ComputableTidilyInPolyTime.cons' hsub + (ComputableTidilyInPolyTime.cons' hsub (.const []))).computableInPolyTime + computableInPolyTime_combine := by + have hacc := computableInPolyTime_stackCombineInput_acc + (encK := encFinEnum Unit) (encD := encCappedNatAcc) (encG := encNat) .id' + have hlv := computableInPolyTime_stackCombineInput_leafVal + (encK := encFinEnum Unit) (encD := encCappedNatAcc) (encG := encNat) .id' + exact (CappedNatAcc.computableInPolyTime_add.comp (hacc.prod hlv)).of_enc_eq fun _ => rfl + +private theorem countdownBranching_leafWord_length_le (s : ℕ) (w : List Bool) + (hw : countdownBranching.IsLeafWord s w) : w.length ≤ s := by + induction w generalizing s with + | nil => exact Nat.zero_le s + | cons b ws ih => + obtain ⟨hnot, htail⟩ := hw + change ¬(s = 0) at hnot + have hsub := ih (s - 1) htail + simp only [List.length_cons] + omega + +private theorem countdownStackSpec_rounds_sufficient (n : ℕ) + (L : List (List Bool)) (hnd : L.Nodup) + (hL : ∀ w, w ∈ L ↔ countdownBranching.IsLeafWord n w) : + 2 * L.length ≤ countdownStackSpec.rounds n + 1 := by + have hcard : L.toFinset.card ≤ ∑ j ∈ Finset.range (n + 1), n.choose j := + countdownBranching.card_le_sum_choose_of_isLeafWord + (fun w hw => (hL w).mp (List.mem_toFinset.mp hw)) + (fun w hw => countdownBranching_leafWord_length_le n w + ((hL w).mp (List.mem_toFinset.mp hw))) + (fun w hw => (Finset.card_filter_le _ _).trans (by + rw [Finset.card_range] + exact countdownBranching_leafWord_length_le n w + ((hL w).mp (List.mem_toFinset.mp hw)))) + rw [Nat.sum_range_choose, List.toFinset_card_of_nodup hnd] at hcard + change 2 * L.length ≤ 2 * 2 ^ n + 1 + omega + +/-- Exact proof for ALL `n : ℕ` via `StackAccumulationSpec.run_cappedSum_eq_root`, instantiated at +`n = 0, 1, 2, 3` (`1, 2, 4, 8` leaves). -/ +theorem countdownStackSpec_run_total (n : ℕ) : + (StackAccumulationSpec.run (encG := encNat) countdownStackSpec (fun _ => 1) n).total = + 2 ^ n := by + refine StackAccumulationSpec.run_cappedSum_eq_root countdownStackSpec (fun _ => 1) n + countdownBranching countdownBranching_terminating rfl rfl (fun _ _ => rfl) + (fun _ => decide_eq_true_eq.to_iff) + (fun _ _ => rfl) (countdownBranching_leafWord_length_le n) + (countdownStackSpec_rounds_sufficient n) + (val := fun s => 2 ^ s) + (fun t ht => by + change ¬(t = 0) at ht + obtain ⟨m, rfl⟩ := Nat.exists_eq_succ_of_ne_zero ht + change 2 ^ (m + 1) = 2 ^ m + 2 ^ m + omega) + (fun t ht => by + change t = 0 at ht + subst ht + rfl) + le_rfl + +example : + (StackAccumulationSpec.run (encG := encNat) countdownStackSpec (fun _ => 1) 0).total = 1 ∧ + (StackAccumulationSpec.run (encG := encNat) countdownStackSpec (fun _ => 1) 1).total = 2 ∧ + (StackAccumulationSpec.run (encG := encNat) countdownStackSpec (fun _ => 1) 2).total = 4 ∧ + (StackAccumulationSpec.run (encG := encNat) countdownStackSpec (fun _ => 1) 3).total = 8 := + ⟨countdownStackSpec_run_total 0, countdownStackSpec_run_total 1, + countdownStackSpec_run_total 2, countdownStackSpec_run_total 3⟩ + +/-! ### 4. `OracleCallBound`, `BoundedOracleProgram`, and `BoundedOracleReduction` -/ + +/-- `OracleCallBound` (`encOracleCallBound`) concrete profile & `ComputableInPolyTime` fields. -/ +example : + OracleCallBound.zero = ⟨0, 0, 0, 0⟩ ∧ + OracleCallBound.single 5 3 = ⟨1, 5, 5, 3⟩ ∧ + ComputableInPolyTime OracleCallBound.qcount encOracleCallBound encNat ∧ + ComputableInPolyTime OracleCallBound.qlen encOracleCallBound encNat ∧ + ComputableInPolyTime OracleCallBound.totalQlen encOracleCallBound encNat ∧ + ComputableInPolyTime OracleCallBound.alen encOracleCallBound encNat := + ⟨rfl, rfl, + encOracleCallBound_qcount_polyTime .id', + encOracleCallBound_qlen_polyTime .id', + encOracleCallBound_totalQlen_polyTime .id', + encOracleCallBound_alen_polyTime .id'⟩ + +/-- Genuine multi-bit word oracle appending `true` (`|appendTrueOracle w| = |w| + 1 ≥ 1`). -/ +def appendTrueOracle (w : List Bool) : List Bool := w ++ [true] + +theorem computableInPolyTime_appendTrueOracle : + ComputableInPolyTime appendTrueOracle encBits encBits := + (ComputableTidilyInPolyTime.bitsAppend .id' (.const [true])).computableInPolyTime + +/-- Identity multi-bit `BoundedOracleProgram` for `appendTrueOracle` (`alenCap w = |w| + 1`). -/ +@[expose] +noncomputable def appendTrueIdProg : + BoundedOracleProgram encBits encBits appendTrueOracle appendTrueOracle := + BoundedOracleProgram.id + (alenCap := fun w => w.length + 1) + (by + exact ((ComputableInPolyTime.unary_eval (Polynomial.X + 1)).comp + (ComputableInPolyTime.encoding_length encBits)).of_enc_eq fun w => by simp) + (by intro w; simp [appendTrueOracle]) + +/-- Composing `appendTrueIdProg` with itself computes `w ↦ w ++ [true]` via `1` inner query of +length `|w|` and transfers to both `ComputableInPolyTime` and `ComputableInPolySpace`. -/ +example : + (appendTrueIdProg.comp appendTrueIdProg).qcount [false, true] = 1 ∧ + ((appendTrueIdProg.compAffine appendTrueIdProg (scale := 1) (offset := 0) + (fun w => by simp [appendTrueIdProg, BoundedOracleProgram.id, + BoundedOracleProgram.ofSingleQuery, BoundedOracleProgram.totalQlen, + OracleCallBound.single])).totalQlen [false, true]) = 2 ∧ + ComputableInPolyTime appendTrueOracle encBits encBits ∧ + ComputableInPolySpace appendTrueOracle encBits encBits := by + have hcomp := appendTrueIdProg.comp appendTrueIdProg + have hpt := hcomp.computableInPolyTime computableInPolyTime_appendTrueOracle + have hps := hcomp.computableInPolySpace + (ComputableInPolySpace.of_polyTime computableInPolyTime_appendTrueOracle) + refine ⟨?_, rfl, hpt, hps⟩ + rw [BoundedOracleProgram.qcount_comp] + have hqc1 : appendTrueIdProg.qcount [false, true] = 1 := rfl + have hql1 : appendTrueIdProg.qlen [false, true] = 2 := rfl + have hqc2 : appendTrueIdProg.qcount = fun _ => 1 := rfl + rw [hqc1, hql1, hqc2, one_mul] + apply le_antisymm + · exact csSup_le ⟨1, ⟨[], Nat.zero_le 2, rfl⟩⟩ (by rintro _ ⟨w, _, rfl⟩; exact le_rfl) + · exact le_wordMax (fun _ => 1) (w := []) (Nat.zero_le 2) + +/-- `BoundedOracleReduction`: lift `dupBitsReduction`, compose via `trans`, bridge to +`PolyTimeTuringReducible` and `PWithOracleQueries`, and transfer `P`, `PSPACE`, and +`DecidableInExpTime`. -/ +noncomputable def nonemptyOracleRed : + BoundedOracleReduction encBits encBits {w : List Bool | w ≠ []} {w : List Bool | w ≠ []} := + BoundedOracleReduction.ofSizeSensitive dupBitsReduction fun w => by + cases w <;> simp [dupBitsReduction] + +example {δ : ℝ} (hδ : 0 ≤ δ) + (hB_P : {w : List Bool | w ≠ []} ∈ P encBits) + (hB_PS : {w : List Bool | w ≠ []} ∈ PSPACE encBits) + (hB_Exp : DecidableInExpTime {w : List Bool | w ≠ []} encBits List.length δ) : + PolyTimeTuringReducible encBits encBits + {w : List Bool | w ≠ []} {w : List Bool | w ≠ []} ∧ + {w : List Bool | w ≠ []} ∈ + PWithOracleQueries (encBits '' {w : List Bool | w ≠ []}) (fun _ => 1) encBits ∧ + {w : List Bool | w ≠ []} ∈ P encBits ∧ + {w : List Bool | w ≠ []} ∈ PSPACE encBits ∧ + DecidableInExpTime {w : List Bool | w ≠ []} encBits List.length (2 * δ) := by + have hlen_pt : ComputableInPolyTime List.length encBits encNat := + (ComputableTidilyInPolyTime.unary_to_binary.comp + (ComputableTidilyInPolyTime.encoding_length encBits)).computableInPolyTime + have hcomp := nonemptyOracleRed.trans nonemptyOracleRed + have hExpA := nonemptyOracleRed.decidableInExpTime Decoder.bits hlen_pt hlen_pt + (scale := 2) (offset := 0) + (fun w q hq b hb => by + simp only [nonemptyOracleRed, BoundedOracleReduction.ofSizeSensitive, + BoundedOracleReduction.ofProgram, BoundedOracleProgram.ofSingleQuery, + OracleComp.queriesWith_map, OracleComp.queriesWith_query, List.mem_singleton] at hq + subst hq + change b = w ++ w at hb + subst hb + simp only [List.length_append] + omega) + hδ hB_Exp + simp only [Nat.cast_ofNat] at hExpA + exact ⟨hcomp.polyTimeTuringReducible, + nonemptyOracleRed.mem_PWithOracleQueries (fun _ => le_rfl), + hcomp.mem_P Decoder.bits hB_P, + hcomp.mem_PSPACE Decoder.bits hB_PS, + hExpA⟩ + + +lemma countdownStackSpec_foldl_acc (a : ℕ) (L' : List (List Bool)) : + ((L'.map (countdownBranching.walk a)).foldl + (fun (d : CappedNatAcc) (_s : ℕ) => countdownStackSpec.combine ⟨(), d, 1⟩) + (countdownStackSpec.initAcc a)).cap = 2 ^ a ∧ + ((L'.map (countdownBranching.walk a)).foldl + (fun (d : CappedNatAcc) (_s : ℕ) => countdownStackSpec.combine ⟨(), d, 1⟩) + (countdownStackSpec.initAcc a)).total ≤ 2 ^ a := by + simp only [countdownStackSpec] + simp only [CappedNatAcc.foldl_add_eq (fun _ : ℕ => 1) + (L'.map (countdownBranching.walk a)) (CappedNatAcc.init (2 ^ a)) (Nat.zero_le _)] + exact ⟨rfl, Nat.min_le_left _ _⟩ + +lemma countdownStackSpec_stateBound (a i : ℕ) (hi : i ≤ countdownStackSpec.rounds a) : + (encStackSearchState (encFinEnum Unit) encNat encCappedNatAcc + ((countdownStackSpec.step (fun _ => 1))^[i] (countdownStackSpec.initState a))).length ≤ + 1000 * (a + 1) ^ 2 := by + have H := StackAccumulationSpec.run_eq_foldl_leafWords countdownStackSpec (fun _ => 1) a + countdownBranching countdownBranching_terminating rfl + (fun _ => decide_eq_true_eq.to_iff) + (fun _ _ => rfl) (countdownBranching_leafWord_length_le a) + (countdownStackSpec_rounds_sufficient a) + obtain ⟨L, hnd, hL, hrun_eq, hstate⟩ := H + obtain ⟨hlen, helem, ⟨L', hsub, hacc⟩⟩ := hstate i hi + have hcap := countdownStackSpec_foldl_acc a L' + rw [← hacc] at hcap + obtain ⟨hcap1, hcap2⟩ := hcap + have hlen_cap := CappedNatAcc.length_encCappedNatAcc_le_of_le_two_pow + (by rw [hcap1]; exact hcap2) (by rw [hcap1]) + have hlen_stack : (encList encNat ((countdownStackSpec.step (fun _ => 1))^[i] + (countdownStackSpec.initState a)).stack).length ≤ (a + 1) * (2 * (a + 1) + 1) + 1 := by + have h_enc_list := length_encList_le encNat ((countdownStackSpec.step (fun _ => 1))^[i] + (countdownStackSpec.initState a)).stack (b := a + 1) (by + intro x hx + obtain ⟨w, hw1, hw2, hw3⟩ := helem x hx + have hwalk : ∀ (s : ℕ) (w : List Bool), countdownBranching.walk s w ≤ s := by + intro s w + induction w generalizing s with + | nil => exact le_rfl + | cons b ws ih => exact (ih (s - 1)).trans (by omega) + have hx_eq : x = countdownBranching.walk a w := hw3.symm + rw [hx_eq] + have hx_le : countdownBranching.walk a w ≤ a := hwalk a w + have hx2 : (encNat (countdownBranching.walk a w)).length ≤ a + 1 := by + have h := length_encNat_mono hx_le + have hpow : (encNat a).length ≤ a + 1 := (length_encNat_le_self a).trans (by omega) + exact h.trans hpow + exact hx2) + have h_mul := Nat.mul_le_mul_right (2 * (a + 1) + 1) hlen + omega + have H_mul2 : (a + 1) * (2 * (a + 1) + 1) = 2 * (a + 1)^2 + (a + 1) := by ring + rw [H_mul2] at hlen_stack + simp only [encStackSearchState_apply, length_encPair] + have hctx : ((encFinEnum Unit) ((countdownStackSpec.step (fun _ => 1))^[i] + (countdownStackSpec.initState a)).ctx).length ≤ 10 := by + have h := length_encFinEnum_lt ((countdownStackSpec.step (fun _ => 1))^[i] + (countdownStackSpec.initState a)).ctx + have hc : Nat.card Unit ≤ 10 := by simp + omega + have H_sq : a + 1 ≤ (a + 1)^2 := by + have h1 : (a + 1) * 1 ≤ (a + 1) * (a + 1) := + Nat.mul_le_mul_left (a + 1) (Nat.le_add_left 1 a) + have h2 : (a + 1) * 1 = a + 1 := by ring + have h3 : (a + 1) * (a + 1) = (a + 1)^2 := by ring + omega + have H_sq2 : 1 ≤ (a + 1)^2 := by + have h1 : 1 * 1 ≤ (a + 1) * (a + 1) := + Nat.mul_le_mul (Nat.le_add_left 1 a) (Nat.le_add_left 1 a) + have h2 : (a + 1) * (a + 1) = (a + 1)^2 := by ring + omega + omega + +example : ∃ c e : ℕ, ∃ Space : ℕ → ℕ, + PolyBounded (fun a => (encUnary a).length) Space ∧ + ComputableInO (countdownStackSpec.run (fun _ => 1)) encUnary encCappedNatAcc + (fun a => c * ((encUnary a).length + 1) ^ e + + (countdownStackSpec.rounds a + 1) * + (c * ((encUnary a).length + 1) ^ e + (encNat 1).length)) Space ∧ + ComputableInPolySpace (countdownStackSpec.run (fun _ => 1)) encUnary encCappedNatAcc := by + have h := StackAccumulationSpec.exists_computableInO_run countdownStackSpec + (g := fun _ => 1) (Tg := fun x => (encNat x).length) (Sg := fun x => (encNat x).length) + (ComputableInO.const 1) + (PolyBounded.self) + (stateBound := fun a => 1000 * (a + 1) ^ 2) (ansBound := fun _ => (encNat 1).length) + (leafMax := fun _ => (encNat 1).length) + (PolyBounded.of_forall_le 1000 2 (fun a => by + simp only [encUnary_apply, List.length_replicate]; exact le_rfl)) + (PolyBounded.const (encNat 1).length) + countdownStackSpec_stateBound + (by + intro a i hi st H + exact le_rfl) + (by + intro a i hi st H + obtain ⟨hnot, hleaf⟩ := H + change decide (st.stack.headD 0 = 0) = true at hleaf + rw [decide_eq_true_eq] at hleaf + change (encNat (st.stack.headD 0)).length ≤ _ + rw [hleaf] + decide) + exact h + + +end CslibFrontierTests.DisjointInstancesAndOracleReduction diff --git a/manual/machines-and-classes/reductions.md b/manual/machines-and-classes/reductions.md index 7926f2d8c2..7af84a463a 100644 --- a/manual/machines-and-classes/reductions.md +++ b/manual/machines-and-classes/reductions.md @@ -81,6 +81,8 @@ The oracle recognizes the **encoded image** of `B`: a word outside the image of [The truth-table-to-Turing bridge](https://github.com/cslib-community/cslib-frontier/blob/13e6a31951bf1c89a1a6258c44f9444aecbbefd8/Complexity/Computability/Complexity/Reduction/Turing.lean#L270) executes a batch of typed queries and evaluates the replies. One-one and all restricted truth-table variants also embed. Hardness consequences include [`NPHard.P_eq_NP_of_turing_mem_P`](https://github.com/cslib-community/cslib-frontier/blob/13e6a31951bf1c89a1a6258c44f9444aecbbefd8/Complexity/Computability/Complexity/Reduction/Turing.lean#L565), with the word-target assumption visible in the theorem. These are conditional transfer principles, not new separations or collapses. +For quantitative query and reply accounting across both multi-bit function oracles and decision oracles, import [`Reduction.BoundedOracle`](../../CslibFrontier/Computability/Complexity/Reduction/BoundedOracle.lean). `OracleCallBound` (`encOracleCallBound`) records `qcount`, per-query `qlen`, summed `totalQlen`, and reply `alen`. `BoundedOracleProgram` packages a deterministic `WordQueryComp` program certified by `IsOraclePPTOn` against a word oracle `List Bool → List Bool`, an `OracleCallBound` profile respected along `OracleComp.queriesWith`, and a polynomial-time unary reply-length allowance `alenCap` for open handler substitution (`IsOraclePPTOn.interpret_preprocess_open'`). `Turing.MultiTapePTM.receiveWord`, `computableInPolyTime_run_word`, and `exists_computableInO_run_word` extend coin-fixed machine simulation from one-bit `receiveBit` to multi-bit word replies while bounding simulator workspace solely in terms of input length, clock, answer-length growth, and simulated oracle workspace—never simulated oracle time. `BoundedOracleProgram.comp` composes call budgets via `wordMax`, and `compAffine` (`totalQueryLength_comp_affine`) refines `totalQlen` linearly (`scale * totalQlen₁ + offset * qcount₁`) when the inner total query length is affine in the outer query length. `BoundedOracleReduction` specializes to typed decision languages `(A, encA)` and `(B, encB)` against `languageOracle (encB '' B)` (`alen ≤ 1`), providing `refl`, `ofPolyTime`, `ofSizeSensitive`, `transDecoded` (using a total polynomial-time `Decoder encB` to reject non-canonical encodings in zero queries), `trans`, bridges to `PolyTimeTuringReducible` and `PWithOracleQueries`, and `mem_P`, `mem_PSPACE`, `decidableInExpTime`, and `decidableInSubexpTime`. + ## Autoreductions and splitting An autoreduction is a reduction to the same language that avoids asking its original instance. [Polynomial-time](https://github.com/cslib-community/cslib-frontier/blob/13e6a31951bf1c89a1a6258c44f9444aecbbefd8/Complexity/Computability/Complexity/Reduction/Autoreducibility.lean#L83) and [logspace](https://github.com/cslib-community/cslib-frontier/blob/13e6a31951bf1c89a1a6258c44f9444aecbbefd8/Complexity/Computability/Complexity/Reduction/Autoreducibility.lean#L101) many-one versions require a fixed-point-free map. The polynomial-time truth-table variants—`k`-bounded, bounded, disjunctive, conjunctive, and unrestricted—require `q(a,i) ≠ a` only for indices actually used, `i < r(a)`. The same resource and answer semantics described above apply. These variants add that avoidance condition to the kernel's `Good`, so their forgetful maps, closure under complement and disjunctive/conjunctive duality are kernel corollaries. @@ -357,9 +359,16 @@ characterization remain open (see `ROADMAP.md`). ## Parameter-sensitive transfer rules -[FPT reductions and kernels](parameterized-complexity.md) separately bound the target parameter by a function of the source parameter. Fine-grained transfer uses more quantitative contracts without defining a new reduction datatype. [`DecidableInExpTime.of_reduction`](https://github.com/cslib-community/cslib-frontier/blob/13e6a31951bf1c89a1a6258c44f9444aecbbefd8/Complexity/Computability/Complexity/FineGrained/Reduction.lean#L117) takes a native polynomial-time membership-preserving map with `μB(f(a)) ≤ c μA(a)+c`. A target time rate `2^(δ μB)` yields source rate `2^(cδ μA)`, up to encoded-length polynomial factors, for `δ ≥ 0`. [`DecidableInSubexpTime.of_reduction`](https://github.com/cslib-community/cslib-frontier/blob/13e6a31951bf1c89a1a6258c44f9444aecbbefd8/Complexity/Computability/Complexity/FineGrained/Reduction.lean#L181) transfers the predicate that permits a decider for each positive rate. +[FPT reductions and kernels](parameterized-complexity.md) separately bound the target parameter by a function of the source parameter. [`DecidableInExpTime.of_reduction`](https://github.com/cslib-community/cslib-frontier/blob/13e6a31951bf1c89a1a6258c44f9444aecbbefd8/Complexity/Computability/Complexity/FineGrained/Reduction.lean#L117) takes a native polynomial-time membership-preserving map with `μB(f(a)) ≤ c μA(a)+c`. A target time rate `2^(δ μB)` yields source rate `2^(cδ μA)`, up to encoded-length polynomial factors, for `δ ≥ 0`. [`DecidableInSubexpTime.of_reduction`](https://github.com/cslib-community/cslib-frontier/blob/13e6a31951bf1c89a1a6258c44f9444aecbbefd8/Complexity/Computability/Complexity/FineGrained/Reduction.lean#L181) transfers the predicate that permits a decider for each positive rate. + +[`DecidableInSubexpTime.of_expReduction`](https://github.com/cslib-community/cslib-frontier/blob/13e6a31951bf1c89a1a6258c44f9444aecbbefd8/Complexity/Computability/Complexity/FineGrained/Reduction.lean#L252) permits the map itself to cost `2^(C m(a)) (L+1)^D`, under `ComputableInO` with that time and output-charged space bound. If the output parameter is at most `c m(a) floor(log₂(m(a))) + c`, target subexponential time implies source subexponential time in `m floor(log₂ m)`. The smaller exponential preprocessing cost is absorbed at each positive target rate. ETH-based lower-bound transport in that module remains an implication from its displayed ETH premise; the snapshot's independent [native counting endpoints](native-counting.md) must be considered when interpreting that premise. + +Structured single-instance, batch, and stack-accumulated parameter-sensitive reductions live in [`FineGrained.DisjointInstances`](../../CslibFrontier/Computability/Complexity/FineGrained/DisjointInstances.lean) (tested alongside [`Reduction.BoundedOracle`](../../CslibFrontier/Computability/Complexity/Reduction/BoundedOracle.lean) in [`DisjointInstancesAndOracleReduction`](../../CslibFrontierTests/DisjointInstancesAndOracleReduction.lean)): -[`DecidableInSubexpTime.of_expReduction`](https://github.com/cslib-community/cslib-frontier/blob/13e6a31951bf1c89a1a6258c44f9444aecbbefd8/Complexity/Computability/Complexity/FineGrained/Reduction.lean#L252) permits the map itself to cost `2^(C m(a)) (L+1)^D`, under `ComputableInO` with that time and output-charged space bound. If the output parameter is at most `c m(a) floor(log₂(m(a))) + c`, target subexponential time implies source subexponential time in `m floor(log₂ m)`. The smaller exponential preprocessing cost is absorbed at each positive target rate. Neither rule introduces an oracle reduction or an unrestricted subexponential-reduction-family notion. ETH-based lower-bound transport in this module remains an implication from its displayed ETH premise; the snapshot's independent [native counting endpoints](native-counting.md) must be considered when interpreting that premise. +- `SizeSensitiveReduction` packages a polynomial-time map `toFun : α → β` with explicit `scale` and `offset` satisfying `μB (toFun a) ≤ scale * μA a + offset`, supporting `refl`, `trans` (`scale` multiplies), `decidableInExpTime` (`δ ↦ scale * δ`), `decidableInSubexpTime`, and `computableInPolySpace_comp`. +- `InstanceBatch` (`encInstanceBatch`), `CNFInstanceBatch` (`encCNFInstanceBatch`), `CappedNatAcc` (`encCappedNatAcc`), and `DisjointBatchReduction` represent materialized subinstance lists with summed parameter bound `sumMeasure μB ≤ scale * μA a + offset`. `DisjointBatchReduction.decidableInExpTime_or` and `decidableInSubexpTime_or` transfer decision running time across the batch, while `exists_computableInO_foldl` and `exists_computableInO_cappedSum` (given polynomial subinstance solver workspace) fold over the batch in polynomial live workspace without storing all subinstance answers simultaneously, clamping running binary counts at `cap` via `CappedNatAcc` so the accumulator stays within `O(log₂ cap)` bits. +- `StackSearchState`, `StackNodeInput`, `StackCombineInput`, and `StackAccumulationSpec` execute depth-first accumulation over up to `K₀ * 2 ^ (ν a)` rounds (`ν a ≤ μA a / M + K₁`) without materializing the exponentially long leaf list. `decidableInExpTime_of_stack` and `decidableInSubexpTime_of_stack` transfer `2 ^ (δ * μB)` and subexponential leaf decision time to `2 ^ ((1 / M + scale * δ) * μA)` and subexponential time, while `exists_computableInO_run` and `exists_computableInO_cappedSum_of_stack` (given polynomial leaf-solver workspace) additionally preserve polynomial live workspace; `iterate_step_eq_binaryBranching`, `run_eq_foldl_leafWords`, and `run_cappedSum_eq_root` connect the stack machine directly to `Cslib.BinaryBranching` trees from disjoint and counting sparsification. +- For adaptive Turing reductions whose queried encodings `encB b` satisfy `μB b ≤ scale * μA a + offset` along `OracleComp.queriesWith`, `BoundedOracleReduction.decidableInExpTime` and `.decidableInSubexpTime` take a total polynomial-time `Decoder encB` together with polynomial-time `μA` and `μB` so the simulated machine guards oracle calls by canonical decoding and the runtime parameter budget `scale * μA a + offset`, transferring `2 ^ (δ * μB)` deciders to `2 ^ ((scale * δ) * μA)` with polynomial overhead absorbing query count and construction cost (`mem_P` and `mem_PSPACE` require `Decoder encB` similarly). Polynomial-rate transfer from orthogonal vectors is a direct composition rather than a reduction datatype. `CslibFrontier.Computability.Complexity.FineGrained.Diameter` formalizes the orthogonal vectors form of Roditty and Vassilevska Williams's diameter two-versus-three construction (Section 4, Theorem 9, stated there from CNF-SAT for graphs with `m` edges). Partial assignments become vectors and clauses become coordinates; the clique on clause vertices and hubs is replaced by hub–coordinate edges, and two padding vertices are added. The graph `OV.toDiameter` has diameter three on instances with an orthogonal pair and two otherwise (`OV.ediam_toDiameter`). Its vertex and edge lists are written by two one-pass streams with binary counters, paired under `ComputableInO` within time `L (log L) ^ D` in the encoded instance length (`OV.exists_computableInO_toDiameter`). `DecidableInTimeO.decidableInTimeO_OV_of_diameter` then turns any procedure separating the two diameters within time `L ^ (2 - ε)` on encoded graphs into an `OV` decider within time `N ^ (2 - min ε 1 / 2) (d + 1) ^ 2`. This transfer is unconditional. The lower bounds are implications from `OVH`. `not_decidableInTimeO_diameter_of_OVH` states them in the encoded length `L`. `not_decidableInTimeO_diameter_size_of_OVH` uses `(n + m) ^ (2 - ε) + L`; the `L` term is needed, because a bound in the number of listed vertices and edges alone cannot read unbounded labels and would hold vacuously. The reduced graphs have `Θ(N d)` edges with unrestricted dimension, so the sparse-graph statement needs the low-dimension form of `OVH` and is not covered. The library neither proves nor refutes `OVH`; it refutes `SETH`, so hardness from `SETH` through `OVH_of_SETH` is vacuous.