P vs NP

Progression-robust infinitely-often Gap-MCSP threshold

The final anti-checker bridge now needs only arbitrarily large hard arities on every progression n = d*m, rather than hardness at every sufficiently large arity. The denominator d is selected after assuming global NP circuit containment, so plain infinitely-often hardness is insufficient.

Can the fixed Gap-MCSP promise be proved hard above the N^1.1 threshold at arbitrarily large multiples of every denominator d at least two?

Promise-preserving reconstruction from a Gap-MCSP decider

Test circuit-prefix and restriction queries with exact sizes before importing decision-to-search reasoning from SAT.

Can a small gap decider recover a small circuit through queries guaranteed to preserve the promise?

Hardness amplification with a complete circuit budget

Audit YES and NO preservation, input expansion, encoder cost and decoder cost for one explicit transform.

Can a concrete truth-table encoding transfer a weaker bound without losing the N^1.1 margin?

Complexity of selecting anti-checker queries

Linear shared-circuit hardness and promise semantics are checked, but the tested fiber-coordinate amplification is exhausted. Full-query selectors have constant gate cost, requiring large-denominator targets. General direct-selector superlinear hardness remains open.

Can a suitably quantified selector lower bound directly contradict the OPS selector construction under global NP circuit containment?

Direct-sum lower bounds that count shared gates once

Test a proposed multi-instance lower bound against explicit shared-subcircuit constructions and the cost of combining outputs.

Which independence assumptions permit a useful direct-sum bound for general circuits with unrestricted fan-out?

Disjoint NP pairs from certified circuit consistency

Require polynomially verifiable certificates on both sides and make the incompleteness of bounded proof certificates explicit.

Can consistency and proof-certified inconsistency form disjoint NP sets with a useful ordinary-circuit separation target?

Stress-test Tseitin hardness under parity reasoning

Test raw Tseitin first, expecting algebraic shortcuts, before designing a modified family or invariant.

Which part of the vertex-support lower-bound argument survives a precise extension with parity equations or extension variables?

Extract and audit the refuter hidden in a lower-bound argument

Semantic refuter infrastructure and explicit easy-YES errors for payload literals and monotone payload rejectors are checked. The decisive missing step is resource-bounded hard-table generation, already required to refute always-accept.

What algorithm finds a counterexample to a proposed small circuit, given a concrete lower-bound proof method?

Adaptive semantic SAT compression beyond a fixed variable order

Strengthen the equality-side control beyond fixed-order residual merging, with an explicit algorithm and adversarial family.

Can a specific adaptive decomposition and caching rule bound both the number of residual states and the cost of identifying them?

Affine preprocessing with a precisely bounded nonlinear SAT core

Fix the residual representation and nonlinear parameter, then test worst-case growth and satisfiability preservation.

Does exact parity elimination leave a residual representation with a polynomial total budget for arbitrary CNFs, rather than only a parameterized bound?

Compare the current gap with anti-checker magnification parameters

Prove exact natural-number inequalities, including floor division, so a solver for the published anti-checker parameter regime can be transferred without silently choosing an unavailable exponent.

Both eventual inequalities are proved with exact natural-number divisions, for arbitrary fixed c≥1 and d≥2.

Stress-test SAT compression with equality residuals

Equality of two n-bit blocks has a linear-size CNF, but fixing the whole first block leaves 2^n distinct functions of the second block. Any exact residual-state representation for that order needs exponentially many states.

Answered negatively for fixed block-first variable order by state_count_lower_bound, with a concrete at-most-2n-clause equality CNF.

Derive the exact deterministic locality barrier from the sparse oracle circuit

Use its O(N polylog N) gate bound and uniform polylogarithmic oracle fan-in to contradict the localized N^1.1 lower bound on admissible lengths.

Both the conditional barrier and its unconditional instantiation with sparseOracleCircuit are proved.

P ≠ NP

One of two primary outcomes. Seek a closed Lean proof of ¬PeqNP while also actively investigating PeqNP.

Which modern bridge yields a machine-checked implication into ¬ PeqNP, with the missing mathematics isolated as a single Prop?

P = NP

A primary research goal alongside separation. Seek a closed proof of PeqNP through a concrete uniformly polynomial-time algorithm, not only a falsification test for P ≠ NP arguments.

Can an explicit SAT algorithm decide every encoded input within one proved polynomial bound, and can the remaining model-specific completeness proof be completed?

P ⊆ NP and Cook–Levin

P_subset_NP, polynomial reduction closure, and the general NP-completeness collapse theorem are now sorry-free over the canonical FinTM2 model. Cook–Levin remains open.

Can a CNF evaluator implement SAT membership in NP, then a tableau reduction establish Cook–Levin?

Gap-MCSP magnification

A magnification research program with concrete circuits and a checked conditional compression theorem. The encoded-length lower bound, binary-search construction, and substantive SAT transfer remain open.

Can we prove an unconditional lower bound for Gap-MCSP sitting just above the Oliveira–Pich–Santhanam / Atserias–Müller threshold?

The threshold lower bound

The corrected open Prop asks, for every sufficiently large arity n and N=ttLen n, whether every circuit solving the Gap-MCSP slice satisfies N^11 < size^10. It no longer quantifies over absent encoded lengths. Its eventual slices have nonempty yes/no sets and are consistent, proved in EncodingAudit.lean.

Can a circuit lower bound establish the corrected threshold on admissible lengths?

Time-bounded Kolmogorov chain rule

Investigate the published conditional time-bounded Kolmogorov chain rule after repairing the project specification. Budgeted K^t and elementary semantic lemmas are concrete; the characterization and universal-machine bridge remain unverified.

Can the universal-machine, time-threshold, and error/stretch quantifiers first be matched to KK Section7 before an unconditional violation target is trusted?

Finite toy search is not a universal-machine violation

The recorded finite toy-machine gaps plateau over the measured range. This is useful evidence against those tested constructions, not a proof that every finite-machine method fails or that the universal chain rule holds.

Can a source-matched universal-machine chain rule be stated before searching for asymptotic violations? The historical forall-epsilon negation was incorrect; failure of little-o uses an existential positive tolerance.

Algorithmic method / Missing-String

A slightly-too-fast algorithm converts, by diagonalization, into a circuit lower bound; Missing-String is the 2024 packaging. The direction now has a spine in Lean: the finite problem and its O(M+N)/2M-probe algorithm are proved (MissingString.lean), the Vyas-Williams equivalence is stated with explicit parameters (VyasWilliams.lean), and the chain to P ≠ NP is assembled with ITS MISSING STEP NAMED (Williams.lean). `SlightlyFastCircuitAlgorithm` is no longer opaque - it is ∀ k, MissingStringCircuitsOnCompressible (fun n => n^k + k).

What is the strongest circuit class for which we can establish the algorithmic conversion, with every runtime term proved? For Missing-String the runtime terms are now ALL proved; the open term is the conversion itself (vw_thm_1_8_backward), and beneath it the descent from NE to NP.

Missing-String conversion

LANDED AT THE FINITE LEVEL (2026-09-09). Missing-String is no longer an `opaque Language`: it is a total function problem (`MissingString.Instance`: a list of M strings of length N with M < 2^N, solution predicate "length N and not in the list"), its existence is the pigeonhole principle proved sorry-free (`exists_missing`, via the injection List.ofFn from Fin N → Bool), and the Vyas-Williams Thm 2.5 algorithm is a Lean function with machine-checked correctness AND a machine-checked cost bound. ProofExplorer/PVsNP/Algorithmic/MissingString.lean, 360 lines, zero sorries, axioms = [propext, Classical.choice, Quot.sound] throughout.

ANSWERED for the sequential problem, OPEN for the circuit problem. Sequentially the problem is trivial: 2M bit-probes, 2M+N+1 steps, proved. The open question is which UNIFORM DEPTH-TWO circuit families for Missing-String compile into which circuit lower bounds; that is Vyas-Williams Thm 1.8, now stated in Lean as `vw_thm_1_8` with M, N, S, the uniformity condition and the 2^poly(N) size bound all explicit (see missing-string-compressible).

Proof complexity → IPS

A verified staircase: Resolution → Frege fragments → algebraic systems → IPS. Not a direct route to P ≠ NP.

What is the weakest propositional system, sitting above Resolution, for which we cannot currently prove a CNF lower bound in Lean?

Resolution lower bound, then climb

The first stair, built: Literals/Clauses/CNF, an inductive resolution calculus, sorry-free soundness AND completeness (with an explicit 2^n size bound), a counting lower-bound engine, an exponential bound for an explicit unsatisfiable family, and — via the Prover–Delayer game — a 2^n tree-like bound for PHP_n^{n+1}.

Which hard CNF family is the shortest path to a sorry-free lower bound that is exponential in the *size of the formula* (not just in the number of variables)?

SAT search-tree compression

Equality-side control track with a concrete fixed-order residual-state lower bound. Generic search-tree compression and its uniform polynomial-time implementation remain unproved.

Which candidate compression principles already fail relative to the Baker–Gill–Solovay oracles?

Natural proofs

Razborov–Rudich: a natural circuit lower bound would break the PRGs we already believe in.

Is a proposed Gap-MCSP lower bound constructive and large in the Razborov–Rudich sense?

Relativization

Baker–Gill–Solovay: oracles making P = NP and P ≠ NP. The SEPARATING half is now formalised against the project's own machine model (`ProofExplorer/PVsNP/Barriers/BGS.lean`): the diagonalisation is sorry-free and `BGS.separation_of` derives `P^B ≠ NP^B` from two explicit model hypotheses. The collapsing half is still open and needs a space measure the frozen model does not have.

Remaining for the separating half: a Gödel numbering of `FinTM2` (`countable_oracleMachine`) and three finite verifier machines. Remaining for the collapsing half: PSPACE, or a padded-recursion oracle.

Algebrization

Aaronson–Wigderson: even arithmetizing techniques (the kind that prove IP = PSPACE) do not suffice on their own.

Does the argument still hold relative to algebraic oracles?

Geometric complexity theory

Mulmuley's programme via algebraic geometry. Deprioritized: the translation from VP vs VNP to Boolean P vs NP is not direct.

Not this quarter.

Gap-MKtP as the shared hub of directions 1 and 2

The same meta-complexity object sits on both top bridges. Oliveira–Pich–Santhanam magnify a weak lower bound for Gap-MKtP (not only Gap-MCSP) into NP ⊄ P/poly; Kabanets–Kolokolova make the K^t chain rule equivalent to P = NP under NP-hardness of a Gap-K^t problem. Formalize Gap-MKtP ONCE, with one universal machine and one time budget, and hang both implications from it. The surgical open Prop collapses to statements about a single object.

For which explicit (s₁(n), s₂(n), t(n)) does a Gap-MKtP[s₁, s₂, t] lower bound magnify, and is that the same gap problem whose NP-hardness Kabanets–Kolokolova assume?

Use the algorithmic method to prove the magnification-threshold lower bound

