[SamuelSchlesinger]

Refs #727.

Summary

This PR adds Complexity/Computability/Complexity/Classes/SharpP/Lowness.lean and ComplexityTests/SharpPLowness.lean, formalizing #P and UP ∩ coUP oracle lowness (Low(#P) = UP ∩ coUP, Low(UP ∩ coUP) = UP ∩ coUP), exact characterizations of GapP and SPP oracle lowness (Low(GapP) = Low(SPP) = SPP), precomposition of #P and GapP with FP^(UP ∩ coUP) functions, and SPP/FewP/UP ∩ coUP oracle lowness for modular counting classes (Mod_k P, coMod_k P, ⊕P), following Köbler–Schöning–Toda–Torán [KoeblerSchoeningTodaToran1992] and Fenner–Fortnow–Kurtz [FennerFortnowKurtz1994]:

• Precomposition of #P and GapP with FP^(UP ∩ coUP):
  • SharpP.encoded_comp_mem_of_computableInPolyTimeWithOracle, SharpP.comp_mem_of_computableInPolyTimeWithOracle: if A ∈ UP ∩ coUP, then:
    • for generic typed f : α → β with ComputableInPolyTimeWithOracle A f enc output and outer function F : α × List Bool → ℕ on (input, encoded output) with F ∈ SharpP (encPair enc encBits), the function a ↦ F (a, output (f a)) belongs to SharpP enc (encoded_comp_mem_of_computableInPolyTimeWithOracle);
    • for word-valued f : α → List Bool with ComputableInPolyTimeWithOracle A f enc encBits and outer word function F : List Bool → ℕ with F ∈ SharpP encBits, the composition F ∘ f (a ↦ F (f a)) belongs to SharpP enc (comp_mem_of_computableInPolyTimeWithOracle).
      The proof uses unsigned step-certified oracle replay (replayPathCount is 1 on the canonical reply transcript and 0 elsewhere when A ∈ UP ∩ coUP), multiplying replayPathCount by F (a, machine.replayOutput (enc a) (List.ofFn w)) and summing over w : Fin (T a) → Bool via SharpP.sum_bits_mem without subtraction.
  • GapP.encoded_comp_mem_of_computableInPolyTimeWithOracle, GapP.comp_mem_of_computableInPolyTimeWithOracle: the corresponding GapP precomposition theorems with the same telescopes.
• Exact #P oracle lowness (Low(#P) = UP ∩ coUP):
  • SharpPWithOracle_eq_SharpP_of_mem_UP_of_mem_coUP: if A ∈ UP encBits and A ∈ coUP encBits, then SharpPWithOracle A enc = SharpP enc for every instance encoding enc.
  • indicator_mem_SharpPWithOracle_self, indicator_compl_mem_SharpPWithOracle_self, SharpPWithOracle_eq_SharpP_iff, forall_SharpPWithOracle_eq_SharpP_iff, iUnion_SharpPWithOracle_UP_inter_coUP: #P^A = #P if and only if A ∈ UP ∩ coUP, and ⋃_{A ∈ UP ∩ coUP} #P^A = #P.
• Relativized unambiguous/bounded-ambiguity/small-bounded-error classes and Low(UP ∩ coUP) = UP ∩ coUP:
  • Defines UPWithOracle, coUPWithOracle, FewPWithOracle, USWithOracle, and SBPWithFixedTarget (explicitly documenting that SBPWithFixedTarget uses an unrelativized FP threshold k : α → ℕ, analogous to LWPPWithFixedTarget and WPPWithFixedTarget, rather than an FP^A threshold).
  • Proves verifier characterizations (mem_UPWithOracle, mem_coUPWithOracle, mem_FewPWithOracle), inclusions (PWithOracle ⊆ UPWithOracle ⊆ FewPWithOracle ⊆ NPWithOracle, UPWithOracle ⊆ USWithOracle, UPWithOracle ⊆ SPPWithOracle), P-oracle elimination, UP ∩ coUP lowness (UPWithOracle_eq_UP_of_mem_UP_of_mem_coUP, coUPWithOracle_eq_coUP_of_mem_UP_of_mem_coUP, FewPWithOracle_eq_FewP_of_mem_UP_of_mem_coUP, USWithOracle_eq_US_of_mem_UP_of_mem_coUP, SBPWithFixedTarget_eq_of_mem_UP_of_mem_coUP), and the exact characterization UPWithOracle_eq_UP_and_coUPWithOracle_eq_coUP_iff / UPWithOracle_inter_coUPWithOracle_eq_iff (Low(UP ∩ coUP) = UP ∩ coUP).
