feat(SharpP): prove SharpPWithOracle closure and ModPWithOracle GapPWithOracle residue characterizations (#727)

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)

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

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,