Skip to content

feat(Classes/Hierarchy): nondeterministic time hierarchy at every integer degree #2036

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 21 commits into from
Oct 31, 2026
Merged

feat(Classes/Hierarchy): nondeterministic time hierarchy at every integer degree #2036

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
21 commits
Select commit Hold shift + click to select a range
415d328
feat(Classes/Time): explicit-time verifier characterization of NTIME …
SamuelSchlesinger Oct 31, 2026
d0d8822
Merge origin/main into claude/ntime-hierarchy
SamuelSchlesinger Oct 31, 2026
4a2a973
feat(Classes/Hierarchy): coarse nondeterministic time hierarchy by la…
SamuelSchlesinger Oct 31, 2026
123ef60
refactor(Classes/Space): use the public bounded-existential edges in …
SamuelSchlesinger Oct 31, 2026
ba518a6
doc(Classes/Hierarchy): state the interval cases of the lazy diagonal…
SamuelSchlesinger Oct 31, 2026
430b810
feat(BigO/PolynomialPadding): unary rounded powers and NTIME_succ_pow_eq
SamuelSchlesinger Oct 31, 2026
99d1724
feat(Classes/Hierarchy): nondeterministic time hierarchy at every int…
SamuelSchlesinger Oct 31, 2026
48a6545
refactor(Machines/PTM): make the pair sampler's proof configurations …
SamuelSchlesinger Oct 31, 2026
0a0db5a
Merge branch 'claude/ntime-hierarchy' into claude/ntime-lazy-diagonal
SamuelSchlesinger Oct 31, 2026
e994581
Merge remote-tracking branch 'origin/main' into claude/ntime-lazy-dia…
SamuelSchlesinger Oct 31, 2026
4e1cc48
refactor(BigO/Bounds): make ComputableInO.mono_time public
SamuelSchlesinger Oct 31, 2026
4336dcd
Merge branch 'claude/ntime-lazy-diagonal' into claude/ntime-pow-hiera…
SamuelSchlesinger Oct 31, 2026
3758452
feat(WordRAM): explicit-degree overhead for the Turing-machine simula…
SamuelSchlesinger Oct 31, 2026
bb6b1c5
feat(Classes/Time): explicit-time verifier characterization of NTIME …
SamuelSchlesinger Oct 31, 2026
4db81ee
feat(Frontier/TensorNetwork): leaf certificate and leaf bound for any…
SamuelSchlesinger Oct 31, 2026
95cbeef
fix(check): keep quick mode available with on-demand comparator chall…
SamuelSchlesinger Oct 31, 2026
02b0ffc
feat(Communication): dag-like protocols give circuits (#2019 M1) (#2048)
SamuelSchlesinger Oct 31, 2026
51354ea
feat(FineGrained): count models of every CNF in 2^O(N/√log N) by tens…
SamuelSchlesinger Oct 31, 2026
fe2f481
feat(Classes/Oracle): bounded-query oracle classes and P^{NP[O(log n)…
SamuelSchlesinger Oct 31, 2026
f5834e4
feat(Classes/Hierarchy): coarse nondeterministic time hierarchy by la…
SamuelSchlesinger Oct 31, 2026
f44bc67
Merge origin/main into claude/ntime-pow-hierarchy
SamuelSchlesinger Oct 31, 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
18 changes: 18 additions & 0 deletions Complexity.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -863,6 +863,7 @@ public import Complexity.Computability.Circuit.Continuity
public import Complexity.Computability.Circuit.Counting
public import Complexity.Computability.Circuit.Cyclic
public import Complexity.Computability.Circuit.Cyclic.Feedback
public import Complexity.Computability.Circuit.DagProtocol
public import Complexity.Computability.Circuit.Decomposable
public import Complexity.Computability.Circuit.Depth
public import Complexity.Computability.Circuit.Encoding.MapOp
Expand Down Expand Up @@ -1024,6 +1025,7 @@ public import Complexity.Computability.Circuit.Monotone.Encoding
public import Complexity.Computability.Circuit.Monotone.Formula
public import Complexity.Computability.Circuit.Monotone.KarchmerWigderson
public import Complexity.Computability.Circuit.Monotone.Set
public import Complexity.Computability.Circuit.Monotone.Synthesis
public import Complexity.Computability.Circuit.Parallel
public import Complexity.Computability.Circuit.Pi
public import Complexity.Computability.Circuit.Pointwise
Expand Down Expand Up @@ -1083,6 +1085,7 @@ public import Complexity.Computability.Circuit.Unfolding
public import Complexity.Computability.Circuit.Wiring
public import Complexity.Computability.Communication.Amplification
public import Complexity.Computability.Communication.Corruption
public import Complexity.Computability.Communication.DagProtocol
public import Complexity.Computability.Communication.Discrepancy
public import Complexity.Computability.Communication.Disjointness
public import Complexity.Computability.Communication.Distributional
Expand Down Expand Up @@ -1179,9 +1182,12 @@ public import Complexity.Computability.Complexity.Classes.FewP.Machine
public import Complexity.Computability.Complexity.Classes.FunctionTime
public import Complexity.Computability.Complexity.Classes.FunctionTime.Bounds
public import Complexity.Computability.Complexity.Classes.FunctionTime.Decide
public import Complexity.Computability.Complexity.Classes.FunctionTime.WordRAM
public import Complexity.Computability.Complexity.Classes.Hierarchy
public import Complexity.Computability.Complexity.Classes.Hierarchy.LogClock
public import Complexity.Computability.Complexity.Classes.Hierarchy.Nondeterministic
public import Complexity.Computability.Complexity.Classes.Hierarchy.NondeterministicPolynomial
public import Complexity.Computability.Complexity.Classes.Hierarchy.NondeterministicTime
public import Complexity.Computability.Complexity.Classes.Hierarchy.Polynomial
public import Complexity.Computability.Complexity.Classes.Hierarchy.ShortDesc
public import Complexity.Computability.Complexity.Classes.Hierarchy.Space
Expand Down Expand Up @@ -1239,13 +1245,15 @@ public import Complexity.Computability.Complexity.Classes.ModP.Time
public import Complexity.Computability.Complexity.Classes.NP
public import Complexity.Computability.Complexity.Classes.NP.Closure
public import Complexity.Computability.Complexity.Classes.NP.GuessVerify
public import Complexity.Computability.Complexity.Classes.NP.Image
public import Complexity.Computability.Complexity.Classes.NP.Nondeterministic
public import Complexity.Computability.Complexity.Classes.NP.SelfReduction
public import Complexity.Computability.Complexity.Classes.NP.TruthTable
public import Complexity.Computability.Complexity.Classes.NP.Witness
public import Complexity.Computability.Complexity.Classes.Operators
public import Complexity.Computability.Complexity.Classes.Oracle
public import Complexity.Computability.Complexity.Classes.Oracle.BakerGillSolovay
public import Complexity.Computability.Complexity.Classes.Oracle.BoundedQuery
public import Complexity.Computability.Complexity.Classes.Oracle.Closure
public import Complexity.Computability.Complexity.Classes.Oracle.Collapse
public import Complexity.Computability.Complexity.Classes.Oracle.Counting
Expand All @@ -1257,6 +1265,7 @@ public import Complexity.Computability.Complexity.Classes.Oracle.Lowness
public import Complexity.Computability.Complexity.Classes.Oracle.Monotone
public import Complexity.Computability.Complexity.Classes.Oracle.PP
public import Complexity.Computability.Complexity.Classes.Oracle.PolyTime
public import Complexity.Computability.Complexity.Classes.Oracle.QueryBit
public import Complexity.Computability.Complexity.Classes.Oracle.Space
public import Complexity.Computability.Complexity.Classes.Oracle.TQBF
public import Complexity.Computability.Complexity.Classes.P
Expand All @@ -1282,6 +1291,7 @@ public import Complexity.Computability.Complexity.Classes.PP.Oracle
public import Complexity.Computability.Complexity.Classes.PP.Time
public import Complexity.Computability.Complexity.Classes.PP.TruthTable
public import Complexity.Computability.Complexity.Classes.Padding
public import Complexity.Computability.Complexity.Classes.Padding.NondeterministicPolynomial
public import Complexity.Computability.Complexity.Classes.Padding.Polynomial
public import Complexity.Computability.Complexity.Classes.ParityP
public import Complexity.Computability.Complexity.Classes.ParityP.Closure
Expand Down Expand Up @@ -1347,7 +1357,9 @@ public import Complexity.Computability.Complexity.Classes.TFNP.Subclasses.Princi
public import Complexity.Computability.Complexity.Classes.Tally
public import Complexity.Computability.Complexity.Classes.Time
public import Complexity.Computability.Complexity.Classes.Time.AcceptCount
public import Complexity.Computability.Complexity.Classes.Time.BoundedExists
public import Complexity.Computability.Complexity.Classes.Time.Polynomial
public import Complexity.Computability.Complexity.Classes.Time.Verifier
public import Complexity.Computability.Complexity.Classes.Toda
public import Complexity.Computability.Complexity.Classes.Toda.Counting
public import Complexity.Computability.Complexity.Classes.Toda.Hierarchy
Expand Down Expand Up @@ -1436,6 +1448,7 @@ public import Complexity.Computability.Complexity.FineGrained.SparseCountingScal
public import Complexity.Computability.Complexity.FineGrained.SparseParitySchedule
public import Complexity.Computability.Complexity.FineGrained.Sparsification
public import Complexity.Computability.Complexity.FineGrained.ThreeOccurrenceReduction
public import Complexity.Computability.Complexity.FineGrained.WideClauseCounting
public import Complexity.Computability.Complexity.HardnessEncoding.PolyTime
public import Complexity.Computability.Complexity.HardnessEncoding.Program
public import Complexity.Computability.Complexity.Parameterized
Expand Down Expand Up @@ -1606,6 +1619,7 @@ public import Complexity.Computability.GenericRAM.Native.BooleanFold
public import Complexity.Computability.GenericRAM.Native.BooleanSearch
public import Complexity.Computability.GenericRAM.Native.Certificate
public import Complexity.Computability.GenericRAM.Native.Combinators
public import Complexity.Computability.GenericRAM.Native.Degree
public import Complexity.Computability.GenericRAM.Native.ExhaustiveCountFallback
public import Complexity.Computability.GenericRAM.Native.HeavyBranchFold
public import Complexity.Computability.GenericRAM.Native.IndexFold
Expand All @@ -1616,6 +1630,7 @@ public import Complexity.Computability.GenericRAM.Native.StackRecursionTree
public import Complexity.Computability.GenericRAM.Native.SubsetPairFold
public import Complexity.Computability.GenericRAM.Signed
public import Complexity.Computability.GenericRAM.Signed.Fits
public import Complexity.Computability.GenericRAM.Simulation.Degree
public import Complexity.Computability.GenericRAM.Simulation.Finite
public import Complexity.Computability.GenericRAM.Simulation.Run
public import Complexity.Computability.GenericRAM.Simulation.Turing
Expand Down Expand Up @@ -2022,6 +2037,7 @@ public import Complexity.Computability.Machines.Turing.MultiTape.Probabilistic.O
public import Complexity.Computability.Machines.Turing.MultiTape.Probabilistic.Oracle
public import Complexity.Computability.Machines.Turing.MultiTape.Probabilistic.OutputPrefix
public import Complexity.Computability.Machines.Turing.MultiTape.Probabilistic.OutputToTape
public import Complexity.Computability.Machines.Turing.MultiTape.Probabilistic.PairSampler
public import Complexity.Computability.Machines.Turing.MultiTape.Probabilistic.PolynomialClock
public import Complexity.Computability.Machines.Turing.MultiTape.Probabilistic.QueryBounds
public import Complexity.Computability.Machines.Turing.MultiTape.Probabilistic.QueryTake
Expand Down Expand Up @@ -2344,6 +2360,7 @@ public import Complexity.Computability.WordRAM.Multiword.Sub
public import Complexity.Computability.WordRAM.Multiword.Transfer
public import Complexity.Computability.WordRAM.Multiword.Workspace
public import Complexity.Computability.WordRAM.Native
public import Complexity.Computability.WordRAM.NativeDegree
public import Complexity.Computability.WordRAM.Notation
public import Complexity.Computability.WordRAM.OfTuring
public import Complexity.Computability.WordRAM.PackedCount
Expand Down Expand Up @@ -2373,6 +2390,7 @@ public import Complexity.Computability.WordRAM.Subroutine
public import Complexity.Computability.WordRAM.Time
public import Complexity.Computability.WordRAM.Trace
public import Complexity.Computability.WordRAM.Turing
public import Complexity.Computability.WordRAM.Turing.Overhead
public import Complexity.Computability.WordRAM.Width
public import Complexity.Crypto.Computational.Basic
public import Complexity.Crypto.Computational.CollisionResistant
Expand Down
Loading
Loading