From 021d0667af489d261d2c626a60ce87037374d836 Mon Sep 17 00:00:00 2001 From: Samuel Schlesinger Date: Sat, 24 Oct 2026 17:33:17 +0000 Subject: [PATCH] feat(SharpP): prove SharpPWithOracle closure and ModPWithOracle GapPWithOracle residue characterizations (#727) --- .../Complexity/Classes/SharpP/Lowness.lean | 74 +++++++++++++++---- .../Complexity/Classes/SharpP/Oracle.lean | 54 ++++++++++++++ ComplexityTests/SharpPLowness.lean | 64 ++++++++++++++++ 3 files changed, 179 insertions(+), 13 deletions(-) diff --git a/Complexity/Computability/Complexity/Classes/SharpP/Lowness.lean b/Complexity/Computability/Complexity/Classes/SharpP/Lowness.lean index cbc1c264f..8c3214f12 100644 --- a/Complexity/Computability/Complexity/Classes/SharpP/Lowness.lean +++ b/Complexity/Computability/Complexity/Classes/SharpP/Lowness.lean @@ -53,10 +53,15 @@ This module completes the unsigned and signed counting oracle-lowness characteri `GapP^A = GapP` (equivalently `SPP^A = SPP`) if and only if `A ∈ SPP`, and every `FewP` oracle is low for `GapP`, `SPP`, `LWPPWithFixedTarget`, `WPPWithFixedTarget`, `C=P`, and `PP`. * **Relativized modular counting classes (`ModPWithOracle`, `coModPWithOracle`, - `ParityPWithOracle`) and `SPP` / `FewP` / `UP ∩ coUP` lowness:** `UP ∩ coUP` is low for - `ModPWithOracle k` and `coModPWithOracle k` at every modulus `k : ℕ`, while for every positive - modulus `0 < k`, `SPP` (and hence `FewP`) is low for `ModPWithOracle k`, `coModPWithOracle k`, - and `ParityPWithOracle` via `GapPWithOracle_eq_GapP_of_mem_SPP` and `mem_ModP_iff_exists_GapP`. + `ParityPWithOracle`), their `GapPWithOracle` residue characterizations, and `SPP` / `FewP` / + `UP ∩ coUP` lowness:** for every positive modulus `0 < k`, `GapPWithOracle` functions have + congruent `SharpPWithOracle` representatives (`GapPWithOracle.exists_SharpPWithOracle_emod`), so + `ModPWithOracle k` and `coModPWithOracle k` are characterized by nonzero and zero residues of + `GapPWithOracle` functions (`mem_ModPWithOracle_iff_exists_GapPWithOracle`, + `mem_coModPWithOracle_iff_exists_GapPWithOracle`). `UP ∩ coUP` is low for `ModPWithOracle k` and + `coModPWithOracle k` at every modulus `k : ℕ`, while for `0 < k`, `SPP` (and hence `FewP`) is low + for `ModPWithOracle k`, `coModPWithOracle k`, and `ParityPWithOracle` via + `GapPWithOracle_eq_GapP_of_mem_SPP` and `mem_ModP_iff_exists_GapP`. All results use the library's strict polynomial-time adaptive word-oracle verifier model; no nondeterministic oracle-machine counting characterization or `FP^A`-threshold `SBP` relativization @@ -99,7 +104,10 @@ is claimed. `Cslib.Complexity.forall_SPPWithOracle_eq_SPP_iff`, `Cslib.Complexity.iUnion_GapPWithOracle_SPP`, `Cslib.Complexity.iUnion_SPPWithOracle_SPP`. -* `Cslib.Complexity.ModPWithOracle_eq_ModP_of_mem_UP_of_mem_coUP`, +* `Cslib.Complexity.GapPWithOracle.exists_SharpPWithOracle_emod`, + `Cslib.Complexity.mem_ModPWithOracle_iff_exists_GapPWithOracle`, + `Cslib.Complexity.mem_coModPWithOracle_iff_exists_GapPWithOracle`, + `Cslib.Complexity.ModPWithOracle_eq_ModP_of_mem_UP_of_mem_coUP`, `Cslib.Complexity.ModPWithOracle_eq_ModP_of_mem_SPP`, `Cslib.Complexity.coModPWithOracle_eq_coModP_of_mem_SPP`, `Cslib.Complexity.ParityPWithOracle_eq_ParityP_of_mem_SPP`, @@ -933,6 +941,50 @@ theorem mem_coModPWithOracle {L : Set α} : theorem compl_mem_coModPWithOracle {L : Set α} : Lᶜ ∈ coModPWithOracle k A enc ↔ L ∈ ModPWithOracle k A enc := by simp [coModPWithOracle] +/-- Constant functions belong to `SharpPWithOracle A enc`. -/ +theorem SharpPWithOracle.natCast_mem (n : ℕ) : (n : α → ℕ) ∈ SharpPWithOracle A enc := + SharpP_subset_SharpPWithOracle A enc (SharpP.natCast_mem n) + +/-- A positive fixed modulus admits a `SharpPWithOracle` count with the same residue as any +`GapPWithOracle` function. The modulus is fixed before the input, so scaling by `k - 1` uses +`SharpPWithOracle` constant multiplication. -/ +theorem GapPWithOracle.exists_SharpPWithOracle_emod {g : α → ℤ} + (hg : g ∈ GapPWithOracle A enc) (hk : 0 < k) : + ∃ f ∈ SharpPWithOracle A enc, ∀ a, (f a : ℤ) % k = g a % k := by + obtain ⟨f₁, h₁, f₂, h₂, hg⟩ := hg + refine ⟨f₁ + (fun _ => k - 1) * f₂, + SharpPWithOracle.add_mem h₁ + (SharpPWithOracle.mul_mem (SharpPWithOracle.natCast_mem (k - 1)) h₂), + fun a => ?_⟩ + have heq : ((f₁ a + (k - 1) * f₂ a : ℕ) : ℤ) = + (f₁ a : ℤ) - f₂ a + k * f₂ a := by + rw [Nat.cast_add, Nat.cast_mul, Nat.cast_sub (by lia : 1 ≤ k)] + push_cast + ring + change ((f₁ a + (k - 1) * f₂ a : ℕ) : ℤ) % k = g a % k + rw [heq, hg a, Int.add_mul_emod_self_left] + +/-- For a positive fixed modulus, nonzero residues of `GapPWithOracle` functions define +`ModPWithOracle`. -/ +theorem mem_ModPWithOracle_iff_exists_GapPWithOracle (hk : 0 < k) {L : Set α} : + L ∈ ModPWithOracle k A enc ↔ ∃ g ∈ GapPWithOracle A enc, ∀ a, a ∈ L ↔ g a % k ≠ 0 := by + constructor + · rintro ⟨f, hf, hL⟩ + exact ⟨fun a => (f a : ℤ), SharpPWithOracle.natCast_mem_GapPWithOracle hf, + fun a => by simpa only [← Int.natCast_emod, ne_eq, Int.natCast_eq_zero] using hL a⟩ + · rintro ⟨g, hg, hL⟩ + obtain ⟨f, hf, hfg⟩ := GapPWithOracle.exists_SharpPWithOracle_emod hg hk + refine ⟨f, hf, fun a => ?_⟩ + rw [hL a, ← hfg a] + simp only [← Int.natCast_emod, ne_eq, Int.natCast_eq_zero] + +/-- For a positive fixed modulus, zero residues of `GapPWithOracle` functions define +`coModPWithOracle`. -/ +theorem mem_coModPWithOracle_iff_exists_GapPWithOracle (hk : 0 < k) {L : Set α} : + L ∈ coModPWithOracle k A enc ↔ ∃ g ∈ GapPWithOracle A enc, ∀ a, a ∈ L ↔ g a % k = 0 := + (mem_ModPWithOracle_iff_exists_GapPWithOracle hk).trans + (exists_forall_mem_compl_iff fun _ _ => not_not) + /-- Modulo two, nonzero residue is oddness: `ModPWithOracle 2 A enc = ParityPWithOracle A enc`. -/ theorem ModPWithOracle_two (A : Set (List Bool)) (enc : α ↪ List Bool) : ModPWithOracle 2 A enc = ParityPWithOracle A enc := by @@ -997,14 +1049,10 @@ theorem ParityPWithOracle_eq_ParityP_of_mem_UP_of_mem_coUP theorem ModPWithOracle_eq_ModP_of_mem_SPP (hk : 0 < k) (hA : A ∈ SPP encBits) (enc : α ↪ List Bool) : ModPWithOracle k A enc = ModP k enc := by - apply Set.Subset.antisymm ?_ (ModP_subset_ModPWithOracle k A enc) - rintro L ⟨f, hf, hL⟩ - have hg_or : (fun a => (f a : ℤ)) ∈ GapPWithOracle A enc := - ⟨f, hf, 0, SharpP_subset_SharpPWithOracle A enc SharpP.zero_mem, fun _ => by simp⟩ - have hg : (fun a => (f a : ℤ)) ∈ GapP enc := - GapPWithOracle_eq_GapP_of_mem_SPP hA enc ▸ hg_or - refine (mem_ModP_iff_exists_GapP hk).mpr ⟨fun a => (f a : ℤ), hg, fun a => ?_⟩ - simpa only [← Int.natCast_emod, ne_eq, Int.natCast_eq_zero] using hL a + ext L + rw [mem_ModPWithOracle_iff_exists_GapPWithOracle hk, + GapPWithOracle_eq_GapP_of_mem_SPP hA enc, + mem_ModP_iff_exists_GapP hk] /-- **`SPP` is low for `coModP k`** for every positive modulus `0 < k`. -/ theorem coModPWithOracle_eq_coModP_of_mem_SPP (hk : 0 < k) (hA : A ∈ SPP encBits) diff --git a/Complexity/Computability/Complexity/Classes/SharpP/Oracle.lean b/Complexity/Computability/Complexity/Classes/SharpP/Oracle.lean index 55e61a063..ca7f1e9bb 100644 --- a/Complexity/Computability/Complexity/Classes/SharpP/Oracle.lean +++ b/Complexity/Computability/Complexity/Classes/SharpP/Oracle.lean @@ -41,6 +41,10 @@ eliminates every polynomial-time decidable oracle. Oracle lowness for other clas `Cslib.Complexity.GapPWithOracle_eq_GapP`: eliminate an oracle in P. * `Cslib.Complexity.computableInPolyTimeWithOracle_andVerifier`, `Cslib.Complexity.computableInPolyTimeWithOracle_selectVerifier`: reuse verifier combinators. +* `Cslib.Complexity.SharpPWithOracle.add_mem`, + `Cslib.Complexity.SharpPWithOracle.mul_mem`, + `Cslib.Complexity.SharpPWithOracle.natCast_mem_GapPWithOracle`: additive and multiplicative + closure of `SharpPWithOracle` and embedding into `GapPWithOracle`. ## References @@ -116,4 +120,54 @@ theorem computableInPolyTimeWithOracle_selectVerifier {V₀ V₁ : α × List Bo (by fun_prop)).map_with (g := fun x b => if x.2.headD false then b.2 else b.1) (output := encBool) (by fun_prop) +namespace SharpPWithOracle + +/-- The zero function is in `SharpPWithOracle A enc`. -/ +theorem zero_mem : (0 : α → ℕ) ∈ SharpPWithOracle A enc := + SharpP_subset_SharpPWithOracle A enc SharpP.zero_mem + +/-- **`SharpPWithOracle` is closed under addition**: the first bit of a certificate chooses the +verifier, and the bits that the chosen verifier does not read must be `false`. -/ +theorem add_mem {f₁ f₂ : α → ℕ} (h₁ : f₁ ∈ SharpPWithOracle A enc) + (h₂ : f₂ ∈ SharpPWithOracle A enc) : + f₁ + f₂ ∈ SharpPWithOracle A enc := by + obtain ⟨p₁, V₁, hV₁, hf₁⟩ := h₁ + obtain ⟨p₂, V₂, hV₂, hf₂⟩ := h₂ + have hfalse : ComputableInPolyTimeWithOracle A (allFalseVerifier (α := α)) + (encPair enc encBits) encBool := + computableTidilyInPolyTime_allFalseVerifier.computableInPolyTimeWithOracle A + refine ⟨p₁ + p₂ + 1, selectVerifier + (andVerifier (fun a => p₁.eval (enc a).length) V₁ allFalseVerifier) + (andVerifier (fun a => p₂.eval (enc a).length) V₂ allFalseVerifier), + computableInPolyTimeWithOracle_selectVerifier + (computableInPolyTimeWithOracle_andVerifier (by fun_prop) hV₁ hfalse) + (computableInPolyTimeWithOracle_andVerifier (by fun_prop) hV₂ hfalse), + fun a => ?_⟩ + have e₁ := acceptCount_andVerifier_allFalseVerifier (fun a => p₁.eval (enc a).length) V₁ a + (p₂.eval (enc a).length) + have e₂ := acceptCount_andVerifier_allFalseVerifier (fun a => p₂.eval (enc a).length) V₂ a + (p₁.eval (enc a).length) + rw [Nat.add_comm (p₂.eval _)] at e₂ + rw [Pi.add_apply, hf₁ a, hf₂ a, Polynomial.eval_add, Polynomial.eval_add, Polynomial.eval_one, + acceptCount_selectVerifier, e₁, e₂] + +/-- **`SharpPWithOracle` is closed under multiplication**: the two verifiers read disjoint parts of +the certificate. -/ +theorem mul_mem {f₁ f₂ : α → ℕ} (h₁ : f₁ ∈ SharpPWithOracle A enc) + (h₂ : f₂ ∈ SharpPWithOracle A enc) : + f₁ * f₂ ∈ SharpPWithOracle A enc := by + obtain ⟨p₁, V₁, hV₁, hf₁⟩ := h₁ + obtain ⟨p₂, V₂, hV₂, hf₂⟩ := h₂ + refine ⟨p₁ + p₂, andVerifier (fun a => p₁.eval (enc a).length) V₁ V₂, + computableInPolyTimeWithOracle_andVerifier (by fun_prop) hV₁ hV₂, + fun a => ?_⟩ + rw [Pi.mul_apply, hf₁ a, hf₂ a, Polynomial.eval_add, acceptCount_andVerifier] + +/-- A function in `SharpPWithOracle`, cast to the integers, is in `GapPWithOracle`. -/ +theorem natCast_mem_GapPWithOracle {f : α → ℕ} (hf : f ∈ SharpPWithOracle A enc) : + (fun a => (f a : ℤ)) ∈ GapPWithOracle A enc := + ⟨f, hf, 0, zero_mem, fun _ => by simp⟩ + +end SharpPWithOracle + end Cslib.Complexity diff --git a/ComplexityTests/SharpPLowness.lean b/ComplexityTests/SharpPLowness.lean index f91175689..973f65288 100644 --- a/ComplexityTests/SharpPLowness.lean +++ b/ComplexityTests/SharpPLowness.lean @@ -101,8 +101,72 @@ example : ModPWithOracle 5 headTrue encBits = ModP 5 encBits := example : ParityPWithOracle headTrue encBits = ParityP encBits := ParityPWithOracle_eq_ParityP_of_mem_FewP headTrue_mem_FewP encBits +open Classical in +example : (fun q => if q ∈ headTrue then 1 else 0) + (fun _ => 2) ∈ + SharpPWithOracle headTrue encBits := + SharpPWithOracle.add_mem (indicator_mem_SharpPWithOracle_self headTrue) + (SharpPWithOracle.natCast_mem 2) + +open Classical in +example : (fun q => if q ∈ headTrue then 1 else 0) * (fun _ => 2) ∈ + SharpPWithOracle headTrue encBits := + SharpPWithOracle.mul_mem (indicator_mem_SharpPWithOracle_self headTrue) + (SharpPWithOracle.natCast_mem 2) + +open Classical in +example : ∃ f ∈ SharpPWithOracle headTrue encBits, + ∀ q, (f q : ℤ) % 3 = (if q ∈ headTrue then (1 : ℤ) else 0) % 3 := + GapPWithOracle.exists_SharpPWithOracle_emod (indicator_mem_GapPWithOracle_self headTrue) + (by decide) + +open Classical in +example : headTrue ∈ ModPWithOracle 3 headTrue encBits := + (mem_ModPWithOracle_iff_exists_GapPWithOracle (by decide)).mpr + ⟨fun q => if q ∈ headTrue then (1 : ℤ) else 0, + indicator_mem_GapPWithOracle_self headTrue, + fun q => by by_cases hq : q ∈ headTrue <;> simp [hq]⟩ + +open Classical in +example : headTrueᶜ ∈ coModPWithOracle 3 headTrue encBits := + (mem_coModPWithOracle_iff_exists_GapPWithOracle (by decide)).mpr + ⟨fun q => if q ∈ headTrue then (1 : ℤ) else 0, + indicator_mem_GapPWithOracle_self headTrue, + fun q => by by_cases hq : q ∈ headTrue <;> simp [hq]⟩ + /-! ### Axiom guards for headline theorems -/ +/-- info: 'Cslib.Complexity.SharpPWithOracle.add_mem' depends on axioms: [propext, Classical.choice, Quot.sound] -/ +#guard_msgs in +#print axioms Cslib.Complexity.SharpPWithOracle.add_mem + +/-- info: 'Cslib.Complexity.SharpPWithOracle.mul_mem' depends on axioms: [propext, Classical.choice, Quot.sound] -/ +#guard_msgs in +#print axioms Cslib.Complexity.SharpPWithOracle.mul_mem + +/-- +info: 'Cslib.Complexity.GapPWithOracle.exists_SharpPWithOracle_emod' depends on axioms: [propext, + Classical.choice, + Quot.sound] +-/ +#guard_msgs in +#print axioms Cslib.Complexity.GapPWithOracle.exists_SharpPWithOracle_emod + +/-- +info: 'Cslib.Complexity.mem_ModPWithOracle_iff_exists_GapPWithOracle' depends on axioms: [propext, + Classical.choice, + Quot.sound] +-/ +#guard_msgs in +#print axioms Cslib.Complexity.mem_ModPWithOracle_iff_exists_GapPWithOracle + +/-- +info: 'Cslib.Complexity.mem_coModPWithOracle_iff_exists_GapPWithOracle' depends on axioms: [propext, + Classical.choice, + Quot.sound] +-/ +#guard_msgs in +#print axioms Cslib.Complexity.mem_coModPWithOracle_iff_exists_GapPWithOracle + /-- info: 'Cslib.Complexity.SharpP.encoded_comp_mem_of_computableInPolyTimeWithOracle' depends on axioms: [propext, Classical.choice,