refactor(machines): lower the admissible-map reduction kernel

Complexity.lean

@@ -1239,6 +1239,7 @@ public import Complexity.Computability.RAM.Cost
 public import Complexity.Computability.RAM.Defs
 public import Complexity.Computability.RAM.Input
 public import Complexity.Computability.RAM.Squaring
+public import Complexity.Computability.Reduction.ManyOne
 public import Complexity.Computability.TreeEval.Ary.Basic
 public import Complexity.Computability.TreeEval.Ary.CookMertz
 public import Complexity.Computability.TreeEval.Basic

Complexity/Computability/Complexity/Reduction/ManyOne.lean

@@ -7,8 +7,7 @@ Authors: Samuel Schlesinger
 module
 -- upstream: candidate
 
-public import Complexity.Init
-public import Mathlib.Data.Set.Operations
+public import Complexity.Computability.Reduction.ManyOne
 public import Mathlib.Logic.Embedding.Basic
 import Mathlib.Order.BooleanAlgebra.Set
 
@@ -19,7 +18,9 @@ Most reductions of complexity theory have one shape: a map `f` of an admissible
 instances of `A` to instances of `B`, preserving membership. Here the admissible maps are an
 arbitrary predicate `Good` on functions, and `ManyOneReducibleBy Good A B` says that such a map
 exists. Polynomial-time and logarithmic-space reductions of encoded problems, and first-order
-reductions of ordered queries, are instances.
+reductions of ordered queries, are instances. The map-parametric kernel and its laws live in
+`Complexity.Computability.Reduction.ManyOne`, publicly re-exported here; only class-level helpers
+are defined in this module.
 
 Reflexivity and transitivity are not assumed: they follow from closure of the admissible maps
 under the identity and composition (`ManyOneReducibleBy.refl`, `ManyOneReducibleBy.trans`), which
@@ -72,70 +73,9 @@ on `Primcodable` types, the instance of this shape for computable maps; it is no
 
 namespace Cslib.Complexity
 