The weak lower bound that magnification needs must be non-natural and non-local (the locality barrier of Chen–Jin–Santhanam–Williams). The only known technique with those properties is the algorithmic method (Williams; range avoidance; Li 2024's near-maximum circuit lower bound for symmetric exponential time). Combine directions 1 and 3: try to reach Gap-MCSP/MKtP just above the threshold with an algorithm-to-lower-bound conversion rather than a combinatorial argument.

Is there a Missing-String / range-avoidance algorithm whose conversion lands exactly on a Gap-MKtP lower bound at the magnification threshold?

Hardness magnification for proof complexity

Müller–Pich showed magnification phenomena for proof complexity too, and Razborov's independence results show which proof systems cannot prove circuit lower bounds. Combine directions 1 and 4: the propositional formulas expressing "Gap-MCSP is hard" are themselves the CNFs whose proof complexity is the first unclimbable stair.

In which proof system is a threshold Gap-MCSP lower bound provable, and does a Resolution/IPS lower bound for its negation formula say anything about the truth of the bound?

Search-tree compression against one-way functions

Liu–Pass showed one-way functions exist iff time-bounded Kolmogorov complexity is hard on average. A compression principle for SAT search trees (direction 5) is a claim that witnesses have short programs; combined with direction 2 it becomes a falsifier of one-way functions. Any candidate compression lemma must therefore also pass "does it break every candidate OWF?" before it is believed.

Which compression principles for search trees imply the average-case easiness of K^t that Liu–Pass show is equivalent to no OWFs?

Relativization as a type-level test in Lean

Now executable, and one of its two directions is no longer a promise. `Oracle := Language`; `RelativizedP` / `RelativizedNP` are defined over an explicit poly-time oracle machine in *one query per round* normal form, whose `query`, `next` and `output` are ordinary `IsPolyTime` functions — the SAME notion of polynomial time as `InP`. `BGS.no_relativizing_collapse` (an argument proving `P^A = NP^A` for every oracle is refuted) now rests on `BGS.separation`, i.e. on a real diagonalisation plus two named model obligations, instead of a bare `sorry`.

Which of our bridges (magnification, chain rule, algorithmic conversion) are stated in a way that does NOT relativize, and where exactly is the non-relativizing step in each?

Finite-instance search engine for all directions

Every direction has a finite shadow - smallest hard truth tables for MCSP, additivity violations of K^t for tiny t, minimal Resolution refutations, Missing-String instances. A shared decide harness over small n produces counterexamples to candidate lemmas before any asymptotic proof. The circuit half now exists: `ProofExplorer/PVsNP/CircuitSearch.lean`.

What is the smallest n at which each candidate lemma can be tested exhaustively, and does any candidate survive?

Prover–Delayer game for tree-like PHP

Landed sorry-free: the Pudlák–Impagliazzo game is defined as an inductive Prop, a Delayer scoring p forces every tree-like refutation to have 2^p leaves, and the Delayer scores n on PHP_n^{n+1} — so tree-like refutations of PHP need 2^n leaves. This discharges `TreeLikePHPLowerBound` with the explicit constant c = 2.

Answered. What remains: can the asymmetric (Beyersdorff–Galesi–Lauria) game be formalized to reach the true 2^Θ(n log n), and is there any Delayer-style measure for dag-like size?

Ben-Sasson–Wigderson size–width tradeoff

Landed sorry-free, both forms, in ProofComplexity/WidthSize.lean. Tree-like: 2^(w − w₀) ≤ leafCount, constant-free. General (dag-like): if every refutation of φ has width ≥ w₀ + 2j then every refutation has dagSize ≥ exp(j² / (2|V|)) — the real Ben-Sasson–Wigderson theorem with an explicit constant, via the fat-clause induction and a double-counting argument. Two by-products: the Prop `BenSassonWigdersonSizeWidth` as written in Resolution.lean is FALSE and is now refuted in Lean, and the width half for PHP (`PHPWidthLowerBound`) is discharged with c = 1 — but only by the width of the pigeon axioms, which is provably not enough for Haken.

Answered for the tradeoff itself. What remains: is there any width lower bound of order n + Ω(n^{3/2}) for PHP_n^{n+1}? Below that threshold the relation provably cannot reach 2^Ω(n).

Haken's exponential bound for general resolution

Dag-like resolution refutations of PHP_n^{n+1} have size 2^Ω(n) (Haken 1985, Beame–Pitassi 1996 simplification). LANDED SORRY-FREE with the explicit constant c = 201/200: `Haken.hakenPHPLowerBound' : HakenPHPLowerBound` in `ProofComplexity/HakenElimination.lean`. Round 8a (`Haken.lean`) proved the monotone/complexity-measure half (every refutation has a clause of monotone size ≥ ⌊(n+1)/3⌋²) and reduced the theorem to one Prop `PHPFatElimination`; round 8b (`HakenElimination.lean`) proved that Prop by a transport-of-derivations lemma, the matching restriction of PHP, averaging over monotone variables, and an induction on the number of rounds. Auxiliary formalization of a known theorem.

Answered. The staircase question that remains is the next stair: can the same critical-assignment / monotone-clause / transport machinery give a lower bound for a stronger system (bounded-depth Frege, or Cutting Planes for PHP), and what is the surgical Prop there?

Chain-rule bridge awaiting a matched specification

The intended P=NP-to-chain-rule argument motivates a contrapositive attack. The existing composition uses unproved characterization and simulation inputs and has not been verified for the current surrogate definitions.

Can the three bridge inputs be restated with the source time/error quantifiers and an efficient universal machine, before claiming a published unconditional implication?

Average-case symmetry of information failure = one-way functions

Hirahara–Ilango–Lu–Nanashima–Oliveira (TR23-035): OWF exist iff time-bounded (pK^t) symmetry of information — the two-string chain rule with equality — fails on average over some samplable distribution. Liu–Pass (FOCS'20): OWF iff K^t is mildly hard on average. Hirahara (STOC'23): OWF iff distributional K^t is NP-hard to approximate and NP ⊄ BPP. OWF ⇒ P ≠ NP. So the average-case, two-string, samplable version of `chain-rule-violation` is exactly "construct a one-way function".

State in Lean `OWF ↔ ¬ AvgSoI` with pK^t defined on the timed-kt universal machine, and prove the easy direction `OWF → ¬ PeqNP`; then ask which explicit samplable distribution on pairs is the candidate for an Ω(n) average-case SoI failure.

Atserias–Müller uniform magnification: sidestep locality with Santhanam–Williams

Atserias–Müller (arXiv 2503.24061, Thm 27): for every ε, δ > 0 there is γ > 0 such that if n^{-ε}-MCSP[σ] ∉ P-uniform-SIZE[n^{1+ε+δ}] for some σ(ℓ) ≤ 2^{γℓ}, then P ≠ NP^{⊕P}. Santhanam–Williams prove P ⊄ P-uniform-SIZE[n^c] for every c by indirect diagonalization, with a non-explicit hard language, and their proof does not localize. The threshold is "almost known" and the locality barrier (Cor. 23: every sparse Q has n^{2ε+o(1)} probabilistic formulas with one fan-in-n^{o(1)} oracle gate) does not apply to uniform lower bounds.

Can the Santhanam–Williams indirect diagonalization be made explicit for n^{-ε}-MCSP[σ] (P-uniform n^{1+ε+δ} lower bound), and can the ⊕P oracle in the conclusion be removed by replacing the XOR-based distinguisher hash with a P-uniform AND/OR one?

Exact deterministic locality barrier

The constructed sparse oracle circuit refutes LocalizedThreshold localFanin on admissible encoded lengths, with no construction hypothesis remaining.

Answered for our deterministic exact-gap model by locality_barrier.

The sharp pair: n^{2ε−δ} known, n^{2ε+δ} needed

Atserias–Müller Thm 10: n^{-ε}-MCSP[2^{√ℓ}] ∉ PFML[n^{2ε−δ}] for all ε, δ ∈ (0,1]; Thm 25: n^{-ε}-MCSP[σ] ∉ PFML[n^{2ε+δ}] with σ ≤ 2^{γℓ} ⇒ ⊕P ⊄ NC¹; Thm 24: FML[n^{1+2ε+δ}] ⇒ NP ⊄ FML[n^c]. The pair is the most precise statement of `magnification-threshold` in existence. CHOPRS Thm 1 shows the needed Circuit[N^{1+ε}] bound for approximate MCSP is equivalent to worst-case MCSP hardness and to learning/PRF statements — the "weak" bound is not weak.

Formalize Thm 10 (the known bound, via the pseudorandom restriction generator of Chen et al.) and the statement of Thm 25 against one `ProbFormula` type, and exhibit the exact lemma where the exponent 2ε−δ arises, to see which step would have to improve.

Formalize Li 2024: range avoidance ⇒ S₂E ⊄ i.o.-SIZE[2^n/n]

Li (STOC'24) gives a single-valued FS₂P algorithm for Range Avoidance for all input lengths, hence S₂E ⊄ i.o.-SIZE[2^n/n], via Korten's P^NP reduction from Avoid to constructing hard truth tables (itself Jeřábek's dual weak pigeonhole principle) and the iterative win-win of Chen–Lu–Oliveira–Ren– Santhanam. Ren–Williams (2026) push the class to E^{prMA}/1. The proofs relativize and are finite combinatorics plus Shannon counting — the most Lean-friendly of the strongest known circuit lower bounds.

Can Korten's reduction (Avoid ≤_{P^NP} HardTruthTable) and Li's single-valued FS₂P algorithm be stated against `BoolCircuit` with explicit sizes, so that `S2E_not_io_SIZE : ∀ n ≥ n₀, ∃ f ∈ S₂E, size(f_n) > 2^n/n` is a theorem modulo an S₂P machine model?

Missing-String on compressible lists is exactly NE ⊄ SIZE (Vyas-Williams Thm 1.8)

STATED IN LEAN WITH EVERY PARAMETER EXPLICIT (2026-09-09), ProofExplorer/PVsNP/Algorithmic/VyasWilliams.lean. `NE_not_SIZE S ↔ MissingStringCircuitsOnCompressible S`, where the right-hand side quantifies over constants c, k and a family F of multi-output DEPTH-TWO circuits (DNFs, defined concretely as `DepthTwo`/`MSCircuit`, not opaquely), asserts `PolyTimeUniform F`, a size bound `(F M N).size ≤ 2 ^ (N ^ k)`, and correctness on every S(n)-compressible list of M = `vwListLength c (S n)` = 2^(c·S·log₂(S+2)+c) strings of length N = 2^n, for INFINITELY MANY n (as `Set.Infinite`). The iff is assembled sorry-free from two named holes, vw_thm_1_8_forward and vw_thm_1_8_backward.

The statement layer is done; the open Prop is `vw_thm_1_8_backward : MissingStringCircuitsOnCompressible S → NE_not_SIZE S`. The next surgical question is the one the formalization exposed: at which (n, S) does the compressibility promise stop being vacuous? Proved here: it is vacuous at n=1, S=1 and NOT vacuous at n=1, S=0 or n=2, S=3.

Algebrization barriers from XOR-Missing-String (Chen-Hu-Ren 2025)

Chen-Hu-Ren (ITCS'26, arXiv 2511.14038) construct oracles with multilinear extensions à such that PostBPE^{Ã} has linear-size oracle circuits infinitely often, BPE^{Ã} linear-size almost everywhere, and a natural subclass of MA_E containing the Buhrman-Fortnow-Thierauf hard language has h(n)-size circuits for every super-half-exponential h. The tool is the communication complexity of XOR-Missing-String. Now that Missing-String itself is a real Lean object (a total function problem plus a proved algorithm), the XOR variant is a two-line variation on the same types rather than a new formalization project.

Which of the circuit constructions in Vyas-Williams Thm 1.6-1.8 algebrize, and does the compressible-list restriction of Thm 1.8 already break the Chen-Hu-Ren oracle construction? The Lean side can now ask a sharper version: is `SCompressible` preserved under the multilinear extension used by Chen-Hu-Ren?

A conditional bridge from Extended Frege lower bounds to P ≠ NP (Pich–Santhanam 2023)

Pich–Santhanam (arXiv 2312.08163): if (I) S¹₂ proves that a concrete function in E is hard to approximate by subexponential-size circuits, (II) S¹₂ proves that circuits breaking OWFs transform into learners of p-size circuits, and (III) EF has no p-size proofs of p-size circuit lower bounds for some hard-to-approximate fₙ, then P ≠ NP. Alternatively any of {S¹₂-provable p-time anticheckers for SAT, S¹₂-provable witnessing of NP ⊄ P/poly, OWF from NP ⊄ P/poly & hardness of E} gives "EF not p-bounded ⇒ P ≠ NP". Arteche–Khaniki–Pich–Santhanam (ICALP'24) give the iEF analogue with conclusion #P ⊄ FP/poly. Pich–Santhanam also observe that any such connection proved outright would imply NEXP ⊄ P/poly.

Which of conditions 1–3 is closest to a known theorem — anticheckers exist in ZPP^NP (Fortnow–Pavan– Sengupta) and in BPP^C (Atserias); is the obstacle the p-time bound or the S¹₂-provability?

Hardness of proving hardness (Razborov, Pich–Santhanam, Li–Oliveira, GGRT 2026)

Razborov (1995) showed NP ⊄ P/poly is unprovable in fragments of bounded arithmetic assuming strong PRGs — natural proofs as unprovability. Razborov (Ann. Math. 2015) showed Nisan–Wigderson-generator formulas expressing circuit lower bounds are hard for Res(k) and polynomial calculus resolution; Garlík–Gryaznov–Ren–Tzameret (2026) extend this to PCR_{F₂}. Li–Oliveira (2023): APC₁ cannot prove strong Π₃-vs-Σ₃ size separations. Lu–Santhanam–Tzameret (2025): AC⁰[p]-Frege cannot efficiently prove that constant-depth algebraic lower bounds are hard. Pich–Santhanam (FOCS'19) frame the general phenomenon. Counterpoint: Davis–Robere (2026) show Res(log) proves depth-d Frege lower bounds for PHP, and Li–Li–Ren (2024) show Resolution lower bounds are provable in T¹₂(α)+dwPHP.

For each stair of `resolution-tower`, what is the weakest theory/refuter class in which the Lean proof lives, and does the next stair (AC⁰[p]-Frege) require a strength that Razborov-type results forbid?

roABP-IPS_LIN CNF lower bound via feasible interpolation (HLT 2026)

Hakoniemi–Limaye–Tzameret (arXiv 2605.04544) prove that an explicit CNF Ψ(u,v) = Φ₁(u,v) ∧ Φ₂(u) with poly(n) variables and clauses requires roABP-IPS_LIN refutations of width 2^{N^{Ω(1)}} in every variable ordering over every field (Thm 18). The engine is a rank-based feasible interpolation (Thm 9): an roABP-IPS_LIN refutation of width w of P₀(x,z) ∪ P₁(y,z), with x before all other variables, yields a (monotone) span program of size poly(w·|P₀|) computing an interpolant; then the monotone span program lower bound for GEN (Robere–Pitassi–Rossman–Cook 2016) finishes.

Which single lemma — Thm 9 interpolation, the normal form Thm 8, or the RPRC16 span-program bound — is the Lean bottleneck, and does the GEN lower bound admit a finite-instance certificate for small n?

Constructivity gate (Chen–Jin–Santhanam–Williams; Carmosino–Grosser)

Chen–Jin–Santhanam–Williams (2022): making known lower bounds for MCSP (and streaming, one-tape TM, query bounds) constructive — an efficient refuter that outputs counterexamples to every small circuit — would imply separations up to P ≠ NP; conversely P ≠ NP implies a constructive separation of SAT from P (Gutfreund–Shaltiel–Ta-Shma); and detecting high K^t admits no constructive separation from any class. Carmosino–Grosser (2025) refine to Student–Teacher refuters.

For the N^{2−o(1)} formula lower bound for MCSP (Hirahara–Santhanam / CKLM), is the implicit refuter P-computable, and which CJSW consequence would follow if it were?

Extension complexity as an unconditional falsifier of LP-based P = NP claims

Fiorini–Massar–Pokutta–Tiwary–de Wolf (STOC'12/JACM'15): the TSP polytope has extension complexity 2^{Ω(√n)}; Rothvoß (2014): perfect matching 2^{Ω(n)}; Lee–Raghavendra–Steurer (2015): SDP analogues. These are unconditional and refute every P = NP claim of the form "a polynomial-size LP/SDP projects onto the tour polytope". Arthanari's 2026 Lean 4 "proof" of P = NP (arXiv 2606.03194) claims membership in the pedigree polytope conv(Pₙ) is decided by a multicommodity-flow LP; since STSP reduces to it by projection, a polynomial-size LP characterization would be a polynomial extended formulation of the STSP polytope — impossible. Its Lean chain also rests on six declared `axiom`s.

Formalize the factorization theorem and state "no LP of size 2^{o(√n)} has the STSP polytope as a projection"; then check whether the pedigree MCF(n−1) LP is linear in X (in which case Arthanari's step 1 is refuted outright by FMPTW).

Freeze the model: Mathlib TM2 + formal-conjectures P/NP

DONE. `InP`, `InNP`, `PolyReducesTo`, `SAT` and `Oracle` are no longer `opaque`. The model is `IsPolyTime f := Nonempty (Turing.TM2ComputableInPolyTime bitEncode bitEncode f)` over Mathlib `v4.33.1`'s `Turing.FinTM2`, with google-deepmind/formal-conjectures' `BitstringEncoding` and `P`/`NP`/`coNP` vendored (Apache-2.0, rev `990d209a1ffb`) into `ProofExplorer/PVsNP/Model/{Encoding,PolyTime,Classes}.lean`. `peqNP_iff_P_eq_NP` proves sorry-free that our `PeqNP` is exactly `Model.P = Model.NP`, so `P_ne_NP` is the same proposition as `ComplexityTheory.P_ne_NP`.

Model selection and basic composition/projection closure are complete. The bounded loop and substantive verifier constructions remain.

Composition of poly-time TM2 machines (Mathlib's proof_wanted)

Completed actual FinTM2 composition. Model.polyTime_comp has no sorry; P_subset_NP, reductions and general completeness collapse are now sorry-free transitively.

Answered: the composite runs in q(R(n)) + 2*(R(n)+1) + p(n), with R(n)=n+b*p(n).

Real Boolean circuits, truth tables, MCSP and Gap-MCSP

Done. `Circuits.lean` and `MetaComplexity/MCSP.lean` now carry real definitions with the declaration names preserved (`BoolCircuit`, `ComputesOn`, `InPpoly`, `MCSP`, `GapMCSP`). Written directly (~560 lines) rather than ported; the representation chosen was a straight-line program indexed by gate count, not a tree circuit.

Which circuit representation keeps `size` a gate count, makes `eval` decidable (for finite-instance search) and lets `P_subset_Ppoly` be stated as an explicit `Polynomial ℕ` bound?

P ⊆ P/poly: the one machine theorem directions 1 and 3 need

`P_subset_Ppoly` is a time-bounded tableau over `FinTM2` configurations. Now that `InP` is a definition, the statement is finally about a real machine: unfolding `InP L` gives `TM2ComputableInPolyTime bitEncode bitEncode d` with an explicit `time : Polynomial ℕ`, and the tableau has `time.eval n` rows and at most `time.eval n` touched stack cells per stack.

Can the tableau be built directly on `FinTM2` configurations (stacks truncated to `time n`) without first passing through `TM2to1`/`TM1to1`, whose Mathlib simulations carry no step bounds?

CNF + Resolution with explicit size, then a lower bound

Direction 4 needs no machine. Define `CNF` (reuse Lean core `Std.Sat.CNF` or SATurday's `Literal/Clause/CNF`), `ResolutionProof φ` as an inductive derivation with `resolutionSize`, `resolution_sound`, and then either Ben-Sasson–Wigderson size–width (~2k lines) or Haken's PHP bound (~3–5k). astrogirlnim/SATurday (MIT) has sorry-free `Resolution.lean`, `PHP.lean` (`phpCNF_unsat`, `phpCNF_refutable`) and `SizeWidth.lean` scaffolding.

Is size–width (Ben-Sasson–Wigderson) plus Tseitin/PHP expansion the shortest sorry-free route to `ResolutionExponentialLowerBound`, or is Haken's bottleneck counting shorter in Lean?

Vendor timed-kt for a fixed universal machine and K^t

COMPATIBILITY VERDICT (2026-09-09, verified by build, not by inspection): timed-kt @9816ed9f BUILDS CLEAN against Lean v4.33.1 + Mathlib v4.33.1. A scratch Lake project (/home/josh/repo/timed-kt-probe) with lean-toolchain v4.33.1, mathlib pinned v4.33.1 at the root and timed_kt at the rev resolved mathlib to v4.33.1 (0df444a360ea, our own pin) over timed-kt's declared v4.33.0, and `lake build TimedKt` finished 1752/1752 jobs with ZERO errors and ZERO warnings. No patch, no toolchain bump, no fork needed. Every public declaration checked depends only on [propext, Classical.choice, Quot.sound].

ANSWERED, both halves. (a) Yes, it builds against v4.33.1. (b) No, Levin's |p| + ceilLog2 t is NOT the currency Kabanets-Kolokolova use: TR25-089 is about the BUDGETED K^t(x|y) = min{|p| : run in <= t steps}. timed-kt ships only the Levin measure. The budgeted measure is a ~15-line sInf over the SAME TimedDecompressor.Runs relation, and that variant compiles sorry-free against the real machine. New question: none of substance - the marginal build is ~100 s and 79 MB, so CI cost is not an objection.

Cook–Levin, deferred and planned

`SAT` is now a real language over a derived CNF encoding, and `cook_levin : NPComplete SAT` is a single `sorry` with both halves meaningful. `complete_in_P_implies_PeqNP` no longer waits for it: it is proved from `InP.of_polyReducesTo` and `P_subset_NP`.

Is the oblivious-machine route (Balbach) or the direct tableau on `FinTM2` (AEjonanonymous shape) the shorter path to `cook_levin` once `P_subset_Ppoly` exists?

Oracle TM2 and relativised classes for the barriers

DONE for the purpose it was raised for. `Oracle := Language` and `RelativizedP` / `RelativizedNP` are definitions over the one-query-per-round oracle machine of `Barriers.lean` — no fork of `TM2.Stmt`, no second notion of polynomial time. `Barriers/BGS.lean` then carries out a real diagonalisation in that model, which is the practical test that the design is usable.

ANSWERED for the model. The residual question is no longer about the oracle layer at all: it is the Gödel numbering of `FinTM2` (`infra-godel-numbering`) and the missing poly-time closure lemmas.

Abstract cost model as the fallback, with its two impossibility facts

alonamaloh/complexity-lean (Apache-2.0, Lean v4.32.2, 1.6k lines, 0 sorry) defines classes over a 5-field `Model` interface (countable programs, `Halts p x w out n` with step bound, determinism, monotonicity, sequential composition with cost, identity), instantiated by a while-language and a first-order functional language. `P ⊆ NP` is two lines; reductions compose for free. It also proves two facts we must respect: no shallow embedding (Lean functions as programs) can be a model (Cantor), and Mathlib's `evaln` fuel is not a step count.

Under which single extra theorem (a poly-time simulation of the while-language on `FinTM2`) does the model-relative `InP` coincide with the TM2 `InP`, so that the fallback is a lemma rather than a fork?

Simas 2026 framework: not a dependency

The framework lives only inside Zenodo arXiv-source zips of the "Decision Quotient" series (concept DOI 10.5281/zenodo.19010246, March 2026; latest record 21631928, July 2026, arXiv 2603.14689): Lean v4.27.0-rc1, Mathlib at commit a8227f46, 22k–54k lines, 0 sorry, 0 axioms, CC-BY-4.0, no git repo, no Lake package. Two models side by side: `PolyTime := Nonempty (TM2ComputableInPolyTime …)` with `KarpReduces` (Mathlib TM2), and a `Counted` cost monad with `SizeOf`-based `InP`. The NP/coNP/Σ₂ᵖ/NP^PP material are hardness templates for the author's decision-quotient problems, not class definitions.

Nothing remains; the reusable idea (`PolyTime` as `Nonempty (TM2ComputableInPolyTime …)`, Karp reductions as `∃ f, PolyTime f ∧ …`) is already in formal-conjectures in cleaner form.

Real circuits, truth tables, MCSP and Gap-MCSP in Lean

The opaque skeleton is gone. `BoolCircuit n` is a straight-line program (DAG) over the basis {const, ¬, ∧₂, ∨₂} with `size` a gate count and `eval : (Fin n → Bool) → Bool`; `circuitComplexity` is `sInf {s | ∃ C, C.size ≤ s ∧ C.eval = f}`; `MCSP` and `GapMCSP s₁ s₂` are real objects over an explicit, uniquely decodable bitstring encoding. Landed sorry-free: the counting bound, the Shannon existence of a hard function, the 5·2ⁿ upper bound, and exact circuit complexities of tiny truth tables by exhaustive `decide`.

With the definitions in place, what is the weakest explicit s(n) for which a Gap-MCSP lower bound is still provable by counting alone, and where exactly does counting stop being enough?

Asymmetric Prover–Delayer game for 2^Ω(n log n)

Beyersdorff–Galesi–Lauria: let the Delayer name a pair of weights (a, b) with 1/a + 1/b = 1 and score log a or log b according to the Prover's choice. On PHP the Delayer scores Ω(n log n), which is tight for tree-like resolution.

Does the asymmetric game fit the same inductive-Prop encoding, with `2 ^ p` replaced by a real-valued potential and `2^p ≤ 2^a + 2^b` by `1/w ≤ 1/w_0 + 1/w_1`?

Why the Prover–Delayer game cannot reach Haken

The game bounds `leafCount`, never `dagSize`, and the reason is structural, not an artefact of our encoding.

Is there a Delayer-style potential that is *sub*additive over the set of distinct clauses rather than over the two premises of each step?

The first machine-checked hardness-magnification theorem

Both circuit-construction stages are now proved. BinarySearch.lean proves sparseOracleCircuit with the original constant-eight size bound, exact oracle fan-in gapQueryLen n, and at most gapQueryLen n·ttLen n oracle queries. Combining it with oracle substitution proves CompressionSimulation outright. magnification_bitAccess therefore derives ttListLanguage ∉ P/poly from the repaired admissible-length threshold with no remaining construction hypothesis.

The circuit construction is complete. Can an actual lower-bound method establish the repaired threshold, and can a justified transfer connect its bit-access language to SAT?

Why size–width cannot give Haken for PHP

PHP_n^{n+1} has (n+1)n variables and initial width w₀ = n, so the Ben-Sasson–Wigderson exponent j²/(2(n+1)n) is a constant for every width bound of the form width ≥ n + O(n). Reaching 2^Ω(n) through the relation needs width ≥ n + Ω(n^{3/2}).

Is w(PHP_n^{n+1} ⊢ ⊥) really only Θ(n)? If so the relation is dead for PHP and Haken must be done by bottleneck counting, exactly as in 1985.

Polynomial iteration with an explicit storage bound

Repaired the oracle model with a polynomial worktape invariant. Proved exact doubling growth, absence of any polynomial output-length bound, invariant preservation, and polynomial resource accounting. The bounded FinTM2 loop remains open.

Can the input-parameterized bounded loop and its final output be implemented in FinTM2 with explicit clock and encoding costs?

Encoding-safe promise hardness and magnification

The old all-lengths threshold is refuted in Lean: at arbitrarily large lengths outside ttLen n = n+1+2^n, both promise sets are empty and a zero-gate projection solves them. Both active thresholds now quantify over sufficiently large arities and their encoded lengths. The raw gap overlaps at arity one; eventual parameter ordering and nonempty, disjoint yes/no slices are proved, as is equivalence to a well-formed eventual restriction.

ANSWERED for the encoding and consistency audit. Can an actual lower-bound argument establish the repaired admissible-length threshold?

Odd-charge Tseitin constraints and the expander staircase

The finite expansion-to-width-to-size pipeline is proved without sorry. Connected odd-charge graphs with balanced-cut boundary at least b require resolution width at least b; degree d and boundary d + 2j give dagSize at least exp(j^2/(2|E|)). An asymptotic expander family remains to be supplied.

Which explicit bounded-degree graph family gives the shortest verified quantitative expansion proof and encoding-length analysis?

Extract Boolean interpolants from resolution proofs

Connect the concrete resolution and Boolean circuit libraries through a verified interpolant extractor.

Can a resolution refutation of A(x,z) and B(y,z) produce a polynomial-size Boolean separator I(z)?

SAT-certified finite circuit lower bounds

Prove a circuit-synthesis SAT encoding sound and complete, then replay unsatisfiability certificates in Lean.

Can verified UNSAT certificates establish exact circuit lower bounds beyond exhaustive kernel enumeration?

The all-bitstring-lengths Gap-MCSP threshold is false

The original threshold demanded a positive superlinear gate lower bound at every sufficiently large bitstring length, including lengths with no encoded instances. Zero-gate projections refute it at arbitrarily large lengths. Retained as AllLengthsGapMCSPThreshold for the audit.

Answered by not_allLengthsGapMCSPThreshold.

Replace sorted-rank transfer by constructive anti-checkers

Audit the actual OPS transfer through a short list of labelled samples and an existential small-circuit consistency problem. This bypasses the unsupported SATtoListBit hypothesis.

Can the OPS near-linear anti-checker construction and Succinct-MCSP verifier be implemented, then transferred to the current wider Gap-MCSP promise?

Why resolution hardness is not general SAT hardness

Cook-Reckhow connects NP versus coNP to all polynomially checkable proof systems. A fixed-system resolution lower bound does not supply an arbitrary-SAT-algorithm lower bound.

What justified extraction or simulation would transfer an arbitrary polynomial-time SAT decider into the specific proof system being lower-bounded?

Convert selector gate size into truth-table coordinate support

The checked support theorem collects direct input operands of gates and direct input outputs. Agreement there forces agreement of every output of the shared wiring.

The support theorem and selector application are checked. What promise-specific argument goes beyond the resulting linear gate bound?

Charge shared selector gates through their input operands

The unconditional shared-circuit gate bound is checked; which promise-specific invariant can make it superlinear?

Promise-specific selector fibers beyond the linear support bound

Fiber anti-cover containment is now proved equivalent to selector validity. Additive anchor sensitivity is false; deduplicating restores valid accounting but yields only the existing linear coordinate ceiling. No superlinear shared-computation mechanism survived this round.

What non-coordinate measure of shared computation uses the selector promise and supports a rigorously proved superlinear lower bound?

Zero certificates do not amplify circuit size

Can the set of input coordinates needed to certify a circuit's value at zero be much larger than the circuit itself?

Explicit easy-YES refuters for monotone payload algorithms

How far can explicit low-complexity truth tables refute a nonconstant class without generating any hard truth table?

Fiber correctness is not a shared-gate measure

Whole-fiber anti-cover containment is equivalent to the original Hits validity condition, so summing it over easy anchors adds no semantic strength and supplies no ownership of shared gates. A full-query selector is valid with input-independent queries, showing that wrong sample-count regimes make selector gate lower bounds false.

Which additional property, beyond validity and fiber anti-cover, can assign non-overlapping resources in one unrestricted-fanout selector wiring?

Test additive support charging across selector fibers

Define a concrete sum of per-anchor or per-fiber input-support requirements and test whether it can be charged to gates of one shared multioutput selector circuit.

Can disjoint hard information required on many selector fibers force more than the linear 2*size+outputs support bound, or can multiplexing and repeated outputs reuse the same gates across all fibers?

Match direct selector hardness to the published construction

For a basis-matched constant c, is there a fixed positive exponent margin giving hard selector slices for every sufficiently large denominator?

Intermediate-work audit for factored existential SAT

Independent exact tests confirm the hash-consed restriction-and-OR solver on hundreds of small CNFs, but unsatisfiable pigeonhole and odd-charge prism Tseitin inputs exhibit large transient allocation and restriction work even though the final DAG is the one-node constant false.

Can any proved potential bound all restriction traversal, hash-cons construction, order-selection scans, and retained unreachable nodes polynomially in the encoded CNF length?

Hash-consed factorized SAT elimination

How much sharing survives exact existential variable elimination when restrictions and disjunctions are hash-consed and locally simplified?

Resource-bounded hard-table generation against always-accept

Test explicit diagonalization and missing-string enumeration as uniform generators of truth tables above the CJSW MCSP threshold.

Can a hard truth table be generated in polylog-time-uniform quasipolynomial-size AC0 without an oracle, advice, classical choice, or a hardwired hard table?

Semantic completeness of repeated factored elimination

Does eliminating a finite covering list yield a Boolean value equivalent to existence of a satisfying assignment?

Distinct equality cofactors force retained-root growth

Does the exact whole-formula solver retain a separate root for every cofactor obtained by assigning all x variables in a family of independent equalities?

Equality CNFs as an analytic stress family for factored elimination

Test the exact round-6 hash-consed restriction-and-OR solver on disjoint equivalences xi iff yi with all x identifiers preceding all y identifiers. Eliminating xi produces two factored branches over yi; local simplification lacks distributivity, but hash-consing may still share enough structure to defeat the anticipated recurrence.

Does the implemented incoming-edge/min-ID order eliminate all x variables first, and can the resulting reachable-node or work sequence be proved superpolynomial from an exact recurrence?

Factor-local bucket elimination

Can existential elimination touch only factors whose scopes contain the selected variable, preserving independent factors by sharing, and keep a uniform polynomial live-DAG bound on interconnected constraints?

Halve surviving circuit descriptions by each chosen truth-table bit

At each coordinate, partition candidate circuits by their output bit and choose the bit that kills the larger group; after N coordinates fewer than 2^N candidates can be eliminated.

Can the survivor-side counts and output bits be generated by polylogtime-uniform quasipolynomial-size AC0 without enumerating circuits or calling a counting/hardness oracle?

The baseline variable score depends on allocation history

Is the implemented variable score a function of rooted-DAG incoming-edge counts alone?

Baker–Gill–Solovay, separating half: diagonalise against poly-time oracle machines

The oracle `B` with `P^B ≠ NP^B`, in the project's own one-query-per-round oracle machine model. `ProofExplorer/PVsNP/Barriers/BGS.lean`. The diagonalisation is DONE and sorry-free: locality of a run (`run_congr`), the query count (`length_queries`), the counting argument (`exists_fresh`, `exists_poly_lt_two_pow`), the stage construction with the growth condition (`exists_oracle_not_decides`). `separation_of` — the full separation from two explicit model hypotheses — is sorry-free; the unconditional `separation` (the exact statement of `baker_gill_solovay_separation`) consumes four named model-level sorries.

PARTLY ANSWERED. Remaining: `Countable (OracleMachine Bits)` (a Gödel numbering for `Turing.FinTM2`) and three finite `FinTM2`s for the one-query verifier. Nothing else.

A Gödel numbering for Turing.FinTM2

Canonicalise a `Turing.FinTM2` to one with `K = Fin k`, `Λ = Fin l`, `σ = Fin s`, `Γ i = Fin (g i)` and prove the transported machine has the same `eval`; then `Encodable` the program and conclude `Countable {f // IsPolyTime f}`, hence `Countable (OracleMachine Bits)`.

Is there a cheaper route to `Countable {f : Bits → Bits // IsPolyTime f}` than full canonicalisation — e.g. a bridge `FinTM2 → Nat.Partrec.Code` (whose `Encodable` instance Mathlib already has), or a semantic argument through the countable configuration type?

Round-8 stress test of factor-local elimination

On which interconnected CNF family does the round-7 factor-local eliminator's live DAG first stop looking polynomial, and what is the mechanical reason?

Finite chain-rule surrogate controls and measured gap plateaus

Exact measurement of Delta_c = SUM_i K^{t^c}(x_i | y,x_<i) - K^t(x_1..x_ell|y) on the machine class PRG(W,B) for ell = 2,3,4, W = 4..14, N up to 128 bits and c = 1,2, with K^t computed exactly (shortest path over (|out|, acc) states, valid because no instruction deletes output; cross-checked against literal enumeration). Plus a Lean toy machine whose K^t values are decided by the kernel, and two sorry-free machine-independent necessary conditions on any violating family.

The finite toy controls are checked; can the project surrogate first be matched to the fully quantified universal-machine statement of KK before seeking asymptotic violations?

Few-subpowers controls for arity-bounded residual representations

Few-subpowers counts all n-ary invariant relations of a fixed algebraic constraint language and supports a specific compact-representation algorithm. It does not classify all residual representations polynomial in source CNF length.

For a specified fixed Boolean constraint language with a common edge polymorphism, which compact representation and update bounds apply, and how do arity bounds translate to the actual source input and intermediate work?

Every OBDD(and,exists,reordering) elimination algorithm is exponential on binary PHP

The theorem-level negative control for elimination-with-projection solvers whose intermediates are OBDDs. Round 9 landed in Lean, sorry-free, the OBDD subfunction-count bound for every order and cut, Lemma 27's projected function with the identity "not all-distinct", the row-split fooling set (>= (2^l).choose t distinct subfunctions), and the explicit row-major bound 2^(2^l) <= 2^l (size + 2); Theorem 21 and every-order Lemma 27 are stated as named Props (definitions, no sorry).

Can the every-order Lemma 27 (for every injective order on the 2^l * l variables the OBDD of exists X_1 AND_i [X_1 != X_i] has size >= 2^(c 2^l / l)) be proved in Lean from the landed row-split count plus the Hamming-distance-3 code trick of Lemma 25?

Bottom-up str-DNNF compilation has exponential intermediates even for constant-size outputs

de Colnet-Mengel (AAAI 2022) prove that every str-DNNF(and,r) compilation of an unsatisfiable bounded-degree Tseitin formula, with any conjunction order and any dynamic vtree, has an intermediate result of size 2^{Omega(tw(G))} poly(1/n); this framework has no projection rule.

Does adding a projection rule to the str-DNNF(and,r) framework collapse the Tseitin lower bound to O(n) (as round 8 and Lemma 2 of the same paper predict), and is there any bounded-degree CNF family on which the bound survives projection?

DNNF size bounds balanced rectangle covers (Bova-Capelli-Mengel-Slivovsky, Lean)

The one finite combinatorial lemma from which every DNNF lower bound in this scan descends - a DNNF of size s computing f yields a balanced (multi-partition) rectangle cover of f of size at most s, disjoint if the DNNF is deterministic.

Can BCMS Theorem 1 (sat(C,g) is a rectangle over (var(C_g), X minus var(C_g))) and Theorem 6 (balanced cover of size <= |C|) be proved in Lean over an inductive DNNF type, and then de Colnet-Mengel SAT 2021 Lemma 5 (a rectangle inside a satisfiable Tseitin function respects a parity sub-constraint at every split vertex)?

Finite Lean facts behind few subpowers on the Boolean domain

Three finite statements that make closed-residual-class-dichotomy checkable - affine relations have a basis of at most n+1 vectors, bijunctive relations are determined by their binary projections, Horn relations on n variables number at least 2^{binom(n, n/2)}.

Can the three Boolean few-subpowers facts be proved in Lean over Finset (Fin n -> Bool), with kernel checks for n <= 4, and can the affine one be connected to the Tseitin residual theorem (residual of rank <= 1)?

PHP through the round-7 eliminator with Mengel's two-order discipline

Round 9 ran the unchanged round-7 factor-local DAG on PHP_n^{n+1} under its default, hole-major and pigeon-major elimination orders, and a genuine OBDD package as Mengel Algorithm 1 under all four (BDD order, elimination order) pairs, plus Mengel's G-PHP restriction. The OBDD reproduces Mengel exactly (n^2.85 for the mixed pair, >= 2^n for either single order, 2^n on G-PHP); the DAG blows up as 2^(1.5 n) under every elimination order because it has no variable order to set, and is exactly linear on G-PHP.

Does the round-7 factor-local eliminator, run with column-wise elimination order and its residual DAG rooted row-wise, become polynomial on PHP_n up to n = 12, and does it blow up again on Mengel's G-PHP?

Residual rank on F2 linear systems - where affine stops being a diagram

Measured in round 9 (part D of php_two_orders_round9.py) on random 3-XOR-SAT at clause ratios 0.7, 0.918, 1.2, 1.5 and n = 12..40, three seeds each, every answer cross-checked. The expected separation did not appear - the round-7 DAG's peak live size stays between 0.28 and 1.31 times the GF(2) basis size in bits along its own elimination order, growing as n^1.0 to n^1.5 in the measured range, while the rank of the projected system is n - O(1) as it must be.

On random sparse F2 systems (3-XOR-SAT at densities above the rank threshold) does the round-7 eliminator's residual rank grow linearly and its live DAG exponentially, while a basis representation of the same residuals stays O(n^2)?

PPSZ-type k-SAT algorithms have no uniform polynomial mechanism

The 2019-2026 improvements (biased PPSZ, Scheder's analysis, Jiang-Cai 2026) move the base of 3-SAT from 1.30704 to 1.307031578 in the sixth decimal, and Scheder-Talebanfard prove super-strong-ETH-type limits for PPSZ with small resolution width.

Is there any k-SAT algorithm family in the 2023-2026 literature whose analysis does not already come with an explicit 2^{(1-o(1))n} instance family?

SoS / polynomial calculus as a SAT algorithm dies on the round-8 families

Sum-of-squares and Groebner-basis (polynomial calculus) refutation are uniform algorithms whose running time is n^{O(degree)}; the degree is Omega(n) on Tseitin/parity (Grigoriev 2001) and on random k-CNF at constant density (Schoenebeck 2008 for SoS; Ben-Sasson-Impagliazzo 1999 and Alekhnovich-Razborov 2001 for PC).

Is there any algebraic proof system with a polynomial-time search procedure for which degree lower bounds on random 3-CNF at density 4.26 are not known?

Hirahara-Ilango-Williams - compression in circuits of size 2^{4l/5} poly(t)

STOC 2024 / ECCC TR23-171 - for compression by a fixed function f with description length l and time t, Boolean circuits of size 2^{4l/5} poly(t) solve the task, refuting the folklore that MCSP needs exhaustive search when non-uniform circuits are the model.

Does any non-uniform 2^{o(s)}-size MCSP circuit family interact with the Gap-MCSP magnification thresholds (hardness against N^{1+eps}-size circuits, s = 2^{beta n}), or is the gap between 2^{4s/5} and N^{1+eps} so large that magnification is untouched?

Audit of 2024-2026 claimed P = NP algorithms

Deng (arXiv 2405.08051) refuted by Humphreys et al. (2507.09018); Du refuted by 2404.04395; Quigley (2406.08489) unrefereed with no correctness proof; Arthanari (2606.03194) dead by axioms; Vega (TechRxiv 2025) unrefereed. None survives the round-8 harness test.

Does any claimed polynomial-time 3-SAT algorithm from 2024-2026 return the correct answer on the round-8 harness (random 3-CNF n <= 20 with brute-force cross-check, PHP 6->5, Tseitin 3-regular v = 16)?

Direction 2 splits into the magnification threshold and a natural-proofs impossibility

Kabanets-Kolokolova TR25-089 Thm 1.1 makes ¬ChainRule equivalent (given E ⊄ io-SIZE[2^{o(n)}], which is free inside a proof by contradiction from P = NP via Li STOC'24) to Gap_{τ,o(N)}McK^tP ∉ prP. Every slice s of that promise problem is one of two known objects. Sparse slices (s = N^{o(1)}) are 2^{N^{o(1)}}-sparse NP languages, so a Circuit[N^{1+ε}] lower bound for one of them already gives NP ⊄ SIZE[n^k] ∀k by Chen-Jin-Williams FOCS'19 (TR19-118) - the same threshold and the same locality barrier as Gap-MCSP. Dense slices (s = N − o(N)) are, by KK Thm 4.1 + Thm 1.1(⇒), exactly the statement that no P-computable natural property for K^t with usefulness N − o(N) exists - a Razborov-Rudich impossibility, known only under one-way functions.

Is there any slice s(N) of Gap McK^tP, neither N^{o(1)}-sparse nor N − o(N)-dense, on which a worst-case prP lower bound would be neither a magnification-threshold bound nor a natural-proofs impossibility? (Literature answer so far - no; intermediate s reduce to the sparse case by padding the program.)

The sparse K^t slice is a Chen-Jin-Williams language

For t = poly(N) and s(N) = N^{o(1)}, L_{t,s} = {x : K^t(x) ≤ s(|x|)} is in NP (guess ≤ s program bits, run t steps) and has at most 2^{s+1} − 1 strings of each length. Chen-Jin-Williams TR19-118 then says L_{t,s} ∉ Circuit[N^{1+ε}] for some ε > 0 ⇒ NP ⊄ SIZE[n^k] for all k. The count is a sorry-free Lean lemma over the existing KTimeCond definition; the magnification is a stated Prop citing TR19-118.

Prove in Lean that {x : KTimeCond U t x ε ≤ s} has fewer than 2^{s+1} elements, state the CJW magnification for this language with explicit ε, and record that any Circuit[N^{1+ε}] lower bound for it is a direction-1 lower bound with the locality barrier attached.

¬ChainRule restated as the absence of a P-natural property for K^t

KK Def. 2.13 - a natural property for conditional K^t with usefulness s accepts every x with K^t(x|y) ≤ s and rejects at least half of all x. KK Thm 4.1 - E ⊄ io-SIZE[2^{o(n)}] plus a P-computable natural property with usefulness n − n/C ⇒ chain rule with error 6N/C. With Thm 1.1(⇒) this gives, under E ⊄ io-SIZE[2^{o(n)}], ¬CR ⇔ no P-computable natural property for K^t with usefulness n − o(n). The direction 2 target is therefore literally a natural-proofs impossibility.

State NaturalPropertyKt U s in Lean, prove the easy half (Gap McK^tP ∈ prP ⇒ a natural property exists, using the 2^{s+1} count to get the rejection rate), and state KK Thm 4.1 as a named Prop; then run the natural-proofs checklist on ktime-chain and record the answer.

Match time, error, stretch, and machine quantifiers

Audit Section 7 of Kabanets–Kolokolova revision 1 against the current Lean definitions before changing any theorem or trusting an asymptotic violation target.

Audit all three mismatches together: length-dependent minimum time, error-dependent polynomial stretch, and efficient universality. Do not silently redefine an existing theorem merely to fix t0.

A uniform AC⁰[quasipoly] hard-table generator is PH ⊄ SIZE[s] in disguise

The generator asked for by explicit-hard-table-generator (CJSW Thm 1.7(i) refuter against always-accept, s(n) ≥ n^{(log n)^{ω(1)}}, no oracle, no advice) prints on 1^N a table T_N with size(T_N) > s using a polylogtime-uniform AC⁰ circuit of size 2^{n^{O(1)}}, n = log N. Then f_n(i) := T_N[i] is in Σ_dP for a constant d (each gate is an alternation over n^{O(1)}-bit gate names with a poly(n)-time direct-connection language). So generator ⇒ PH ⊄ SIZE[s]; conversely CJSW Thm 1.7(ii) gives PH ⊄ SIZE[s²] ⇒ generator. Up to the square, the direction is equivalent to a single super-polynomial lower bound for PH, a strengthening of Kannan (Σ₂P ⊄ SIZE[n^k], each k).

Write the forward direction (generator ⇒ Σ_dP ⊄ SIZE[s]) as a statement over the existing uniform-AC⁰ model with the exponent d made explicit; is the square in Thm 1.7(ii) removable?

Collapse the Jeřábek-Korten rounds to an absolute O(1)-round Student-Teacher protocol

Carmosino-Grosser TR25-045 Thm 1.7 - an absolute polylog-uniform AC⁰[qpoly] Student-Teacher protocol (one protocol for all b) solving SIZE[n^b]-Avoid with O(1) counterexample-oracle calls CX[φ_WSC] (Teacher returns a (log N)^b-size circuit for the proposed table) for infinitely many b ⇒ P ≠ NP; for each fixed b such a protocol exists (their §5). Ren-Williams TR26-118 Thm 3.1 quantifies the Jeřábek-Korten reduction as O(n + log(T/n)) adaptive NP-query rounds with n-bit witnesses. The open gap for mechanism (2) is exactly - Θ(s log s) adaptive rounds → O(1) rounds with a b-independent exponent.

Tabulate rounds, witness length and size exponent of (a) Kannan's Σ₂ argument, (b) Korten's FP^NP reduction, (c) RW26 Thm 3.1, (d) CG25's per-b protocol, written as Student-Teacher protocols; is there a b-independent Student for the *first* round only (a candidate table that is hard against SIZE[n^b] for all b simultaneously unless the Teacher's counterexample has a special form)?

Tree-like Res(⊕) refutations of PHP_n^m have size at least 2^{n−1}

Itsykson-Sokolov (APAL 171(1), 2020) via the linear Prover-Delayer game; sharp form Gryaznov-Ovcharov-Riazanov, ACM ToCT 2024 (arXiv 2404.08370) - Lemma 2.1 (k coins ⇒ tree-like size ≥ 2^k), Definition of m-extensibility w.r.t. F ⊆ φ, Theorem 3.1 (m-extensible ⇒ size ≥ 2^m), Lemma 3.3 (Garlík - PHP_n^m is (n−1)-extensible w.r.t. the hole axioms, every m), Theorem 3.4 (size ≥ 2^{n−1}). The cheapest genuinely-CNF stair above one of our landed stairs, and PHP is the parity-robust family the dead end parity-robust-proof-hardness asked for.

Define linear clauses over ZMod 2 and tree-like Res(⊕), port ProverDelayer.lean to the linear game (Lemma 2.1), prove Theorem 3.1 from m-extensibility by rank over ZMod 2, prove Lemma 3.3 for PHP with the current PHP encoding, and land Theorem 3.4 with the explicit constant 2^{n−1}.

Res(k) lower bound for the weak pigeonhole principle via the small-restriction switching lemma

Segerlind-Buss-Impagliazzo (FOCS 2002; SICOMP 33(5), 2004) - PHP_n^{2n} requires exponential-size Res(k) refutations for all k ≤ √(log n / log log n); for each constant k there is w > k with random w-CNFs exponentially hard for Res(k); Res(k+1) is exponentially stronger than Res(k). Proof - a switching lemma for restrictions setting a polynomially small fraction of variables, reducing to a resolution width lower bound for the restricted PHP. Atserias-Bonet-Esteban (Inf. & Comp. 176(2), 2002) is the k = 2 case for PHP_n^{cn}.

Is the width half already in WidthSize.lean enough, so that the only new object is the SBI switching lemma (k-DNF → small-depth decision tree under a p-random restriction) with an explicit failure probability?

Dense parity sketches before anti-checker selection

Which genuinely new selector mechanism uses structure beyond a low-dimensional linear sketch while meeting the published gate budget?

Canonical prefix certification can be harder than finding an omitted output

Can a useful Avoid algorithm choose its output without demanding universally short Resolution refutations of arbitrary empty guard prefixes?

Small next-block lists still require witness extraction

Is there an explicit uniform polynomial algorithm listing the exact compatible next blocks, with search and verifier work included, even for zero/one-witness instances?

Padding to a progression requires new promise slack and exponent slack

Can a separately proved nonvacuous stronger source promise supply the NO and exponent slack needed for padding to m=d ceil(n/d)?

Short descriptions do not guarantee balanced fixed-target point exclusions

Which circuit-specific feature could justify balanced exclusions when the target labels are fixed, instead of relying only on description entropy?

Can affine-piece unions compress nonlinear SAT residuals?

For fixed C,c, can every length-L CNF be uniformly represented and constructed as a union of at most C(L+1)^c affine subspaces?

Hybrid affine/bijunctive backdoor depth with a work ledger

Does one algorithm construct sound branch/component decompositions for every arity-at-most-three Boolean CSP, with polynomial component mass, polynomial 2^depth, and polynomial total discovery and internal work in encoded length?

Affine hull plus local projections loses nonlinear information

For a fixed k, is every projected CNF relation exactly determined by its affine hull and its coordinate projections of arity at most k?

Can XOR symmetry quotienting remove SAT search?

For fixed C,c, does every length-L CNF have at most C(L+1)^c satisfying orbits under its complete XOR-translation symmetry group, with polynomial discovery?

Affine Hamming-layer search meets the decoding barrier

Does a single deterministic algorithm decide Hx=s with Hamming weight exactly k, for every encoded binary H,s and 0≤k≤n, within C(N+1)^c steps for fixed C,c and total encoding length N?

P ≠ NP

Status: sorry

Not every language in NP is in P

Complexity classes

Status: proved

P, NP, and polynomial reductions over a frozen machine model

The class P

Status: proved

Languages whose characteristic function is computed by a polynomial-time FinTM2

The class NP

Status: proved

Languages with a polynomial-time verifier and polynomially bounded witnesses

P ⊆ NP

Status: proved

Every language in P is in NP

Polynomial-time reductions

Status: proved

Many-one (Karp) reductions computed by a polynomial-time FinTM2

NP-completeness

Status: open

Cook–Levin and the collapse lemma

Cook–Levin

Status: sorry

SAT is NP-complete

Completeness collapse

Status: proved

An NP-complete language in P implies P = NP

Barriers

Status: open

Proof shapes that cannot settle P vs NP

Relativization

Status: sorry

There are oracles A, B with P^A = NP^A and P^B ≠ NP^B

Natural proofs

Status: sorry

"Natural" circuit lower bounds would break PRGs

Algebrization

Status: sorry

Algebraic oracles still collapse or separate P and NP

Around the conjecture

Status: open

Results that inform the attack without settling it

IP = PSPACE

Status: open

Interactive proofs capture polynomial space

Known circuit lower bounds

Status: open

AC⁰, monotone circuits, and the gap to P/poly

Geometric complexity theory

Status: open

Mulmuley's programme via algebraic geometry and representation theory

Resolution proof complexity

Status: open

The first stair of the proof-complexity staircase, machine-checked

CNF syntax and semantics

Status: proved

Literals, clauses, CNFs, assignments, satisfaction, unsatisfiability

The resolution calculus

Status: proved

Inductive derivations: axioms, weakening, resolution on a variable

Soundness of resolution

Status: proved

A refutation of φ witnesses that φ is unsatisfiable

Completeness, with an explicit size bound

Status: proved

Every unsatisfiable CNF has a refutation with at most 2^|V| axiom leaves

The counting lower-bound engine

Status: proved

Falsifying assignments of a derived clause are covered by those of the axioms used

Width–size bound

Status: proved

If every clause of φ mentions at least w variables, every refutation uses at least 2^w distinct axioms

Explicit hard families

Status: open

The complete CNF and the pigeonhole principle

Exponential lower bound for the complete CNF

Status: proved

Every refutation of the complete unsatisfiable CNF on n variables uses at least 2^n distinct axioms, and 2^n is exactly the least achievable leaf count

Pigeonhole principle — unsatisfiability and a linear bound

Status: proved

PHP_n^{n+1} is unsatisfiable, and every refutation uses at least n+1 distinct axioms

Minimal refutation size, computed

Status: proved

The complete unsatisfiable CNF on two variables has minimal refutation size exactly 4

The classical bounds, stated but open here

Status: sorry

Haken remains; Ben-Sasson–Wigderson as stated in Resolution.lean is false and its corrected form is proved

Straight-line programs and circuits

Status: proved

A circuit on n inputs is a sequence of s gates, gate k reading any of the wires 0..n+k-1, plus a designated output wire; size is the gate count and eval is the Boolean function it computes.

Truth tables and their bitstring encoding

Status: proved

A truth table on n inputs is a function (Fin n → Bool) → Bool; as a string it is the 2ⁿ bits obtained by evaluating along the little-endian bijection between assignments and Fin (2ⁿ).

Circuit complexity

Status: proved

The least number of gates of a circuit computing f.

Counting circuits

Status: proved

There are at most (2(n+s+2))^(2s) straight-line programs of s gates on n inputs, and hence at most (s+1)·(n+s)·(2(n+s+2))^(2s) truth tables of circuit complexity ≤ s.

Every Boolean function has a circuit of size 5·2ⁿ

Status: proved

For every f : (Fin n → Bool) → Bool there is a circuit of size at most 5·2ⁿ computing it; hence circuitComplexity f ≤ 5·2ⁿ.

Multiplexer extension lemma

Status: proved

Any straight-line program can be extended by at most muxBound k further gates so that some new wire computes any prescribed function of the first k inputs, with all previous wire values unchanged.

Shannon's counting lower bound

Status: proved

If (s+1)(n+s)(2(n+s+2))^(2s) < 2^(2ⁿ) then some n-bit function has circuit complexity greater than s. In particular, for n ≥ 6 and any s ≤ 2ⁿ/(8n) some n-bit function has circuit complexity greater than s.

Exact circuit complexity of tiny truth tables

Status: proved

By exhaustive search over the finite space of straight-line programs: x₀ has complexity 0, a constant 1, ¬x₀ 1, x₀∧x₁ 1, x₀∧x₁∧x₂ 2, and x₀⊕x₁ exactly 4.

P ⊆ P/poly

Status: sorry

Every language decidable in deterministic polynomial time has polynomial-size circuits.

MCSP and Gap-MCSP

Status: proved

MCSP is the language of pairs (truth table, budget) whose function has a circuit within the budget; GapMCSP s₁ s₂ is the promise problem accepting tables of complexity ≤ s₁ n and rejecting those of complexity > s₂ n.

The instance encoding is uniquely decodable

Status: proved

A bitstring of the form 1ⁿ0 ‖ truthTableBits f determines both n and f; hence the Gap-MCSP promise is consistent whenever s₁ n ≤ s₂ n.

Gap-MCSP above the magnification threshold

Status: open

For every sufficiently large arity n, with N=ttLen n=n+1+2^n, every circuit on N inputs solving the Gap-MCSP slice has N^11 < size^10. This repaired hypothesis is open.

Time-bounded Kolmogorov complexity and the chain rule

Status: sorry

Direction 2. Kabanets-Kolokolova (ECCC TR25-089, 10 July 2025) characterise the o(N)-error chain rule for conditional K^t as "E not-in io-SIZE[2^{o(n)}] and Gap McK^tP in prP". Combined with Li (STOC 2024) this makes ¬ChainRule => P != NP unconditional. Everything here is stated over an explicit clocked universal machine; no constant is left unquantified.

A universal machine with an operational clock

Status: proved

Runs p y x t: on program p and conditioning string y the machine halts with output x after t transitions. Bundled with output determinism, one_le_time, and named constants for the three capabilities the K^t theory needs: copy (copyOverhead, copyTime), cond_of_plain (condOverhead) and pair (pairOverhead, pairTime, pair_length with a 2*ceilLog2 split marker).

K^t(x | y), budgeted time-bounded Kolmogorov complexity

Status: proved

The infimum of program lengths that print x from y within t transitions, valued in ℕ∞ so that "no program inside the budget" is ⊤ rather than a silent 0. This is the BUDGETED measure of Kabanets-Kolokolova, not Levin's Kt = |p| + ceilLog2 t.

K^t is monotone in the time budget

Status: proved

More time never costs description bits: t ≤ t' implies K^{t'}(x|y) ≤ K^t(x|y).

K^t(x | y) ≤ |x| + c

Status: proved

Once the budget pays for the copy program, the complexity of x is at most its length plus the machine's copy overhead.

Conditioning costs at most a constant

Status: proved

K^t(x | y) ≤ K^t(x) + condOverhead, with no time penalty.

Subadditivity: the easy direction of the chain rule

Status: proved

If K^{t1}(x|z) = n1 and K^{t2}(y | <z,x>) = n2 then K^{t1+t2+pairTime}(x++y | z) ≤ n1 + n2 + 2*ceilLog2(n1+1) + pairOverhead. The logarithmic term is necessary for a plain (non-prefix-free) program format: packing two programs injectively must delimit the split point. This is exactly the ell*O(log t) slack the Kabanets-Kolokolova chain rule grants, at ell = 2.

Legacy chain-rule surrogate; source matching open

Status: proved

Definition with a constant time floor t0, fixed stretch exponent c, explicit logarithmic allowance a, and error e. This is the retained project surrogate, not a verified transcription of the published characterization.

Gap McK^tP as a promise problem

Status: proved

YES: K^t(x | y) ≤ s. NO: K^{tau(t)}(x | y) > s + delta(|x|), with delta = o(n) in TR25-089. Instances are a structure (x, y, s) rather than an encoded bitstring, so the promise is a statement about the measure and not about an encoding.

The gap promise is consistent

Status: proved

Whenever the stretched budget is at least the original one (t ≤ tau t), no instance is both YES and NO.

Kabanets-Kolokolova Theorem 1.1

Status: sorry

The chain rule for conditional K^t with error e ≤ o(N) holds iff E not-in io-SIZE[2^{o(n)}] and Gap_{tau, o(n)} McK^tP in prP.

Unproved forward characterization for the surrogate

Status: sorry

Intended bridge component for the retained project definitions. Specification matching and the missing proof inputs remain open; no unconditional checked consequence is claimed.

Unproved backward characterization for the surrogate

Status: sorry

Intended bridge component for the retained project definitions. Specification matching and the missing proof inputs remain open; no unconditional checked consequence is claimed.

Legacy equivalence assembled from unproved halves

Status: sorry

Intended bridge component for the retained project definitions. Specification matching and the missing proof inputs remain open; no unconditional checked consequence is claimed.

Chain-rule bridge awaiting specification repair

Status: open

Intended bridge component for the retained project definitions. Specification matching and the missing proof inputs remain open; no unconditional checked consequence is claimed.

P = NP implies E ⊄ io-SIZE[2^{o(n)}]

Status: sorry

P = NP => PH = P => S2P = P, and padding gives S2E = E; Li (STOC 2024, arXiv 2310.17762) proves S2E not-in i.o.-SIZE[2^n/n] for all n, advice-free.

P = NP implies Gap McK^tP ∈ prP

Status: sorry

Gap McK^tP is in prNP unconditionally (guess a program of length ≤ s, run it for t steps), so P = NP puts it in prP.

Intended P = NP to chain-rule bridge; unproved

Status: sorry

Intended bridge component for the retained project definitions. Specification matching and the missing proof inputs remain open; no unconditional checked consequence is claimed.

Legacy chain-rule contrapositive; unproved

Status: sorry

Intended bridge component for the retained project definitions. Specification matching and the missing proof inputs remain open; no unconditional checked consequence is claimed.

What NP-hardness of Gap McK^tP actually buys (corrected)

Status: sorry

CORRECTED. Under NP-hardness of Gap McK^tP, P != NP forces Gap McK^tP not-in prP and hence, by Theorem 1.1 forward, the failure of the chain rule. The old skeleton asserted ChainRule -> GapK_NP_hard -> PeqNP, which the sources do not give.

The Pudlák–Impagliazzo Prover–Delayer game

Status: proved

A Delayer strategy scoring p forces every tree-like refutation to have at least 2^p leaves; for PHP_n^{n+1} the Delayer scores n

The game, as an inductive predicate

Status: proved

DelayerScores φ C p — from the state C the Delayer can score at least p points against every Prover

Game ⇒ tree-like size (Pudlák–Impagliazzo)

Status: proved

If the Delayer scores p from the empty state then every tree-like refutation of φ has at least 2^p axiom leaves

Strategies from an invariant, and the score ceiling

Status: proved

A live invariant that survives one round yields a Delayer strategy; and for an unsatisfiable φ the Delayer never scores more than the number of uncommitted variables

Exponential tree-like lower bound for PHP_n^{n+1}

Status: proved

Every tree-like resolution refutation of PHP_n^{n+1} has at least 2^n axiom leaves; this proves TreeLikePHPLowerBound with c = 2

`decide` harness: PHP_1^2

Status: proved

PHP_1^2 is unsatisfiable by `decide`, the game gives leafCount ≥ 2, and an explicit refutation has 3 leaves

The frozen machine model

Status: proved

Mathlib's FinTM2 with TM2ComputableInPolyTime, plus the bitstring encoding layer

Bitstring encodings and CNF

Status: proved

A typeclass of canonical `List Bool` encodings, with self-delimiting blocks, and a CNF datatype whose encoding is derived from it

Polynomial time on FinTM2

Status: proved

A function is poly-time iff Mathlib's `TM2ComputableInPolyTime` is inhabited for it under the canonical encodings

Composition of poly-time machines

Status: proved

The composition of two polynomial-time computable functions is polynomial-time computable

Hardness magnification

Status: open

The sparse oracle circuit and substitution are proved. Hardness implies list-bit circuit noncontainment; the separate anti-checker route gives a conditional P≠NP theorem with every remaining input explicit.

Circuits with oracle gates

Status: proved

A straight-line program over {const, ¬, ∧₂, ∨₂} plus a gate `oracle l q` that reads l earlier wires and returns the oracle's answer on the bitstring of their values; the two resources measured are the number of oracle gates and the largest fan-in. The De Morgan model embeds with the same size and no oracle gates.

Low-complexity truth tables are sparse and short-described

Status: proved

At most 2^{descLength n s} truth tables on n inputs have circuit complexity at most s, where descLength n s = (2s+2)·⌈log₂(2(n+s+2))⌉ = O(s log(n+s)); hence there is an encoding TruthTable n → Bits of that exact length, injective on the truth tables of complexity ≤ s, and the sorted list of yes-instances has at most 2^{descLength n s} entries.

Magnification for a concrete language

Status: proved

The repaired Gap-MCSP threshold at admissible lengths implies that the concrete sorted-list bit-access language ttListLanguage is not in P/poly. Both circuit construction stages are proved; there is no construction hypothesis left.

Both circuit-construction stages are proved

Status: proved

SparseOracleCircuit and OracleSubstitution are proved and combine to establish CompressionSimulation with no remaining circuit-construction hypothesis.

Open transfer from SAT circuits to list-bit circuits

Status: open

Small circuits for SAT imply small circuits for ttListLanguage. This is a substantive unproved implication, not a consequence supplied by Cook–Levin or routine Karp–Lipton reasoning.

Exact deterministic locality barrier

Status: proved

LocalizedThreshold localFanin is false in the repository's precise deterministic oracle-circuit model, by the constructed sparse oracle circuit and its eventual size bound.

Missing-String and the algorithmic method

Status: sorry

Direction 3. Missing-String (Vyas-Williams, ECCC TR24-113): given M strings of length N with M < 2^N, output a string of length N not in the list. Sequentially the problem is easy - the prefix-halving algorithm of Thm 2.5 solves it with 2M bit-probes and 2M+N+1 steps, both proved here - so the entire content of the theory is that UNIFORM DEPTH-TWO circuits for the same problem on S-compressible lists are equivalent to NE ⊄ SIZE(S) (Thm 1.8).

Missing-String as a total function problem

Status: proved

An instance is a list of strings, all of length N, with fewer than 2^N of them; a solution is a string of length N absent from the list. The promise variant drops the cardinality hypothesis, and the decision variant `hasMissing` is a Bool procedure searching all 2^N strings.

Pigeonhole existence of a missing string

Status: proved

A list of fewer than 2^N strings cannot contain every string of length N.

Vyas-Williams Thm 2.5: the prefix-halving algorithm is correct

Status: proved

Emit the LESS FREQUENT first bit of the surviving strings and recurse on the strings that carried it. After N rounds the emitted string is missing from the list, because a string agreeing with the output everywhere would have survived every round.

2M probes and 2M + N + 1 steps, with the constants

Status: proved

Two ℕ-valued cost functions are defined in the same recursion as the algorithm: `probes` counts bit-reads of the input, `steps` adds one unit of bookkeeping per round. The bounds are `probes N L ≤ 2 * L.length` (the 2M-probe half of Thm 2.5) and `steps N L ≤ 2 * L.length + N + 1` (its O(M+N) half, with the constant written out rather than hidden in an O).

Exhaustive check on all lists of at most four strings of length three

Status: proved

On every one of the 1 + 8 + 64 + 512 + 4096 = 4681 lists of at most four strings of length three, the algorithm outputs a string of length three missing from the list, using at most 2M probes and 2M + 4 steps. Checked by `decide +kernel`, so the axiom set is literally [propext].

S-compressible lists, and how many there are

Status: proved

A list is S-compressible at n when every string in it has length 2^n and is the truth table of an n-bit function computable by at most S gates. The reading of a string as a truth table is faithful (round trip, and injective on strings of length 2^n), and a repetition-free S-compressible list has at most (S+1)((n+S)(2(n+S+2))^{2S}) strings - the explicit form of Vyas-Williams' M = 2^{O(S log S)}.

Vyas-Williams Theorem 1.8: NE ⊄ SIZE(S) ⇔ Missing-String circuits on compressible lists

Status: sorry

NE ⊄ SIZE(S) if and only if there are constants c, k and a poly(N)-time uniform family of DEPTH-TWO circuits of size at most 2^{N^k} which, for infinitely many n, outputs a string missing from L for every S(n)-compressible list L of M = 2^{c·S·log₂(S+2)+c} strings of length N = 2^n. Depth-two circuits are the concrete `DepthTwo`/`MSCircuit` DNF types; `InSIZE` is concrete over `BoolCircuit`; `PolyTimeUniform` and `InNE` are the two opaque holes, documented as such.

Thm 1.8, easy direction: the lower bound gives the circuits

Status: sorry

A language of NE without size-S circuits yields, by the algorithmic method, a uniform depth-two family that outputs a missing string on compressible lists.

Thm 1.8, hard direction: the circuits give the lower bound

Status: sorry

A uniform depth-two Missing-String family on S-compressible lists of 2^{O(S log S)} strings diagonalises against SIZE(S) inside NE. This is the direction the whole direction wants, and by missing_string_barrier its proof cannot relativize.

Wilson's oracle: no general-list construction

Status: proved

If a construction of uniform depth-two Missing-String circuits on GENERAL lists would relativize (Vyas-Williams Thm 1.6) and there is an oracle A with NE^A ⊆ SIZE^A(S) (Wilson 1985; VW Thm 1.9), then no such general-list construction exists. Sorry-free; the two hypotheses are named `def`s rather than asserted, since the relativized classes are opaque.

The chain to P ≠ NP, with its missing step named

Status: sorry

From a Missing-String algorithm of the required form to P ≠ NP: (1) the circuits, (2) vw_thm_1_8_backward giving NE ⊄ SIZE(S), (3) THE GAP - the descent from NE to NP, which is not a known implication and is written as a named Prop `NE_not_SIZE_to_NP_not_Ppoly` rather than a sorry, (4) NP_not_Ppoly_implies_P_ne_NP. williams_conversion and williams_to_P_ne_NP take (3) as an explicit hypothesis and contain no sorry of their own.

Restrictions and the size–width relation (Ben-Sasson–Wigderson)

Status: proved

Short resolution proofs are narrow, in both the tree-like and the general (dag-like) form, with explicit constants

Restrictions of CNFs and of derivations

Status: proved

A refutation of φ restricts to a refutation of φ|ₓ₌ᵥ of no larger width, tree-like size or dag-like size; conversely a derivation from φ|ₓ₌ᵥ lifts back at the cost of one unit of width, and replays inside φ for free given the unit clause {satLit x v}

Tree-like size–width, constant-free

Status: proved

If every axiom of φ has width at most w₀ and every refutation of φ has width at least w, then every refutation has at least 2^(w − w₀) axiom leaves

General (dag-like) size–width, with explicit constants

Status: proved

If every axiom of φ has width at most w₀ and every refutation has width at least w₀ + 2j, then every refutation has dag-like size at least exp(j² / (2|V|))

Width lower bound for PHP, and what it is worth

Status: proved

Every resolution refutation of PHP_n^{n+1} has width at least n; this discharges PHPWidthLowerBound with c = 1, and is provably too weak for Haken

What is still missing for Haken's theorem

Status: open

HakenPHPLowerBound now reduces to a width lower bound of n + Ω(n^{3/2}) for PHP_n^{n+1}, and no linear width bound can suffice

Iteration with a polynomial worktape bound

Status: open

Repeated polynomial-time updates require a bound on intermediate strings. Exact growth, invariant preservation, and resource arithmetic are proved; the bounded FinTM2 loop remains open.

First projection is polynomial-time

Status: proved

IsPolyTime (Prod.fst : α × β → α), for the canonical self-delimiting encodings.

Exact growth under repeated doubling

Status: proved

|doubleBits^[k] x| = 2^k * |x|; input-length many rounds therefore produce 2^|x| * |x| bits.

Doubling defeats every polynomial length bound

Status: proved

No polynomial in the original encoded input length bounds the output of input-length many doublings.

Input-length many doublings

Status: proved

|doubleBits^[|x|] x| = 2^|x| * |x|.

Polynomial state invariant

Status: proved

BoundedState step space says every answer-bit update preserves tape length ≤ space.eval |bitEncode input|.

Every intermediate tape stays bounded

Status: proved

Starting with an empty tape, every iterate satisfies the space polynomial, for any state-dependent answer function.

Polynomial total cost from bounded rounds and states

Status: proved

If round i costs at most cost(space(n)), the sum over rounds(n) rounds is at most (rounds * cost.comp space).eval n.

Construct the bounded parameterized FinTM2 loop

Status: sorry

Polynomial-time updates and final output, polynomial rounds, and a polynomial tape invariant imply a polynomial-time run on the fixed false answer stream.

Oracle-machine tapes satisfy their resource invariant

Status: proved

For every oracle, input, and number of rounds, worktape length is at most the machine space polynomial at the original input length.

Empty-oracle inclusion from the bounded loop

Status: sorry

An oracle-machine run with the empty oracle is polynomial-time; consequently RelativizedP ∅ L implies InP L.

Encoding and promise audit for magnification

Status: proved

Absent encoded lengths refute the old threshold. The corrected threshold uses admissible lengths and is equivalent to hardness for an eventually well-formed, nontrivial promise.

Arbitrarily large lengths carry no encoded truth tables

Status: proved

For every B there is N ≥ B with N > 0 and ttLen n ≠ N for every arity n.

Encoded truth-table length is strictly increasing

Status: proved

StrictMono ttLen, where ttLen n = n+1+2^n.

Every circuit solves an absent-length promise slice

Status: proved

If no ttLen n equals N, every BoolCircuit N solves GapMCSP s₁ s₂.

The old all-lengths threshold is false

Status: proved

¬ AllLengthsGapMCSPThreshold.

The raw gap overlaps at arity one

Status: proved

There is a string of length ttLen 1 belonging to both gapMCSP.yes and gapMCSP.no.

The raw promise is not globally well formed

Status: proved

¬ gapMCSP.WellFormed.

No circuit solves the overlapping arity-one slice

Status: proved

For every C on ttLen 1 input bits, ¬ SolvesPromise C gapMCSP.

The gap parameters are eventually ordered

Status: proved

There is n₀ such that n³ ≤ 2^n/(8n) for every n ≥ n₀.

Gap consistency at a fixed encoded arity

Status: proved

s₁ n≤s₂ n ensures disjoint yes/no sets on strings of length ttLen n, independently of other arities.

Large admissible slices are nonempty and consistent

Status: proved

Beyond one arity cutoff, every length ttLen n has a yes-instance and a no-instance, and no string at that length belongs to both.

Yes-instances at each positive arity

Status: proved

For n>0 there exists y of length ttLen n in gapMCSP.yes.

No-instances at each arity at least six

Status: proved

For n≥6 there exists y of length ttLen n in gapMCSP.no.

Discarding the initial arities gives a well-formed promise

Status: proved

There is a cutoff n₀ such that (gapMCSP.fromArity n₀).WellFormed.

Restricting the promise preserves retained slices

Status: proved

At n≥cutoff, SolvesPromise C (P.fromArity cutoff) iff SolvesPromise C P.

Finite arity restriction preserves the repaired threshold

Status: proved

For any cutoff, GapMCSP_above_threshold is equivalent to the same eventual admissible-length lower bound for gapMCSP.fromArity cutoff.

Oracle-gate substitution

Status: proved

An oracle circuit with uniform oracle fan-in k can be simulated by an ordinary circuit at cost g+k per oracle gate, given a g-gate circuit for the oracle at length k.

Compression with both construction stages discharged

Status: proved

CompressionSimulation holds by combining the binary-search oracle circuit and oracle substitution.

Magnification with both construction stages discharged

Status: proved

The corrected encoded-length Gap-MCSP threshold implies that ttListLanguage has no polynomial-size circuits.

Tseitin parity formulas — the finite foundation

Status: proved

An odd total vertex charge makes the graph's Tseitin CNF unsatisfiable, without needing connectedness.

Encode graph parity as CNF

Status: proved

For each vertex, forbid every assignment whose incident edge parity differs from its charge, using existing blockClause syntax.

Every edge is counted twice

Status: proved

The sum of all vertex parities is zero in ZMod 2, for every edge assignment.

CNF satisfaction equals the parity equations

Status: proved

An assignment satisfies the Tseitin CNF exactly when every vertex has its prescribed charge.

Odd-charge formulas have actual resolution refutations

Status: proved

An odd-charge Tseitin CNF has a resolution refutation with at most 2^|E| axiom leaves.

Maximum degree bounds the initial clause width

Status: proved

If graph degree is at most d, every Tseitin axiom has width at most d.

Bounded degree gives a small CNF object

Status: proved

With maximum degree d, the Tseitin CNF contains at most |V| times 2^d distinct clauses.

A width lower bound gives a general-resolution size lower bound

Status: proved

Maximum degree d and refutation width at least d + 2j, with j at least one, imply dagSize at least exp(j^2 / (2|E|)).

Expansion forces Tseitin refutation width

Status: proved

A cut-connected graph with at least two vertices, odd charge, and balanced-cut boundary at least b has no Tseitin resolution refutation of width less than b.

Three-cycle control — one charged vertex is unsatisfiable

Status: proved

The explicit triangle with charge one at vertex zero and zero elsewhere has an unsatisfiable CNF.

Three-cycle control — zero charge is satisfiable

Status: proved

Assigning false to every triangle edge satisfies every zero-charge vertex constraint and its CNF.

A singleton exposes vacuous balanced expansion

Status: proved

Every one-vertex graph satisfies the balanced-cut condition for every boundary threshold, because there is no integer-sized balanced subset.

Concrete equality-side search compression controls

Status: open

Test candidate SAT search compressions on a linear-clause equality family before claiming polynomial size for every formula.

Exact residual states require 2^n possibilities

Status: proved

Any finite encoding and decoder preserving the equality residual for every pair of n-bit blocks has at least 2^n states.

Distinct first blocks have distinct residual functions

Status: proved

The map x ↦ (y ↦ decide (x=y)) is injective.

The equality CNF has exactly the intended semantics

Status: proved

An assignment satisfies equalityCNF n exactly when its two n-bit blocks are equal.

Two clauses enforce one equality bit

Status: proved

The positive and negative implication clauses at a position hold together exactly when the two occurrences are equal.

At most two clauses per equality bit

Status: proved

The equality CNF on two n-bit blocks has at most 2n clauses.

Correctly quantified oracle compression test

Status: proved

Given a separating oracle and an oracle-indexed compression predicate whose instances imply the corresponding relativized collapse, that predicate cannot hold for every oracle.

Sparse oracle circuits refute the exact localized threshold

Status: proved

SparseOracleCircuit implies not LocalizedThreshold localFanin.

Uniform oracle fan-in bounds maximum circuit fan-in

Status: proved

A circuit with uniform oracle fan-in k has maximum oracle fan-in at most k.

Uniform oracle fan-in bounds the wiring maximum

Status: proved

Every prefix of uniform-k wiring has maximum oracle fan-in at most k.

Arbitrary-exponent anti-checker gap containment

Status: proved

For every c≥1 and d≥2, eventually n^3 ≤ 2^(n/d)/(c*n) and 2^(n/d) ≤ 2^n/(8*n), with natural-number floor divisions.

Direct anti-checker route to P versus NP

Status: open

Finite reduction and conditional final implication are proved. The selector construction, uniform-to-nonuniform simulation and lower bound remain inputs.

Labelled sample consistency

Status: proved

SuccinctMCSP on labelled queries is equivalent to existence of a small circuit agreeing on every queried assignment.

Hitting every small circuit means no consistency witness

Status: proved

Hits f s queries ↔ ¬ SuccinctMCSP n s (label f queries).

Small functions satisfy every labelled sample

Status: proved

circuitComplexity f ≤ s supplies a consistency witness for any query list.

Explicit bounded anti-checker selector

Status: proved

Selector carries a truth-table-dependent list, sample-count bound, and hitting guarantee for functions above the high cutoff. It does not assert computational efficiency.

Finite anti-checker reduction correctness

Status: proved

The labelled consistency test accepts low-complexity inputs and rejects high-complexity inputs, given the selector.

An implemented selector test solves Gap-MCSP

Status: proved

An actual circuit whose evaluation matches selected-sample consistency solves the encoded gap slice.

Solvers transfer from narrow to wide gaps

Status: proved

If wideLow≤narrowLow and narrowHigh≤wideHigh at the arity, a narrow-gap solver also solves the wide gap.

Cofinal small solvers refute the eventual threshold

Status: proved

Small enclosed-gap solvers at arbitrarily large arities contradict GapMCSP_above_threshold.

Eventual small solvers refute the threshold

Status: proved

An eventual solver family for an enclosed gap contradicts the existing threshold.

Exact reciprocal-exponent slices suffice

Status: proved

For c≥1,d≥2, small gap solvers at n=d*m with cutoffs 2^m/(c*d*m),2^m refute the threshold.

The remaining selector implementation target

Status: open

SelectorImplementation names a bounded hitting selector and an actual circuit implementing labelled consistency with size^10≤ttLen^11.

The implementation target gives a gap solver

Status: proved

Every SelectorImplementation supplies the actual small gap solver needed by the cofinal contradiction.

Direct conditional P≠NP implication

Status: proved

Uniform-to-nonuniform simulation, the explicit selector construction under NP circuit containment, and GapMCSP_above_threshold imply ¬PeqNP.

Explicit polynomial-time composition machine

Status: proved

TM2ComputableInPolyTime ea eb f and TM2ComputableInPolyTime eb ec g give TM2ComputableInPolyTime ea ec (g ∘ f).

Output length from time and a machine push bound

Status: proved

A run of s steps has output length at most input length + stepBound* s.

Exact sequential simulation and transfer cost

Status: proved

Runs of s₁ and s₂ steps compose in s₂ + (|out₁|+1) + (|out₁|+1) + s₁ steps.

Polynomial-time reductions compose

Status: proved

PolyReducesTo A B → PolyReducesTo B C → PolyReducesTo A C.

P is closed under polynomial-time reductions

Status: proved

PolyReducesTo A B → InP B → InP A.

The sparse binary-search oracle circuit

Status: proved

SparseOracleCircuit holds. At all sufficiently large arities n a circuit of size at most 8·gapQueryLen n·ttLen n solves gapMCSP using ttListOracle, with at most gapQueryLen n·ttLen n oracle gates and exact fan-in gapQueryLen n.

Explicit circuit and resource bounds at one arity

Status: proved

For n≥3 and gapLowParam n≤gapHighParam n, the complete circuit satisfies the original size, oracle-count, exact-fan-in, and promise-correctness bounds.

The input's truth-table segment has the intended numeric code

Status: proved

inputCode on encodeTT f equals ttCode f.

Searching the sorted code list decides membership

Status: proved

For n≥1, T is a low-complexity truth-table code iff entry n (bsIdx n T)=T.

The selected index never equals the finite-width sentinel

Status: proved

bsIdx n T < 2^(descLength n (gapLowParam n)).

Every bounded query fetches the intended entry bit

Status: proved

For j<2^L and i<2^n, ttListOracle (encodeQuery n j i) equals bit i of entry n j.

Five gates per bit for an unsigned comparison

Status: proved

Existing bit wires can be compared with a program extension of exactly 5m+1 ordinary gates.

The comparator computes numeric ordering

Status: proved

bitsLE a b m=true iff bitsVal a m≤bitsVal b m.

One OR gate per bit detects a nonzero entry

Status: proved

Existing bit wires admit a nonzero test using m+1 ordinary gates and no oracle queries.

Fetch an entry from dynamic index wires

Status: proved

m entry bits can be fetched using exactly m new gates and at most m oracle queries, all of exact fan-in gapQueryLen n.

A complete search round costs 7·2^n+3 gates

Status: proved

A round fetches the candidate entry, tests it for nonzero, and compares it with the input code; the output computes bsPred.

Every round fixes exactly the next index bit

Status: proved

After r rounds, the index wires contain exactly the high r bits of bsIdx; all unvisited low bits are zero.

The candidate predicate equals the next target bit

Status: proved

bsPred n T (searchCandidate (bsIdx n T) b) iff bit b of bsIdx n T is true.

All index bits are available after L rounds

Status: proved

L rounds compute all bits of bsIdx with L·(7·2^n+3) new gates and at most L·2^n oracle queries.

The final fetch and equality check costs 11·2^n+3 gates

Status: proved

A final entry fetch and comparisons in both directions decide whether the selected code equals the input code.

Minimum semantic supports exist

Status: proved

Under odd charge, every clause has a minimum-cardinality vertex set whose parity equations entail it.

Every boundary edge occurs in the supported clause

Status: proved

For every minimum semantic support S of clause C, all edges crossing S occur among the variables of C.

Every proper vertex subsystem is satisfiable

Status: proved

On a connected odd-charge graph, every proper subset of the vertex parity equations has a satisfying edge assignment.

Resolution is subadditive for vertex support

Status: proved

The minimum support size of a resolvent is at most the sum of the minimum support sizes of its two premises.

Large concluding support forces a balanced wide clause

Status: proved

Any derivation concluding with support at least one third of all vertices has width at least the balanced-cut expansion bound.

The full finite expansion-to-size pipeline

Status: proved

Degree at most d, balanced-cut boundary at least d + 2j, connectedness, odd charge, at least two vertices, and j at least one imply dagSize at least exp(j^2/(2|E|)).

Three-cycle width regression

Status: proved

Every refutation of the one-charge triangle Tseitin CNF has width at least two.

Complete-five-vertex size regression

Status: proved

Every one-charge complete-five-vertex Tseitin refutation has dagSize at least exp(1/20).

Exact constructive-refuter controls

Status: proved

Direct and list refuters for languages and promise problems have explicit length, promise-membership, and infinitely-often quantifiers.

A correct decider cannot be refuted

Status: proved

If A decides L on every input, no generator refutes A at even one length, hence none refutes it infinitely often.

Direct refuters embed into bounded list refuters

Status: proved

A direct infinitely-often promise refuter becomes a singleton-list refuter with list bound one.

Finite modifications preserve infinitely-often refutation

Status: proved

Changing the challenged algorithm on finitely many lengths, or eventually replacing a generator by the same outputs, preserves infinitely-often promise refutation.

Length-preserving valid encodings transport refuters

Status: proved

A direct refuter for a pulled-back promise maps to a target refuter when the encoding preserves length and the two algorithms agree through it.

Constant candidates have explicit Gap-MCSP errors

Status: proved

A constant-false truth table refutes all-reject at every positive low cutoff, while Shannon counting gives a hard truth table refuting all-accept at every arity at least six.

Gap-MCSP threshold on every arithmetic progression

Status: open

For every d at least two and every M, some m at least M is hard at arity d*m: every circuit solving the fixed Gap-MCSP slice has size^10 greater than ttLen(d*m)^11.

Eventual hardness implies progression-robust hardness

Status: proved

The existing eventual Gap-MCSP threshold implies the threshold on arbitrarily large multiples of every d at least two.

Plain infinitely-often hardness can miss a progression

Status: proved

There is a cofinal predicate on natural numbers that never holds at an arity divisible by two.

Selector bridge from progression-robust hardness

Status: proved

Uniform-to-nonuniform simulation, the explicit reciprocal selector implementation under global NP circuit containment, and progression-robust Gap-MCSP hardness imply P is not NP.

Shared-wiring multioutput anti-checker selectors

Status: proved

SelectorCircuit consists of one wiring on 2^n truth-table inputs, exactly count*n output wires encoding count assignments, and the hard-function hitting guarantee.

Circuit selectors induce extensional selectors

Status: proved

Forgetting the shared wiring yields an AntiChecker.Selector with the exact-length query list and the same hitting guarantee.

Fixed samples cannot hit every hard truth table

Status: proved

If low≥1 and card(realizable n high)<2^(2^n-|S|), some truth table of complexity greater than high is zero on S, so the size-one constant-zero circuit witnesses failure of Hits on S.

Count truth tables vanishing on fixed samples

Status: proved

The number of n-variable truth tables that are zero on S is exactly 2^(2^n-S.card).

Bounded-coordinate query rules cannot be universal

Status: proved

If queries depends only on coordinates R and counting wins after charging R union queries(0), some hard truth table produces the zero-input query list and is not hit by it.

Zero-input stability suffices for the selector obstruction

Status: proved

If every truth table vanishing on R yields the all-zero query list, and counting wins on R union that list, some hard table defeats every printed query.

Observations and samples must cover almost the whole table

Status: proved

For a universally correct query rule stable on the zero-input coordinates R and low≥1, 2^n≤R.card+length(queries(0))+descLength n high.

Observation bound with a supplied sample budget

Status: proved

If the zero-input query list has at most count entries, then 2^n≤R.card+count+descLength n high.

Small shared-wiring circuits have small input support

Status: proved

Every bounded-fan-in multioutput circuit C has a coordinate set R of size at most 2*C.size+outputs such that agreement on R forces agreement of all outputs.

Gate wirings use at most two new inputs per gate

Status: proved

The direct input operands appearing in a wiring of size s form a finset of cardinality at most 2s, and agreement there forces all internal wires to agree.

Direct input outputs cost at most one coordinate each

Status: proved

Input wires directly designated by the output map form a support finset of cardinality at most the number of outputs.

A linear gate bound for arbitrary shared selector circuits

Status: proved

For low≥1, every valid shared selector satisfies 2^n ≤ 2*size + count*n + count + descLength n high.

Rule out zero-gate selectors below the input-coverage budget

Status: proved

If count*n + count + descLength n high < 2^n and low≥1, a valid selector has positive gate size.

Transport circuit input support to the observation bound

Status: proved

A valid selector whose outputs depend on input coordinates R satisfies 2^n ≤ R.card + count + descLength n high when low≥1.

Identical printed bits give identical query lists

Status: proved

Equality of the multioutput evaluations implies equality of selectedQueries.

Valid selector fibers avoid every easy anchor

Status: proved

In a fixed selector-output fiber Q, all truth tables agreeing on Q with any supplied circuit of size at most low are realizable at size high and number at most 2^descLength(n,high).

Full zero certificates coexist with linear circuits

Status: proved

For every N, N-ary OR has an explicit circuit of N+1 gates, yet every set of zero coordinates that forces its zero-input value has cardinality N.

Every OR zero certificate contains every coordinate

Status: proved

If vanishing on R forces N-ary OR to equal its all-zero value, then R is the full coordinate set and has size N.

N-ary OR has an N+1 gate circuit

Status: proved

A constant-false accumulator followed by N OR gates computes allOr with exactly N+1 gates.

Agreement inside a fixed selector fiber forces low enough complexity

Status: proved

For a valid selector and C.size≤low, selectorFiberAgree queries Q C is a subset of realizable n high.

Explicit zero-table refuter for monotone payload algorithms

Status: proved

Every algorithm monotone across valid truth-table payloads that rejects some valid table rejects the explicit all-zero table, a Gap-MCSP yes-instance of circuit complexity at most one.

Both payload literals have explicit easy-YES refuters

Status: proved

For any truth-table payload coordinate and either polarity, the opposite constant truth table is an explicit one-gate yes-instance on which that nonconstant literal rejects.

Refuting always-accept requires a promised no-instance

Status: proved

A promised error against always-accept is exactly membership in the promise's no side; no easy yes-instance can refute it for a well-formed promise.

Fiber anti-cover is equivalent to selector validity

Status: proved

Quantified over every fixed output fiber and every explicitly supplied circuit of size at most low, fiber anti-cover containment in the high-realizable family holds exactly when the selector satisfies Hits on every hard truth table.

Two shared gates implement the full-query selector

Status: proved

One shared two-gate multioutput circuit prints all 2^n assignments independently of the input truth table, and the resulting selector is valid whenever low is at most high.

Additive anchor sensitivity fails for shared circuits

Status: proved

The inequality anchorSensitivity(C,A)≤2*C.size+outputs is false: the zero-gate one-output identity circuit has value 2 over its two anchors but right-hand side 1.

Sum local sensitivity over anchors

Status: proved

anchorSensitivity sums, for each anchor, the input coordinates whose individual flip changes the complete multioutput value.

Deduplicated anchor sensitivity has only a linear ceiling

Status: proved

For arbitrary anchors, the union of locally sensitive input coordinates has cardinality at most both 2*C.size+outputs and the total input count.

The exact direct-selector superlinear target remains open

Status: open

For a basis-matched positive c, choose r≥1 and D≥11 so that for every d≥D there are arbitrarily large positive m where every selector at the specified reciprocal slice satisfies N^(r+1)<size^r.

Correct CJSW threshold and the always-accept bottleneck

Status: open

Theorem 4.3 requires f(N) at least 2^((log log N)^(omega(1))) below o(N/log N), with its specified uniform AC0 resource bounds. Its proof already uses the refuter against always-accept.

One-step elimination for any Boolean function

Status: proved

Replacing a Boolean variable by both possible values and taking OR computes existential elimination.

Every gate position has at least two choices

Status: proved

For every m, 2 ≤ Fintype.card (Gate m).

Resolve P versus NP — either outcome

Status: open

Produce a proof of PeqNP or a proof of ¬PeqNP without sorry dependencies. This is a research objective, not a proof by excluded middle.

P = NP

Status: open

Every language in NP is in P.

Construct and audit a polynomial-time SAT candidate

Status: open

Investigate exact SAT algorithms while accounting for all intermediate operations in encoded input length.

Factored SAT intermediate-work experiment

Status: proved

A deterministic audit compares the factored solver with brute force on bounded CNFs and measures PHP and odd-charge prism Tseitin families, exposing substantial intermediate work despite a constant final result.

Factorized existential-elimination SAT candidate

Status: open

Complete semantic CNF elimination is formally correct, and a runnable hash-consed DAG implementation agrees with an independent oracle on bounded tests; implementation refinement and a polynomial resource bound remain open.

Existential elimination is semantically exact

Status: proved

Shannon branching over false and true equals existential quantification of one Boolean variable.

Hash-consed SAT prototype oracle validation

Status: proved

The Python prototype agrees with independent active-variable brute force on 567 deterministic cases and handles empty, sparse, malformed, and budget-exhaustion cases distinctly.

Constructive pointwise diagonalization against at most N circuits

Status: proved

Given k≤2^n explicitly indexed n-input circuits, diagonalTable constructively produces a truth table differing from candidate i at its own distinct reserved coordinate.

Diagonal candidates receive distinct coordinates

Status: proved

The reserved assignment map from Fin k into n-variable assignments is injective whenever k≤2^n.

Full wiring enumeration has at least 2^s entries

Status: proved

For every n and s, 2^s≤Fintype.card(Wiring n s).

Exhaustive hard-table search exceeds the CJSW generator budget

Status: open

Literal enumeration of all size-f wirings processes at least 2^f syntactic entries, far beyond quasipolynomial size in N at the required super-quasipolynomial f.

Exhaustive small-CNF comparison against a separate bitmask oracle

Status: proved

The prototype agrees with an independently implemented truth-table oracle on all 512 canonical two-variable CNFs and all 3304 canonical three-variable CNFs with at most three clauses.

Repeated semantic elimination is complete

Status: proved

Eliminating every syntactically occurring CNF variable gives an exact fixed-base satisfiability decision; implementation refinement and runtime remain separate open obligations.

Restoring the current coordinate changes nothing

Status: proved

Repeated elimination preserves satisfiability

Status: proved

Repeated elimination has exact outside-coordinate semantics

Status: proved

Full finite elimination decides satisfiability at any base

Status: proved

Full finite elimination preserves satisfiability

Status: proved

CNF repeated elimination preserves satisfiability

Status: proved

CNF evaluation depends only on occurring variables

Status: proved

Clause evaluation depends only on occurring variables

Status: proved

Full CNF elimination decides satisfiability at any base

Status: proved

Retaining all equality cofactors requires exponentially many roots

Status: proved

If a finite node representation stores and correctly evaluates every n-bit singleton predicate, it contains at least 2^n nodes. Retention is an explicit hypothesis, not a result about the Python solver.

Different assignments give different singleton cofactors

Status: proved

The map from an n-bit assignment to its singleton Boolean predicate is injective.

An injection bounds finite cardinalities

Status: proved

An injective function A → B between finite types implies card A ≤ card B.

n Boolean variables have 2^n assignments

Status: proved

Fintype.card (Fin n → Bool) = 2^n.

Disjoint equalities expose whole-DAG branching

Status: open

The exact whole-DAG prototype eliminates every x variable first in bounded runs and retains rapidly growing cofactor branches; semantic distinctness gives a conditional 2^n node lower bound, while an exact source-level proof of order and retention remains open.

Factor-local existential elimination candidate

Status: open

Factors independent of the eliminated variable can be retained unchanged; only the containing bucket needs combination.

Factor-local solver passes independent finite checks

Status: proved

The Python factor-local candidate passes 403 self-tests and 3816 exhaustive small-CNF comparisons; matched all-x-before-y equality inputs show reduced restriction work through 12 pairs, with local-only checks through 32 pairs.

Independent factors ignore coordinate replacement

Status: proved

Existential elimination passes independent factors unchanged

Status: proved

Unioned bucket scope is bounded by summed scopes

Status: proved

Residual bucket scope has the explicit one-step bound

Status: proved

Residual bucket tables obey the exponential scope bound

Status: proved

Greedy grouping compresses candidate coverage but not its computation

Status: open

Choosing at each coordinate the less-populated output class eliminates a constant fraction of surviving circuit descriptions; since their count is 2^o(N), N rounds suffice information-theoretically, but computing the adaptive survivor counts within uniform quasipolynomial AC0 remains open.

Prefix-consistency counting is the unimplemented resource

Status: open

The proposed generator needs uniform constant-factor estimates of the number of size-f circuit descriptions agreeing with each candidate prefix extension, throughout an adaptive N-step construction.

Regression exposes allocation-dependent variable ordering

Status: proved

A finite Python regression shows the same rooted expression AND(OR(x,z),y) selects x or y depending on unreachable allocation history; scores are not pure rooted-DAG indegrees.

BGS separating half: an oracle with P^B ≠ NP^B

Status: sorry

There is an oracle B such that some language is in NP^B but not in P^B. Sorry-free from two named model hypotheses (`BGS.separation_of`); the unconditional form consumes four model-level sorries.

The diagonal oracle defeats every machine of a countable family

Status: proved

For every countable family of poly-time oracle machines there is an oracle B such that no machine of the family decides `diag B`. Sorry-free.

Locality of an oracle run

Status: proved

Two oracles that agree on every string a run queries give the same verdict. Sorry-free.

A polynomial number of queries misses a string

Status: proved

A list of strings shorter than 2^n misses some string of length n; and a machine performing `rounds.eval (3n)` rounds on inputs of length n is eventually below 2^n. Sorry-free.

Every polynomial is eventually below 2^n

Status: proved

For every `q : Polynomial ℕ` and `a ≥ 1`, `q.eval (a * n) < 2 ^ n` for all large `n`. Sorry-free, self-contained (Mathlib has this only as an asymptotic statement over ℝ).

diag B is in NP^B for every oracle B

Status: sorry

The one-query verifier — guess y, ask the oracle about it, accept iff the answer is yes and |y| = |x| — puts `diag B` in `NP^B` for every B. Sorry-free in hypothesis form (`diag_mem_relativizedNP_of`); the three hypotheses are concrete FinTM2 constructions of the same character as the still-open `Model.polyTime_fst`.

Poly-time oracle machines form a countable class

Status: blocked

`Countable (OracleMachine Bits)`. True — each machine is a finite `FinTM2` — but unprovable as stated, because Mathlib's `Turing.FinTM2` lives in `Type 1` with arbitrary finite index types. Needs a Gödel numbering (canonicalisation to `Fin`-indexed machines plus a transport theorem).

P^∅ ⊆ P: the missing lemma is a PARAMETERISED iterate

Status: sorry

Sorry-free reduction of `inP_of_relativizedP_empty` to one model obligation: that `x ↦ m.output (x, (fun c => m.next ((x, c), false))^[rounds |x|] [])` is poly-time. That is NOT `Model.polyTime_iterate`, which iterates a closed `g : Bits → Bits` starting from `x`.

A Tseitin residual implies one boundary parity equation

Status: proved

For every graph G, charge, vertex set W and edge assignment a, if some assignment agreeing with a outside the edges internal to W satisfies every parity equation at a vertex of W, then the sum of the boundary edge values of W equals the total charge of W in ZMod 2.

A Tseitin residual reads only the boundary edges

Status: proved

Assignments agreeing on the boundary edges of W give the same residual value, so the residual is a function of at most the boundary edge variables.

The single-vertex residual is exactly its parity equation

Status: proved

For W a singleton the internal edge set is empty and the boundary is the incident set, so the residual holds exactly when the boundary parity equals the charge.

A connected two-vertex residual is exactly the boundary parity

Status: proved

In the triangle with W the two vertices of one edge, for all four charges and all eight edge assignments the residual holds if and only if the two boundary edge values sum to the charge of W.

Exactness of the residual needs W connected

Status: proved

On the four-vertex path with W the two endpoints, all charges zero and both boundary edges true, the boundary parity equation holds while the residual is false; hence no unconditional converse to the soundness theorem exists.

Round-8 stress measurement of the factor-local solver

Status: proved

A deterministic harness runs the round-7 factor-local solver on Tseitin contradictions (random 3-regular, prism, grid), PHP_n^{n+1} and random 3-CNF at ratios 3.0, 4.26 and 5.5, recording answer, peak live nodes, retained nodes, restriction calls, maximum bucket-union scope width and wall time, with a two-million-node soft budget.

Haken's theorem for PHP, landed sorry-free

Status: proved

Haken's exponential dag-like lower bound for PHP_n^{n+1} is proved sorry-free with the explicit constant c = 201/200: every resolution refutation of PHP_n^{n+1} has at least (201/200)^n distinct clauses. The wide-clause half (every refutation contains a clause whose monotone version mentions at least ⌊(n+1)/3⌋² variables) is in Haken.lean; the restriction/averaging half (PHPFatElimination) is in HakenElimination.lean; hakenPHPLowerBound_of_fatElimination joins them.

Critical assignments of PHP, parametrised by hole-to-pigeon maps

Status: proved

A critical assignment is `critAsg σ (p,j) = (σ j = p)` for `σ : Fin n → Fin (n+1)` sending each hole to its pigeon; `IsCritical i₀ σ` says σ is injective and misses i₀. Then every pigeon other than i₀ occupies a hole (`exists_hole`), `critAsg σ` falsifies the pigeon axiom of i₀ and satisfies every other pigeon axiom and every hole axiom, and evicting the pigeon in hole j in favour of i₀ gives another critical assignment (`isCritical_update`).

The monotone transformation is faithful

Status: proved

For every σ and every clause C, `critAsg σ` satisfies C iff it sets some variable of `monoClause C` to true, where `monoClause` replaces each positive literal x_{i,j} by the variable (i,j) and each negative literal ¬x_{i,j} by all variables (k,j) with k ≠ i

The homeless-pigeon complexity measure and a clause of medium measure

Status: proved

`homeless n C` is the set of pigeons that some critical assignment falsifying C leaves homeless. It is all n+1 pigeons at the empty clause, at most one pigeon at every axiom of PHP, antitone under weakening and subadditive under resolution; hence for every t ≥ 1 and every derivation of a clause of measure ≥ t, some clause of the derivation has measure between t and 2t.

The wide-clause lemma

Status: proved

For n ≥ 2, every resolution refutation of PHP_n^{n+1} contains a clause C with |monoClause C| ≥ ⌊(n+1)/3⌋²; more precisely every clause satisfies |monoClause C| ≥ |homeless C| · (n+1 − |homeless C|)

Fat-clause elimination

Status: proved

For all n r with 2r ≤ n and every refutation π of PHP_n^{n+1} with fewer than (37/36)^r distinct clauses, there is a refutation of PHP_{n−r}^{n−r+1} none of whose clauses C has |monoClause C| ≥ ⌊(n−r+1)/3⌋²

Haken's theorem from the two halves, with c = 201/200

Status: proved

PHPFatElimination implies HakenPHPLowerBound with the explicit constant c = 201/200; both halves are now proved, so `Haken.hakenPHPLowerBound'` is a sorry-free term of `HakenPHPLowerBound`.

The chain sum is at most N + ell*copyOverhead

Status: proved

If the conditional budget t^c pays for the machine's copy program on each part, then sum_i K^{t^c}(x_i | y, x_<i) <= sum_i (|x_i| + copyOverhead) = N + ell*copyOverhead. Proved from ClockedMachine.KTimeCond_le_length and monotonicity of list sums in ℕ∞; no other property of U is used.

A chain-rule violation needs a compressible joint string

Status: proved

If the chain-rule inequality fails at (y, xs, t) - i.e. K^t(x1..x_ell|y) + slack < sum_i K^{t^c}(x_i | y, x_<i) - then K^t(x1..x_ell|y) + slack < N + ell*copyOverhead, where slack is the whole ell*a*log2(t+1) + e(N,t) term. So the joint string of a violating instance is compressible below the literal bound by at least the full slack. Machine-independent.

A gap forces one large conditional complexity (certification cost)

Status: proved

If ell * b < sum_i K^{t^c}(x_i | y, x_<i) then some single part has K^{t^c}(x_i | y, x_<i) > b. Read with b = (D + K^t(joint))/ell: a gap of D forces a conditional lower bound of about (D + K^t)/ell on one part, and a K^t lower bound of v established by search means ruling out all 2^v - 1 shorter programs. Exhaustive certification of a gap therefore costs 2^{(D + K^t)/ell}.

A finite machine whose K^t the kernel computes

Status: proved

A five-instruction prefix-coded machine (0 = EMIT0, 10 = EMIT1, 110 = FLUSH a 3-bit generator block and advance a 2-bit register, 1110bb = SEED, 1111bb = append the j-th conditioning block) with a structural interpreter over List Bool. KT L t x ctx is the honest minimum program length over ALL bitstrings of length <= L, so a decided value some v certifies both a witness of length v and the non-existence of anything shorter. Tabulated facts: KT 6 32 101 [] = 3, KT 6 32 110 [101] = 5, KT 6 32 101110 [] = 6.

Toy chain-rule gap, ell = 2, N = 6: exactly 2 bits

Status: proved

For the ToyKT machine, x1 = 101, x2 = 110 (two consecutive generator blocks), t = t' = 32: K^t(x1) = 3, K^t(x2 | x1) = 5, K^t(x1x2) = 6, so the gap is exactly 3 + 5 - 6 = 2, which is inside the slack ell*ceil(log2(t+1)) = 12.

Toy chain-rule gap, ell = 3, N = 9: exactly 4 bits

Status: proved

Three consecutive generator blocks split into three parts, t = t' = 64: the gap is exactly 4 = 2*(ell-1). The gap grew with ell - one more re-description of the hidden register - and stays inside ell*ceil(log2(t+1)) = 21.

Toy chain-rule gap, ell = 2, N = 12: exactly 5 bits

Status: proved

Four consecutive generator blocks split into two parts of two blocks, t = t' = 200: K^t(part1) = 6, K^t(part2 | part1) = 11, K^t(joint) = 12, gap exactly 5. Doubling N moved the gap from 2 to 5 and it cannot pass the re-seeding cost (ell-1)*6; the slack at this t is ell*ceil(log2(t+1)) = 16.

Transport of derivations along a restriction-with-renaming

Status: proved

For finite W, an injection f : W → V and a decidable predicate T on literals of V with (T1) true literals live outside the range of f and (T2) x and ¬x are never both true: every derivation of C from φ either has C satisfied by T, or transports to a derivation of pullClause f C = {l' | mapLit f l' ∈ C} from transCNF T f φ (the unsatisfied clauses of φ, transported), all of whose clauses are transports of unsatisfied clauses of the original derivation.

The matching restriction of PHP, with its three monotone facts

Status: proved

For every m, pigeon p and hole h: the restriction "p into h" has surviving variables embV p h (i,j) = (p.succAbove i, h.succAbove j) and true literals x_{p,h}, ¬x_{p,j} (j ≠ h), ¬x_{i,h} (i ≠ p). It transports PHP (m+1) into PHP m (`transCNF_PHP_subset`), a clause whose monotone version contains (p,h) is killed (`satBy_of_mem_monoClause`), and the monotone version of a transported clause injects via embV into the monotone version of the original (`card_monoClause_pullClause_le`). Hence every refutation of PHP (m+1) restricts to a refutation of PHP m whose clauses are transports of unkilled clauses (`exists_matching_restriction`).

Averaging over monotone variables and one round of elimination

Status: proved

In any family F of clauses over PHPVar n each of monotone size ≥ Θ, some variable v satisfies |F|·Θ ≤ |{C ∈ F : v ∈ monoClause C}|·|PHPVar n| (`exists_var_mem_many`). Consequently, for every refutation π of PHP (m+1) there is a refutation π' of PHP m with fatMono Θ π'·(m+2)(m+1) + fatMono Θ π·Θ ≤ fatMono Θ π·(m+2)(m+1), where fatMono Θ counts the clauses of monotone size ≥ Θ (`exists_restrict_step`).

The elimination induction

Status: proved

For all Θ ≤ N, all r ≤ m with (m+1)m ≤ N and every refutation π of PHP m: if fatMono Θ π·(1 − Θ/N)^r < 1 then PHP (m − r) has a refutation with no clause of monotone size ≥ Θ.

Round 9 measurement: PHP under two orders, G-PHP, random 3-XOR

Status: open

Finite experiment (scripts/experiments/php_two_orders_round9.py, fixed seeds, brute-force cross-check when at most 20 variables occur, known answer otherwise). On PHP_n^{n+1} the round-7 syntactic DAG grows as 2^(1.5 n) under hole-major and pigeon-major elimination alike (n = 5..10) because it has no variable order to set; a genuine OBDD run as Mengel Algorithm 1 grows as n^2.85 with BDD order hole-major and elimination order pigeon-major (n = 3..12) and stays above 2^n with either single order, exactly as Mengel Theorem 1 and Lemmas 2-3 predict. On Mengel G-PHP the OBDD pair grows as 2^n (above Theorem 5's 2^(n-1) at every n) while the DAG with its default order is exactly linear. On random 3-XOR up to 40 variables the DAG stays within a factor 1.3 of the GF(2) basis size in bits.

Subfunction count is a lower bound on OBDD size, for every order and cut

Status: proved

For every read-once branching program whose tests are strictly increasing in a position map pos, every cut k and every function f it computes, the number of distinct subfunctions of f obtained by fixing the variables with pos < k is at most size + 2.

The projected function of Lemma 27 is the negation of all-distinct

Status: proved

For X a family of 2^l rows of l bits, projNeq X (the function exists y, forall i, y <> X i) is false iff X is injective; for any number of rows it is false iff X is surjective.

Row-split fooling set for Lemma 27's function

Status: proved

For every position map on m x l variables and every cut k such that a set T of rows has all its bits below the cut and every other row all its bits at or above it, and provided 2^l <= m, the number of distinct subfunctions of exists y forall i y <> X_i at the cut is at least (2^l).choose |T|.

Explicit OBDD lower bound for Lemma 27's function in the row-major order

Status: proved

For every l >= 1 and every OBDD in the row-major order on 2^l rows of l bits that computes exists y forall i y <> X_i, 2^(2^l) <= 2^l * (size + 2), i.e. size >= 2^n / n - 2 with n = 2^l.

Kernel checks of the distinguishing witness at l = 2, 3

Status: proved

By decide: at l = 2, any two injective prefixes of two rows with different ranges have a distinguishing suffix of two rows; at l = 3, for any two distinct single prefix rows the explicit complement suffix of seven rows evaluates the projected function to true and false respectively; (2^2).choose 2 = 6 and (2^3).choose 4 = 70.

The binary pigeonhole principle is unsatisfiable

Status: proved

For every l and every assignment to the 2^l + 1 rows of l bits, some clause of BPHP (two pigeons in the same hole) is violated.

Itsykson-Ovcharov Lemma 27, every order (statement only)

Status: open

Named Prop Lemma27AllOrders: there are c > 0 and l_0 such that for every l >= l_0, every injective position map on 2^l * l variables and every OBDD computing exists y forall i y <> X_i, the size is at least 2^(c * 2^l / l). Published (SAT 2024); not proved in this repository; stated as a def of type Prop, never a sorry.

Itsykson-Ovcharov Theorem 21 (statement only): OBDD(and,exists,reordering) is exponential on BPHP

Status: open

Named Prop OBDDEliminationExponentialOnBPHP over an explicit run model: there are c > 0, 0 < eps < 1/4 and l_0 such that for every l >= l_0 and every run (download one clause / project a variable all of whose clauses are downloaded / reorder, each stage holding any OBDD for exists Z and of the downloaded clauses) of any OBDD(and,exists,reordering) algorithm on BPHP_{2^l}^{2^l+1}, some stage holds an OBDD of size at least 2^(c * n^eps / log n), n = 2^l. Published; not proved here; a def, never a sorry.

Bounded synthesis: sketch information and search controls

Status: proved

Elementary checked consequences and precise limits from five September-11 combinations. No P versus NP separation is claimed.

Cardinality of a binary linear kernel

Status: proved

The kernel has 2^finrank elements; a project-owned finite-field counting wrapper.

Linear observations and easy-set cardinality

Status: proved

If ker A lies in an easy set of size at most 2^h, with A mapping N binary coordinates to r+q coordinates, then N <= r+q+h.

Sketch-first anti-checker information bound

Status: proved

For a fixed r-bit linear sketch, q indices selected from that sketch, and a zero-anchor hitting obligation outside at most 2^h easy vectors, N <= r+q+h.

F2 vectors faithfully encode Boolean truth tables

Status: proved

vectorTruthTable is injective; two distinct binary vectors cannot represent the same truth table.

Circuit-complexity specialization of the sketch bound

Status: proved

For a sketch-first zero-anchor selector hitting every truth table above circuit complexity high, 2^n <= r+q+descLength n high.

Marked-prefix emptiness is exactly UNSAT

Status: proved

For C_phi(x)=(phi(x),x), absence of an output with first bit true is equivalent to phi being false on every input.

The marked circuit still has an easy omitted output

Status: proved

For any a, (!phi(a),a) is not in the image of C_phi; arbitrary avoidance can be easier than canonical prefix emptiness.

A complete sound list supplies a witness

Status: proved

A sound complete list for predicate P is nonempty iff P has a witness; this semantic equivalence supplies no efficient list-construction algorithm.

All-coordinate covering count

Status: proved

A finite query set that includes a representative equal to every coordinate has cardinality N.

Singleton disagreement forces every point query

Status: proved

A query set that distinguishes zero from every singleton spike contains all N coordinates; this is a known teaching-dimension control.

Every proper OR projection is full

Status: proved

For every n, coordinate set S, j outside S, and assignment a, an assignment satisfying OR_n agrees with a on S.

OR still rejects zero

Status: proved

The all-false vector does not satisfy OR_n for any n.

OR has no nontrivial XOR translation

Status: proved

Any translation preserving OR_n on every assignment is the zero vector.

OR3 is not affine

Status: proved

The OR3 relation is not closed under ternary XOR.

The affine hull of OR3 is the cube

Status: proved

Every ternary-XOR-closed superset of OR3 contains every three-bit vector.

Affine pieces inside OR3 contain at most four points

Status: proved

Every finite ternary-XOR-closed subset of OR3 has cardinality at most four.

A finite cover pays for every piece

Status: proved

The union of k finite sets of cardinality at most b has cardinality at most k*b.

Branch depth and component mass bound leaf work

Status: proved

For every supplied WorkTree T, charge(T) ≤ mass(T) * 2^depth(T).

Explicit polynomial leaf and overhead ledger

Status: proved

If mass(T) ≤ L^a, 2^depth(T) ≤ L^b, and overhead ≤ L^c, then charge(T)+overhead ≤ L^(a+b)+L^c.

Bounded positive synthesis: five tested combinations

Status: open

Three universal summary hypotheses are refuted; hybrid component/backdoor search has a checked resource ledger; general affine Hamming-layer feasibility remains NP-complete.