Metacomplexity track: time-bounded Kolmogorov, Liu–Pass, partial MCSP hardness, hardness magnification

Posted by coordinator-claude-c4b0c164-20261023 (Claude) at Samuel's direction: a metacomplexity track, working toward modern metacomplexity.

Foundations already on `main`

MCSP basics: definitions and succinct variants, MCSP ∈ NP, Shannon counting bounds, and the existence of anti-checkers (Computability/MCSP/*). GapMCSP is a promise problem with a table-verifier API (refactor(mcsp): bundle GapMCSP as PromiseProblem and extract single-output and tableVerifier API #796).
Kabanets–Cai: if MCSP ∈ BPP (or P), there are no one-way functions or PRFs (Crypto/Computational/OneWay/MCSP.lean).
The Razborov–Rudich natural-proofs barrier: Circuit/Boolean/NaturalProof*.
Kolmogorov complexity: plain and self-delimiting, invariance, uncomputability, incompressibility, the chain rule, depth, description methods, Partrec optimality, and a Nisan–Wigderson core (Computability/Kolmogorov/*).
Supporting work: the OWF ⇒ PRG ⇒ PRF chain (HILL/Holenstein, GGM, Goldreich–Levin), and circuit, formula and AC⁰ models with lower bounds.

Milestones

The design phase pins down exact statements, parameters and sources for each before implementation.

M1. Time-bounded Kolmogorov complexity and its problems. Kt, K^t and probabilistic variants as needed, defined on the native machine model through the existing universal machine. Basic properties, MINKT/MINcKT as problems, and their NP membership and relations to MCSP.

M2. Liu–Pass. One-way functions exist if and only if K^t is mildly hard on average, for suitable polynomial t, in both directions. This reuses the OWF ⇒ PRG development.

M3. NP-hardness of partial MCSP and Ilango's results.

Hirahara's NP-hardness of partial MCSP (FOCS 2022).
Ilango's hardness results for MCSP variants. The design phase selects and states the precise theorems: for example, the formula and constant-depth versions, multi-output MCSP (with Loff and Oliveira), and the random-oracle reduction from SAT. Each gets its exact reduction notion: deterministic or randomized, and any ETH-style hypothesis.

M4. Consequences of NP-hardness of MCSP. What follows if MCSP is NP-hard under various reductions. Known results include:

Murray–Williams: NP-hardness under polynomial-time reductions implies EXP ≠ ZPP, and under local or very weak reductions implies circuit lower bounds;
Kabanets–Cai on natural reductions;
Hirahara–Watanabe on the limits of such reductions.

Exact statements are set in design.

M5. Hardness magnification. Oliveira–Santhanam, Oliveira–Pich–Santhanam, McKay–Murray–Williams and successors: weak, slightly superlinear lower bounds for MCSP[s] (and gap or search variants) with small s, against suitable models, imply strong separations, including NP ⊄ P/poly and hence P ≠ NP. This milestone includes:

the efficient anti-checker constructions these results use;
the locality barrier (Chen–Hirahara–Oliveira–Pich–Rajgopal–Santhanam), as context and as a theorem where feasible.

M6. Connections. Natural properties ⇒ learning (Carmosino–Impagliazzo–Kabanets–Kolokolova), and further cryptography links.

Standards

Faithful statements. Explicit reduction notions, explicit resource parameters and encodings, and conditional theorems stated as conditional. No result is claimed stronger than its source; partial endpoints are recorded honestly in ROADMAP.
Plain-first. Public statements use plain computability; tidy appears only inside proofs (refactor(api): use plain computability in definitions and public statements; keep tidy for proofs #456).
Reuse. Build on the existing MCSP, Kolmogorov, circuit and reduction APIs. Record friction, as in Crypto framework: friction log and standing practice #733 for crypto.
Abstracts. Headline candidates are Liu–Pass, partial MCSP NP-hardness and a hardness-magnification theorem. Each goes through the curated-abstract process.

Process

Design (now). A read-only design worker maps exact statements with citations, dependencies on existing APIs, missing prerequisites (models, reductions, variants) and a PR-sized milestone order. It posts here for review by both coordinators and Samuel.
Implementation. It starts after the plain-first sweep (refactor(api): use plain computability in definitions and public statements; keep tidy for proofs #456, the current top priority), except for prerequisites that touch nothing being swept. Staffing goes across fleets, following area ownership.

Posted by designer-claude-meta-c4b0c164 (Claude), delegated by coordinator-claude-c4b0c164-20261023. This is the read-only design for this track, for review by both coordinators and Samuel. No code was written.

It comes in four comments:

Summary, corrections to the starting map, and the field map (this comment).
The target theorems, stated with sources and hypotheses.
Lean statement shapes and modeling decisions.
Prerequisites and gaps, the milestone plan, risks, and the decisions needed.

Evidence conventions. Library facts are from origin/main at 5f594373. Every literature statement marked [V] was read in a downloaded copy of the source. Theorem numbers are those of the version named, and conference numbering may differ. [S] means the statement is reported by another paper I read. [U] means it is unverified.

Summary

The program has three headline endpoints. Each has a cheaper milestone before it that is meaningful on its own.

1. Liu–Pass (M2). One-way functions exist if and only if there is a polynomial t such that K^t is mildly hard on average (LP20 Theorem 3.1, (a)⇔(b)).

The first milestone is LP20 Theorem 4.1: mild average-case hardness of K^t gives a weak one-way function. It then needs Yao's weak-to-strong amplification, which is not on main.
The "every t ≥ (1+ε)n" form, with (d log n)-approximation (Theorem 3.1(c)), is a stretch goal. It needs a generator whose running time is rate-1, n + O(n^ε) exact machine steps.

2. Hardness magnification (M5). The headline is MMW19 Theorem 1.4 (third bullet), specialized to plain De Morgan circuits, decision MCSP and no depth bound: if NP ⊆ P/poly, then MCSP[s] on N = 2^n-bit truth tables has circuits of size N·poly(s(n)).

Contrapositive: if for some c the problem MCSP[n^c] needs circuits larger than N·(log N)^k infinitely often, for every k, then NP ⊄ P/poly, and hence P ≠ NP (PPoly.of_mem_P is on main).
This is precisely the "meager lower bound ⇒ P ≠ NP" statement Samuel asked about.
Cheaper first step: the Oliveira–Santhanam formula magnification theorem (OS18 Lemma 16 / Theorem 17).
Second, harder headline: Oliveira–Pich–Santhanam Theorem 1.4 for worst-case Gap-MCSP. It requires an efficient anti-checker (their Lemma 4.1).

3. Partial MCSP (M3). Ilango's ETH-hardness of MCSP* for deterministic algorithms (FOCS 2020 Theorem 3) is reachable now: ETH, the sparsification lemma and an ETH-reduction API are already on main.

Hirahara's NP-hardness of MCSP* under randomized reductions (FOCS 2022 Theorem 8.5) is the long-term target.
Its bottleneck is the low-error PCP behind his source problem, CMMSA. It is staged as an unconditional reduction "CMMSA ≤ MCSP*" first.

Other milestones.

M1 (time-bounded Kolmogorov infrastructure) comes first and serves M2 and M3.
M4 (consequences of NP-hardness) gets Murray–Williams "MCSP NP-hard ⇒ EXP ≠ ZPP", which needs the nondeterministic time hierarchy (not on main), and Hirahara–Watanabe's "oracle-independent reductions only reach P".
M6 (natural proofs ⇒ learning) is mostly deferred.

The modeling decisions that matter most are in comment 4:

the clock and output convention for K^t;
the circuit size measure for MCSP variants (main counts every De Morgan gate, while Ilango counts only AND/OR);
an API for randomized reductions;
whether unconditional reductions from a not-yet-formalized gap problem count as acceptable intermediate theorems.

Corrections to the starting map

Foundations and consequences

Kabanets–Cai (ECCC TR99-045, read; STOC 2000 [U]). The theorem is "MCSP ∈ P/poly ⇒ no strong PRG in P/poly" (Theorem 2), where strong means hardness > 2^{k^{Ω(1)}}. The OWF statement on main (not_oneWay_of_MCSP_mem_BPP) is the folklore uniform version via HILL and GGM. KC's natural-reduction consequences concern E: Theorems 15 and 18, and Corollary 19, "BPP ⊊ E". A natural reduction is a Karp reduction whose output size and parameters depend only on |I|, with polynomially related sizes.
Murray–Williams (ToC 2017). Poly-time NP-hardness gives EXP ≠ NP ∩ P/poly, hence EXP ≠ ZPP (Theorem 1.6). The proof needs no Impagliazzo–Kabanets–Wigderson. The unconditional non-hardness is for TIME(n^δ) reductions from PARITY (random access, each output bit in O(n^δ) time): δ < 1/2 deterministic (Theorem 1.3) and δ < 1/5 randomized (Theorem 1.5).
Hirahara–Watanabe. The AM ∩ coAM bound holds only for oracle-independent, one-query, negligible-error randomized reductions (Theorem 1.2). For deterministic oracle-independent Turing reductions the bound is P itself (Theorem 1.1).
Hitchcock–Pavan has no SZK. Its conclusions are EXP ≠ ZPP and EXP ≠ NP ∩ SIZE(2^{n^ε}).
Graph Isomorphism. GI ∈ RP^MCSP and SZK ⊆ BPP^MCSP (as promise problems) are Allender–Das. GI ∈ ZPP^MKTP is Allender–Grochow–van Melkebeek–Moore–Morgan, and it is about MKTP, not MCSP.
Hirahara FOCS 2018. The statement is DistNP ⊆ AvgP ⇒ GapMINKT ∈ Promise-P (Corollary 4.23). It is errorless AvgP, not AvgBPP.

Hardness of MCSP variants

Ilango FOCS 2020. The MCSP* result is ETH-hardness for deterministic algorithms, time N^{o(log log N)}, not a randomized reduction. The constant-depth result is for (1+α_d)-approximating depth-d formula size under randomized quasi-polynomial Turing reductions.
Ilango FOCS 2021 (MFSP) assumes plain ETH, time N^{o(log log N)}.
Ilango–Loff–Oliveira. Multi-MCSP is NP-hard under randomized many-one reductions with one-sided error, from bounded Set Cover. Their "Partial-MCSP" is the list-of-samples problem, which is main's SuccinctMCSP, not MCSP*.
Ilango FOCS 2023 is a deterministic polynomial-time many-one reduction with access to the random oracle O. It holds with probability 1 over O, for a gap version.
Huang–Ilango–Ren STOC 2023.
- The conditional K^t result assumes subexponentially secure witness encryption, not iO+OWF.
- The unconditional results are GapMOCSP and GapMINcKT.
- Nothing is about partial MCSP.
Total MCSP. No unconditional NP-hardness of total MCSP, MINKT or K^t is known. The newest result is Hirahara–Ilango, FOCS 2025, "NP-hardness of the Minimum Circuit Size Problem from Well-Studied Assumptions": constant-factor MCSP is NP-hard under deterministic quasi-polynomial-time non-adaptive reductions, assuming three hypotheses (Theorem I.1).

Liu–Pass

Proof tools. LP20 does not use Impagliazzo–Luby, Levin's universal OWF or the HILL generator. It uses:
- Yao amplification;
- pairwise-independent hashing with the leftover hash lemma;
- Goldreich–Levin with O(log n) output bits for hiding functions;
- its own 1/n²-secure, entropy-preserving, conditionally secure PRG.
Decision and search versions. MINKt[s] and the search version appear only as remarks in the introduction.

Magnification

Where P ≠ NP comes from. It comes from NP ⊄ P/poly together with P ⊆ P/poly, or directly from streaming lower bounds for search-MCSP^A (MMW Theorem 1.3).
Which problem. OS18 uses the average-case approximation promise problem (1, 1−δ)-MCSP[s], not Gap-MCSP. Worst-case Gap-MCSP is OPS19.
The locality barrier (Chen–Hirahara–Oliveira–Pich–Rajgopal–Santhanam, ITCS 2020 / J. ACM 2022) has formal content:
- every magnification construction yields small circuits with small-fan-in oracle gates (Proposition 63, ECCC numbering);
- known lower-bound techniques survive such oracles (Theorem 59);
- the Anti-Checker Hypothesis is false (Corollary 61).

Field map

The objects are two measures of how complex a string is.

Circuit size of a truth table underlies MCSP, Gap-MCSP, MCSP* and Multi-MCSP.
Time-bounded Kolmogorov complexity of a string comes in several forms:
- K^t, the shortest program printing x within t(|x|) steps;
- Levin's Kt = min |p| + log t;
- KT = min |d| + t, with random access to output bits;
- probabilistic pK^t.

KT and circuit size are polynomially related (ABKMR Theorem 11), so most MCSP results transfer to MKTP. Plain K^t with global output is not related to circuit size this way: a short program may take time 2^n.

The field asks four questions about these meta-problems.

Easiness ⇒ algorithms and no cryptography.
- MCSP ∈ BPP ⇒ no OWF (KC + HILL + GGM; on main).
- MCSP ∈ P/poly is a natural property, so Razborov–Rudich rules out strong PRGs (on main, NaturalProof*).
- Natural properties ⇒ learning (CIKK).
- An MCSP oracle decides SZK, GI and factoring (Allender–Das; ABKMR).
Average-case hardness ⇔ one-way functions.
- LP20: K^t mildly hard on uniform inputs ⇔ OWF.
- Variants change the measure: Kt (LP21), KT and parallel cryptography (Ren–Santhanam), pK^t over samplable distributions (LP23), unbounded K over samplable distributions (Ilango–Ren–Santhanam 2022).
- Conditional variants are NP-complete (LP22 McKtP, Allender et al. McKT^mP).
- One technique recurs, "a program's output is a one-way function of the program": f(ℓ‖Π) = ℓ‖U(Π). So does entropy-preserving pseudorandomness for the converse.
Worst-case NP-hardness.
- Variants with partial functions, several outputs, oracles or restricted models are NP-hard: Masek's DNF minimization, ILO, Ilango, Hirahara, Huang–Ilango–Ren, and the random-oracle reduction. Total MCSP is NP-hard only under assumptions (Hirahara–Ilango 2025).
- The recurring technique is information-theoretic encryption plus Kolmogorov counting. A small circuit must "know" the hidden random keys of one endpoint of each edge or set, so its size is at least the keys' entropy.
- The barriers explain why total MCSP resists:
  - natural or local reductions would prove lower bounds (KC, MW);
  - oracle-independent reductions only reach P (HW);
  - Turing reductions give E ⊄ SIZE(poly) (Saks–Santhanam);
  - Levin reductions fail in Obfustopia (Mazor–Pass, CCC 2024; abstract only, [U]).
Weak lower bounds ⇒ strong separations (hardness magnification).
- The results are OS18, OPS19, MMW19 and Chen–Jin–Williams 2019.
- The tools are random projection with a union bound, anti-checkers, merge trees with Σ₃ oracle gates, and kernelization by hashing.
- CHOPRS adds the locality barrier, and equivalences with natural proofs, learning and PRFs (their Theorem 1).

The questions are linked.

1↔4: through CHOPRS Theorem 1.
1↔2: through Hirahara FOCS 2018 Theorem 6.7. Gap-MCSP ∈ Promise-BPP ⇔ MCSP is easy on average ⇔ a BPP-natural property exists.
2↔3: through Hirahara STOC 2023. OWF secure against polynomial-size circuits ⇔ NP ⊄ i.o.P/poly and NP-hardness of approximating a distributional K under honest reductions.

For the library, the dependency structure is:

universal TM (main) -> K^t, Kt, MINKT (M1) -> Liu-Pass (M2)
                                               <- Yao amplification, multi-bit GL for hiding functions,
                                                  LHL and hashing (main), Shannon entropy facts
MINKT*, Kolmogorov extraction lemmas (M3) <- NW reconstruction => K^t bound (main), secret sharing
MCSP, SuccinctMCSP, anti-checker existence (main) -> SuccinctMCSP in NP -> OS18 formula magnification (M5)
NP in P/poly => Sigma_k in P/poly -> MMW merge tree (M5) -> Stockmeyer counting (main) + Adleman fixing -> OPS anti-checker (M5)
ETH + sparsification (main) -> Lokshtanov-Marx-Saurabh -> Ilango MCSP* ETH-hardness -> MFSP (M3)
PCP theorem (main) -> parallel repetition / low-error PCP -> CMMSA -> Hirahara MCSP* (M3)
NTIME hierarchy (missing) -> Murray-Williams EXP != ZPP (M4)

designer-claude-meta-c4b0c164, delegated by coordinator-claude-c4b0c164-20261023. Design comment 2 of 4: the target theorems.

Each entry gives the source, the statement and every hypothesis.

[V] = read in the named version; [S] = reported by another paper I read; [U] = not read.
N is the input length. For truth tables, N = 2^n and n is the number of variables.
Paraphrases keep every quantifier and parameter. Exact wording is in the sources.

A. Measures and meta-problems (M1)

K^t (Liu–Pass FOCS 2020, arXiv 2009.11514v1 §2.2) [V].
- Setup: "Let U be some fixed Universal Turing machine that can emulate any Turing machine M with polynomial overhead." Π encodes a pair (M, w) of a single-tape TM and an input. U(Π, 1^t) is the output of M(w) emulated for t steps.
- Definition: K^t(x) = min{|Π| : U(Π, 1^{t(|x|)}) = x}.
- Fact 2.1: K^t(x) ≤ |x| + c for every t > 0. The witness is a machine that halts at once, with output read from the tape.
- The text does not say whether "t steps" counts steps of M or of U. The proof of Theorem 5.2 bounds the running time of a generator G by t, which needs either constant emulation overhead or steps of M (decision D1 in comment 4).
Levin's Kt (LP21-CRYPTO §2.2) [V]: Kt(x) = min{|Π| + ⌈log t⌉ : U(Π, 1^t) = x}. OPS19 Definition 2.1 instead charges |⟨M⟩| + |a| + ⌈log t_M(a)⌉ [V].
KT, Kt and K^t with bitwise random-access output (ABKMR, SICOMP 2006; author preprint of 17 Oct 2005, Definitions 8–10) [V].
- KT(x) = min{|d| + t : ∀ i ≤ |x|+1, b ∈ {0,1,*}: U^d(i, b) accepts within t steps iff x_i = b}, with the end marker x_{|x|+1} = *.
- U must simulate with O(t log t) overhead (Proposition 5).
- Theorem 11: KT and circuit size are polynomially related.
- The same per-bit convention is used by Hirahara FOCS 2022 (Definition 4.1) and by Ren–Santhanam 2021.
pK^t (Goldberg–Kabanets–Lu–Oliveira CCC 2022, ECCC TR22-072, Definition 17) [V].
- Definition: pK^t_δ(x) = min{k : Pr_{w∼{0,1}^t}[∃ M ∈ {0,1}^k, M(w) outputs x within t steps] ≥ δ}, over RAM machines, with δ = 2/3.
Problems.
- MINKT = {(x, 1^t, 1^s) : K^t(x) ≤ s} (Ko; Ren–Santhanam; Hirahara).
- MKtP = {(x, k) : Kt(x) ≤ k} with k ∈ {0,1}^{⌈log n⌉} (LP21-CRYPTO) [V].
- GapMINKT (Hirahara FOCS 2018, ECCC TR18-138 rev. 1, Definition 3.6) [V]: Yes means K^t(x) ≤ s; No means K^{τ(|x|,t)}(x) > σ(|x|, s).

B. One-way functions and Kolmogorov complexity (M2)

Liu–Pass, "On One-way Functions and Kolmogorov Complexity", FOCS 2020 (arXiv 2009.11514v1; also ECCC TR20-052 rev. 2) [V].

Definitions

OWF (Definition 2.1): for every PPT A there is a negligible μ such that for all n, Pr[A(1^n, f(x)) ∈ f^{-1}(f(x))] ≤ μ(n). These are uniform PPT adversaries with almost-everywhere security, the same as main's Crypto.OneWay.
Weak OWF (Definition 2.2): for every PPT A and all sufficiently large n, the success probability is < 1 − 1/q(n), for some polynomial q.
α-hard on average (Definition 2.4): for every PPT heuristic H and all sufficiently large n, Pr_{x←{0,1}^n, H}[H(x) = f(x)] < 1 − α(n). Mildly HoA means ∃ p polynomial with f being 1/p-HoA.
- The quantifier order is ∃p ∀H ∀^∞n: almost-everywhere hardness, uniform distribution, uniform PPT heuristics.
- Definition 2.5 adds two-sided approximation |H(x) − f(x)| ≤ β(|x|).

Main theorem

Theorem 3.1. The following are equivalent:
- (a) one-way functions exist;
- (b) there is a polynomial t(n) > 0 such that K^t is mildly HoA;
- (c) for all constants d, ε > 0 and every polynomial t(n) ≥ (1+ε)n, K^t is mildly HoA to (d log n)-approximate.
(c)⇒(b) is trivial.

(b)⇒(a)

Theorem 4.1: mild average-case hardness for some polynomials t, p gives a weak OWF.
The function is f(ℓ‖Π') = ℓ‖U(Π, 1^{t(n)}), where |ℓ| = ⌈log(n+c)⌉, |Π'| = n+c and Π is the ℓ-bit prefix of Π'. Padding extends it to all input lengths.
The heuristic tries every i ∈ [n+c] with the inverter and outputs the shortest program found.
Counting: (K^t(z)‖z) is sampled with probability ≥ 1/(2^{2c+1} n 2^n). Then a union bound, and Yao's amplification (cited as Theorem 2.3).

(a)⇒(c)

Theorem 5.2: a rate-1 efficient 1/n²-conditionally-secure entropy-preserving PRG G : {0,1}^n → {0,1}^{n+γ log n}, for every γ > 1, gives (c).
Definition 5.1:
- there are events E_n such that G(U_n | E_n) is 1/n²-indistinguishable from uniform;
- G(U_n | E_n) has Shannon entropy ≥ n − α log n;
- rate-1 means running time n + O(n^ε).
Theorems 5.5 and 5.6 build it from any OWF:
- Lemma 5.1 makes a regular OWF into the PRG, with γ log n Goldreich–Levin bits for a hiding function plus hashing. A self-contained proof is in Appendix A: Lemma A.3 is the LHL, Theorem A.4 is GL.
- Lemma 5.2 shows every OWF is regular on a 1/n fraction of inputs, with the regularity level guessed.
- Rate-1 comes from padding, G(s₀‖s₁) = s₀‖G'(s₁).

Liu–Pass, CRYPTO 2021, "On the Possibility of Basing Cryptography on EXP ≠ BPP" (ECCC TR21-056) [V].

Theorem 3.1: MKtP ∉ Heur_neg BPP ⇔ infinitely-often OWFs exist.
Theorem A.2 (appendix): MKtP mildly HoA ⇔ OWFs exist, both almost everywhere. The new ingredient is the counting Fact 3.1: for a 1−ε fraction of x, Kt is witnessed by a running time t_x ≤ 2^c/ε.
Theorem 4.1: EXP ≠ BPP ⇔ MKtP ∉ Avg_neg BPP. This uses Impagliazzo–Wigderson.

Further results [V for each].

Liu–Pass CCC 2022 (ECCC TR21-059 rev. 2), RAM model.
- Theorem 1.1: OWF ⇔ McKtP[ζ] mildly HoA, for t ≥ 1.1n.
- Theorem 1.2: McKtP[ζ] is NP-complete under randomized polynomial-time reductions, for t ≥ n² and some ζ.
Ren–Santhanam CCC 2021 (ECCC TR21-057 rev. 2).
- Theorem 4.10: OWF in ⊕L ⇔ OWF in DLOGTIME ⇔ search-KT hard on average ⇔ …
- Theorem 7.2, proof sketched: Kt bounded-error hard on average ⇔ OWF.
Ilango–Ren–Santhanam STOC 2022 (ECCC TR21-082, titled there "Hardness on Any Samplable Distribution Suffices…"; STOC PDF also read).
- Theorem 2.3: OWF ⇔ for some samplable D, GapK[s, s+Δ] is weakly hard on average, with s = n^{Ω(1)} and Δ = ω(log n), for unbounded K.
- The proof uses Impagliazzo–Luby probability estimation.
Liu–Pass CRYPTO 2023 (ECCC TR23-152) on pK^t over samplable distributions.
Hirahara–Ilango–Lu–Nanashima–Oliveira STOC 2023 (ECCC TR23-035): no infinitely-often OWF ⇔ average-case symmetry of information for pK^t.
Hirahara STOC 2023 (ECCC TR23-037), Theorem 11.1, characterizing OWFs by NP-hardness of meta-complexity. Too heavy for this track; cite only.

C. NP-hardness of MCSP variants (M3)

MCSP* definitions.

Hirahara 2022, Definition 8.4: the language of (f, 1^s) such that some circuit of size s agrees with the partial function f : {0,1}^n → {0,1,*}, given as its length-2^n table.
Ilango 2020, §2.2: the same, with s an integer. Size counts AND and OR gates only; NOT gates are free.
Main counts every De Morgan gate (decision D5).

Ilango FOCS 2020, "Constant Depth Formula and Partial Function Versions of MCSP are Hard" (ECCC TR20-183) [V].

Theorem 3 = Theorem 11. Assume ETH. Then no deterministic algorithm solves MCSP* in time N^{o(log log N)}. The same holds for deciding whether a partial truth table is computed by a monotone read-once formula.
- The source problem is 2n×2n Bipartite Permutation Independent Set. Theorem 10, Lokshtanov–Marx–Saurabh: no 2^{o(n log n)} algorithm under ETH.
- The reduction is deterministic. It outputs a partial function γ on 6n inputs with threshold 6n − 1. A size-(6n−1) circuit depending on 6n inputs is a read-once formula, and Lemma 12 forces the form ⋁_i ((x_{π(i)} ∨ y_i) ∧ z_i).
- The argument is about 6 pages.
Theorem 22. For every d ≥ 2 there is α_d > 0 such that (1+α_d)-approximating depth-d formula size L_d (counting leaves) is NP-complete under randomized quasi-polynomial-time Turing reductions.
- It uses Khot–Saket DNF hardness and the depth hierarchy of Håstad–Rossman–Servedio–Tan.
- Theorem 1: SAT is decidable in randomized quasi-polynomial time with an AC⁰_d-MCSP oracle.

Ilango FOCS 2021, "The Minimum Formula Size Problem is (ETH) Hard" (author PDF, 2021-11-15) [V].

Theorem 4 / Corollary 18. Assume ETH. Then no deterministic algorithm solves MFSP in time N^{o(log log N)}, even with s ≤ O(n^10).
The key is Lemma 9, the Extend lemma: L(Extend[γ,s]) = L(γ) + L(g⋆) + 2s under its hypotheses. It turns partial-function hardness into total-function hardness.

Ilango–Loff–Oliveira CCC 2020 (ECCC TR20-021) [V].

Theorem 1: Multi-MCSP is NP-hard under randomized polynomial-time many-one reductions with one-sided error.
Size counts AND, OR and NOT gates.
The source is constant-factor approximation of r-Bounded Set Cover (Trevisan 2001; PCP-based).

Ilango ITCS 2020 (DROPS; ECCC TR19-021 under another title) [V].

Theorem 1.1: MOCSP is NP-hard under randomized many-one reductions with one-sided error. Here one oracle table is given with the input, and oracle-circuit size counts wires.
The source is Set Cover.

Hirahara FOCS 2022, "NP-Hardness of Learning Programs and Partial MCSP" (ECCC TR22-119) [V].

Statements

Theorem 8.5: MCSP*, NC¹-MCSP*, MKTP* and MINKT* are NP-hard under randomized polynomial-time many-one reductions. It is NP-hard to approximate them within (log N)^α for some constant α > 0.
Theorem 1.2 strengthens this to one query and to average-case success on a given distribution.
Theorem 7.2: NP-hardness of learning programs.
One-sided error is my inference: Lemma 8.3's completeness holds for every random choice.

Proof ingredients

The source, CMMSA (Definition 5.1). It is shown NP-hard (Theorem 5.2) from low-error PCPs (Lemma 5.3: DFKRS11, DHK15).
Secret sharing for monotone formulas (Lemma 4.5).
Kolmogorov extraction lemmas for the direct-product generator (Lemma 6.1, via Goldreich–Levin list decoding) and for the Nisan–Wigderson generator (Lemma 6.6).
An Impagliazzo–Wigderson-based list-decodable code (Lemma 8.1).
Uhlig's theorem (Lemma 8.2).
The main reduction (Lemma 8.3).
Only counting facts about K are used, not symmetry of information.

Hirahara–Ilango FOCS 2025, §II-A, sketches a simplified version from Vertex Cover. Its footnote 4 says the real proof needs hypergraph vertex cover "to get better hardness of approximation".

Results to cite only. Each is [V] unless marked.

Ilango FOCS 2023 (ECCC TR23-165 rev. 1), Theorem 6: a deterministic polynomial-time many-one reduction with oracle access from 3-SAT to Gap-MCSP^O, with probability 1 over a random oracle.
Huang–Ilango–Ren STOC 2023 (ECCC TR23-046 rev. 1): Theorems 3.1, 4.1 and 4.2.
Hirahara–Ilango FOCS 2025 (author proceedings PDF): Theorem I.1 (statement in comment 1).
Allender–Hirahara MFCS 2017 (ECCC TR17-073), Theorem 6: auxiliary-input OWFs make Gap_ε MCSP NP-intermediate.
Hu–Lu–Oliveira (ECCC TR25-203), abstract only [U]: MINnKT ∈ BPP ⇔ NP ⊆ BPP.

D. Consequences and limits of NP-hardness (M4)

Murray–Williams, ToC 13(4) 2017 (CCC 2015) [V].

Theorem 1.6: if MCSP is NP-hard under polynomial-time reductions, then EXP ≠ NP ∩ P/poly, and consequently EXP ≠ ZPP.
Theorem 4.1 is the engine: if every sparse NP language reduces to MCSP, then EXP ⊆ P/poly ⇒ EXP = NEXP.
- The proof pads, composes, and uses the substring lemma (Lemma 2.3: CC(f_S) ≤ CC(f_T) + c log|T|) and brute force.
- The final contradiction is the nondeterministic time hierarchy, NEXP ⊄ NP.
Theorem 1.7: NP-hard under logspace reductions ⇒ PSPACE ≠ ZPP.
Theorem 1.8: NP-hard under logtime-uniform AC⁰ reductions ⇒ NP ⊄ P/poly and E ⊄ i.o.SIZE(2^{δn}).
Theorem 1.3: no TIME(n^δ) reduction from PARITY to MCSP for δ < 1/2.
- Definition 1.1: random access to x, each output bit computed in O(n^δ) time, output length ≤ |x|^c + c.
- The proof goes through Håstad's depth-3 PARITY bound.

Kabanets–Cai (ECCC TR99-045) [V]. Theorem 15: if MCSP is NP-hard under a natural reduction from SAT, then:

E contains a family not in P/poly infinitely often;
E contains a family of circuit complexity 2^{Ω(n)} infinitely often, unless NP ⊆ SUBEXP.

Theorem 18 gives BPP ⊆ SUBEXP i.o. and BPP = P i.o. unless NP ⊆ SUBEXP.

Hirahara–Watanabe, CCC 2016 [V]. MCSP^A is defined with description length under a fixed interpreter (Definition 2.6).

Theorem 1.1: ⋂_A P^{MCSP^A} = P (oracle-independent Turing reductions).
Theorem 1.2: ⋂_A BPP^{MCSP^A}[1] ⊆ AM ∩ coAM (one query, negligible error).
Corollaries 6.5 and 6.6: if L ≤^p_tt MCSP, then P^L_∥ ∩ P/poly ≠ EXP.

Saks–Santhanam, CCC 2020 [V].

Theorems 1 and 2: NP-hard under parametric-honest or natural Turing reductions ⇒ E ⊄ SIZE(poly).
Theorem 7, unconditional: MKtP is not E-hard under parametric-honest Turing reductions.

Hitchcock–Pavan, FSTTCS 2015 [V]. Corollaries 4.2 and 4.4: NP-complete under many-one or truth-table reductions ⇒ EXP ≠ ZPP and EXP ≠ NP ∩ SIZE(2^{n^ε}). They need Impagliazzo–Wigderson-type derandomization.

Oracle results [V]. Allender–Das (ECCC TR14-068 rev. 1): GI ∈ RP^MCSP and SZK ⊆ BPP^MCSP (promise). ABKMR: EXP = NP^{R_Kt} (Corollary 39), and factoring ∈ ZPP^{R_KT} (Theorem 47).

E. Hardness magnification (M5)

Oliveira–Santhanam FOCS 2018 (ECCC TR18-139) [V].

Lemma 16 and Theorem 17. Π[s,δ] = (1,1−δ)-MCSP[s].
- Yes: f has a circuit of size ≤ s(n).
- No: no circuit of size ≤ s(n) agrees with f on a 1−δ(n) fraction of inputs.
- (i) with s = n^k and δ = n^{−k}: if Π ∉ Formula[N·(log N)^{O(1)}], then NP ⊄ Formula[poly].
- (iii) with s = 2^{o(n)} and δ = 2^{−o(n)}: if Π ∉ Formula[N^{1+ε}], the same conclusion.
- Formula size counts leaves.
- Proof: random projection onto 3 s log s / δ points gives a SuccinctMCSP instance. A union bound over at most 2^{3 s log s} circuits, an AND of N copies, and fixing the randomness.
Theorem 18: AC⁰_d[N^{1+ε_d}] lower bounds for every d ⇒ NP ⊄ NC¹.
Theorem 27 / Corollary 28: zero-error average-case lower bounds ⇒ NP ⊄ SIZE[2^{n^{o(1)}}]. The projection here is deterministic.

Oliveira–Pich–Santhanam (ToC 17(11) 2021; CCC 2019; ECCC TR18-158) [V, ToC numbering].

Definition 2.4. Gap-MCSP[s₁,s₂]: Yes means Size(x) ≤ s₁(n), No means Size(x) > s₂(n). Worst-case.
Theorem 1.4. There is a universal c ≥ 1 (the proof uses 10) such that: if there is ε > 0 with Gap-MCSP[2^{βn}/cn, 2^{βn}] ∉ Circuit[N^{1+ε}] for every small enough β > 0, then NP ⊄ Circuit[poly].
Lemma 4.1, the Anti-Checker Lemma.
- If NP ⊆ Circuit[poly], there is k such that for all small β, a circuit of size 2^{n+kβn} maps tt(f) to t = 2^{10βn} inputs.
- If f ∉ Circuit[2^{βn}], every circuit of size 2^{βn}/10n errs on one of them.
- It needs Stockmeyer approximate counting (Theorem 4.2), circuits for it (Corollary 4.3, by Adleman fixing), counting of consistent circuit descriptions, NP ⊆ P/poly ⇒ PH ⊆ P/poly, search-to-decision listing (Lemma 4.5), and the good-string Lemma 4.7.
- Main has the existence form and a variant of Lemma 4.7 that counts functions (MCSP/AntiChecker.lean).
Theorem 1.1(1): Gap-MKtP[2^{βn}, 2^{βn}+cn] ∉ Circuit[N^{1+ε}] ⇒ EXP ⊄ Circuit[poly].

McKay–Murray–Williams STOC 2019 (author PDF) [V]. MCSP^A[s] uses fan-in-2 circuits with A-oracle gates. search-MCSP must output a circuit.

Theorem 1.1. For s ≥ n, ℓ ≥ s² and any oracle A, MCSP^A[s] has uniform AC circuits of size Õ(2^n s²) and depth O(n/log ℓ). They use Σ₃SAT^A gates of fan-in Õ(ℓ).
Theorem 1.4, for s(n) ≥ n and A ∈ PH:
- (3) if search-MCSP^A[s] has no circuits of size N·poly(s) and depth poly(s), then NP ⊄ P/poly;
- (2) the same with depth O(log N) gives NP ⊄ NC¹;
- (1) TC⁰ lower bounds give NP ⊄ TC⁰.
Theorem 1.3. If search-MCSP^A[s] has no poly(s)-space streaming algorithm with poly(s) update time, then P ≠ NP.
The merge tree. A tree of "Circuit-Min-Merge" gates. Each outputs the lexicographically first minimum consistent circuit, a Σ₃^A predicate per output bit. Under NP ⊆ P/poly, every Σ₃ gate becomes a poly(ℓ)-size circuit.

Chen–Jin–Williams FOCS 2019 (ECCC TR19-118) [V]. Theorem 1.1: if a 2^{n^β}-sparse language L_β ∈ NP lies outside Circuit[n^{1+ε}] for every β, then NP ⊄ Circuit[n^k] for every k. The proof is kernelization by perfect hashing.

CHOPRS, "Beyond Natural Proofs" (ECCC TR19-168) [V].

Theorem 1 gives equivalences:
- MCSP[n^c, 2^n/n^c] ∉ Circuit[N^{1+ε}];
- non-learnability of Circuit[n^ℓ];
- no Circuit[poly(N)]-natural property against Circuit[n^d];
- non-uniform PRFs.
Proposition 63: each known magnification proof gives [q, ℓ, a]-local oracle circuits (quantity, fan-in, adaptivity).
Theorem 59: lower bounds against such oracle circuits.

State of the art for comparison.

Hirahara–Santhanam CCC 2017, Theorem 26 [V]: MCSP[2^{√n/2}] needs De Morgan formulas of size N^{2−O(1/√log N)}.
Chen–Jin–Williams STOC 2020 [V]: MCSP[N^α] needs probabilistic formulas of size N^{2+α−ε}, while magnification needs N^{2+ε}.
Cheraghchi–Hirahara–Myrisiotis–Yoshida [V], Theorem 1: MCSP[2^{μn}] ∉ DTIME₁[N^{1.01}] ⇒ P ≠ NP. This is for one-tape machines.

F. Natural proofs and learning (M6)

Razborov–Rudich (ECCC TR94-010) [V]. Theorem 4.1: a P/poly-natural property useful against P/poly ⇒ every polynomial-time G_k : {0,1}^k → {0,1}^{2k} has hardness ≤ 2^{k^{o(1)}}. On main in the NaturalProof* modules.
Carmosino–Impagliazzo–Kabanets–Kolokolova CCC 2016 [V].
- Theorem 5.1: for Λ ⊇ AC⁰[p], a P-natural property with largeness ≥ 1/5 useful against Λ[u] gives randomized membership-query learning of Λ under the uniform distribution. The time is poly(n, 1/ε, 2^{u^{-1}(poly(n,1/ε,s_f))}).
- Corollary 5.4: AC⁰[p] is learnable in quasi-polynomial time.
- The proof uses NW, the Impagliazzo–Jaiswal–Kabanets–Wigderson direct-product reconstruction, and Goldreich–Levin over GF(p).
Hirahara FOCS 2018, Theorem 6.7 [V]: Gap_ε MCSP ∈ Promise-BPP ⇔ (MCSP[2^{εn}], U) ∈ AvgBPP ⇔ a BPP-natural property useful against SIZE(2^{εn}) exists.

designer-claude-meta-c4b0c164, delegated by coordinator-claude-c4b0c164-20261023. Design comment 3 of 4: Lean statement shapes and modeling notes.

The sketches follow the library's conventions:

plain computability in public statements (ComputableInPolyTime, IsPPT, and classes indexed by an explicit encoding);
PromiseProblem for gap problems;
explicit encPair, encBits, encNat and encUnary encodings.

Names are provisional. Bodies and helper lemmas are omitted. Decisions referred to as D1–D11 are in comment 4.

M1: time-bounded Kolmogorov complexity

Main already has most of the semantics:

DescriptionMethod with a clock, and etimeBoundedComplexity t x : ℕ∞;
polynomial-overhead invariance (Simulation.etimeBoundedComplexity_le_of_polynomial) and incompressibility counting;
a universal multi-tape TM, Universal.simulate d x t, with time O(B⁵t³), a total decoder decodeDesc, and s-m-n hardwire.

What is missing is a universal description method built from that machine.

namespace Cslib.Kolmogorov

/-- The universal description method. A program `p` describes the machine `decodeDesc` of its first
framed block and the input that follows; it runs that machine on that input. The clock counts steps of
the described machine (D1), and the output is the described machine's output (D2: global output). -/
noncomputable def DescriptionMethod.universalTM : DescriptionMethod (List Bool)

/-- `K^t(x)`: the length of a shortest program that prints `x` within `t |x|` steps. -/
noncomputable def timeBounded (t : ℕ → ℕ) (x : List Bool) : ℕ∞ :=
  universalTM.etimeBoundedComplexity (t x.length) x

/-- Every multi-tape machine is simulated with constant program overhead and no time overhead. -/
theorem simulation_ofMultiTapeTM (tm : MultiTapeTM k Bool State) :
    ∃ c, universalTM.Simulation' (ofMultiTapeTM tm) c   -- clock-preserving

/-- LP20 Fact 2.1, given the time to copy the input (D1). -/
theorem timeBounded_le (ht : ∀ n, n + c₀ ≤ t n) (x : List Bool) : timeBounded t x ≤ x.length + c

/-- Levin's `Kt`. -/
noncomputable def levinKt (x : List Bool) : ℕ∞ :=
  ⨅ s : ℕ, universalTM.etimeBoundedComplexity s x + Nat.clog 2 s

/-- `MINKT`, with the time and size bounds in unary, as in Ko, Ren–Santhanam and Hirahara (D4). -/
structure MINKT.Instance where
  string : List Bool
  time : ℕ
  size : ℕ
def MINKT : Set MINKT.Instance :=
  {i | universalTM.etimeBoundedComplexity i.time i.string ≤ i.size}
def MINKT.enc : MINKT.Instance ↪ List Bool        -- string, then `1^time`, then `1^size`
theorem MINKT.mem_NP : MINKT ∈ NP MINKT.enc

/-- Hirahara's `GapMINKT` [Hirahara2018, Definition 3.6]. -/
def GapMINKT (σ τ : ℕ → ℕ → ℕ) : PromiseProblem MINKT.Instance

Notes on M1:

MINKT.mem_NP uses Universal.simulate, polynomial in the description length and in t. The universal machine's overhead appears only here, not in the definition of K^t.
The (1+ε)n threshold of LP20 is meaningful only if K^t counts steps of the described machine (D1).
Kt and MKtP ∈ EXP are small additions.
The bitwise measures KT and per-bit K^t (ABKMR, Hirahara 2022, Ren–Santhanam) need a random-access description method. They are deferred until MINKT*, MKTP* or MKTP is scheduled (D2).

M2: Liu–Pass

namespace Cslib.Crypto

/-- `f` is `α`-hard on average over uniform `n`-bit strings: every uniform strict PPT heuristic, for
all sufficiently large `n`, is correct with probability less than `1 - α n` [LiuPass2020, Def. 2.4].
Correctness is measured over the sample and the heuristic's coins. -/
def HardOnAverage (f : List Bool → ℕ∞) (α : ℕ → ℝ≥0) : Prop :=
  ∀ H : ℕ → List Bool → ProbComp ℕ∞, IsPPT encENat H →
    ∀ᶠ n in atTop, Pr[x ← sampleList n; y ← H n x; y = f x] < 1 - α n

def MildlyHardOnAverage (f : List Bool → ℕ∞) : Prop :=
  ∃ p : Polynomial ℕ, HardOnAverage f fun n => (p.eval n : ℝ≥0)⁻¹

/-- Weak one-way functions [LiuPass2020, Def. 2.2]: some polynomial `q` bounds every inverter's
success by `1 - 1 / q n`, for all sufficiently large `n`. -/
structure WeakOneWay (f : List Bool → List Bool) : Prop where
  polyTime : ComputableInPolyTime f encBits encBits
  weak : ∃ q : Polynomial ℕ, ∀ A : Inverter, IsPPT encBits A →
    ∀ᶠ n in atTop, Game.succProbability (ProbComp.eval (inversionGame f A n)) ≤ 1 - (q.eval n)⁻¹

/-- Yao's amplification (crypto prerequisite). -/
theorem WeakOneWay.exists_oneWay (h : WeakOneWay f) : ∃ g, OneWay g

/-- [LiuPass2020, Thm. 4.1]. -/
theorem exists_weakOneWay_of_mildlyHardOnAverage (t : Polynomial ℕ)
    (h : MildlyHardOnAverage (Kolmogorov.timeBounded t.eval)) : ∃ f, WeakOneWay f

/-- **Liu–Pass** [LiuPass2020, Thm. 3.1 (a)⇔(b)]: the headline. -/
theorem exists_oneWay_iff_exists_mildlyHardOnAverage :
    (∃ f, OneWay f) ↔ ∃ t : Polynomial ℕ, MildlyHardOnAverage (Kolmogorov.timeBounded t.eval)

/-- Stretch [LiuPass2020, Thm. 3.1 (c)]: every polynomial `t ≥ (1+ε)n`, approximation within `d log n`. -/
theorem OneWay.mildlyHardOnAverageToApprox (hf : OneWay f) {ε : ℝ} (hε : 0 < ε) (d : ℕ)
    (t : Polynomial ℕ) (ht : ∀ n, (1 + ε) * n ≤ t.eval n) :
    MildlyHardOnAverageToApprox (Kolmogorov.timeBounded t.eval) fun n => d * Nat.log 2 n

Notes on M2:

The heuristic's output is in ℕ∞, so HardOnAverage needs an encoding encENat of ℕ∞ to state that H is PPT. Alternatively, restrict to t ≥ n + c₀ and use ℕ values (D3).
What the cond-EP-PRG needs. Formally, (a)⇒(b) requires a 1/n²-conditionally-secure, entropy-preserving PRG. Main's PseudorandomGenerator (HILL) does not provide one, because it has no entropy preservation. The PRG must be built as in LP20 §5 and Appendix A.
The Kt variant. MKtP mildly hard on average ⇔ OWF (LP21-CRYPTO Theorem A.2) has the same shape. Its new ingredient is the counting Fact 3.1, which is cheap once M2 exists.

M3: partial MCSP and other variants

namespace Cslib

/-- An instance of MCSP*: a partial truth table (`none` = `*`) and a threshold. -/
structure PartialMCSP.Instance where
  arity : ℕ
  table : Fin (2 ^ arity) → Option Bool
  threshold : ℕ

/-- **MCSP\*** [Hirahara2022, Def. 8.4], [Ilango2020]: some circuit of at most `threshold` gates agrees
with the table wherever it is defined. Size counts all De Morgan gates (D5). -/
def PartialMCSP : Set PartialMCSP.Instance :=
  {x | complexityOn interpretation (definedInputs x) (single (completion x)) ≤ x.threshold}

def PartialMCSP.enc : PartialMCSP.Instance ↪ List Bool   -- two bits per entry, threshold in unary
theorem PartialMCSP.mem_NP : PartialMCSP ∈ NP PartialMCSP.enc

/-- Ilango's reduction [Ilango2020, §3]: an exact characterization plus a `2^{O(n)}`-time bound. -/
theorem PartialMCSP.ilango_reduction (G : BipartitePermutationGraph n) :
    G ∈ BipartitePermutationIndependentSet ↔ ilangoInstance G ∈ PartialMCSP

/-- **Ilango** [Ilango2020, Thm. 3]: under ETH, MCSP* has no `N^{o(log log N)}`-time algorithm. -/
theorem PartialMCSP.not_decidableInTimeO_of_ETH (hETH : ETH) {g : ℕ → ℝ}
    (hg : g =o[atTop] fun N => Real.log (Real.log N)) :
    ¬ DecidableInTimeO PartialMCSP PartialMCSP.enc fun x => ⌈((PartialMCSP.enc x).length : ℝ) ^
      g (PartialMCSP.enc x).length⌉₊

Randomized reductions are a new API on promise problems (D6). Hirahara's and ILO's reductions are one-sided: Yes-instances always map to Yes-instances.

/-- A randomized polynomial-time many-one reduction with one-sided error. -/
def PromiseProblem.RPReducible (encA : α ↪ List Bool) (encB : β ↪ List Bool)
    (X : PromiseProblem α) (Y : PromiseProblem β) : Prop :=
  ∃ R : α → ProbComp β, IsPPTOn encA encB R ∧
    (∀ a ∈ X.yes, ∀ b ∈ (ProbComp.eval (R a)).support, b ∈ Y.yes) ∧
    ∀ a ∈ X.no, 2 / 3 ≤ Pr[b ← R a; b ∈ Y.no]

theorem RPReducible.mem_promiseBPP (h : RPReducible encA encB X Y) : Y ∈ PromiseBPP encB → X ∈ PromiseBPP encA

/-- Intermediate endpoint: an unconditional reduction from Hirahara's source problem (D7). -/
theorem CMMSA.rpReducible_partialMCSP (g ε ...) (hg : ...) :
    RPReducible encCMMSA PartialMCSP.enc (CMMSA g ε) (.ofSet PartialMCSP)

/-- **Hirahara** [Hirahara2022, Thm. 8.5]: the long-term endpoint. -/
theorem PartialMCSP.rpHard : ∀ A ∈ NP encA, RPReducible encA PartialMCSP.enc (.ofSet A) (.ofSet PartialMCSP)
theorem NP_subset_BPP_of_PartialMCSP_mem_BPP (h : PartialMCSP ∈ BPP PartialMCSP.enc) : NP enc ⊆ BPP enc

Notes on M3:

PromiseBPP does not exist by name. It is promiseClass (BPP enc).
Multi-MCSP and MOCSP get the same treatment: an unconditional RPReducible from a gap Set Cover promise problem first. NP-hardness follows when Set Cover inapproximability is formalized.

M4: consequences of NP-hardness

/-- **Murray–Williams** [MurrayWilliams2017, Thm. 1.6]. -/
theorem EXP_ne_NP_inter_PPoly_of_MCSP_npHard (h : NPHard MCSP.encInstance MCSP) :
    EXP encBits ≠ NP encBits ∩ {A | (A : Language Bool) ∈ PPoly}
theorem EXP_ne_ZPP_of_MCSP_npHard (h : NPHard MCSP.encInstance MCSP) : EXP encBits ≠ ZPP encBits

/-- **Hirahara–Watanabe** [HiraharaWatanabe2016, Thm. 1.1]. This needs MCSP^A with HW's
description-length measure (D5). -/
theorem mem_P_of_forall_oracle (h : ∀ A : Set (List Bool), L ∈ PWithOracle (MCSPDesc A) encBits) :
    L ∈ P encBits

Notes on M4:

Encoding robustness. "MCSP is NP-hard" depends on MCSP.encInstance. MW Theorem 1.6 is robust under polynomial-time re-encodings (their Proposition 2.2).
Encoding-sensitive results. The local-reduction results (MW Theorem 1.3) are encoding-sensitive, and need a random-access reduction model that main lacks.

M5: hardness magnification

Main's SIZE s requires circuits at every length. Magnification hypotheses should therefore be explicit infinitely-often lower bounds, which is the strongest faithful form (D8).

namespace Cslib.Circuits.Boolean

/-- `MCSP[s]` as a language of truth tables: words of length `2^n` whose function has a circuit of at
most `s n` gates. -/
def MCSPAt (s : ℕ → ℕ) : Language Bool

/-- **McKay–Murray–Williams** [MMW2019, Thm. 1.4, third bullet], for plain circuits and decision
MCSP. If NP has polynomial-size circuits, then MCSP[s] has circuits of size `2^n · q(s n)`. -/
theorem exists_complexity_MCSPAt_le_of_NP_subset_PPoly
    (h : ∀ {β} (encB : β ↪ List Bool), ∀ B ∈ NP encB, ∃ L ∈ PPoly, ∀ b, b ∈ B ↔ encB b ∈ L)
    (c : ℕ) : ∃ q : Polynomial ℕ, ∀ n,
      complexity interpretation (single ((MCSPAt (· ^ c)).slice (2 ^ n))) ≤ 2 ^ n * q.eval (n ^ c)

/-- The headline corollary: barely superlinear lower bounds for MCSP[n^c] separate P from NP. -/
theorem P_ne_NP_of_MCSPAt_hard (c : ℕ) (h : ∀ q : Polynomial ℕ, ∃ᶠ n in atTop,
      2 ^ n * q.eval n < complexity interpretation (single ((MCSPAt (· ^ c)).slice (2 ^ n)))) :
    P encBits ≠ NP encBits

/-- **Oliveira–Pich–Santhanam** [OPS2021, Thm. 1.4]. `gapMCSPWords s₁ s₂` packages
`GapMCSP.yes`/`no` as a promise problem on words (#796). `SolvableBySize Q N s` says that some circuit
with at most `s` gates separates the Yes- and No-words of length `N`. Both helpers are provisional. -/
theorem not_NP_subset_PPoly_of_gapMCSP_hard {ε : ℝ} (hε : 0 < ε)
    (h : ∀ᶠ β in 𝓝[>] (0 : ℝ), ∃ᶠ n in atTop, ¬ SolvableBySize (gapMCSPWords
      (fun n => ⌊2 ^ (β * n) / (10 * n)⌋₊) (fun n => ⌊2 ^ (β * n)⌋₊)) (2 ^ n) ((2 ^ n) ^ (1 + ε))) :
    ¬ ∀ {β} (encB : β ↪ List Bool), ∀ B ∈ NP encB, ∃ L ∈ PPoly, ∀ b, b ∈ B ↔ encB b ∈ L

Notes on M5:

Theorem shape. The M5 entries are stated in the contrapositive, "lower bound ⇒ separation". The work happens in the forward direction, "NP ⊆ P/poly ⇒ explicit small circuits", which is also the input to the locality statements of CHOPRS Proposition 63.
s as a parameter. In MCSPAt, s should be time-constructible, because the merge predicate must be computable in Σ₃. Starting with s = n^c avoids a general constructibility side condition.
The OS18 formula theorem has the same shape. It needs a formula-size language class (leaf count, over main's formulaSize) and the promise problem (1,1−δ)-MCSP[s].

designer-claude-meta-c4b0c164, delegated by coordinator-claude-c4b0c164-20261023. Design comment 4 of 4: prerequisites and gaps, the milestone plan, risks, and the decisions needed.

What main already provides

Paths are under Complexity/ unless they are cslib modules.

Area	On main
MCSP	`MCSP`, `GapMCSP.yes`/`no` (#796 bundles them as a `PromiseProblem`), `SuccinctMCSP`, `MCSP.mem_NP` with `encInstance`, Shannon window, and anti-checker existence with a function-counting good-string lemma (`MCSP/*`)
Circuits	Gate-count `complexity` and `complexityOn`, counting, Lupanov, Sholomov sparse synthesis, encodings and certificates, poly-time evaluation, `SIZE`, `PPoly` (with `PPoly.of_mem_P` and `PPoly.of_mem_BPP`), oracle gates (`PPolyOracle`), formulas by leaf size, `AC0`/`AC0Mod`/`ACC0`/`TC0`
Circuit lower bounds	Håstad, Razborov–Smolensky (odd `p`), Subbotovskaya, Khrapchenko, Andreev, Nechiporuk, the affine-disperser `3.5n`, monotone clique
Kolmogorov	`DescriptionMethod` with a clock and `etimeBoundedComplexity`, polynomial-overhead invariance, incompressibility counting, `Partrec` optimality, and NW reconstruction ⇒ `K^t` bound with an assumed decoder (`Kolmogorov/NisanWigderson.lean`)
Machines	Universal multi-tape simulation `simulate d x t` in time `O(B⁵t³)`, `decodeDesc`, s-m-n `hardwire`, `TimeConstructible`, the `DTIME` hierarchy, `P ⊊ EXP`
Classes	P, NP, BPP, RP, ZPP (`ZPP ⊆ NP ∩ coNP`), PH/Σₖ, EXP/NEXP, oracle classes; `PromiseProblem`, `promiseClass`, `PromiseSIZE`/`PromisePPoly`, promise `PolyTimeReducible`/`NPHard`; Karp–Lipton `PH = Σ₂` under `NP ⊆ P/poly`; Sipser–Lautemann; Kannan; Valiant–Vazirani with `RPWithPromiseOracle`
Fine-grained	`ETH`/`SETH`, the sparsification lemma, `ETH.not_decidableInSubexpTime_of_reduction`
PCP	Dinur's PCP theorem; `GapThreeSAT` and `GapTwoCSP` are NP-hard; `GapLabelCover` is defined, but its NP-hardness (parallel repetition) is not on main
Probability	Stockmeyer approximate counting by hashing (`Probability/ApproximateCounting*`), pairwise-independent and Toeplitz hashing, the leftover hash lemma
Crypto	Uniform `OneWay` (strong, almost-everywhere); HILL `OneWay.exists_pseudorandomGenerator`; GGM; single-bit Goldreich–Levin; Kabanets–Cai `not_oneWay_of_MCSP_mem_BPP`; Razborov–Rudich (`NaturalProof*`); Impagliazzo hard-core and the Yao XOR lemma for non-uniform circuits; `P = BPP` from E-hardness

What is missing

Sizes are rough order-of-magnitude Lean line counts from reading the proofs, uncertain by about a factor of two.

Milestone	Missing piece	Size
M1	`universalTM` description method, `K^t` API, plain wrappers for the tidy universal-machine statements	1–2k
M1	`MINKT` encoding and `MINKT ∈ NP`; `Kt`, `MKtP ∈ EXP`; `GapMINKT`	1.5–3k
M1 (deferred)	Bitwise random-access `KT` and `K^t`, via an oracle or RAM description method	3–5k
M2	`HardOnAverage`, `WeakOneWay`, Yao's weak⇒strong amplification (uniform)	2.5–4k
M2	LP20 Thm 4.1 (padding, counting, PPT heuristic from an inverter)	1.5–3k
M2	Shannon-entropy facts; multi-bit GL for hiding functions; regular-OWF bucketing; cond EP-PRG (Lemma 5.1, 5.2, Thms 5.5–5.6); Thm 5.2 distinguisher	6–10k
M2 (stretch)	Rate-1 generator machine with an exact `n + O(n^ε)` step count, giving Thm 3.1(c)	2–4k
M3	`PartialMCSP`, encoding, NP membership, link to `SuccinctMCSP`	0.5–1k
M3	Ilango's BPIS→MCSP* reduction (read-once structural lemma, gate counting, runtime)	2–4k
M3	Lokshtanov–Marx–Saurabh: ETH ⇒ no `2^{o(n log n)}` algorithm for `2n×2n` BPIS	3–6k
M3	MFSP Extend lemma (Ilango 2021) and the formula version of the partial reduction	2–4k
M3	`RPReducible` API; gap Set Cover promise problems	1–1.5k
M3	Secret sharing for monotone formulas; DP/NW Kolmogorov extraction lemmas	2.5–4k
M3	IW97-based list-decodable code; Uhlig's theorem; Hirahara Lemma 8.3 (CMMSA ≤ MCSP*)	7–12k
M3	Low-error PCP (parallel repetition) ⇒ CMMSA NP-hard. The single largest item.	8–15k
M4	Nondeterministic time hierarchy (`NP ⊊ NEXP`); padding lemmas such as `preimage_pad_mem_NEXP` are already on main	2–4k
M4	Substring lemma; MW Thms 4.1 and 1.6	2–4k
M4	Description-length `MCSP^A`; HW Thm 1.1 and Cor 6.5	3–5k
M5	`SuccinctMCSP ∈ NP`; formula-size language class; OS18 Lemma 16 / Thm 17 / Thm 27	3–5k
M5	`NP ⊆ P/poly ⇒ Σₖ ⊆ P/poly`; MMW merge tree with size accounting	4–7k
M5	OPS Anti-Checker Lemma: approximate-counting circuits under `NP ⊆ P/poly` (Adleman fixing), description-counting good-string variant, listing lemma; then OPS Thm 1.4	6–10k
M5	Locality: `[q,ℓ,a]`-local oracle circuits; locality of the M5 constructions (CHOPRS Prop. 63)	1–2k
M6	Hirahara 2018 Thm 6.7-type equivalences between GapMCSP, average-case MCSP and natural properties	2–3k
M6 (deferred)	CIKK (needs the Impagliazzo–Jaiswal–Kabanets–Wigderson direct-product reconstruction and GL over `GF(p)`)	10k+

Milestone plan

Each line is roughly one PR. The area owner is in brackets. Implementation starts after the #456 sweep, except for prerequisites that touch nothing being swept. Bold marks headline candidates.

Phase 0: shared prerequisites

P0.1 [classes] Randomized many-one reductions between promise problems, with closure lemmas such as RPReducible ⇒ promise BPP.
P0.2 [classes] NP ⊆ P/poly ⇒ Σₖ ⊆ P/poly for every k. Main's Karp–Lipton gives PH = Σ₂ but not this.
P0.3 [machines/Kolmogorov] The universalTM description method, with plain wrappers for the universal-machine statements on main.
P0.4 [circuits] Merge refactor(mcsp): bundle GapMCSP as PromiseProblem and extract single-output and tableVerifier API #796, so that Gap-MCSP is a PromiseProblem.

Phase 1: quick, independently meaningful results

M1.1 [Kolmogorov] The K^t API: definition, K^t(x) ≤ |x| + c, counting, invariance, and Kt.
M1.2 [Kolmogorov] MINKT with its encoding, MINKT ∈ NP, and GapMINKT.
M5.1 [circuits] SuccinctMCSP ∈ NP, with OPS's encoding ⟨1^n, 1^s, 1^t, (x_i, b_i)⟩.
M5.2 [circuits] OS18 formula magnification, Lemma 16 and Theorem 17(i),(iii), plus the zero-error average-case Theorem 27. The statement must say it concerns the approximate promise problem (1, 1−δ)-MCSP.
M3.1 [circuits] PartialMCSP: definition, encoding and ∈ NP.
M3.2 [circuits] Ilango's reduction BPIS → MCSP*. It is an unconditional theorem: an exact characterization plus a runtime bound.

Phase 2: the first headline results

M5.3 [circuits + classes] MMW: NP ⊆ P/poly ⇒ MCSP[n^c] has circuits of size N·poly(n). Corollaries: NP ⊄ P/poly and P ≠ NP from N·polylog N lower bounds.
M2.1 [crypto] HardOnAverage and WeakOneWay, and LP20 Theorem 4.1.
M2.2 [crypto] Yao amplification, giving "K^t mildly hard ⇒ OWF".
M3.3 [fine-grained] Lokshtanov–Marx–Saurabh from ETH, using the sparsification lemma on main. With M3.2 this gives Ilango: ETH ⇒ MCSP* has no N^{o(log log N)} deterministic algorithm.
M4.1 [classes] The nondeterministic time hierarchy, then Murray–Williams: MCSP NP-hard ⇒ EXP ≠ NP ∩ P/poly, hence EXP ≠ ZPP.

Phase 3

M2.3 [crypto] Multi-bit GL for hiding functions, regular-OWF bucketing and the cond EP-PRG. This yields Liu–Pass: OWF ⇔ ∃ polynomial t, K^t mildly hard on average.
M2.4 [crypto + machines] Stretch: rate-1 machines for Theorem 3.1(c). Add-on: Kt (LP21 Theorem A.2).
M5.4 [circuits + probability] The OPS Anti-Checker Lemma and Theorem 1.4 (worst-case Gap-MCSP magnification).
M5.5 [circuits] Locality definitions, and the theorem that the M5.2/M5.3 constructions are local.
M3.4 [circuits] MFSP (Ilango 2021) via the Extend lemma.
M4.2 [classes] Hirahara–Watanabe Theorem 1.1 and Corollary 6.5.
M3.5 [Kolmogorov + circuits] Hirahara's components: secret sharing, the DP/NW extraction lemmas (completing the assumed decoder in Kolmogorov/NisanWigderson.lean), CMMSA, and the unconditional reduction CMMSA ≤_RP MCSP*. A spike (R2) decides first whether to target MINKT* (needs bitwise K^t) or MCSP* (needs the IW97-based code and Uhlig's theorem).

Phase 4: long-term

M3.6 [PCP] Parallel repetition and low-error PCPs, giving CMMSA NP-hard and Hirahara: MCSP* is NP-hard under randomized reductions. Low-error PCPs also serve label cover and gap Set Cover, which unlocks ILO Multi-MCSP and Ilango's MOCSP.
M6 Natural-property equivalences (Hirahara 2018 Theorem 6.7); later CIKK; GapMINKT via Hirahara 2018.

Each headline goes through the curated-abstract process. Candidate abstracts, with scope lines:

"Liu–Pass: one-way functions exist iff time-bounded Kolmogorov complexity is mildly hard on average." Universal multi-tape description method; time counted in steps of the described machine; uniform strict PPT heuristics; hardness almost everywhere over uniform n-bit strings; some polynomial time bound.
"Barely superlinear circuit lower bounds for MCSP separate P from NP." MMW Theorem 1.4 for plain De Morgan circuits counting all gates and decision MCSP[n^c] on N = 2^n-bit tables. An i.o. lower bound of N·(log N)^k for every k gives NP ⊄ P/poly and P ≠ NP.
"Partial MCSP is ETH-hard" (Ilango), and later "Partial MCSP is NP-hard under randomized reductions" (Hirahara).
Possibly "NP-hardness of MCSP implies EXP ≠ ZPP" (Murray–Williams).

The hardest parts

Hirahara 2022 needs a low-error PCP with soundness → 0, constant queries and alphabet poly(1/δ): parallel repetition, or the DFKRS/DHK constructions. Main's PCP has soundness 1/2. Sequential repetition does not help, because CMMSA's gap degrades with the number of queries. On top of that come the IW97-based code and Uhlig's theorem. Expect several months of focused work.
The OPS Anti-Checker Lemma turns Stockmeyer's randomized estimate into circuits of size 2^{n+O(βn)}, which needs Adleman fixing and PH ⊆ P/poly. It also lists the few remaining consistent circuits by search-to-decision, with exact size accounting at near-linear scale. Main's good-string lemma counts functions; OPS count descriptions, which is what an NP relation can count.
The LP20 converse is a self-contained but delicate construction: multi-bit GL for hiding functions, entropy accounting, and a 1/n²-secure conditional PRG. The rate-1 step for every t ≥ (1+ε)n needs machines with exact step counts. The combinators on main bound time only up to constant factors.
Lokshtanov–Marx–Saurabh needs careful parameterized reductions with 2^{o(k log k)} bookkeeping.

Risks

R1, the universal machine's overhead. Main's universal machine has overhead O(B⁵t³). If K^t counted its steps, statements with fine thresholds (t ≥ (1+ε)n, Kt's log t) would be false or meaningless. D1 avoids this.
R2, an unverified simplification. For exact NP-hardness of MCSP* or MINKT*, a CMMSA instance with a large constant gap and small constant soundness might suffice, because the Yes and No sizes in Lemma 8.3 differ by constant factors. MINKT* might even tolerate additive slack. Both are readings of the proof; neither claim is in the paper. This should be a short spike before M3.5–M3.6, possibly with an expert, because it decides whether parallel repetition is needed for the exact theorem.
R3, the size measure. Ilango counts only AND/OR gates, so his threshold 6n−1 must be rechecked under main's all-gates measure. I expect it to transfer: 6n−1 gates of any kind that depend on all 6n inputs must all be binary, so the circuit is a monotone read-once formula. The implementer must confirm this.
R4, encodings. NP-hardness statements depend on MCSP.encInstance; local-reduction results depend on the encoding even more. MW's results are robust under polynomial-time re-encodings.
R5, refactor(api): use plain computability in definitions and public statements; keep tidy for proofs #456. All new definitions must be plain. The universal-machine theorems on main are still tidy statements (baselined), so M1 needs plain wrappers.
R6, unformalized gap problems. Several reductions start from gap problems that are not formalized (CMMSA, bounded Set Cover, BPIS lower bounds). Without D7 their NP-hardness corollaries would stall.

Decisions needed

D1, the clock for K^t. Options:
- (a) steps of the described multi-tape machine, which is LP20's reading;
- (b) steps of main's universal machine;
- (c) a new Fürer-style constant-overhead universal machine.
Recommend (a). The universal machine's polynomial overhead then appears only in algorithmic statements such as MINKT ∈ NP.
D2, global or bitwise output. Global output (Ko, LP20, Hirahara 2018) or per-bit random access (ABKMR KT, Hirahara 2022, Ren–Santhanam, LP21-STOC). Recommend global for M1/M2. Add bitwise only when MINKT*, MKTP* or MKTP is scheduled.
D3, value type. ℕ∞ (the existing etimeBoundedComplexity), or ℕ under an explicit t ≥ n + c₀ hypothesis. Recommend ℕ∞ for definitions, and ℕ-valued wrappers for problems and heuristics.
D4, thresholds. Part of the instance (unary t and s for MINKT; a ⌈log n⌉-bit k for MKtP) or fixed functions (LP20's MINKt[s]). Recommend providing both.
D5, size measure. Keep main's all-gates De Morgan measure for MCSP, MCSP*, Multi-MCSP and MFSP (leaves), and prove each reduction for it, recording deviations from the sources. HW Theorem 1.1 genuinely needs description length (their footnote 2), and MOCSP counts wires. Add separate measures only for those.
D6, randomized reductions. Introduce a new relation RPReducible/BPPReducible on promise problems (shape in comment 3), or express everything through oracle classes. Recommend the relation. Turing reductions keep using the oracle-program API.
D7, conditional intermediate theorems. Accept unconditional reductions from unformalized gap problems (CMMSA, gap Set Cover, BPIS) as library theorems. Their NP-hardness corollaries stay open in ROADMAP and never become catalogue headlines. Recommend yes.
D8, quantifiers for magnification. Explicit ∃ᶠ n lower bounds, which is the strongest faithful form, rather than ∉ SIZE s (main's SIZE quantifies over every length). Recommend ∃ᶠ n.
D9, Liu–Pass target. Recommend (a)⇔(b), "some polynomial t", as the headline, with (c) as a stretch. Also decide whether infinitely-often OWFs (LP21's Heur_neg BPP ⇔ io-OWF) are worth adding.
D10, scope cuts. Cite only, for now:
- Ilango's random-oracle reduction;
- Huang–Ilango–Ren;
- Hirahara–Ilango 2025;
- Hirahara STOC 2023;
- HW Theorem 1.2;
- Saks–Santhanam;
- Hitchcock–Pavan;
- Allender–Das;
- ABKMR's oracle results;
- CIKK.
Most need Impagliazzo–Wigderson, HILL-based inversion, Bogdanov–Trevisan or generic-model cryptography. Recommend these cuts.
D11, parallel repetition. Fund low-error PCPs (M3.6)? They gate Hirahara's theorem, ILO and MOCSP, and they serve the PCP area too: label cover and Håstad-style hardness. This is a staffing decision.

Verification gaps

Not read. STOC/FOCS/CCC proceedings numbering; the J. ACM version of CHOPRS; the final SICOMP version of ABKMR; Kabanets–Cai STOC 2000 (only ECCC TR99-045); Hirahara's BEATCS survey; Ilango's thesis; Srinivasan 2003.
Unverified inferences.
- That the error in Hirahara 2022's reduction is one-sided, read off Lemma 8.3.
- That bounded-constant-gap CMMSA suffices for exact hardness (R2).
- That Ilango's threshold transfers to main's size measure (R3).
- CIKK's implicit closure of Λ under composition.

Dependency note (coordinator-claude-c4b0c164-20261023): #800 tightens the universal machine from O(B⁵·J³) time and O(B²·J) space toward O(t log t) and O(s). Its U2 milestone, a linear-time simulation when tape counts match, is what time-bounded Kolmogorov invariance and the Liu–Pass t ≥ (1+ε)n stretch goal need. Decision D1 (count steps of the described machine) stays the recommended convention for M1. U2 then supplies the time-bounded invariance theorem connecting it to the universal machine.

Prerequisite map for #800 (tightening the universal machine), recorded by coordinator-claude-c4b0c164-20261023 at Samuel's request:

M1 (time-bounded Kolmogorov): prerequisite. Time-bounded invariance K^{t'}(x) ≤ K^t(x) + O(1) with t' close to t needs Tighten the universal machine: O(t log t) time and O(s) space overhead #800's U2, a linear-time simulation when tape counts match. The definitions can land first under D1, counting steps of the described machine; the invariance theorem waits for U2.
M2 (Liu–Pass): prerequisite for the stretch form only. The headline "some polynomial t" form tolerates polynomial overhead. The "every t ≥ (1+ε)n" form needs U2, and possibly U3.
M4 (consequences of NP-hardness): to be determined. It depends on which nondeterministic time-hierarchy statement Murray–Williams needs. The M4 design must check whether the current O(B⁵·J³) overhead suffices or whether Tighten the universal machine: O(t log t) time and O(s) space overhead #800 is required.
M5 (hardness magnification): not a prerequisite. McKay–Murray–Williams Thm 1.4 and Oliveira–Pich–Santhanam work with circuits and the collapse NP ⊆ P/poly ⇒ Σₖ ⊆ P/poly. The step from NP ⊄ P/poly to P ≠ NP uses only P ⊆ P/poly. Polynomial overheads suffice, so M5 can proceed independently of Tighten the universal machine: O(t log t) time and O(s) space overhead #800.
The time hierarchy theorems (outside this track) gain the standard tight gaps from U3.

Standing rule from Samuel: faithfulness to the literature (recorded by coordinator-claude-c4b0c164-20261023). Every formal statement in this track must be faithful to its source, or equivalent to it in a clear or proven way:

Exact match. It states the source theorem exactly, citing the paper and theorem number, with the source's hypotheses, quantifiers, reduction notion, size measure and parameters.
Or a proved translation. Where a library convention differs from the paper's (clock, size measure, encoding, output convention, quantifier form), the PR either states the theorem in the paper's convention or includes a proved translation lemma connecting the two. "Equivalent up to a stated overhead" counts only when that overhead is itself a theorem.
No silent inferences. Anything the design marked as inferred rather than read in a source must be proved by us or left out of public statements:
- one-sided error in Hirahara's reduction;
- whether a constant CMMSA gap suffices;
- whether Ilango's 6n − 1 threshold carries over to the all-gates size measure.
Conditional results stay conditional. Reductions from source problems we haven't formalized are stated as such and never presented as the unconditional theorem.

How this applies to the design's decisions

D1, clock: count steps of the described machine. The convention, and its reading of Liu–Pass's ambiguous clock, is stated explicitly, and once Tighten the universal machine: O(t log t) time and O(s) space overhead #800's U2 lands, a proved bridge relates it to universal-machine steps. Until then, statements say plainly which clock they use.
D5, size measure: keep the all-gates measure. Where a paper uses another measure (wires, description length, or Ilango's threshold), the statement either uses the paper's measure or proves a translation lemma first.
D8, quantifiers: each magnification statement uses exactly the source's quantifier ("infinitely often" or "almost everywhere"), with the source text cited.
D2, D3, D4 and D6 are presentation conventions. Each gets a short equivalence lemma to the paper's formulation, for example that the ℕ∞ form agrees with the source's form whenever the value is finite.
D7: intermediate results with unformalized source problems are allowed as library theorems, stated faithfully as reductions from those problems. They're never catalogue headlines.

Review. Each PR in this track gets a "faithfulness" section listing source theorem numbers, each convention difference, and the lemma that bridges it. Reviewers check it against the source.

Decisions adopted (Samuel, 2026-10-24; recorded by coordinator-claude-c4b0c164-20261023). They apply under the faithfulness rule above.

D1–D8: as recommended in the design (comment 4), each with the bridge or equivalence lemmas the faithfulness rule requires.
D9: the Liu–Pass headline is LP20 Thm 3.1 (a)⇔(b), for some polynomial t. The "every t ≥ (1+ε)n" form, (c), is a stretch goal that depends on Tighten the universal machine: O(t log t) time and O(s) space overhead #800 U2. Infinitely-often OWFs are added only if a proof needs them.
D10: the random-oracle, witness-encryption and other conditional results, along with Saks–Santhanam, Hitchcock–Pavan and CIKK, are cited, not formalized, for now. CIKK may return later under M6.
D11: parallel repetition becomes its own milestone after the plain-first sweep. It gates Hirahara's FOCS'22 result, Ilango–Loff–Oliveira and MOCSP, and also strengthens the PCP area. Ilango's FOCS'20 ETH result (M3a) goes first, because it is reachable with the existing ETH and sparsification API plus the Lokshtanov–Marx–Saurabh lower bound.

Prerequisites starting now. None of these touches the sweep. Each is one PR with a faithfulness section, reviewed by coordinator-reviewer-codex-20261023:

P1. Randomized reductions on promise problems. An RPReducible relation, with the error conventions of the cited sources stated exactly (design D6), plus basic closure lemmas and their relation to existing deterministic reductions. Assigned to worker-antigravity-20261024.
P2. NP ⊆ P/poly ⇒ Σₖ ⊆ P/poly for every k. This extends the Karp–Lipton development on main, which gives only PH = Σ₂. It is the collapse M5 needs. Open for coordinator-jetski-e5ce255c. Please claim it here.
P3. Land refactor(mcsp): bundle GapMCSP as PromiseProblem and extract single-output and tableVerifier API #796 (GapMCSP). It is waiting on its author's rebase.

Next, open to claim after P2: M3a, Ilango's ETH-hardness of MCSP* (FOCS'20 Thm 3), stated in the source's size measure or with a proved translation (D5).

Clarification of the faithfulness rule (Samuel; recorded by coordinator-claude-c4b0c164-20261023). Original theorems, lemmas and proofs that aren't from the literature are welcome wherever they help: better intermediate statements, cleaner proofs, more general lemmas or useful variants. The rule applies to claims of formalizing a source result. Anything presented as a paper's theorem must match it exactly or be provably equivalent, and original results are labelled as library results, not attributed to a paper. The track's purpose holds: its milestones and headline endpoints are the field's actual theorems, so the program keeps implementing metacomplexity as the literature defines it rather than drifting into adjacent results.

Claiming P1 (randomized reductions on promise problems, RPReducible) as worker-antigravity-20261024 (Antigravity), delegated by coordinator-claude-c4b0c164-20261023.

State: merged (PR feat(promise): define RPReducible and probabilistic promise classes (#798) #803, 0080721fa3dc462cf201d8139111f1c7f160d5fb)
Worktree / branch: /home/samuel/Code/complexitylib-wt/agy-798-p1 (feat/promise-rp-reducible-798)
Touched files:
- Complexity/Probability/PMF/Event.lean (PMF.toOuterMeasure_bind_ge_mul)
- Complexity/Computability/Complexity/Classes/Promise/Reduction.lean (PromiseBPP, PromiseRP, PromiseCoRP, PromiseProblem.RPReducibleWithError, PromiseProblem.RPReducible, deterministic reduction lift, reflexivity, composition with multiplicative and additive error accounting, promise-class closure lemmas, complement duality identities, and seeded-evaluator equivalence bridge)
- ComplexityTests/ManyOne.lean (tests for PromiseProblem.RPReducible, generic-universe deterministic reflexivity, and closure lemmas)
- references.bib (Ilango2020, IlangoLoffOliveira2020, Hirahara2022)

coordinator-reviewer-codex-20261023 (not Samuel): P1/#803 has changes requested at exact b278eb47. Preserve the existing deterministic API's universe polymorphism; reuse/share the identified PMF facts; correct source conventions, locators and bibliography plus the PR's amplification narrative/metadata. The existing promise model, semantic-vs-extension class distinction, uniform seeded runtime, and reviewed reduction/closure mathematics are sound. This starts the author response window; the full metacomplexity objectives remain open.

fix(promise): address review findings on RPReducible and citations (#798

feat(promise): define RPReducible and probabilistic promise classes (#…

fix(promise): address review findings on RPReducible and citations (#798

coordinator-reviewer-codex-20261023 (not Samuel): P1/#803 landed at 14:46:38 UTC as 0080721fa3dc462cf201d8139111f1c7f160d5fb, from approved exact head e75d570c. The universe, reuse and source-faithfulness repairs are retained. Exact PR CI 40101557821 and actual merge-group 40103366424 pass all six gates and the ratchet.

This completes the bounded randomized promise-reduction/class prerequisite. The broader metacomplexity endpoints, including P2 and the later source reductions, remain open.

M5.5 follow-up is filed as #4430. It adds CHOPRS Definition 11 for circuits, shared with #4388's formula class, and the [OPS19] Gap-MCSP and [MMW19] bullets of Prop 63.

The barrier itself (Thm 59 / Cor 61) stays open here. It is statable on main but not provable: it needs exponent-2 shrinkage under k-wise independent restrictions and Hirahara–Santhanam's formula bound for MCSP, and neither exists in the library yet. CHOPRS Theorem 1 (the equivalences between natural proofs, learning and PRFs) is proposed to move to M6.

Metacomplexity coordinator (Jetski 7f8dd292); AI-written.

MINKT hardness, M1/M3. Filed #4447: Hirahara FOCS'22 Thm I.2 ("In particular") shows MINKT* (partial-string MINKT) is NP-hard under one-sided randomized reductions. Unconditional. It reuses #4362's route B: the same GapCMMSA, table and knowledge-set analysis, with program counting in place of circuit counting on the No side.

NP-hardness of total MINKT/MINcKT for TM programs is open (Ko'91 relativization; Liu–Pass CCC'22 fn 4). It is recorded on #4447 as an open problem, not a milestone, and ROADMAP's "hardness of MINKT and MINcKT" line will point to #4447 when K1 lands.

K1 and K2 are assigned to meta-os18-thm5. K3 and K4 share #4362 H5's poly-time table evaluator.

M6 is now scoped as #4451: CIKK16 "Learning Algorithms from Natural Proofs", natural properties ⇒ membership-query learning, targeting AC⁰[2] first. It has eight milestones, starting with the NW reconstruction as a query learner. Recorded decisions: an early gate pins RR97's p = 2 rank property before the AC⁰[2] work, and each learner is named explicitly, with certified query and hypothesis-size bounds and uncertified running time (labelled). Odd p and a machine-level runtime certificate stay open.

AI disclosure: metacomplexity coordinator agent (Jetski 7f8dd292).

M5.4 (#4383) is complete. #4429 landed on 2026-11-11 and added OPS Lemma 4.1 (exists_antiChecker_circuit_of_NP_subset_PPoly, through a hash-threshold greedy variant of the proof) and the unconditional Gap-MCSP oracle circuit exists_oracleCircuit_gapMCSP. Theorem 1.4 had already landed in #4393, proved through MMW. OPS's own Stockmeyer/BPP^NP route is still not formalized. The LocalCircuitClass wrapper for CHOPRS Prop. 63 continues under #4430 (#4441).

Coordinator note (Jetski 7f8dd292), agent-written.

docs: ROADMAP out-of-scope items for #4362; manual and docstring nits (…

M3 milestone: #4405 is complete. Ilango–Loff–Oliveira (CCC 2020) Theorem 4, Multi-output MCSP is NP-hard under one-sided randomized reductions, landed in #4462 (MultiMCSP.rpHard). M3 stays open:

Hirahara's partial MCSP via Hirahara FOCS'22: partial MCSP is NP-hard under randomized reductions (#798 M3.5/M3.6) #4362 is in its last PR (feat(MCSP/PartialHardness): Partial MCSP is NP-hard under randomized reductions (#4362 H5c) #4480).
MINKT* via Hirahara FOCS'22: MINKT* (partial-string MINKT) is NP-hard under randomized reductions (#798 M1/M3) #4447 has three PRs left.
Ilango's formula, constant-depth, MOCSP and random-oracle results are not yet designed.

feat(MCSP/PartialHardness): Partial MCSP is NP-hard under randomized …

M5.5 milestone landed: CHOPRS local circuit classes (#4430). The circuit form of CHOPRS Def 11/62 is on main (ECCC TR19-168 numbering). It comes with two circuit bullets of Prop 63:

[OPS19] Gap-MCSP. localCircuitClass_gapMCSP, registry gap-mcsp-oracle-circuits, from feat(MCSP): Gap-MCSP in a local circuit class (#4430 B) #4441.
[MMW19] MCSP[s]. An explicit oracle merge tree, localCircuitClass_MCSP, registry mmw-merge-tree-locality, from feat(MCSP/Magnification): merge-tree oracle for the MMW locality bullet (#4430 C1) #4443, feat(MCSP/Magnification): MMW merge tree as an oracle circuit (#4430 C2) #4446 and feat(MCSP/Magnification): MCSP[s] in a local circuit class (#4430 C) #4458. This bullet assumes n ≤ s(n) and 2 ≤ s(n), and its docstring labels that.

The core of the class is in #4437. The formula class from #4388 is now an instance of it, with its statements unchanged.

Still open. The locality barrier itself (Thm 59 / Cor 61) and the [AK10], [LW13], [OS18] k-VC and [OPS19] Gap-MKtP bullets are not done. They are recorded in the ROADMAP entry "Hardness magnification and the locality barrier" (#4512). Thm 59 / Cor 61 need exponent-2 shrinkage under k-wise independent restrictions, plus the Hirahara–Santhanam formula bound for MCSP.

Posted by the metacomplexity coordinator (Jetski 7f8dd292). Agent-written; no human review.

feat(Kolmogorov/MINKTStar): MINKT* is NP-hard under randomized reduct…

fix(UniformLearning/CIKK): address review-4553 on AC0Mod (#4451 M6.8b2)

feat(UniformLearning/CIKK): learning AC⁰[2] with the rank property (c…

feat(UniformLearning/CIKK): hypothesis size of the AC⁰[2] learner (cs…

chore(records): register the AC⁰[2] middle-slice lower bound and repo…

Progress note from the metacomplexity coordinator (Jetski session 7f8dd292). This covers the second wave, M6 / #4451: learning from natural proofs, CIKK16, for p = 2.

Mathematics. #4451 is complete. Cor 5.4 for p = 2 now holds as explicit theorems about the library's cikkLearner (MachineLearning/UniformLearning/CIKK/AC0Mod.lean, registry cikk-learning-ac0-2). For fixed depth d, cikkLearner learns AC⁰[2] circuits of depth d and size s under the uniform distribution with membership queries. The query bound is closed-form and quasi-polynomial, and every hypothesis has a quasi-polynomial-size De Morgan circuit. The theorem is built from:

the NW reconstruction as a weak learner (M6.1), best-of-k selection (M6.2), the IJKW direct-product reconstruction (M6.3) and the GL amplification reconstruction (M6.4);
the per-function black-box theorem learns_cikkLearner with its hypothesis-size bound (M6.5: feat(UniformLearning/CIKK): parameters of the CIKK learner (#4451 M6.5a) #4521, feat(UniformLearning/CIKK): the CIKK learner from a dense test (#4451 M6.5b) #4542, feat(UniformLearning/CIKK): the learner's hypotheses are small circuits relative to the test (#4451 M6.5c) #4552);
AC⁰[2]-efficiency of the generator (M6.6);
the RR97 rank property as a natural property against AC⁰[2] (M6.7);
the class form (M6.8: feat(Circuit/Boolean/Razborov): the rank property is useful against AC⁰[2] (Part of #4451, M6.8a) #4517, feat(Circuit/Boolean/Razborov): parameters of the CIKK learner for AC⁰[2] (#4451 M6.8b1) #4541, feat(UniformLearning/CIKK): learning AC⁰[2] with the rank property (#4451 M6.8b2) #4553, feat(UniformLearning/CIKK): hypothesis size of the AC⁰[2] learner (#4451 M6.8b3) #4578).

Labelled deviations: queries are certified, not running time; hypothesis size is certified, not depth; we use our rank-property variant (δ = 1/2, truth-table circuit size rather than NC²); p = 2 only.

Along the way:

majority ∉ AC⁰[p] and TC⁰ ⊄ AC⁰[p] for every prime p (feat(Circuit/Boolean): majority ∉ AC⁰[2]; TC⁰ ⊄ AC⁰[p] and P ⊄ AC⁰[p] for every prime p (Part of #4451) #4528);
a reusable two-stage sampling count form (refactor(TwoStage, DirectProduct): two-stage counting over finsets; DP headline as a client (part of #4451 follow-ups) #4565);
several simplifications and dependency cuts (refactor(List/GetD, Kolmogorov/TimeBounded): shared getD membership; move the poly-time K^t bound #4529, refactor(Circuit, NisanWigderson): replace directProductInput with BitString.block; derive restrict_binaryPolynomial #4538, refactor(Circuit/Boolean): split the P side out of Razborov/MiddleSlice to cut Smolensky/Majority's import closure (Part of #4451) #4539, refactor(Foundations/Data/Fintype): migrate agreement counts onto Fintype.card_filter_forall_mem_eq #4543, refactor(DirectProduct): AgreeOn clients and move tuple-sampler lemmas to TupleSampler (part of #4451 follow-ups) #4563);
a fix that stops cached builds hiding warnings in changed files (fix(scripts): re-elaborate changed files restored from the artifact cache #4527).
The records pass (chore(records): register the AC⁰[2] middle-slice lower bound and repoint CIKK records to #798 (#4451 records pass) #4595) registered the AC⁰[2] middle-slice lower bound, repointed the CIKK records and the ROADMAP line to this issue, and added the checked CIKK §5 locators to manual/sources.md. It assessed both manuals and edited the metacomplexity-and-methods chapter. Two small refactors from this wave are still in flight: refactor(CSP, Sorting, Iteration): one-line bitWidth bound; flatten and Record.pack as blocksEquiv.symm (part of #4451 follow-ups) #4600 (approved, queued) and refactor(Circuit, Log): complexity_decide_exists_mem_le; Real.log_two_lt_one (part of #4451 follow-ups) #4608 (in review).

Still open under M6 (also in ROADMAP.md):

CIKK Thm 5.1 in abstract form, including the (→) IsUseful bridge;
odd p (GRS list decoding over GF(p), the von Neumann step, Smolensky's dimension property for odd p);
a machine-level runtime certificate;
compression (Cor 5.2/5.5) and the MCSP search-to-decision consequence;
CHOPRS Thm 1 (natural proofs ⇔ learning ⇔ PRFs, proposed for M6 in feat(Circuit/Oracle, MCSP): CHOPRS local classes for circuits and the OPS19/MMW bullets of Prop 63 (#798 M5.5) #4430) and the other "further cryptography links";
a page-level check of the Cor 5.4 locator (p. 10:20) for manual/sources.md.

AI disclosure: written by an AI coordinator agent. The reviews cited in the PRs are agent reviews, not human reviews.

M6 wave 3 is filed as two issues:

feat(MachineLearning, NaturalProof): CIKK Theorem 5.1 from natural properties, P/poly and constant-depth forms (#798 M6) #4635: CIKK Thm 5.1 in abstract form. It derives the learner from IsNatural/IsUseful for P/poly (in the shape of CHOPRS Thm 5) and for constant-depth bases containing AC⁰[2], and proves the missing (→) usefulness bridge for ConstDepth. It is staffed: W3.1 and W3.3 to meta-rr97-gate, W3.2 to meta-proj.
feat(MachineLearning): CIKK learners as non-adaptive oracle circuits of size 2^{O(ℓ+g+e)} (#798 M6) #4634: the CIKK learner as a non-adaptive circuit of size 2^{O(ℓ)}, design first. In the query model, brute-force Occam learning already beats the certified query and hypothesis-size numbers, so the learner's own circuit size is what certifies CIKK's efficiency. It is also a prerequisite for the CHOPRS Thm 1 directions that involve learning, which are planned as wave 4.

The design check confirmed every CIKK locator in the repo against the LIPIcs PDF. The only gap is missing rows in sources.md (Cor 5.4, Def 2.6/Lemma 2.7, the runtime remark), to be added in #4635's Records step.

AI coordinator note (Jetski 7f8dd292); agent design, no human review yet.

Navigation Menu

Repository navigation

Metacomplexity track: time-bounded Kolmogorov, Liu–Pass, partial MCSP hardness, hardness magnification #798

Foundations already on `main`

Milestones

Standards

Process

Summary

Corrections to the starting map

Field map

A. Measures and meta-problems (M1)

B. One-way functions and Kolmogorov complexity (M2)

C. NP-hardness of MCSP variants (M3)

D. Consequences and limits of NP-hardness (M4)

E. Hardness magnification (M5)

F. Natural proofs and learning (M6)

M1: time-bounded Kolmogorov complexity

M2: Liu–Pass

M3: partial MCSP and other variants

M4: consequences of NP-hardness

M5: hardness magnification

What main already provides

What is missing

Milestone plan

The hardest parts

Risks

Decisions needed

Verification gaps

104 remaining items

Metadata

Assignees

Labels

Type

Projects

Milestone

Relationships

Development

Metacomplexity track: time-bounded Kolmogorov, Liu–Pass, partial MCSP hardness, hardness magnification #798

Description

Foundations already on main

Milestones

Standards

Process

Activity

SamuelSchlesinger commented on Oct 24, 2026

Summary

Corrections to the starting map

Field map

SamuelSchlesinger commented on Oct 24, 2026

A. Measures and meta-problems (M1)

B. One-way functions and Kolmogorov complexity (M2)

C. NP-hardness of MCSP variants (M3)

D. Consequences and limits of NP-hardness (M4)

E. Hardness magnification (M5)

F. Natural proofs and learning (M6)

SamuelSchlesinger commented on Oct 24, 2026

M1: time-bounded Kolmogorov complexity

M2: Liu–Pass

M3: partial MCSP and other variants

M4: consequences of NP-hardness

M5: hardness magnification

SamuelSchlesinger commented on Oct 24, 2026

What main already provides

What is missing

Milestone plan

The hardest parts

Risks

Decisions needed

Verification gaps

SamuelSchlesinger commented on Oct 24, 2026

SamuelSchlesinger commented on Oct 24, 2026

SamuelSchlesinger commented on Oct 24, 2026

SamuelSchlesinger commented on Oct 24, 2026

SamuelSchlesinger commented on Oct 24, 2026

SamuelSchlesinger commented on Oct 24, 2026

SamuelSchlesinger commented on Oct 24, 2026

SamuelSchlesinger commented on Oct 24, 2026

104 remaining items

SamuelSchlesinger commented on Nov 11, 2026

SamuelSchlesinger commented on Nov 11, 2026

SamuelSchlesinger commented on Nov 11, 2026

SamuelSchlesinger commented on Nov 11, 2026

SamuelSchlesinger commented on Nov 11, 2026

SamuelSchlesinger commented on Nov 11, 2026

SamuelSchlesinger commented on Nov 11, 2026

SamuelSchlesinger commented on Nov 11, 2026

Metadata

Metadata

Assignees

Labels

Type

Projects

Milestone

Relationships

Development

Issue actions

Foundations already on `main`