Skip to content

feat(Complexity): parameter-sensitive reductions, DFS batching, and word-oracle transfer #4530

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
SamuelSchlesinger merged 15 commits into from
Nov 13, 2026
Merged

feat(Complexity): parameter-sensitive reductions, DFS batching, and word-oracle transfer #4530

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
15 commits
Select commit Hold shift + click to select a range
5a074ae
feat(complexity): disjoint-instance, stack, and bounded-oracle reduct…
SamuelSchlesinger Nov 11, 2026
bc63e0f
Merge remote-tracking branch 'origin/main' into feat/218c-facility-lo…
SamuelSchlesinger Nov 11, 2026
582c534
chore(complexity): factor shared proof plumbing and clarify manual pr…
SamuelSchlesinger Nov 11, 2026
3e66d52
fix(complexity): rename BoundedOracleReduction.complLeft/complSelf fo…
SamuelSchlesinger Nov 11, 2026
c57d646
fix(Complexity): reuse reduce_add_decide_le and add dummyStackSpec ex…
SamuelSchlesinger Nov 11, 2026
e73a3e5
fix(Complexity): resolve reviewer findings for DisjointInstances
SamuelSchlesinger Nov 11, 2026
de6fa2b
Fix dummyStackSpec proofs for exponential rounds
SamuelSchlesinger Nov 11, 2026
96cb5b8
chore: wrap line 413 to satisfy 100 char limit
SamuelSchlesinger Nov 11, 2026
b073827
test: make dummyStackSpec non-vacuous for 4530 review
SamuelSchlesinger Nov 11, 2026
cc3a552
Merge remote-tracking branch 'origin/main' into feat/218c-facility-lo…
Nov 11, 2026
dbb91b4
tests: cleanly verify active exponential traversal using countdownSta…
Nov 11, 2026
9789511
tests: wrap long lines > 100 chars in DisjointInstancesAndOracleReduc…
Nov 11, 2026
64c97bc
tests: wrap remaining lines > 100 chars in DisjointInstancesAndOracle…
Nov 11, 2026
ec86a27
Merge main and repair M04 reduction/resource clients
edemaine Nov 13, 2026
ff356b5
Import the shared reduction bound at its proof client
edemaine Nov 13, 2026
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
2 changes: 2 additions & 0 deletions CslibFrontier.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down Expand Up @@ -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
Expand Down
Loading
Loading