diff --git a/Complexity/Computability/Circuit/Monotone/Clique/Asymptotic.lean b/Complexity/Computability/Circuit/Monotone/Clique/Asymptotic.lean index e8ceb0d79..9288f8b63 100644 --- a/Complexity/Computability/Circuit/Monotone/Clique/Asymptotic.lean +++ b/Complexity/Computability/Circuit/Monotone/Clique/Asymptotic.lean @@ -28,7 +28,7 @@ more than `2 ^ (2 ⌊√k⌋)` gates (`two_pow_two_mul_sqrt_lt_size`), hence mor (`two_rpow_sqrt_lt_size`). This is the `2 ^ (ε √k)` bound of Razborov and of Alon and Boppana, in the form of [Arora and Barak, Theorem 14.7][AroraBarak09], with `ε = 1`. -`Monotone/Clique/LogarithmicPetals.lean` gives stronger finite parameter bounds by choosing +[LogarithmicPetals](LogarithmicPetals.html) gives stronger finite parameter bounds by choosing `4 * w * t` petals for dyadic `w = 2 ^ t`: the lower bound becomes `w ^ w` when `k ^ 4 ≤ n`, or remains `64 ^ w` with only `1024 * t ^ 2 * w ^ 4 * k ≤ n` vertices. diff --git a/Complexity/Computability/Complexity/FineGrained.lean b/Complexity/Computability/Complexity/FineGrained.lean index 83e531a86..c12945319 100644 --- a/Complexity/Computability/Complexity/FineGrained.lean +++ b/Complexity/Computability/Complexity/FineGrained.lean @@ -48,6 +48,11 @@ The negation of `ETH` is `Cslib.Complexity.DecidableInSubexpTime`: decidability `2 ^ (δ n)` times a polynomial for every `δ > 0`, by a decider that may depend on `δ` (`Cslib.Complexity.ETH_iff_not_decidableInSubexpTime`). +The companion CountingNativeEndpoint module proves subexponential decidability of k-SAT for each +fixed width using an exact-counting algorithm with polynomial workspace. It derives zero SAT +exponents and the negations of ETH and SETH. The hypotheses remain defined here so their +conditional consequences can still be stated. + ## Main definitions * `Cslib.Complexity.DecidableInTimeO`, `Cslib.Complexity.DecidableInExpTime`, diff --git a/ComplexityTests/Abstracts/SubexponentialSATTests.lean b/ComplexityTests/Abstracts/SubexponentialSATTests.lean new file mode 100644 index 000000000..9eef948f5 --- /dev/null +++ b/ComplexityTests/Abstracts/SubexponentialSATTests.lean @@ -0,0 +1,70 @@ +/- +Copyright (c) 2026 Samuel Schlesinger. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Samuel Schlesinger +-/ + +import ComplexityAbstracts.SubexponentialSATAbstract +import Complexity.Computability.Complexity.FineGrained +import Complexity.Computability.Complexity.FineGrained.CountingScale +import Complexity.Logics.Propositional.CNF.ModelCount + +/-! # Semantic checks for the subexponential SAT abstract + +These checks identify the displayed definitions with the existing library interfaces and exercise +empty cases and repeated or non-dense variable labels. They also exercise the exact counter +theorem. The implementation imports stay outside the abstract's audited statement surface. +-/ + +namespace ComplexityTests.Abstracts.SubexponentialSATTests + +open ComplexityAbstracts.SubexponentialSATAbstract + +example (φ : Formula) (σ : ℕ → Bool) : eval φ σ = Cslib.Logic.PL.CNF.eval σ φ := rfl + +example (φ : Formula) : Satisfiable φ ↔ Cslib.Logic.PL.CNF.Satisfiable φ := Iff.rfl + +example (φ : Formula) : numVars φ = Cslib.Logic.PL.CNF.numVars φ := rfl + +example (φ : Formula) : modelCount φ = Cslib.Logic.PL.CNF.modelCount φ := rfl + +example (k : ℕ) (φ : Formula) : HasWidth k φ ↔ ∀ c ∈ φ, c.length ≤ k := Iff.rfl + +example : encCNF = Cslib.Complexity.encCNF := rfl + +example {α : Type} (A : Set α) (enc : α ↪ List Bool) (T : α → ℝ) : + DecidableInTimeO A enc T ↔ Cslib.Complexity.DecidableInTimeO A enc T := Iff.rfl + +example {α : Type} (A : Set α) (enc : α ↪ List Bool) (μ : α → ℕ) (δ : ℝ) : + DecidableInExpTime A enc μ δ ↔ Cslib.Complexity.DecidableInExpTime A enc μ δ := Iff.rfl + +example (k : ℕ) : KSAT k = Cslib.Complexity.KSAT k := rfl + +example (k : ℕ) : satExponent k = Cslib.Complexity.satExponent k := rfl + +example : ETH ↔ Cslib.Complexity.ETH := Iff.rfl + +example : SETH ↔ Cslib.Complexity.SETH := Iff.rfl + +example (n : ℕ) : + interpolationScale n = Cslib.Complexity.SubexponentialSAT.interpolationScale n := rfl + +-- The empty formula has one satisfying assignment (of no variables); an empty clause has none. +example : modelCount [] = 1 := by decide +example : modelCount [[]] = 0 := by decide + +-- Variables are counted once each, independent of their labels and repetitions. +example : modelCount [[(0, true)]] = 1 := by decide +example : modelCount [[(5, true), (5, true)], [(9, false)]] = 1 := by decide +example : modelCount [[(0, true), (1, true)]] = 3 := by decide +example : modelCount [[(0, true)], [(0, false)]] = 0 := by decide +example : numVars [[(100, true), (100, false)]] = 1 := by decide + +-- One witness counts all these width-`2` inputs exactly. +example : ∃ count : Formula → ℕ, + count [] = 1 ∧ count [[(7, true), (3, false)]] = 3 ∧ + count [[(0, true)], [(0, false)]] = 0 := by + obtain ⟨count, _, _, _, hcount, _⟩ := exact_count 2 + refine ⟨count, ?_, ?_, ?_⟩ <;> rw [hcount _ (by simp [HasWidth])] <;> decide + +end ComplexityTests.Abstracts.SubexponentialSATTests diff --git a/abstracts/ComplexityAbstracts.lean b/abstracts/ComplexityAbstracts.lean index 01d9b7454..465ab0653 100644 --- a/abstracts/ComplexityAbstracts.lean +++ b/abstracts/ComplexityAbstracts.lean @@ -40,6 +40,8 @@ import ComplexityAbstracts.ShamirAbstract import ComplexityAbstracts.ShamirBridge import ComplexityAbstracts.SipserLautemannAbstract import ComplexityAbstracts.SipserLautemannBridge +import ComplexityAbstracts.SubexponentialSATAbstract +import ComplexityAbstracts.SubexponentialSATBridge import ComplexityAbstracts.SubsetSumAbstract import ComplexityAbstracts.SubsetSumBridge import ComplexityAbstracts.TQBFAbstract diff --git a/abstracts/ComplexityAbstracts/SubexponentialSATAbstract.lean b/abstracts/ComplexityAbstracts/SubexponentialSATAbstract.lean new file mode 100644 index 000000000..ee100402a --- /dev/null +++ b/abstracts/ComplexityAbstracts/SubexponentialSATAbstract.lean @@ -0,0 +1,218 @@ +/- +Copyright (c) 2026 OpenAI, Samuel Schlesinger, Anton Kovsharov. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: OpenAI, Samuel Schlesinger, Anton Kovsharov +-/ + +-- upstream: local-only (formal abstract library) + +import ComplexityAbstracts.Check +import ComplexityAbstracts.Encoding +import ComplexityAbstracts.SubexponentialSATBridge +import Complexity.Computability.Machines.Turing.MultiTape.ResourceBounds +import Mathlib.Analysis.SpecialFunctions.Pow.Real +import Mathlib.Analysis.SpecialFunctions.Sqrt +import Mathlib.Data.Fintype.Pi + +/-! # OpenAI: the Exponential Time Hypothesis is false + +The four theorems below are proved through `SubexponentialSATBridge` from the unconditional +native counting endpoint. + +The primary result is one deterministic machine for each fixed clause width that computes the +number of satisfying assignments of every formula of that width. With `n` the number of distinct +variables, its running time is exponential in a constant times +`n (log log (n + 16))² / sqrt (log (n + 16))`, multiplied by a polynomial in the encoded formula +length. Its work space, including a separate charge for the encoded output, is polynomial in that +same length. This is the interpolation-scale route of Sections 3–6 and +Proposition 6.4 of [OpenAI2026ETH], not the sharper Theorem 1.1 / Appendix D bound. + +The definitions here display the existing CNF semantics, encodings and fine-grained classes; +they are not alternative library interfaces. The accompanying regression module checks their +agreement with the canonical definitions. Machinery is existential. The bridge imports the +public unconditional endpoint, whose native counter and consequences prove the displayed +statements without any branch-certificate or exactness hypothesis. + +**What a reader inspects.** Read the definitions below, the displayed `Encoding` foundation, +and the one additional allowed module, `MultiTape.ResourceBounds`. The latter contributes only +the plain native `ComputableInO` resource convention, explained below, over upstream deterministic +machines. No CNF implementation, complexity-class definition or counting construction is +allowlisted. Lean checks the bridge proofs; `#check_abstract` audits the dependency boundary +of the definitions and theorem statements, not their English interpretation. + +## References and credit + +* [OpenAI, *The Exponential Time Hypothesis is False*][OpenAI2026ETH], revised 25 October 2026, + Sections 3–6, Proposition 6.4, pp. 43–44, and Appendices A–B. Source revision: + `openai/math@7ef5c0cc5ca4b0e072b7a050fca09ab24bc6fa3a`. +* [R. Impagliazzo and R. Paturi, *On the complexity of k-SAT*][ImpagliazzoPaturi2001]: the + exponential-time hypotheses and the infimum exponent. + +The native port is the joint work recorded in #1226, including Samuel Schlesinger, +Anton Kovsharov, Erik Demaine and the contributing Codex, Claude and Jetski workers. The native +machine and encoding foundations include Christian Reitwiessner's contributions. +Construction provenance is recorded in +`SubexponentialSATBridge`. +-/ + +namespace ComplexityAbstracts.SubexponentialSATAbstract + +/-! ## Formulas and model counting + +A literal is a variable or its negation. Clauses are disjunctions of literals and formulas are +conjunctions of clauses; repeated literals and clauses are permitted. A width bound counts literal +occurrences, including repetitions. +-/ + +/-- A literal: the variable `var`, positive or negated. It is the pair `(var, positive)`. -/ +abbrev Literal := ℕ × Bool + +/-- The variable of a literal. -/ +abbrev Literal.var (l : Literal) : ℕ := l.1 + +/-- Whether the literal is the variable itself (`true`) or its negation (`false`). -/ +abbrev Literal.positive (l : Literal) : Bool := l.2 + +/-- A clause is a disjunction of literals. -/ +abbrev Clause := List Literal + +/-- A CNF formula is a conjunction of clauses. -/ +abbrev Formula := List Clause + +/-- Evaluate a formula: every clause must contain a literal that is true under `σ`, that is, +whose variable's value matches its polarity. -/ +def eval (φ : Formula) (σ : ℕ → Bool) : Bool := + φ.all fun clause => clause.any fun literal => σ literal.var == literal.positive + +/-- A formula is satisfiable when some total Boolean assignment makes it true. -/ +def Satisfiable (φ : Formula) : Prop := ∃ σ : ℕ → Bool, eval φ σ = true + +/-- Variables in occurrence order, retaining repetitions. -/ +def vars (φ : Formula) : List ℕ := φ.flatten.map Literal.var + +/-- The number of distinct occurring variables, independent of their numeric labels. -/ +def numVars (φ : Formula) : ℕ := (vars φ).toFinset.card + +/-- The number of satisfying assignments of `φ`: assignments of its distinct variables, each +variable counted once, that make `φ` true. -/ +def modelCount (φ : Formula) : ℕ := + (Finset.univ.filter fun σ : (vars φ).toFinset → Bool => + eval φ (fun v => if h : v ∈ (vars φ).toFinset then σ ⟨v, h⟩ else false) = true).card + +/-- Every clause of `φ` has at most `k` literals. -/ +def HasWidth (k : ℕ) (φ : Formula) : Prop := ∀ clause ∈ φ, clause.length ≤ k + +/-! ## Representation details + +The input is the encoded formula `encCNF φ`. Literal indices are binary; large or non-dense +labels are not silently treated as small. A natural output uses canonical binary digits, with zero +encoded by the empty word. The shared foundation spells out all framing and list conventions. +-/ + +/-- Encode each literal as a framed binary index followed by its polarity bit; frame the +literals within clauses and the clauses within the formula. This is the native `encCNF`. -/ +def encCNF : Formula ↪ List Bool := + ComplexityTests.Abstracts.Encoding.encList (ComplexityTests.Abstracts.Encoding.encList + (ComplexityTests.Abstracts.Encoding.encPair ComplexityTests.Abstracts.Encoding.encNat + ComplexityTests.Abstracts.Encoding.encBool)) + +/-! ## Deterministic machine and resource conventions + +The upstream model is a deterministic binary multi-tape Turing machine with finitely many +states and a fixed finite number of work tapes. Each transition performs bounded head moves +and symbol operations. The input tape is read-only, and output is write-only. Time counts +transitions until halting; work space counts visited work-tape cells over every run prefix. +No condition is imposed on bitstrings outside the chosen encoding's image. + +The native predicate `Turing.MultiTapeTM.ComputableInO f encIn encOut T S` means that there +exists a constant `C` and one such machine computing `f` on every encoded input `x` within +`C * (T x + 1)` steps and `C * (S x + 1)` work cells, with the additional bound +`(encOut (f x)).length ≤ C * (S x + 1)`. Thus output is charged even though its tape is not a +work tape. Time and space are independent budgets; a time bound does not supply polynomial +space. This is the library's existing resource predicate, not a unit-cost arithmetic machine. + +For decision problems below, `DecidableInTimeAndSpace` computes the exact Boolean membership +bit and halts on every encoded instance. Its finite machine and all bounds precede the inputs. +-/ + +/-- A decision problem is decidable in time `O(T x)`, with some independent space bound. -/ +def DecidableInTimeO {α : Type} (A : Set α) (enc : α ↪ List Bool) (T : α → ℝ) : Prop := + ∃ c : ℕ, ∃ t s : α → ℕ, (∀ x, (t x : ℝ) ≤ c * T x + c) ∧ + Turing.MultiTapeTM.DecidableInTimeAndSpace A enc t s + +/-- Exponential time in a parameter, with a polynomial factor in the encoded input length. -/ +def DecidableInExpTime {α : Type} (A : Set α) (enc : α ↪ List Bool) + (μ : α → ℕ) (δ : ℝ) : Prop := + ∃ e : ℕ, DecidableInTimeO A enc fun x => 2 ^ (δ * μ x) * ((enc x).length + 1) ^ e + +/-! ## The exponential time hypotheses + +The decision parameter is the number of distinct occurring variables, not the largest label. +The bridge therefore uses the native dense-relabeling correspondence. Zero infimum exponent alone +does not assert a polynomial-time algorithm. +-/ + +/-- `k`-SAT consists of satisfiable formulas whose clauses have at most `k` literals. -/ +def KSAT (k : ℕ) : Set Formula := + {φ | (∀ clause ∈ φ, clause.length ≤ k) ∧ Satisfiable φ} + +/-- The infimum of all nonnegative exponential rates admitting a `k`-SAT decider. -/ +noncomputable def satExponent (k : ℕ) : ℝ := + sInf {δ | 0 ≤ δ ∧ DecidableInExpTime (KSAT k) encCNF numVars δ} + +/-- ETH asserts that some positive exponential rate is unattainable for 3SAT. -/ +def ETH : Prop := + ∃ δ : ℝ, 0 < δ ∧ ¬DecidableInExpTime (KSAT 3) encCNF numVars δ + +/-- SETH asserts that every improvement below rate one fails for some fixed clause width. -/ +def SETH : Prop := + ∀ ε : ℝ, 0 < ε → ∃ k : ℕ, ¬DecidableInExpTime (KSAT k) encCNF numVars (1 - ε) + +/-! ## Exact counting and the exponential time hypotheses + +The primary theorem fixes the counter, constants and native machine for each `k` before every +input. It includes `k = 0, 1`, empty formulas and empty clauses. On formulas with a clause longer +than `k` the output is unspecified; the time and space bounds still hold there. + +The scale uses natural logarithms and a shift by sixteen to cover all natural `n`; this changes +only constants in the asymptotic bound. It is the scale of Proposition 6.4, not the smaller +exponent of Theorem 1.1. The proof relabels the variables densely and runs the native +declared-variable counter. +-/ + +/-- The interpolation-scale exponent, defined at every natural input. -/ +noncomputable def interpolationScale (n : ℕ) : ℝ := + n * Real.log (Real.log ((n : ℝ) + 16)) ^ 2 / Real.sqrt (Real.log ((n : ℝ) + 16)) + +/-- For each fixed width `k`, one machine counts the satisfying assignments of every width-`k` +formula in time `2 ^ (A · n (log log n)² / sqrt(log n)) · poly(L)` and space `poly(L)`, where `n` +is the number of variables and `L` the encoding length. -/ +theorem exact_count (k : ℕ) : + ∃ (count : Formula → ℕ) (A e b : ℕ), + (∀ φ, HasWidth k φ → count φ = modelCount φ) ∧ + Turing.MultiTapeTM.ComputableInO count encCNF ComplexityTests.Abstracts.Encoding.encNat + (fun φ => ⌈(2 : ℝ) ^ (A * interpolationScale (numVars φ))⌉₊ * ((encCNF φ).length + 1) ^ e) + (fun φ => ((encCNF φ).length + 1) ^ b) := + SubexponentialSATBridge.exact_count k + +/-- The exponential time hypothesis is false. -/ +theorem not_eth : ¬ETH := SubexponentialSATBridge.not_eth + +/-- The strong exponential time hypothesis is false. -/ +theorem not_seth : ¬SETH := SubexponentialSATBridge.not_seth + +/-- Every fixed-width SAT exponent is zero. -/ +theorem satExponent_eq_zero : ∀ k, satExponent k = 0 := + SubexponentialSATBridge.satExponent_eq_zero + +end ComplexityAbstracts.SubexponentialSATAbstract + +/-- +info: abstract audit passed for `ComplexityAbstracts.SubexponentialSATAbstract`: +25 root declarations, 139 dependencies checked +-/ +#guard_msgs (whitespace := lax) in +#check_abstract ComplexityAbstracts.SubexponentialSATAbstract allowing [ + ComplexityAbstracts.Encoding, + Complexity.Computability.Machines.Turing.MultiTape.ResourceBounds +] diff --git a/abstracts/ComplexityAbstracts/SubexponentialSATBridge.lean b/abstracts/ComplexityAbstracts/SubexponentialSATBridge.lean new file mode 100644 index 000000000..4d6a9e070 --- /dev/null +++ b/abstracts/ComplexityAbstracts/SubexponentialSATBridge.lean @@ -0,0 +1,72 @@ +/- +Copyright (c) 2026 OpenAI, Samuel Schlesinger, Anton Kovsharov. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: OpenAI, Samuel Schlesinger, Anton Kovsharov +-/ + +-- upstream: local-only (formal abstract library) + +import Complexity.Computability.Complexity.FineGrained.CountingNativeEndpoint +import Complexity.Computability.Complexity.FineGrained.CountingNativeModelCount + +/-! # Bridge for exact subexponential counting and the ETH refutation + +Transfer the unconditional native counting endpoint to the abstract. Its list-of-list CNF +representation, Boolean evaluation, model count, encoding combinators, fine-grained +classes and interpolation scale are definitionally equal to the definitions displayed in +`SubexponentialSATAbstract.lean`. Thus these four transfers require no semantic weakening, +additional hypothesis or alternative machine notion. The abstract does not import the native +definitions into its statement surface, and this bridge does not import the abstract. + +## Construction provenance + +`Cslib.Complexity.CountingNativeEndpoint.exists_declaredCounter` composes uniform disjoint +counting sparsification, the normalized sparse CNF leaf counter and Anton Kovsharov's concrete +bounded-incidence evaluator with its exactness and independent native time/workspace +certificates. Its witnesses are uniform for each width. The external validity guard retains the +original clause width, even though the construction uses `max 2 k` internally. The proof uses +one inner support normalization and one outer declared-variable correction, accounting for +every unused declared variable and all small or zero sizes. +`Cslib.Complexity.CountingNativeEndpoint.exists_modelCounter` restates it on the plain formula by +dense relabeling, with all resource charges referring to `encCNF φ`. + +The native endpoint's dense-relabeling argument supplies the decision consequences for formulas +with arbitrary natural labels and the occurring-variable parameter. Its SAT exponent and +ETH/SETH results are transferred directly here. No branch-certificate or exactness premise +remains in any of the four theorems. + +The argument follows OpenAI's *The Exponential Time Hypothesis is False*, revised 25 October +2026, Sections 3–6, Proposition 6.4 (pp. 43–44), and Appendices A–B [OpenAI2026ETH], pinned to +`openai/math@7ef5c0cc5ca4b0e072b7a050fca09ab24bc6fa3a`. It establishes the interpolation-scale +bound, not the sharper Theorem 1.1 / Appendix D bound. The native port is the joint work recorded +in #1226, including Samuel Schlesinger, Anton Kovsharov, Erik Demaine and the contributing +Codex, Claude and Jetski workers; the machine and encoding foundations include Christian +Reitwiessner's contributions. These transfer proofs reuse that development. +-/ + +namespace ComplexityAbstracts.SubexponentialSATBridge + +open Cslib.Complexity Cslib.Logic.PL Turing.MultiTapeTM + +/-- The bounded-width model counter on the abstract's underlying list representation. -/ +theorem exact_count (k : ℕ) : + ∃ (count : List (List (ℕ × Bool)) → ℕ) (A e b : ℕ), + (∀ φ : List (List (ℕ × Bool)), (∀ clause ∈ φ, clause.length ≤ k) → + count φ = CNF.modelCount φ) ∧ + ComputableInO count encCNF encNat + (fun φ => ⌈(2 : ℝ) ^ ((A : ℝ) * SubexponentialSAT.interpolationScale (CNF.numVars φ))⌉₊ * + ((encCNF φ).length + 1) ^ e) + (fun φ => ((encCNF φ).length + 1) ^ b) := + CountingNativeEndpoint.exists_modelCounter k + +/-- The native counter refutes the library's Exponential Time Hypothesis. -/ +theorem not_eth : ¬ETH := CountingNativeEndpoint.not_ETH + +/-- The native counter refutes the library's Strong Exponential Time Hypothesis. -/ +theorem not_seth : ¬SETH := CountingNativeEndpoint.not_SETH + +/-- Every fixed-width SAT exponent is zero in the native fine-grained classes. -/ +theorem satExponent_eq_zero : ∀ k, satExponent k = 0 := + CountingNativeEndpoint.satExponent_eq_zero + +end ComplexityAbstracts.SubexponentialSATBridge diff --git a/abstracts/README.md b/abstracts/README.md index cb15a97f6..3570835c9 100644 --- a/abstracts/README.md +++ b/abstracts/README.md @@ -1,6 +1,6 @@ # Selected formal abstracts -The catalogue promotes nineteen major result groups. Each has a checked Lean abstract with the +The catalogue promotes twenty major result groups. Each has a checked Lean abstract with the definitions needed to understand its statement, a bridge to the library proof, and an audited dependency boundary. Some abstracts also allowlist a few library modules for foundational models (for example circuit signatures or oracle runs); each such abstract names them in its docstring, and @@ -49,7 +49,8 @@ former paper/TeX index is retired; Git history retains its sources. | [Communication: disjointness and inner product resist randomness](ComplexityAbstracts/CommunicationAbstract.lean) · [PDF](https://www.cslib.io/complexitylib/abstracts/communication.pdf) | Shared randomness, per-input error at most one third and explicit linear bounds; exact deterministic equality records the final-answer convention. | | [Sipser–Gács–Lautemann: BPP lies in the second polynomial level](ComplexityAbstracts/SipserLautemannAbstract.lean) · [PDF](https://www.cslib.io/complexitylib/abstracts/sipser-lautemann.pdf) | Fair random bits, explicit quantifier blocks and total native polynomial-time tests. | | [Chor–Goldreich: the inner product extracts from two weak sources](ComplexityAbstracts/ChorGoldreichAbstract.lean) · [PDF](https://www.cslib.io/complexitylib/abstracts/chor-goldreich.pdf) | Arbitrary sources with real min-entropy bounds, the exact bias bound and its strong form, sharpness at k1 + k2 = n; information-theoretic. | -| [Ilango: Partial MCSP is hard under the Exponential Time Hypothesis](ComplexityAbstracts/PartialMCSPAbstract.lean) · [PDF](https://www.cslib.io/complexitylib/abstracts/partial-mcsp.pdf) | Explicit 3SAT and PartialMCSP encodings (unary and binary thresholds), De Morgan all-gates and binary-gate costs, and deterministic multi-tape lower bounds 2^o(m log m) = N^o(log log N) plus NP membership. *Note (October 2026):* OpenAI's [*The Exponential Time Hypothesis is False*](https://github.com/openai/math/blob/main/lean/docs/378.md) claims, with a Lean formalization, that ETH fails; if so, this conditional result stays valid but is vacuous. A native port is tracked in [#1226](https://github.com/cslib-community/complexitylib/issues/1226). | +| [OpenAI: the Exponential Time Hypothesis is false](ComplexityAbstracts/SubexponentialSATAbstract.lean) · [PDF](https://www.cslib.io/complexitylib/abstracts/subexponential-sat.pdf) | One fixed native machine per width, exact model counts, and interpolation-scale time with polynomial overhead and polynomial space in the encoded formula length; all SAT exponents zero and ETH/SETH false. §§3–6 and Proposition 6.4, not the sharper Theorem 1.1 / Appendix D bound. | +| [Ilango: Partial MCSP is hard under the Exponential Time Hypothesis](ComplexityAbstracts/PartialMCSPAbstract.lean) · [PDF](https://www.cslib.io/complexitylib/abstracts/partial-mcsp.pdf) | Explicit 3SAT and PartialMCSP encodings (unary and binary thresholds), De Morgan all-gates and binary-gate costs, and deterministic multi-tape lower bounds 2^o(m log m) = N^o(log log N) plus NP membership. *Note (October 2026):* the native formalization now [proves ETH false](ComplexityAbstracts/SubexponentialSATAbstract.lean). This conditional entry is retained and its theorem remains valid, but its premise is false. | | [McKay–Murray–Williams: barely superlinear circuit lower bounds for MCSP separate P from NP](ComplexityAbstracts/MagnificationAbstract.lean) · [PDF](https://www.cslib.io/complexitylib/abstracts/magnification.pdf) | Plain De Morgan circuits counting all operation gates, decision MCSP[n^k] on N = 2^n-bit truth tables in standard binary order, and native multi-tape P and NP; conditional magnification from a size lower bound at some arity per exponent. | ## Generate and review PDFs diff --git a/abstracts/catalogue.json b/abstracts/catalogue.json index 8c122db10..7767a945b 100644 --- a/abstracts/catalogue.json +++ b/abstracts/catalogue.json @@ -230,6 +230,22 @@ "summary": "Two independent weak random sources whose min-entropies add up to more than the string length give a nearly fair bit through the inner product modulo two.", "scope": "Arbitrary sources with real min-entropy bounds, the exact bias bound 2^((n - k1 - k2)/2)/2 and its strong form, and sharpness at k1 + k2 = n; information-theoretic, with no running time asserted." }, + { + "id": "subexponential-sat", + "title": "OpenAI: the Exponential Time Hypothesis is false", + "module": "ComplexityAbstracts.SubexponentialSATAbstract", + "headline_theorems": [ + "ComplexityAbstracts.SubexponentialSATAbstract.exact_count", + "ComplexityAbstracts.SubexponentialSATAbstract.not_eth", + "ComplexityAbstracts.SubexponentialSATAbstract.not_seth", + "ComplexityAbstracts.SubexponentialSATAbstract.satExponent_eq_zero" + ], + "summary": "For each fixed clause width, one deterministic native machine exactly counts satisfying assignments in subexponential time and polynomial space. Every fixed-width SAT exponent is zero, and ETH and SETH are false. Native formalization of OpenAI's manuscript, revised 25 October 2026, by the contributors to #1226.", + "scope": "Explicit CNF semantics, model counts over the occurring variables, and binary formula/output encodings; the interpolation-scale exponent n (log log (n + 16))² / sqrt(log(n + 16)) from §§3–6 and Proposition 6.4, where n is the number of variables, with polynomial time overhead and polynomial workspace in the encoded formula length. Includes all fixed widths and sizes; the count is exact on every formula of the given width. This does not establish the sharper Theorem 1.1 / Appendix D bound.", + "foundations": [ + "ComplexityAbstracts.Encoding" + ] + }, { "id": "partial-mcsp", "title": "Ilango: Partial MCSP is hard under the Exponential Time Hypothesis", @@ -244,7 +260,7 @@ "ComplexityAbstracts.PartialMCSPAbstract.partialMCSP_mem_NP", "ComplexityAbstracts.PartialMCSPAbstract.partialMCSP_mem_NP_encBinary" ], - "summary": "Under the Exponential Time Hypothesis, deciding circuit size for partial Boolean functions requires at least quasi-polynomial time in the truth-table size. Note (October 2026): OpenAI's manuscript “The Exponential Time Hypothesis is False” claims, with a Lean formalization, a deterministic subexponential-time algorithm for k-SAT. If it holds, ETH is false and this conditional theorem, while still valid, is vacuous; a native port into complexitylib is in progress.", + "summary": "Under the Exponential Time Hypothesis, deciding circuit size for partial Boolean functions requires at least quasi-polynomial time in the truth-table size. Note (October 2026): the native formalization of OpenAI's manuscript now proves ETH false; see the catalogue entry ‘OpenAI: the Exponential Time Hypothesis is false’. This conditional theorem is retained and remains valid, but its premise is false.", "scope": "Explicit 3SAT and PartialMCSP encodings (both unary and binary size thresholds), De Morgan all-gates and binary-gate cost measures, and deterministic multi-tape subexponential-time lower bounds 2^o(m log m) = N^o(log log N).", "foundations": [ "ComplexityAbstracts.Encoding",