-universe u v w x
-
-variable {α : Type u} {β : Type v} {γ : Type w}
-
-/-- `A` many-one reduces to `B` by an admissible map: some `f` satisfying `Good` has
-`a ∈ A ↔ f a ∈ B` for every `a`. -/
-def ManyOneReducibleBy (Good : (α → β) → Prop) (A : Set α) (B : Set β) : Prop :=
-  ∃ f : α → β, Good f ∧ ∀ a, a ∈ A ↔ f a ∈ B
-
-variable {Good : (α → β) → Prop} {A : Set α} {B : Set β}
-
-namespace ManyOneReducibleBy
-
-/-- Every problem reduces to itself when the identity is admissible. -/
-theorem refl {Good : (α → α) → Prop} (hid : Good id) (A : Set α) : ManyOneReducibleBy Good A A :=
-  ⟨id, hid, fun _ => Iff.rfl⟩
-
-/-- Reductions compose when composites of admissible maps are admissible. The three classes of
-maps may differ, as they do when admissibility depends on encodings. -/
-theorem trans {Good₁ : (α → β) → Prop} {Good₂ : (β → γ) → Prop} {Good₃ : (α → γ) → Prop}
-    {C : Set γ} (hcomp : ∀ f g, Good₁ f → Good₂ g → Good₃ (g ∘ f))
-    (hAB : ManyOneReducibleBy Good₁ A B) (hBC : ManyOneReducibleBy Good₂ B C) :
-    ManyOneReducibleBy Good₃ A C :=
-  let ⟨f, hf, hfAB⟩ := hAB
-  let ⟨g, hg, hgBC⟩ := hBC
-  ⟨g ∘ f, hcomp f g hf hg, fun a => (hfAB a).trans (hgBC (f a))⟩
-
-/-- More admissible maps give more reductions. -/
-theorem mono {Good' : (α → β) → Prop} (hle : ∀ f, Good f → Good' f)
-    (h : ManyOneReducibleBy Good A B) : ManyOneReducibleBy Good' A B :=
-  let ⟨f, hf, hAB⟩ := h
-  ⟨f, hle f hf, hAB⟩
-
-/-- A reduction from `A` to `B` is also a reduction from `Aᶜ` to `Bᶜ`. -/
-theorem compl (h : ManyOneReducibleBy Good A B) : ManyOneReducibleBy Good Aᶜ Bᶜ :=
-  let ⟨f, hf, hAB⟩ := h
-  ⟨f, hf, fun a => not_congr (hAB a)⟩
-
-/-- If reductions preserve membership from `D` to `C`, they also preserve membership in the
-complement classes `{B | Bᶜ ∈ D}` and `{A | Aᶜ ∈ C}`. -/
-theorem mem_compl {C : Set (Set α)} {D : Set (Set β)}
-    (hCD : ∀ {A : Set α} {B : Set β}, ManyOneReducibleBy Good A B → B ∈ D → A ∈ C)
-    (h : ManyOneReducibleBy Good A B) (hB : Bᶜ ∈ D) : Aᶜ ∈ C :=
-  hCD h.compl hB
-
-/-- **Transfer along partial decodings.** Suppose representations `α'` and `β'` partially decode
-to `α` and `β`, and every admissible map `f` is simulated by an admissible map `F` of
-representations, in that `F` decodes to `f` on decodable inputs and to nothing elsewhere. Then a
-reduction of `A` to `B` gives one of the representations of members of `A` to those of members of
-`B`. -/
-theorem lift {α' : Type w} {β' : Type x} {Good' : (α' → β') → Prop}
-    (dec : α' → Option α) (dec' : β' → Option β)
-    (hsim : ∀ f, Good f → ∃ F, Good' F ∧ ∀ y, dec' (F y) = (dec y).map f)
-    (h : ManyOneReducibleBy Good A B) :
-    ManyOneReducibleBy Good' {y | ∃ a ∈ A, dec y = some a} {z | ∃ b ∈ B, dec' z = some b} := by
-  obtain ⟨f, hf, hAB⟩ := h
-  obtain ⟨F, hF, hFf⟩ := hsim f hf
-  refine ⟨F, hF, fun y => ?_⟩
-  simp only [Set.mem_ofPred_eq, hFf]
-  cases dec y with
-  | none => simp
-  | some a => simpa using hAB a
-
-end ManyOneReducibleBy
+universe u v w
+
+variable {α : Type u} {β : Type v} {A : Set α} {B : Set β}
 
 /-! ### Complement-class helpers -/
 

Complexity/Computability/Machines/Turing/MultiTape/Halting/Reduction.lean

@@ -7,7 +7,7 @@ Authors: Samuel Schlesinger
 module
 -- upstream: candidate
 
-public import Complexity.Computability.Complexity.Reduction.ManyOne
+public import Complexity.Computability.Reduction.ManyOne
 public import Complexity.Computability.Machines.Turing.MultiTape.Halting.Computable
 
 /-!

Complexity/Computability/Reduction/ManyOne.lean

@@ -0,0 +1,112 @@
+/-
+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 Complexity.Init
+public import Mathlib.Data.Set.Operations
+
+/-!
+# Many-one reductions by admissible maps
+
+`Cslib.Complexity.ManyOneReducibleBy Good A B` asks for a membership-preserving map from `A` to
+`B` satisfying an arbitrary predicate `Good`. No machine model, encoding, complexity class, or
+closure assumption is built into the definition. The namespace is retained for existing clients.
+Polynomial-time, logarithmic-space and computable mapping reductions instantiate this kernel.
+
+Mathlib's `ManyOneReducible` is specialized to computable maps on `Primcodable` types; it does
+not replace this map-parametric notion.
+
+## Main definitions
+
+* `Cslib.Complexity.ManyOneReducibleBy`: many-one reducibility by admissible maps.
+
+## Main results
+
+* `Cslib.Complexity.ManyOneReducibleBy.refl`, `Cslib.Complexity.ManyOneReducibleBy.trans`:
+  reflexivity and transitivity from identity and composition closure.
+* `Cslib.Complexity.ManyOneReducibleBy.mono`: enlarging the admissible maps preserves reductions.
+* `Cslib.Complexity.ManyOneReducibleBy.compl`, `Cslib.Complexity.ManyOneReducibleBy.mem_compl`:
+  complement reductions and transfer to complement classes.
+* `Cslib.Complexity.ManyOneReducibleBy.lift`: transfer along partial decodings.
+
+## References
+
+* [S. Arora, B. Barak, *Computational Complexity: A Modern Approach*][AroraBarak09],
+  Definition 2.7.
+-/
+
+@[expose] public section
+
+namespace Cslib.Complexity
+
+universe u v w x
+
+variable {α : Type u} {β : Type v} {γ : Type w}
+
+/-- `A` many-one reduces to `B` by an admissible map: some `f` satisfying `Good` has
+`a ∈ A ↔ f a ∈ B` for every `a`. -/
+def ManyOneReducibleBy (Good : (α → β) → Prop) (A : Set α) (B : Set β) : Prop :=
+  ∃ f : α → β, Good f ∧ ∀ a, a ∈ A ↔ f a ∈ B
+
+variable {Good : (α → β) → Prop} {A : Set α} {B : Set β}
+
+namespace ManyOneReducibleBy
+
+/-- Every problem reduces to itself when the identity is admissible. -/
+theorem refl {Good : (α → α) → Prop} (hid : Good id) (A : Set α) : ManyOneReducibleBy Good A A :=
+  ⟨id, hid, fun _ => Iff.rfl⟩
+
+/-- Reductions compose when composites of admissible maps are admissible. The three classes of
+maps may differ, as they do when admissibility depends on encodings. -/
+theorem trans {Good₁ : (α → β) → Prop} {Good₂ : (β → γ) → Prop} {Good₃ : (α → γ) → Prop}
+    {C : Set γ} (hcomp : ∀ f g, Good₁ f → Good₂ g → Good₃ (g ∘ f))
+    (hAB : ManyOneReducibleBy Good₁ A B) (hBC : ManyOneReducibleBy Good₂ B C) :
+    ManyOneReducibleBy Good₃ A C :=
+  let ⟨f, hf, hfAB⟩ := hAB
+  let ⟨g, hg, hgBC⟩ := hBC
+  ⟨g ∘ f, hcomp f g hf hg, fun a => (hfAB a).trans (hgBC (f a))⟩
+
+/-- More admissible maps give more reductions. -/
+theorem mono {Good' : (α → β) → Prop} (hle : ∀ f, Good f → Good' f)
+    (h : ManyOneReducibleBy Good A B) : ManyOneReducibleBy Good' A B :=
+  let ⟨f, hf, hAB⟩ := h
+  ⟨f, hle f hf, hAB⟩
+
+/-- A reduction from `A` to `B` is also a reduction from `Aᶜ` to `Bᶜ`. -/
+theorem compl (h : ManyOneReducibleBy Good A B) : ManyOneReducibleBy Good Aᶜ Bᶜ :=
+  let ⟨f, hf, hAB⟩ := h
+  ⟨f, hf, fun a => not_congr (hAB a)⟩
+
+/-- If reductions preserve membership from `D` to `C`, they also preserve membership in the
+complement classes `{B | Bᶜ ∈ D}` and `{A | Aᶜ ∈ C}`. -/
+theorem mem_compl {C : Set (Set α)} {D : Set (Set β)}
+    (hCD : ∀ {A : Set α} {B : Set β}, ManyOneReducibleBy Good A B → B ∈ D → A ∈ C)
+    (h : ManyOneReducibleBy Good A B) (hB : Bᶜ ∈ D) : Aᶜ ∈ C :=
+  hCD h.compl hB
+
+/-- **Transfer along partial decodings.** Suppose representations `α'` and `β'` partially decode
+to `α` and `β`, and every admissible map `f` is simulated by an admissible map `F` of
+representations, in that `F` decodes to `f` on decodable inputs and to nothing elsewhere. Then a
+reduction of `A` to `B` gives one of the representations of members of `A` to those of members of
+`B`. -/
+theorem lift {α' : Type w} {β' : Type x} {Good' : (α' → β') → Prop}
+    (dec : α' → Option α) (dec' : β' → Option β)
+    (hsim : ∀ f, Good f → ∃ F, Good' F ∧ ∀ y, dec' (F y) = (dec y).map f)
+    (h : ManyOneReducibleBy Good A B) :
+    ManyOneReducibleBy Good' {y | ∃ a ∈ A, dec y = some a} {z | ∃ b ∈ B, dec' z = some b} := by
+  obtain ⟨f, hf, hAB⟩ := h
+  obtain ⟨F, hF, hFf⟩ := hsim f hf
+  refine ⟨F, hF, fun y => ?_⟩
+  simp only [Set.mem_ofPred_eq, hFf]
+  cases dec y with
+  | none => simp
+  | some a => simpa using hAB a
+
+end ManyOneReducibleBy
+
+end Cslib.Complexity

ComplexityTests.lean

@@ -231,6 +231,7 @@ import ComplexityTests.MachinePrograms
 import ComplexityTests.MachineSequential
 import ComplexityTests.MachineStateMap
 import ComplexityTests.ManyOne
+import ComplexityTests.ManyOneKernel
 import ComplexityTests.MassProduction
 import ComplexityTests.MassProduction.Fine
 import ComplexityTests.MassProduction.HighRate

ComplexityTests/ManyOneKernel.lean

@@ -0,0 +1,31 @@
+/-
+Copyright (c) 2026 Samuel Schlesinger. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Samuel Schlesinger
+-/
+
+import Complexity.Computability.Reduction.ManyOne
+
+/-! The admissible-map API works without importing machines or complexity classes. -/
+
+namespace ComplexityTests.ManyOneKernel
+
+open Cslib.Complexity
+
+private theorem flip : ManyOneReducibleBy (fun _ => True)
+    {b : Bool | b = false} {b : Bool | b = true} :=
+  ⟨Bool.not, trivial, fun b => by cases b <;> simp⟩
+
+-- Complementing and then composing the flip gives a reduction of a proper, inhabited set to
+-- itself. This uses only the lower import, retaining the existing public names.
+example : ManyOneReducibleBy (fun _ => True) {b : Bool | b = false} {b : Bool | b = false} := by
+  have back : ManyOneReducibleBy (fun _ => True)
+      {b : Bool | b = true} {b : Bool | b = false} := by
+    have hfalse : ({b : Bool | b = false}ᶜ : Set Bool) = {b : Bool | b = true} := by
+      ext b; cases b <;> simp
+    have htrue : ({b : Bool | b = true}ᶜ : Set Bool) = {b : Bool | b = false} := by
+      ext b; cases b <;> simp
+    simpa only [hfalse, htrue] using flip.compl
+  exact flip.trans (fun _ _ _ _ => trivial) back
+
+end ComplexityTests.ManyOneKernel