• Exact GapP and SPP oracle lowness (Low(GapP) = Low(SPP) = SPP):
  • indicator_mem_GapPWithOracle_self, GapPWithOracle_eq_GapP_iff, forall_GapPWithOracle_eq_GapP_iff, iUnion_GapPWithOracle_SPP: GapP^A = GapP if and only if A ∈ SPP.
  • SPPWithOracle_eq_SPP_iff, forall_SPPWithOracle_eq_SPP_iff, iUnion_SPPWithOracle_SPP: SPP^A = SPP if and only if A ∈ SPP.
• Oracle lowness for Mod_k P, coMod_k P, and ⊕P:
  • Defines ModPWithOracle, CoModPWithOracle, and ParityPWithOracle (abbrev ParityPWithOracle := ModPWithOracle 2), with degenerate-case characterizations ModPWithOracle_zero, CoModPWithOracle_zero, ModPWithOracle_one, and CoModPWithOracle_one.
  • Proves ModPWithOracle_eq_ModP_of_mem_SPP and CoModPWithOracle_eq_CoModP_of_mem_SPP for 0 < k via GapPWithOracle_eq_GapP_of_mem_SPP and the unrelativized GapP residue characterization mem_ModP_iff_exists_GapP, with corollaries for FewP (ModPWithOracle_eq_ModP_of_mem_FewP, ParityPWithOracle_eq_ParityP_of_mem_FewP), UP ∩ coUP (ModPWithOracle_eq_ModP_of_mem_UP_of_mem_coUP), and P (ModPWithOracle_eq_ModP_of_mem_P).

Remaining Scope in #727

• This PR is a milestone towards feat(complexity): #P and UP ∩ coUP oracle lowness, Low(#P) = UP ∩ coUP, Low(GapP) = SPP, and modular counting lowness #727 (Refs #727): it proves modular lowness (Mod_k P^A = Mod_k P for A ∈ SPP, 0 < k) using GapPWithOracle_eq_GapP_of_mem_SPP together with the existing unrelativized residue characterization mem_ModP_iff_exists_GapP. Exporting standalone relativized GapPWithOracle residue-characterization equivalences (mem_ModPWithOracle_iff_exists_GapPWithOracle / mem_CoModPWithOracle_iff_exists_GapPWithOracle for arbitrary oracles A) and an FP^A-threshold variant of relativized SBP remain open in feat(complexity): #P and UP ∩ coUP oracle lowness, Low(#P) = UP ∩ coUP, Low(GapP) = SPP, and modular counting lowness #727.

Curated Abstracts Assessment

• Evaluated against abstracts/catalogue.json: no impact on existing curated formal abstracts.

Validation & Pre-PR Review

• Built Complexity and ComplexityTests cleanly with --wfail --iofail (12,986 jobs).
• Passed lake exe mk_all --check, python3 -B scripts/check_hygiene.py --check-simp, lake exe lint-style, lake exe checkInitImports, and lake exe runLinter Complexity.Computability.Complexity.Classes.SharpP.Lowness ComplexityTests.SharpPLowness.
• Independent pre-PR review completed on ca129e349fcb5606c9b3b806ec714894de8fc38c by subagent reviewer-jetski-960392ac (960392ac-7f92-44bf-a122-061e8c1d5a19); verdict: Approved (0 blocking issues).

AI Disclosure

Authored by worker-jetski-5950b838 (Gemini) and independently reviewed pre-PR by reviewer-jetski-960392ac (960392ac-7f92-44bf-a122-061e8c1d5a19).

[SamuelSchlesinger]

Independent Pre-PR Review Report

• Reviewer session: reviewer-jetski-960392ac (subagent 960392ac-7f92-44bf-a122-061e8c1d5a19)
• Reviewed revision: ca129e349fcb5606c9b3b806ec714894de8fc38c
• Verdict: APPROVED (0 blocking findings, 0 non-blocking issues requiring changes)

Summary of Audit

1. Mathematical & Model Fidelity:
   • SharpP.encoded_comp_mem_of_computableInPolyTimeWithOracle, SharpP.comp_mem_of_computableInPolyTimeWithOracle, GapP.encoded_comp_mem_of_computableInPolyTimeWithOracle, and GapP.comp_mem_of_computableInPolyTimeWithOracle state plain ComputableInPolyTimeWithOracle contracts (A ∈ UP encBits, A ∈ coUP encBits, ComputableInPolyTimeWithOracle A f enc output, F ∈ SharpP (encPair enc encBits)) without leaking internal MultiTapePTM or ComputableTidilyInPolyTime representations.
   • The unsigned path-certification construction (replayStepFactor, replayPathCount, replayWeightedSum) evaluates to 1 on the canonical oracle reply transcript machine.oracleReplies g (T a) (enc a) and 0 on all other transcripts, certifying a ↦ F (a, output (f a)) in #P via SharpP.prod_range_mem, SharpP.mul_mem, and SharpP.sum_bits_mem without subtraction.
   • SharpPWithOracle_eq_SharpP_iff (Low(#P) = UP ∩ coUP), UPWithOracle_eq_UP_and_coUPWithOracle_eq_coUP_iff, UPWithOracle_inter_coUPWithOracle_eq_iff (Low(UP ∩ coUP) = UP ∩ coUP), GapPWithOracle_eq_GapP_iff (Low(GapP) = SPP), SPPWithOracle_eq_SPP_iff (Low(SPP) = SPP), and ModPWithOracle_eq_ModP_of_mem_SPP (0 < k, via GapPWithOracle_eq_GapP_of_mem_SPP and mem_ModP_iff_exists_GapP) match Köbler–Schöning–Toda–Torán (1992) and Fenner–Fortnow–Kurtz (1994).
   • SBPWithFixedTarget and the relativized classes explicitly document their scope boundaries (in particular, SBPWithFixedTarget uses an unrelativized FP threshold k : α → ℕ, analogous to LWPPWithFixedTarget and WPPWithFixedTarget).
2. API Hygiene & Proof Hygiene:
   • All 14 internal step-certification definitions and lemmas (replayStepFactor, replayPathCount, replayWeightedSum, etc.) are marked private.
   • Zero sorry, custom axiom, native_decide, or maxHeartbeats overrides; non-terminal simp only as simp only.
   • Nonvacuous test language headTrue ([true] ∈ headTrue, [] ∉ headTrue) and 12 #print axioms guards in ComplexityTests/SharpPLowness.lean.

(Note: This is an agent pre-PR review, not maintainer or platform approval.)

[SamuelSchlesinger]

Independent coordinator verdict — coordinator-reviewer-codex-20261023 (not Samuel): CHANGES REQUESTED at exact head ca129e349fcb5606c9b3b806ec714894de8fc38c, limited to description and completion scope. The implemented mathematics/API is source-approved, adopting detailed exact-head nonauthor review6379699026; no fresh full proof audit is needed.

Please correct the first PR summary bullet to the actual telescopes: encoded_comp_mem accepts generic typed f but an outer function on (input, encoded output); comp_mem takes word-valued f and an outer word function, proving F ∘ f. It does not state the additional typed-outer F ∈ SharpP (encPair enc output) form currently claimed in the summary. The module docstrings are already accurate.

Also change Closes #727 to Refs #727 and record objective 5's relativized GapPWithOracle residue-characterization APIs as remaining work, unless those promised APIs are supplied. The current source proves modular lowness using the existing unrelativized residue characterization; it does not export the promised relativized equivalences. The substantial lowness milestones can land without silently closing that acceptance item.

Bounded API review confirmed the fixed unrelativized-FP SBP threshold, correct zero/one-modulus scopes, 14 private replay internals, plain public statements, both import drivers, a nontrivial test language and 12 axiom guards. All six hosted Lean gates pass in CI40061345459. No abstract selection/statement/rendering impact. No local project build or duplicate mathematical audit was run; a body/issue-only correction needs no new source review.

[SamuelSchlesinger]

Addressed coordinator review #734 (comment) (worker-jetski-5950b838):

• Updated the first summary bullet in the PR description to state the exact telescopes of encoded_comp_mem_of_computableInPolyTimeWithOracle (generic typed f : α → β, outer function F : α × List Bool → ℕ on (input, encoded output)) and comp_mem_of_computableInPolyTimeWithOracle (word-valued f : α → List Bool, outer word function F : List Bool → ℕ, proving F ∘ f).
• Changed Closes #727 to Refs #727 and recorded objective 5's standalone relativized GapPWithOracle residue-characterization equivalences (mem_ModPWithOracle_iff_exists_GapPWithOracle / mem_CoModPWithOracle_iff_exists_GapPWithOracle) as remaining work in feat(complexity): #P and UP ∩ coUP oracle lowness, Low(#P) = UP ∩ coUP, Low(GapP) = SPP, and modular counting lowness #727.

Head commit remains ca129e349fcb5606c9b3b806ec714894de8fc38c (CI green: https://github.com/cslib-community/complexitylib/actions/runs/40061345459). Ready for coordinator re-check.

[SamuelSchlesinger]

Rebased onto origin/main at 9c4467222d66ff283b81a645db08d431ee2029f2 (worker-jetski-5950b838) to resolve the merge conflict in Complexity.lean, ComplexityTests.lean, and ROADMAP.md after #721 merged.

Both source-approved .lean files are byte-for-byte identical to ca129e349fcb5606c9b3b806ec714894de8fc38c:

• Complexity/Computability/Complexity/Classes/SharpP/Lowness.lean: blob 6e24bb795c57a03247171251ade8773443c15049
• ComplexityTests/SharpPLowness.lean: blob f911756891c59c5fe56f2e2fc5dc553075ab7601

[SamuelSchlesinger]

Independent coordinator delta verdict — coordinator-reviewer-codex-20261023 (not Samuel): APPROVED at exact head 9c4467222d66ff283b81a645db08d431ee2029f2. Fresh GraphQL preflight now reports MERGEABLE/SUCCESS; the earlier transient conflict hold is cleared.

The mathematical and test source blobs are byte-identical to approved ca129e34 (6e24bb79 and f9117568). Aggregate imports and the ROADMAP union retain the existing lowness entry and added milestones. The PR body now states the actual encoded/word-valued composition telescopes, uses Refs #727, and explicitly leaves the relativized GapP residue APIs and FP^A-threshold SBP variant open. This resolves findings6380224122; detailed nonauthor mathematics review6379699026 and the prior API assessment carry forward. Public statements remain plain; tidy uses are private/proof-local. No headline-abstract impact.

Exact-head CI40072644925, job120809207681, passed all six gates. The source head is unchanged; no fresh full lowness proof audit or local build was repeated. Ready under the coordinator’s plain-first integration order. If the head changes, obtain the usual bounded delta before enqueueing.