From b6d6e2657d7eb87b0ec43e226bf5332ad9eabbee Mon Sep 17 00:00:00 2001 From: Samuel Giuseppe Schlesinger Date: Tue, 27 Oct 2026 09:29:56 -0400 Subject: [PATCH 01/12] doc(abstracts): draft interpolation-scale SAT counting contracts Prepare #1226 with audited but unproved headline propositions; no bridge or catalogue promotion. Match existing CNF semantics, encodings, fine-grained classes and CountingScale by definitional equality, with concrete declared-input controls. Credit OpenAI and native suppliers in the abstract. Validation: strict narrow abstract/test builds; guard 23 roots / 138 dependencies; 23 renderer and 34 catalogue tests; mk_all, hygiene and changed-file checks; unchanged 19-entry catalogue and rejected Prop-headline control. Catalogue-layout six-page preview passed margin checks and was visually inspected. Full aggregate/CI validation remains separate; no unconditional endpoint claimed. --- .../Abstracts/SubexponentialSATTests.lean | 78 +++++++ abstracts/ComplexityAbstracts.lean | 1 + .../SubexponentialSATAbstract.lean | 218 ++++++++++++++++++ abstracts/drafts/SubexponentialSAT.md | 51 ++++ 4 files changed, 348 insertions(+) create mode 100644 ComplexityTests/Abstracts/SubexponentialSATTests.lean create mode 100644 abstracts/ComplexityAbstracts/SubexponentialSATAbstract.lean create mode 100644 abstracts/drafts/SubexponentialSAT.md diff --git a/ComplexityTests/Abstracts/SubexponentialSATTests.lean b/ComplexityTests/Abstracts/SubexponentialSATTests.lean new file mode 100644 index 000000000..27946e529 --- /dev/null +++ b/ComplexityTests/Abstracts/SubexponentialSATTests.lean @@ -0,0 +1,78 @@ +/- +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.Declared + +/-! # Semantic checks for the pending subexponential SAT abstract + +These checks identify the displayed definitions with the existing library interfaces and exercise +declared unused variables, empty cases and invalid inputs. They prove no counting algorithm or +refutation headline. The implementation imports are confined to this test module, 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) (n : ℕ) : + modelCountOn φ n = Cslib.Logic.PL.CNF.modelCountOn φ (Finset.range n) := rfl + +example (k n : ℕ) (φ : Formula) : + validDeclaredInput k n φ = Cslib.Logic.PL.CNF.validDeclaredInput k n φ := rfl + +example : encCNF = Cslib.Complexity.encCNF := rfl + +example : encInput = Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encUnary + 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 + +-- Empty formulas retain all declared free variables; the empty assignment is counted once. +example : modelCountOn [] 0 = 1 := by decide +example : modelCountOn [] 3 = 8 := by decide + +-- An empty clause is unsatisfiable, while a single positive literal leaves two variables free. +example : modelCountOn [[]] 3 = 0 := by decide +example : modelCountOn [[(0, true)]] 3 = 4 := by decide +example : modelCountOn [[(0, true)], [(0, false)]] 3 = 0 := by decide + +-- Both halves of validity matter, including repetition in the clause-width convention. +example : validDeclaredInput 0 0 [] = true := by decide +example : validDeclaredInput 0 0 [[]] = true := by decide +example : validDeclaredInput 1 1 [[(0, true)]] = true := by decide +example : validDeclaredInput 1 1 [[(0, true), (0, true)]] = false := by decide +example : validDeclaredInput 1 1 [[(1, true)]] = false := by decide + +-- The declared unary header survives even on an empty formula. +example : (encInput (3, [])).length = 7 := by decide +example : numVars [[(100, true), (100, false)]] = 1 := by decide + +end ComplexityTests.Abstracts.SubexponentialSATTests diff --git a/abstracts/ComplexityAbstracts.lean b/abstracts/ComplexityAbstracts.lean index 01d9b7454..43940059b 100644 --- a/abstracts/ComplexityAbstracts.lean +++ b/abstracts/ComplexityAbstracts.lean @@ -40,6 +40,7 @@ import ComplexityAbstracts.ShamirAbstract import ComplexityAbstracts.ShamirBridge import ComplexityAbstracts.SipserLautemannAbstract import ComplexityAbstracts.SipserLautemannBridge +import ComplexityAbstracts.SubexponentialSATAbstract 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..a3d498961 --- /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 draft; endpoint pending) + +import ComplexityAbstracts.Check +import ComplexityAbstracts.Encoding +import Complexity.Computability.Machines.Turing.MultiTape.ResourceBounds +import Mathlib.Analysis.SpecialFunctions.Pow.Real +import Mathlib.Analysis.SpecialFunctions.Sqrt +import Mathlib.Data.Fintype.Pi + +/-! # Draft: exact subexponential counting and the exponential time hypotheses + +**Unproved contracts, not headline theorems.** This draft prepares the formal abstract requested +in #1226. `ExactCounting`, `ETHRefutation`, `SETHRefutation`, and `ZeroSATExponents` below are +propositions describing the intended results; this file supplies no proof of any of them. There +is no bridge yet, and this draft is not selected in the public catalogue. In particular, a passing +`#check_abstract` checks the dependency boundary of these definitions, not their truth. + +The intended primary result is one deterministic machine for each fixed clause width, counting +exactly over the declared variables. Its target running time is exponential in a constant times +`n (log log (n + 16))² / sqrt (log (n + 16))`, multiplied by a polynomial in the original encoded +input length. Its target work space, including a separate charge for the encoded output, is +polynomial in that same external 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, and no private endpoint +preparation is imported. The native endpoint, its proof bridge, and outside source review must +be completed before these contracts can become catalogue theorems. + +**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. Once a bridge exists, Lean will check its proofs against these statements. + +## 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. This draft +does not claim authorship of those implementations. Construction provenance will be recorded in +the bridge when the unconditional endpoint is available. +-/ + +namespace ComplexityAbstracts.SubexponentialSATAbstract + +/-! ## Formulas and declared-variable counting + +A literal `(v, b)` asserts that variable `v` has Boolean value `b`. Clauses are disjunctions +and formulas are conjunctions; repeated literals and clauses are permitted. A width bound +counts literal occurrences, including repetitions. +-/ + +/-- A CNF formula is a list of clauses, each a list of variable/polarity pairs. -/ +abbrev Formula := List (List (ℕ × Bool)) + +/-- Evaluate a formula: every clause must contain a literal of the assigned polarity. -/ +def eval (φ : Formula) (σ : ℕ → Bool) : Bool := + φ.all fun clause => clause.any fun literal => σ literal.1 == literal.2 + +/-- 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 Prod.fst + +/-- The number of distinct occurring variables, independent of their numeric labels. -/ +def numVars (φ : Formula) : ℕ := (vars φ).toFinset.card + +/-- Count satisfying assignments on the declared range `{0, …, n - 1}`, extending by `false` +outside it. Valid inputs below require every occurring variable to lie in that range. -/ +def modelCountOn (φ : Formula) (n : ℕ) : ℕ := + (Finset.univ.filter fun σ : (Finset.range n) → Bool => + eval φ (fun v => if h : v ∈ Finset.range n then σ ⟨v, h⟩ else false) = true).card + +/-- The input has clauses of width at most `k`, with every variable strictly below `n`. -/ +def validDeclaredInput (k n : ℕ) (φ : Formula) : Bool := + (φ.all fun clause => decide (clause.length ≤ k)) && + ((vars φ).all fun v => decide (v < n)) + +/-- A declared counting instance consists of its variable count and formula. -/ +abbrev Input := ℕ × Formula + +/-! ## Representation details + +The external input is `encPair encUnary encCNF (n, φ)`. Its length is +`2 * n + 1 + (encCNF φ).length`, so even an empty formula retains the cost of its declared +variables. 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)) + +/-- Frame the unary declared-variable count, then append the encoded formula. -/ +def encInput : Input ↪ List Bool := + ComplexityTests.Abstracts.Encoding.encPair ComplexityTests.Abstracts.Encoding.encUnary encCNF + +/-! ## 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 declared count +or the largest label. The intended bridge must therefore use 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 - ε) + +/-! ## Intended headline contracts — proofs pending + +All declarations in this section are definitions of propositions, not theorems. The primary +contract fixes the counter, time and space functions, constants and native machine for each `k` +before every input. It includes `k = 0, 1`, `n = 0`, empty formulas and empty clauses. Invalid +width or variable-range inputs return zero. In particular, a valid empty formula returns `2^n`, +including one assignment when `n = 0`; unused declared variables remain free choices. + +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 future proof uses width `max 2 k` internally while retaining the +original width guard, one inner support normalization and one outer declared-variable correction. +Those proof details do not weaken the total external contract. +-/ + +/-- 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)) + +/-- Pending primary claim: one exact native counter per fixed width, with interpolation-scale +time and polynomial space in the length of the original declared input. -/ +def ExactCounting : Prop := + ∀ k : ℕ, ∃ (count : Input → ℕ) (T S : Input → ℕ) (A c e a b : ℕ), + Turing.MultiTapeTM.ComputableInO count encInput + ComplexityTests.Abstracts.Encoding.encNat T S ∧ + (∀ x, count x = if validDeclaredInput k x.1 x.2 then modelCountOn x.2 x.1 else 0) ∧ + (∀ x, (T x : ℝ) ≤ c * ((2 : ℝ) ^ ((A : ℝ) * interpolationScale x.1) * + (((encInput x).length : ℝ) + 1) ^ e) + c) ∧ + (∀ x, S x ≤ a * ((encInput x).length + 1) ^ b) + +/-- Pending headline: the exponential time hypothesis is false. -/ +def ETHRefutation : Prop := ¬ETH + +/-- Pending headline: the strong exponential time hypothesis is false. -/ +def SETHRefutation : Prop := ¬SETH + +/-- Pending headline: every fixed-width SAT exponent is zero. -/ +def ZeroSATExponents : Prop := ∀ k, satExponent k = 0 + +end ComplexityAbstracts.SubexponentialSATAbstract + +/-- +info: abstract audit passed for `ComplexityAbstracts.SubexponentialSATAbstract`: +23 root declarations, 138 dependencies checked +-/ +#guard_msgs (whitespace := lax) in +#check_abstract ComplexityAbstracts.SubexponentialSATAbstract allowing [ + ComplexityAbstracts.Encoding, + Complexity.Computability.Machines.Turing.MultiTape.ResourceBounds +] diff --git a/abstracts/drafts/SubexponentialSAT.md b/abstracts/drafts/SubexponentialSAT.md new file mode 100644 index 000000000..7ef1e7f5e --- /dev/null +++ b/abstracts/drafts/SubexponentialSAT.md @@ -0,0 +1,51 @@ +# Pending catalogue proposal: subexponential SAT + +This is staging material for [#1226](https://github.com/cslib-community/complexitylib/issues/1226), +not an entry in the selected catalogue. Samuel decides the final title. The +[draft abstract](../ComplexityAbstracts/SubexponentialSATAbstract.lean) defines the intended +contracts as propositions; it does not prove them. Its audit verifies only their dependency +boundary. No PDF for these claims is published. + +The proposed entry below is for use **after** the unconditional native endpoint and bridge are +checked and independently reviewed. The proposed theorem names are deliberately absent today; +the catalogue validator must reject selecting the draft propositions as headline theorems. + +```json +{ + "id": "subexponential-sat", + "title": "OpenAI: exact subexponential counting and the failure of ETH", + "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, declared-variable counts, unary declared size 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, with polynomial time overhead and polynomial workspace charged to the original external input length. Includes all fixed widths and sizes, and rejects invalid declared inputs. This does not establish the sharper Theorem 1.1 / Appendix D bound.", + "foundations": ["ComplexityAbstracts.Encoding"] +} +``` + +Proposed README selection row, also pending the endpoint and Samuel's wording decision: + +| Result | Model and scope | +| --- | --- | +| [OpenAI: exact subexponential counting and the failure of ETH](../ComplexityAbstracts/SubexponentialSATAbstract.lean) | One fixed native machine per width, exact declared-variable counts, and interpolation-scale time with polynomial overhead and polynomial space in the original external encoded input length; all SAT exponents zero and ETH/SETH false. §§3–6 and Proposition 6.4, not the sharper Theorem 1.1 / Appendix D bound. | + +Before promotion, discharge the four concrete branch obligations recorded in #1226: the native +branch certificate, feasible-branch exactness, global polynomial branch space, and the branch +polylogarithmic time bound. Then prove the unconditional native endpoint, add the bridge with +construction provenance, and replace the four pending proposition definitions by the four +proved theorem statements, displaying the full exact-count telescope. Recheck the guard and +native-definition correspondence tests, add the entry to `catalogue.json`, move the row into +the README selection (adjusting its relative link), and build and inspect the generated PDFs. +Delete this staging file in that same promotion. Only then can the #1227 note change from +“claimed” to “proved in this library”, linking the new abstract; whether the conditional entry +remains is Samuel's decision. + +Source: OpenAI, *The Exponential Time Hypothesis is False*, revised 25 October 2026, +[Proposition 6.4, pp. 43–44](https://github.com/openai/math/blob/7ef5c0cc5ca4b0e072b7a050fca09ab24bc6fa3a/preprints/The-Exponential-Time-Hypothesis-is-False-October-25-2026/paper.pdf). +The draft uses the accepted native join's original-input accounting and declared-range semantics, +including small sizes and width lifting. It does not import the private join or introduce a +conditional replacement headline. From edbcc9c192b0a4c13b1b62cc4e89c87387e805d9 Mon Sep 17 00:00:00 2001 From: Samuel Giuseppe Schlesinger Date: Tue, 27 Oct 2026 10:52:22 -0400 Subject: [PATCH 02/12] doc(abstracts): apply the selected ETH headline title MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Apply Samuel’s wording from #587 comment 6445129935 to the draft heading and staged catalogue/README title. All Lean declarations and the endpoint/promotion holds are unchanged. --- .../ComplexityAbstracts/SubexponentialSATAbstract.lean | 2 +- abstracts/drafts/SubexponentialSAT.md | 9 +++++---- 2 files changed, 6 insertions(+), 5 deletions(-) diff --git a/abstracts/ComplexityAbstracts/SubexponentialSATAbstract.lean b/abstracts/ComplexityAbstracts/SubexponentialSATAbstract.lean index a3d498961..753019a4a 100644 --- a/abstracts/ComplexityAbstracts/SubexponentialSATAbstract.lean +++ b/abstracts/ComplexityAbstracts/SubexponentialSATAbstract.lean @@ -13,7 +13,7 @@ import Mathlib.Analysis.SpecialFunctions.Pow.Real import Mathlib.Analysis.SpecialFunctions.Sqrt import Mathlib.Data.Fintype.Pi -/-! # Draft: exact subexponential counting and the exponential time hypotheses +/-! # Draft: OpenAI: the Exponential Time Hypothesis is false **Unproved contracts, not headline theorems.** This draft prepares the formal abstract requested in #1226. `ExactCounting`, `ETHRefutation`, `SETHRefutation`, and `ZeroSATExponents` below are diff --git a/abstracts/drafts/SubexponentialSAT.md b/abstracts/drafts/SubexponentialSAT.md index 7ef1e7f5e..851676f3b 100644 --- a/abstracts/drafts/SubexponentialSAT.md +++ b/abstracts/drafts/SubexponentialSAT.md @@ -1,7 +1,8 @@ # Pending catalogue proposal: subexponential SAT This is staging material for [#1226](https://github.com/cslib-community/complexitylib/issues/1226), -not an entry in the selected catalogue. Samuel decides the final title. The +not an entry in the selected catalogue. Samuel selected the title below in +[#587](https://github.com/cslib-community/complexitylib/issues/587#issuecomment-6445129935). The [draft abstract](../ComplexityAbstracts/SubexponentialSATAbstract.lean) defines the intended contracts as propositions; it does not prove them. Its audit verifies only their dependency boundary. No PDF for these claims is published. @@ -13,7 +14,7 @@ the catalogue validator must reject selecting the draft propositions as headline ```json { "id": "subexponential-sat", - "title": "OpenAI: exact subexponential counting and the failure of ETH", + "title": "OpenAI: the Exponential Time Hypothesis is false", "module": "ComplexityAbstracts.SubexponentialSATAbstract", "headline_theorems": [ "ComplexityAbstracts.SubexponentialSATAbstract.exact_count", @@ -27,11 +28,11 @@ the catalogue validator must reject selecting the draft propositions as headline } ``` -Proposed README selection row, also pending the endpoint and Samuel's wording decision: +Proposed README selection row, pending the endpoint: | Result | Model and scope | | --- | --- | -| [OpenAI: exact subexponential counting and the failure of ETH](../ComplexityAbstracts/SubexponentialSATAbstract.lean) | One fixed native machine per width, exact declared-variable counts, and interpolation-scale time with polynomial overhead and polynomial space in the original external encoded input length; all SAT exponents zero and ETH/SETH false. §§3–6 and Proposition 6.4, not the sharper Theorem 1.1 / Appendix D bound. | +| [OpenAI: the Exponential Time Hypothesis is false](../ComplexityAbstracts/SubexponentialSATAbstract.lean) | One fixed native machine per width, exact declared-variable counts, and interpolation-scale time with polynomial overhead and polynomial space in the original external encoded input length; all SAT exponents zero and ETH/SETH false. §§3–6 and Proposition 6.4, not the sharper Theorem 1.1 / Appendix D bound. | Before promotion, discharge the four concrete branch obligations recorded in #1226: the native branch certificate, feasible-branch exactness, global polynomial branch space, and the branch From adf1ff040ce7ac9da20b4425965341db196ad113 Mon Sep 17 00:00:00 2001 From: Samuel Giuseppe Schlesinger Date: Tue, 27 Oct 2026 11:54:23 -0400 Subject: [PATCH 03/12] feat(FineGrained): integrate the native counting endpoint on main Integrate only the approved endpoint payload from ec16665a461d6c0664b158b42ba75190bb4926e6 onto verified actual main 1a87faeffa9d21feaa806193cdd569ccbd00862b (#1342 squash), which already contains the actual #1340/#1341/#1343 suppliers. Preserve all main and supplier files. The complete CountingNativeEndpoint source is byte- identical to the approved checkpoint; only its aggregate import and narrow #1226 ROADMAP paragraph are reconciled with actual main. The unconditional declared-count telescope and all five public exports retain their exact meaning, fixed witnesses, all-input scope, original external encoding charge, and independent time/polynomial workspace. The interpolation-scale bound remains Sections 3-6 and Appendices A-B, not the sharper Appendix D runtime. No new test mirrors the statements. Existing outside source approval: https://github.com/cslib-community/complexitylib/issues/1226#issuecomment-6446105238 Validation: fetch confirmed origin/main = 1a87faeff; cache ensure ran. Strict narrow actual-main consumer check passed in 5.05 seconds with -DautoImplicit=false -DwarningAsError=true and normal budgets. Endpoint source comparison to ec16665a4 is empty, as are comparisons of the four new concrete supplier modules. Staged whitespace checks passed. No supplier dependency rebuild or broad duplicate local campaign was run; final hosted gates and bounded integration-delta review remain required. Preserve Anton Kovsharov's supplier credit and OpenAI/Samuel endpoint credit. AI-assisted mechanical integration by OpenAI Codex for coordinator-codex-01a16ab8 under #1226. All frozen checkpoints remain untouched. The formal abstract bridge/catalogue promotion is separate in #1338; this change does not edit abstract statements or catalogue. --- Complexity.lean | 1 + .../FineGrained/CountingNativeEndpoint.lean | 746 ++++++++++++++++++ ROADMAP.md | 13 +- 3 files changed, 755 insertions(+), 5 deletions(-) create mode 100644 Complexity/Computability/Complexity/FineGrained/CountingNativeEndpoint.lean diff --git a/Complexity.lean b/Complexity.lean index d3e65470d..6596901c0 100644 --- a/Complexity.lean +++ b/Complexity.lean @@ -763,6 +763,7 @@ public import Complexity.Computability.Complexity.FineGrained public import Complexity.Computability.Complexity.FineGrained.Assignment public import Complexity.Computability.Complexity.FineGrained.BruteForce public import Complexity.Computability.Complexity.FineGrained.CountingEndpoint +public import Complexity.Computability.Complexity.FineGrained.CountingNativeEndpoint public import Complexity.Computability.Complexity.FineGrained.CountingParameterBounds public import Complexity.Computability.Complexity.FineGrained.CountingScale public import Complexity.Computability.Complexity.FineGrained.CountingSparsification diff --git a/Complexity/Computability/Complexity/FineGrained/CountingNativeEndpoint.lean b/Complexity/Computability/Complexity/FineGrained/CountingNativeEndpoint.lean new file mode 100644 index 000000000..77215c30f --- /dev/null +++ b/Complexity/Computability/Complexity/FineGrained/CountingNativeEndpoint.lean @@ -0,0 +1,746 @@ +/- +Copyright (c) 2026 OpenAI, Samuel Schlesinger. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: OpenAI, Samuel Schlesinger +-/ + +module +-- upstream: candidate + +public import Complexity.Init +import Complexity.Computability.Complexity.FineGrained.CountingSparsificationUniform +import Complexity.Computability.Complexity.FineGrained.CountingParameterBounds +import Complexity.Computability.PolyTime.FineGrained.ParameterCheck +import Complexity.Logics.Propositional.ClauseSet.Sparsification.CountingParametersPolyTime +import Complexity.Computability.Machines.Turing.MultiTape.Universal.Complexity +public import Complexity.Computability.Machines.Turing.MultiTape.Complexity.BigO.Plain +import Complexity.Computability.Machines.Turing.MultiTape.Complexity.PolyTime.Nat +import Complexity.Computability.Complexity.Problems.SAT.PolyTime +import Complexity.Computability.PolyTime.CNF.BranchedSparseCNFCounter +import Complexity.Computability.Complexity.FineGrained.SparseCountingScale +public import Complexity.Computability.Complexity.FineGrained.CountingEndpoint +import Complexity.Computability.Complexity.FineGrained.CountingSparsification +import Complexity.Computability.Machines.Turing.MultiTape.Complexity.PolyTime.Basic +import Complexity.Computability.PolyTime.BooleanAnalysis.BoundedIncidenceCounter +import Complexity.Computability.PolyTime.BooleanAnalysis.BoundedIncidenceExactness +public import Complexity.Logics.Propositional.CNF.ModelCount.Declared + +/-! +# Native declared-variable counting and the ETH/SETH consequences + +For every fixed clause-width bound `k`, this module constructs one native counter on the full +external input `(N, φ)`, encoded by `encPair encUnary encCNF`. It returns the number of satisfying +assignments on `Finset.range N` when `validDeclaredInput k N φ` holds, and zero otherwise. +The contract covers every input, including small and zero declared sizes. + +Time is bounded by `c * (2 ^ (A * interpolationScale N) * (L + 1) ^ e) + c`, and independent +workspace by `a * (L + 1) ^ b`, where `L` is the original external encoded input length. The +counter, both natural-valued resource functions, and all natural constants are fixed before the +input is supplied. No leaf, branch, schedule, certificate, or semantic hypothesis remains. + +The proof combines uniform counting sparsification with Anton Kovsharov's concrete bounded- +incidence branch evaluator, its native resource certificates and exactness theorem, and the +normalized sparse leaf interface. The selected validity guard avoids charging invalid-support +inputs for their occurring-support search clock. The downstream bridge charges dense relabeling +in the original CNF encoding and derives subexponential-time `k`-SAT, zero SAT exponents, `¬ETH`, +and `¬SETH`. + +The quantitative bound is the interpolation-scale conclusion of Sections 3–6 and Appendices A–B +of [OpenAI2026ETH]. It does not assert the sharper Appendix D runtime from Theorem 1.1. + +## Main results + +* `CountingNativeEndpoint.exists_declaredCounter`: exact guarded declared counting with fixed + native witnesses and independent time and polynomial workspace on every input. +* `CountingNativeEndpoint.decidableInSubexpTime_KSAT`: subexponential-time `k`-SAT for every `k`. +* `CountingNativeEndpoint.satExponent_eq_zero`, `CountingNativeEndpoint.not_ETH`, and + `CountingNativeEndpoint.not_SETH`: the fine-grained complexity consequences. + +## References + +* [OpenAI, *The Exponential Time Hypothesis is False*][OpenAI2026ETH], Sections 3–6 and + Appendices A–B, through the imported counting and leaf interfaces. +-/ + +/-! ## Parameters, original input charges, and selected guard -/ + +namespace Cslib.Complexity.CountingNativeEndpointPrep + +open Cslib.Logic.PL Cslib.Logic.PL.CNF.Sparsification +open Cslib.Logic.PL.CNF (validDeclaredInput validDeclaredInput_eq_true_iff) +open Cslib.Logic.PL.ClauseSet.Sparsification Turing.MultiTapeTM +open Turing.MultiTapeTM.Universal (encUnit encUnit_apply) +open CountingSparsify SubexponentialSAT SubexponentialSAT.ReplacementParams +open SubexponentialSAT.SparseCountingScale Filter + +private abbrev Input := ℕ × CNF ℕ +private abbrev Context := Unit × ℕ +private abbrev FullInput := Unit × ℕ × CNF ℕ +private abbrev encInput := encPair encUnary encCNF +private abbrev encContext := encPair encUnit encUnary +private abbrev encFullInput := encPair encUnit encInput + +private def inputSize (x : Input) : ℕ := (encInput x).length +private def width (k : ℕ) : ℕ := max 2 k +private def divisor (p : Context) : ℕ := BranchedSparseCNFCounter.leafSearchDivisor p.2 +private def thresholdBase (k : ℕ) (p : Context) : ℕ := BranchedSparseCNFCounter.leafThresholdBase k p.2 +private def depthCoeff (k : ℕ) (p : Context) : ℕ := countingDepthCoeff (width k) (thresholdBase k p) +private def prepare (x : Input) : FullInput := ((), x) + +private theorem two_le_width (k : ℕ) : 2 ≤ width k := le_max_left _ _ +private theorem le_width (k : ℕ) : k ≤ width k := le_max_right _ _ +private theorem one_le_divisor (p : Context) : 1 ≤ divisor p := le_max_left _ _ +private theorem two_le_thresholdBase (k : ℕ) (p : Context) : 2 ≤ thresholdBase k p := + two_le_countingThresholdBase _ _ + +private theorem computableInPolyTime_divisor_unary : + ComputableInPolyTime divisor encContext encUnary := by + have hn : ComputableInPolyTime (fun p : Context => p.2) encContext encNat := + ComputableInPolyTime.unary_to_binary.comp (ComputableInPolyTime.snd _ _) + have hs := ParameterCheck.computableInPolyTime_numGroups_unary.comp hn + exact (ComputableInPolyTime.of_tidy ComputableTidilyInPolyTime.unary_max).comp + ((ComputableInPolyTime.const 1).prod hs) + +private theorem computableInPolyTime_divisor : + ComputableInPolyTime divisor encContext encNat := + ComputableInPolyTime.unary_to_binary.comp computableInPolyTime_divisor_unary + +private theorem computableInPolyTime_thresholdBase (k : ℕ) : + ComputableInPolyTime (thresholdBase k) encContext encNat := + (computableInPolyTime_countingThresholdBase (width k)).comp computableInPolyTime_divisor + +private theorem computableInPolyTime_thresholdCompare (k : ℕ) : + ComputableInPolyTime + (fun x : Context × ℕ × ℕ => decide (countingThreshold (thresholdBase k x.1) x.2.1 ≤ x.2.2)) + (encPair encContext (encPair encUnary encUnary)) encBool := + computableInPolyTime_countingThreshold_le_binary.comp + (((computableInPolyTime_thresholdBase k).comp (ComputableInPolyTime.fst _ _)).prod + (ComputableInPolyTime.snd _ _)) + +private theorem treeBound (k : ℕ) (p : Context) : + CountingTreeBound (thresholdBase k p) (width k) (divisor p) (depthCoeff k p) + ((by decide : 1 ≤ 2).trans (two_le_thresholdBase k p)) + ((by decide : 1 ≤ 2).trans (two_le_width k)) := + countingTreeBound_countingThresholdBase _ (one_le_divisor p) + +private theorem declaredSize_le_inputSize (x : Input) : x.1 ≤ inputSize x := by + simp only [inputSize, encInput, length_encPair, encUnary_apply, List.length_replicate] + omega + +private theorem polyBounded_depthCoeff (k : ℕ) : + PolyBounded inputSize (fun x => depthCoeff k ((), x.1)) := + polyBounded_countingDepthCoeff_numGroups (two_le_width k) + (PolyBounded.self.mono declaredSize_le_inputSize) + +private theorem polyBounded_depthCoeff_full (k : ℕ) : + PolyBounded (fun x : FullInput => (encFullInput x).length) + (fun x => depthCoeff k (x.1, x.2.1)) := + polyBounded_countingDepthCoeff_numGroups_encPair encUnit encCNF (two_le_width k) + +private theorem computableInPolyTime_prepare : + ComputableInPolyTime prepare encInput encFullInput := by + unfold prepare + fun_prop + +private theorem length_prepare (x : Input) : (encFullInput (prepare x)).length = inputSize x + 1 := by + simp [encFullInput, prepare, inputSize, encUnit_apply] + +private theorem length_leaf_input (N : ℕ) (ψ : CNF ℕ) : + (encPair encContext encCNF (((), N), ψ)).length = 2 * N + 3 + (encCNF ψ).length := by + simp only [encContext, length_encPair, encUnit_apply, List.length_nil, encUnary_apply, + List.length_replicate] + omega + +private theorem divisor_eq_numGroups {p : Context} (h : 1 ≤ numGroups p.2) : + divisor p = numGroups p.2 := max_eq_right h + +private theorem finite_clamped_sizes : {N : ℕ | divisor ((), N) ≠ numGroups N}.Finite := + (finite_numGroups_lt 1).subset fun N h => by + change numGroups N < 1 + by_contra hn + exact h (divisor_eq_numGroups (p := ((), N)) (Nat.le_of_not_gt hn)) + +private theorem computableInPolyTime_valid (k : ℕ) : + ComputableInPolyTime (fun x : Input => validDeclaredInput k x.1 x.2) encInput encBool := by + have hN := ComputableInPolyTime.unary_to_binary.comp + (ComputableInPolyTime.fst encUnary encCNF) + have hlt : ComputableInPolyTime + (fun x : Input × ℕ => decide (x.2 < x.1.1)) (encPair encInput encNat) encBool := + (ComputableInPolyTime.of_tidy ComputableTidilyInPolyTime.binary_lt).comp + ((ComputableInPolyTime.snd _ _).prod (hN.comp (ComputableInPolyTime.fst _ _))) + have hs : ComputableInPolyTime + (fun x : Input => x.2.vars.all fun v => decide (v < x.1)) encInput encBool := + ComputableInPolyTime.allWithInput (by fun_prop) hlt + unfold validDeclaredInput + fun_prop + +private theorem numVars_le_of_valid {k : ℕ} {x : Input} + (hx : validDeclaredInput k x.1 x.2 = true) : x.2.numVars ≤ x.1 := by + have hsub := (validDeclaredInput_eq_true_iff.mp hx).2 + simpa only [CNF.numVars, Finset.card_range] using Finset.card_le_card hsub + +/-- Polynomial workspace in the full Unit context remains polynomial in the original external +encoding. Guarding the false branch adds only the external input-length charge. -/ +private theorem polyBounded_selectedSpace (k d : ℕ) {S : FullInput → ℕ} + (hS : PolyBounded (fun x => (encFullInput x).length) S) : + PolyBounded inputSize (fun x => (inputSize x + 1) ^ d + + if validDeclaredInput k x.1 x.2 then S (prepare x) else inputSize x) := by + have hprepared : PolyBounded inputSize (fun x => S (prepare x)) := + hS.comp computableInPolyTime_prepare.polyBounded_length + have hbranch : PolyBounded inputSize + (fun x => if validDeclaredInput k x.1 x.2 then S (prepare x) else inputSize x) := + (hprepared.add PolyBounded.self).mono fun x => by split_ifs <;> omega + exact ((PolyBounded.self.add (.const 1)).pow d).add hbranch + +/-- Reapply the already-present input guard to retain the cost of only the selected branch. +This avoids charging an invalid-support input for its unbounded occurring-support clock. -/ +private theorem exists_computableInO_selectedSearch (k : ℕ) + (g : Context × CNF ℕ → ℕ) {T S : FullInput → ℕ} + (hsearch : ComputableInO + (fun x : FullInput => searchDeclaredWith Prod.snd (thresholdBase k) divisor (width k) k g + (x.1, x.2.1) x.2.2) encFullInput encNat T S) : + ∃ d, ComputableInO + (fun x : Input => searchDeclaredWith Prod.snd (thresholdBase k) divisor (width k) k g + ((), x.1) x.2) encInput encNat + (fun x => (inputSize x + 1) ^ d + + if validDeclaredInput k x.1 x.2 then T (prepare x) else inputSize x) + (fun x => (inputSize x + 1) ^ d + + if validDeclaredInput k x.1 x.2 then S (prepare x) else inputSize x) := by + obtain ⟨dp, _, hp⟩ := computableInPolyTime_prepare.tidy.exists_degree + obtain ⟨dv, _, hv⟩ := (computableInPolyTime_valid k).tidy.exists_degree + have hcore := hsearch.comp (ComputableInO.of_tidy hp.inO) + have hguard := (ComputableInO.of_tidy hv.inO).ite hcore + (ComputableInO.const (encIn := encInput) 0) + have hsum (x : Input) : (inputSize x + 1) ^ dv + (inputSize x + 1) ^ dp ≤ + 2 * (inputSize x + 1) ^ (dv + dp) := by + have hv' := Nat.pow_le_pow_right (by omega : 1 ≤ inputSize x + 1) (Nat.le_add_right dv dp) + have hp' := Nat.pow_le_pow_right (by omega : 1 ≤ inputSize x + 1) (Nat.le_add_left dp dv) + omega + refine ⟨dv + dp, (hguard.mono 2 (fun x => ?_) (fun x => ?_)).of_enc_eq ?_⟩ + · change (inputSize x + 1) ^ dv + + (if validDeclaredInput k x.1 x.2 then (inputSize x + 1) ^ dp + T (prepare x) + else inputSize x) ≤ _ + split_ifs <;> have := hsum x <;> omega + · change (inputSize x + 1) ^ dv + + (if validDeclaredInput k x.1 x.2 then (inputSize x + 1) ^ dp + S (prepare x) + else inputSize x) ≤ _ + split_ifs <;> have := hsum x <;> omega + · intro x + by_cases hx : validDeclaredInput k x.1 x.2 = true <;> + simp [Function.comp_apply, prepare, searchDeclaredWith, hx] + +end Cslib.Complexity.CountingNativeEndpointPrep + +/-! ## All-input clamped round estimate -/ + +namespace Cslib.Complexity.SubexponentialSAT + +open Filter ReplacementParams + +/-- One fixed natural coefficient bounds the clamped round count, including its extra terminal +step, for every `N` and `v ≤ N`. No lower bound on `N` or `numGroups N` is assumed. -/ +private theorem exists_clamped_rounds_le_interpolationScale : + ∃ C : ℕ, 0 < C ∧ ∀ N v : ℕ, v ≤ N → + ((2 ^ (v / max 1 (numGroups N) + 2) + 1 : ℕ) : ℝ) ≤ + (C : ℝ) * (2 : ℝ) ^ (16 * interpolationScale N) := by + obtain ⟨N₀, hN₀⟩ := eventually_atTop.mp + (SparseCountingScale.eventually_two_le_numGroups.and + SparseCountingScale.eventually_div_numGroups_le) + let C : ℕ := 2 ^ (N₀ + 2) + 5 + refine ⟨C, by dsimp [C]; positivity, fun N v hv => ?_⟩ + have hscale : (1 : ℝ) ≤ (2 : ℝ) ^ (16 * interpolationScale N) := + Real.one_le_rpow one_le_two (mul_nonneg (by norm_num) (interpolationScale_nonneg N)) + by_cases hN : N < N₀ + · have hexp : v / max 1 (numGroups N) + 2 ≤ N₀ + 2 := + Nat.add_le_add_right ((Nat.div_le_self _ _).trans (hv.trans hN.le)) 2 + have hrounds : 2 ^ (v / max 1 (numGroups N) + 2) + 1 ≤ C := by + have := Nat.pow_le_pow_right (by decide : 1 ≤ 2) hexp + dsimp [C] + omega + exact (Nat.cast_le.mpr hrounds).trans + (le_mul_of_one_le_right (Nat.cast_nonneg C) hscale) + · obtain ⟨hgroups, hdiv⟩ := hN₀ N (Nat.le_of_not_lt hN) + have hclamp : max 1 (numGroups N) = numGroups N := max_eq_right (by omega) + have hexp : ((v / max 1 (numGroups N) : ℕ) : ℝ) ≤ 16 * interpolationScale N := by + calc + ((v / max 1 (numGroups N) : ℕ) : ℝ) ≤ (v : ℝ) / (max 1 (numGroups N) : ℕ) := + Nat.cast_div_le + _ ≤ (N : ℝ) / (numGroups N : ℝ) := by + rw [hclamp] + exact div_le_div_of_nonneg_right (Nat.cast_le.mpr hv) (Nat.cast_nonneg _) + _ ≤ 16 * interpolationScale N := hdiv + have htwo : (2 : ℝ) ^ (v / max 1 (numGroups N)) ≤ + (2 : ℝ) ^ (16 * interpolationScale N) := by + rw [← Real.rpow_natCast] + exact Real.rpow_le_rpow_of_exponent_le one_le_two hexp + have hrounds : ((2 ^ (v / max 1 (numGroups N) + 2) + 1 : ℕ) : ℝ) ≤ + 5 * (2 : ℝ) ^ (16 * interpolationScale N) := by + push_cast + rw [pow_add] + norm_num + nlinarith + have hC : (5 : ℝ) ≤ C := Nat.cast_le.mpr (Nat.le_add_left 5 _) + exact hrounds.trans (mul_le_mul_of_nonneg_right hC (by positivity)) + +end Cslib.Complexity.SubexponentialSAT + +/-! ## Dense counting and SAT consequences -/ + +namespace Cslib.Complexity.CountingNativeEndpointConsequencesPrep + +open Cslib.Logic.PL Turing.MultiTapeTM CountingSparsify SubexponentialSAT +open Cslib.Logic.PL.CNF (validDeclaredInput validDeclaredInput_eq_true_iff) + +private abbrev Input := ℕ × CNF ℕ +private abbrev encInput := encPair encUnary encCNF +private def declareInput (φ : CNF ℕ) : Input := (φ.numVars, φ) + +private theorem computableInPolyTime_declareInput : + ComputableInPolyTime declareInput encCNF encInput := by + unfold declareInput + fun_prop + +private theorem length_declareInput (φ : CNF ℕ) : + (encInput (declareInput φ)).length + 1 ≤ 3 * ((encCNF φ).length + 1) := by + have hn := φ.numVars_le_length_vars.trans (SAT.length_vars_le φ) + simp only [declareInput, encInput, length_encPair, encUnary_apply, List.length_replicate] + omega + +private theorem dense_spec {k : ℕ} {count : Input → ℕ} + (hspec : ∀ x, count x = if validDeclaredInput k x.1 x.2 then + x.2.modelCountOn (Finset.range x.1) else 0) + {ψ : CNF ℕ} (hw : ∀ cl ∈ ψ, cl.length ≤ k) + (hdense : ψ.vars.toFinset = Finset.range ψ.numVars) : + count (declareInput ψ) = ψ.modelCountOn (Finset.range ψ.numVars) := by + have hv := validDeclaredInput_eq_true_iff.mpr ⟨hw, hdense.subset⟩ + simpa only [declareInput, hv, ↓reduceIte] using hspec (declareInput ψ) + +/-- Construct the common allowance needed by the existing dense-counting bridge only after +charging preparation and transferring the independent workspace bound to `encCNF`. -/ +private theorem exists_common_dense_resources {count : Input → ℕ} {T S : Input → ℕ} + (hcount : ComputableInO count encInput encNat T S) {A c e a b : ℕ} + (hT : ∀ x, (T x : ℝ) ≤ c * ((2 : ℝ) ^ ((A : ℝ) * interpolationScale x.1) * + (((encInput x).length : ℝ) + 1) ^ e) + c) + (hS : ∀ x, S x ≤ a * ((encInput x).length + 1) ^ b) : + ∃ t : CNF ℕ → ℕ, ∃ C E : ℕ, + ComputableInO (fun φ => count (declareInput φ)) encCNF encNat t t ∧ + ∀ φ, (t φ : ℝ) ≤ C * ((2 : ℝ) ^ ((A : ℝ) * interpolationScale φ.numVars) * + (((encCNF φ).length : ℝ) + 1) ^ E) + C := by + obtain ⟨d, _, hp⟩ := computableInPolyTime_declareInput.tidy.exists_degree + have hcomp := hcount.comp (ComputableInO.of_tidy hp.inO) + let P (φ : CNF ℕ) := ((encCNF φ).length + 1) ^ d + S (declareInput φ) + have hspace : PolyBounded (fun x => (encInput x).length) S := + PolyBounded.of_forall_le a b hS + have hP : PolyBounded (fun φ : CNF ℕ => (encCNF φ).length) P := + ((PolyBounded.self.add (.const 1)).pow d).add + (hspace.comp computableInPolyTime_declareInput.polyBounded_length) + obtain ⟨p, q, hP⟩ := hP.exists_le + let t (φ : CNF ℕ) := P φ + T (declareInput φ) + let C := p + c * 3 ^ e + c + refine ⟨t, C, q + e, hcomp.mono_le (fun φ => ?_) (fun φ => ?_), fun φ => ?_⟩ + · dsimp only [t, P] + omega + · dsimp only [t, P] + omega + · let Y : ℝ := (encCNF φ).length + 1 + let X : ℝ := (2 : ℝ) ^ ((A : ℝ) * interpolationScale φ.numVars) + have hY : 1 ≤ Y := by dsimp [Y]; exact le_add_of_nonneg_left (Nat.cast_nonneg _) + have hX : 1 ≤ X := + Real.one_le_rpow (by norm_num) (mul_nonneg (Nat.cast_nonneg A) (interpolationScale_nonneg _)) + have hYq : Y ^ q ≤ Y ^ (q + e) := pow_le_pow_right₀ hY (by omega) + have hYe : Y ^ e ≤ Y ^ (q + e) := pow_le_pow_right₀ hY (by omega) + have hYP : Y ^ (q + e) ≤ X * Y ^ (q + e) := + le_mul_of_one_le_left (by positivity) hX + have hPr : (P φ : ℝ) ≤ p * Y ^ q := by + dsimp only [Y] + exact_mod_cast hP φ + have hlen : ((encInput (declareInput φ)).length : ℝ) + 1 ≤ 3 * Y := by + dsimp only [Y] + exact_mod_cast length_declareInput φ + have hpower : (((encInput (declareInput φ)).length : ℝ) + 1) ^ e ≤ + (3 : ℝ) ^ e * Y ^ (q + e) := by + calc + _ ≤ (3 * Y) ^ e := pow_le_pow_left₀ (by positivity) hlen e + _ = 3 ^ e * Y ^ e := mul_pow _ _ _ + _ ≤ _ := mul_le_mul_of_nonneg_left hYe (by positivity) + have hPfinal : (P φ : ℝ) ≤ p * (X * Y ^ (q + e)) := + hPr.trans (mul_le_mul_of_nonneg_left (hYq.trans hYP) (Nat.cast_nonneg p)) + have hTfinal : (T (declareInput φ) : ℝ) ≤ + (c : ℝ) * 3 ^ e * (X * Y ^ (q + e)) + c := by + have hT' := hT (declareInput φ) + change (T (declareInput φ) : ℝ) ≤ + c * (X * (((encInput (declareInput φ)).length : ℝ) + 1) ^ e) + c at hT' + refine hT'.trans ?_ + have hmul := mul_le_mul_of_nonneg_left + (mul_le_mul_of_nonneg_left hpower (by positivity : 0 ≤ X)) (Nat.cast_nonneg c) + nlinarith + have hc : (c : ℝ) ≤ C := by exact_mod_cast (show c ≤ C by dsimp [C]; omega) + have hcoeff : (p : ℝ) + c * 3 ^ e ≤ C := by + exact_mod_cast (show p + c * 3 ^ e ≤ C by dsimp [C]; omega) + have hfactor : 0 ≤ X * Y ^ (q + e) := by positivity + change ((P φ + T (declareInput φ) : ℕ) : ℝ) ≤ C * (X * Y ^ (q + e)) + C + push_cast + nlinarith [mul_le_mul_of_nonneg_right hcoeff hfactor] + +private theorem KSAT_of_declared_contract {k : ℕ} {count : Input → ℕ} {T S : Input → ℕ} + (hcount : ComputableInO count encInput encNat T S) + (hspec : ∀ x, count x = if validDeclaredInput k x.1 x.2 then + x.2.modelCountOn (Finset.range x.1) else 0) {A c e a b : ℕ} + (hT : ∀ x, (T x : ℝ) ≤ c * ((2 : ℝ) ^ ((A : ℝ) * interpolationScale x.1) * + (((encInput x).length : ℝ) + 1) ^ e) + c) + (hS : ∀ x, S x ≤ a * ((encInput x).length + 1) ^ b) : + DecidableInSubexpTime (KSAT k) encCNF CNF.numVars := by + obtain ⟨t, C, E, hc, ht⟩ := exists_common_dense_resources hcount hT hS + exact DecidableInSubexpTime.KSAT_of_dense_modelCount_interpolationScale hc + (fun _ hw hdense => dense_spec hspec hw hdense) ht + +/-- The complete accepted contract is still a premise here. These downstream consequences become +unconditional only when the native construction supplies that contract for every fixed width. -/ +private theorem consequences_of_declared_contract + (h : ∀ k : ℕ, ∃ count : Input → ℕ, ∃ T S : Input → ℕ, ∃ A c e a b : ℕ, + ComputableInO count encInput encNat T S ∧ + (∀ x, count x = if validDeclaredInput k x.1 x.2 then + x.2.modelCountOn (Finset.range x.1) else 0) ∧ + (∀ x, (T x : ℝ) ≤ c * ((2 : ℝ) ^ ((A : ℝ) * interpolationScale x.1) * + (((encInput x).length : ℝ) + 1) ^ e) + c) ∧ + (∀ x, S x ≤ a * ((encInput x).length + 1) ^ b)) : + (∀ k, satExponent k = 0) ∧ ¬ETH ∧ ¬SETH := by + have hSAT (k : ℕ) : DecidableInSubexpTime (KSAT k) encCNF CNF.numVars := by + obtain ⟨count, T, S, A, c, e, a, b, hc, hspec, hT, hS⟩ := h k + exact KSAT_of_declared_contract hc hspec hT hS + exact ⟨fun k => satExponent_eq_zero_of_decidableInSubexpTime (hSAT k), + not_ETH_of_decidableInSubexpTime (hSAT 3), not_SETH_of_forall_decidableInSubexpTime hSAT⟩ + +end Cslib.Complexity.CountingNativeEndpointConsequencesPrep + +/-! ## Uniform search and normalized leaf assembly -/ + +namespace Cslib.Complexity.CountingNativeEndpointPrep + +open Cslib.Logic.PL Cslib.Logic.PL.CNF Cslib.Logic.PL.CNF.Sparsification +open Cslib.Logic.PL.ClauseSet.Sparsification Turing.MultiTapeTM Cslib.GenericRAM +open Turing.MultiTapeTM.Universal (encUnit encUnit_apply) +open CountingSparsify SubexponentialSAT SubexponentialSAT.SparsePolyCounter +open BranchedSparseCNFCounter + +private abbrev LeafInput := Context × CNF ℕ +private abbrev encLeafInput := encPair encContext encCNF + +/-- The prefix-size charge includes the original declared unary size and retained Unit context. -/ +private def leafSize (k : ℕ) (x : FullInput) : ℕ := + 2 * x.2.1 + 3 + nodeBound (width k) (depthCoeff k (x.1, x.2.1)) x.2.2 + +private theorem polyBounded_leafSize (k : ℕ) : + PolyBounded (fun x : FullInput => (encFullInput x).length) (leafSize k) := by + have hN : PolyBounded (fun x : FullInput => (encFullInput x).length) (fun x => x.2.1) := + PolyBounded.self.mono fun x => by + simp only [encFullInput, encInput, length_encPair, encUnary_apply, List.length_replicate] + omega + have hL : PolyBounded (fun x : FullInput => (encFullInput x).length) + (fun x => (encCNF x.2.2).length) := + PolyBounded.self.mono fun x => + (length_le_encPair_right encUnary encCNF x.2).trans + (length_le_encPair_right encUnit encInput x) + have hn := hL.mono fun x => x.2.2.numVars_le_length_vars.trans (SAT.length_vars_le x.2.2) + have hm := hL.mono fun x => length_le_length_encList _ x.2.2 + have hnode := ((hm.add (.const 1)).add + ((PolyBounded.const (width k)).mul ((polyBounded_depthCoeff_full k).mul hn))).mul + (((PolyBounded.const 2).mul ((PolyBounded.const (width k)).mul + (((PolyBounded.const 2).mul hL).add (.const 1)))).add (.const 1)) + exact (((PolyBounded.const 2).mul hN).add (.const 3)).add hnode + +/-- Every active prefix, including the terminal prefix, meets the exact supplier clause cap. -/ +private theorem prefix_leaf_bounds (k : ℕ) (g : LeafInput → ℕ) (x : FullInput) + (hx : validDeclaredInput k x.2.1 x.2.2 = true) (i : ℕ) + (hactive : let p := (x.1, x.2.1) + let st := (step (thresholdBase k p) (width k) (fun ψ => g (p, ψ)))^[i] (init k x.2.2) + st.2.1.isEmpty = false ∧ isSparse (countingThreshold (thresholdBase k p)) (width k) + (st.2.1.headD []) = true) : + let p := (x.1, x.2.1) + let ψ := ((step (thresholdBase k p) (width k) (fun ψ => g (p, ψ)))^[i] + (init k x.2.2)).2.1.headD [] + ψ.length ≤ leafOccBound k x.2.1 * x.2.1 + 1 ∧ + (encLeafInput (p, ψ)).length ≤ leafSize k x := by + have hb := (iterate_step_prefix_bounds + ((by decide : 1 ≤ 2).trans (two_le_thresholdBase k (x.1, x.2.1))) + ((by decide : 1 ≤ 2).trans (two_le_width k)) + (two_le_thresholdBase k (x.1, x.2.1)) (le_width k) (treeBound k (x.1, x.2.1)) + (fun ψ => g ((x.1, x.2.1), ψ)) x.2.2 i).2.2.2 hactive + have hn := numVars_le_of_valid (x := x.2) hx + refine ⟨?_, ?_⟩ + · rw [leafOccBound_eq_occBound] + exact hb.2.2.2.1.trans (Nat.add_le_add_right (Nat.mul_le_mul_left _ hn) 1) + · simp only [encLeafInput, encContext, length_encPair, encUnit_apply, + List.length_nil, encUnary_apply, List.length_replicate, leafSize] + have := hb.2.2.2.2 + omega + +/-- The polynomial part of the selected search cost and the ceiled leaf envelope combine with +one fixed all-input round estimate. Small declared sizes are already absorbed in that estimate. -/ +private theorem selected_time_envelope (k d c e Cₜ dₜ Aₜ : ℕ) : + let U (x : FullInput) := Cₜ * (leafSize k x + 1) ^ dₜ + let R (x : FullInput) := ⌈(U x : ℝ) * (2 : ℝ) ^ ((Aₜ : ℝ) * interpolationScale x.2.1)⌉₊ + let W (x : FullInput) := c * ((encFullInput x).length + 1) ^ e + ∃ C E : ℕ, ∀ x : Input, + (((inputSize x + 1) ^ d + if validDeclaredInput k x.1 x.2 then + W (prepare x) + (rounds (divisor ((), x.1)) x.2 + 1) * + (W (prepare x) + R (prepare x)) else inputSize x : ℕ) : ℝ) ≤ + C * ((2 : ℝ) ^ (((Aₜ + 16 : ℕ) : ℝ) * interpolationScale x.1) * + ((inputSize x : ℝ) + 1) ^ E) + C := by + dsimp only + let U (x : FullInput) := Cₜ * (leafSize k x + 1) ^ dₜ + let R (x : FullInput) := ⌈(U x : ℝ) * (2 : ℝ) ^ ((Aₜ : ℝ) * interpolationScale x.2.1)⌉₊ + let W (x : FullInput) := c * ((encFullInput x).length + 1) ^ e + let P (x : Input) := (inputSize x + 1) ^ d + W (prepare x) + U (prepare x) + 1 + inputSize x + have hW : PolyBounded (fun x : FullInput => (encFullInput x).length) W := + (PolyBounded.const c).mul ((PolyBounded.self.add (.const 1)).pow e) + have hU : PolyBounded (fun x : FullInput => (encFullInput x).length) U := + (PolyBounded.const Cₜ).mul (((polyBounded_leafSize k).add (.const 1)).pow dₜ) + have hP : PolyBounded inputSize P := + (((((PolyBounded.self.add (.const 1)).pow d).add + (hW.comp computableInPolyTime_prepare.polyBounded_length)).add + (hU.comp computableInPolyTime_prepare.polyBounded_length)).add (.const 1)).add PolyBounded.self + obtain ⟨Cₚ, E, hP⟩ := hP.exists_le + obtain ⟨Cq, _, hq⟩ := exists_clamped_rounds_le_interpolationScale + refine ⟨(Cq + 1) * Cₚ, E, fun x => ?_⟩ + let X : ℝ := (2 : ℝ) ^ ((Aₜ : ℝ) * interpolationScale x.1) + let Y : ℝ := (2 : ℝ) ^ (16 * interpolationScale x.1) + let p : ℝ := Cₚ * ((inputSize x : ℝ) + 1) ^ E + have hX : 1 ≤ X := Real.one_le_rpow one_le_two + (mul_nonneg (Nat.cast_nonneg Aₜ) (interpolationScale_nonneg _)) + have hY : 1 ≤ Y := Real.one_le_rpow one_le_two + (mul_nonneg (by norm_num) (interpolationScale_nonneg _)) + have hp : 0 ≤ p := by dsimp [p]; positivity + have hPXY : p ≤ p * (X * Y) := + le_mul_of_one_le_right hp (one_le_mul_of_one_le_of_one_le hX hY) + have hPr : (P x : ℝ) ≤ p := by + dsimp only [p] + exact_mod_cast hP x + have hceil : (R (prepare x) : ℝ) ≤ (U (prepare x) : ℝ) * X + 1 := + (Nat.ceil_lt_add_one (by positivity : 0 ≤ (U (prepare x) : ℝ) * X)).le + have hjoin : X * Y = (2 : ℝ) ^ (((Aₜ + 16 : ℕ) : ℝ) * interpolationScale x.1) := by + rw [← Real.rpow_add (by norm_num : (0 : ℝ) < 2)] + congr 1 + push_cast + ring + have htarget : (Cq + 1 : ℝ) * p * (X * Y) ≤ + (((Cq + 1) * Cₚ : ℕ) : ℝ) * + ((2 : ℝ) ^ (((Aₜ + 16 : ℕ) : ℝ) * interpolationScale x.1) * + ((inputSize x : ℝ) + 1) ^ E) + ((Cq + 1) * Cₚ : ℕ) := by + rw [hjoin] + dsimp only [p] + push_cast + nlinarith [show (0 : ℝ) ≤ (Cq + 1) * Cₚ by positivity] + by_cases hx : validDeclaredInput k x.1 x.2 = true + · have hround : ((rounds (divisor ((), x.1)) x.2 + 1 : ℕ) : ℝ) ≤ Cq * Y := by + simpa only [rounds, CNF.length_distinctVars, divisor, leafSearchDivisor, Y] using + hq x.1 x.2.numVars (numVars_le_of_valid hx) + have hpol : (((inputSize x + 1) ^ d + W (prepare x) : ℕ) : ℝ) ≤ p := by + apply le_trans _ hPr + exact_mod_cast (show (inputSize x + 1) ^ d + W (prepare x) ≤ P x by dsimp [P]; omega) + have hinside : ((W (prepare x) + R (prepare x) : ℕ) : ℝ) ≤ p * X := by + have hWU : ((W (prepare x) + U (prepare x) + 1 : ℕ) : ℝ) ≤ p := by + apply le_trans _ hPr + exact_mod_cast (show W (prepare x) + U (prepare x) + 1 ≤ P x by dsimp [P]; omega) + have hscale := mul_le_mul_of_nonneg_right hWU (by positivity : 0 ≤ X) + push_cast at hscale ⊢ + nlinarith [mul_le_mul_of_nonneg_left hX (Nat.cast_nonneg (W (prepare x)))] + have hprod := mul_le_mul hround hinside (by positivity) (by positivity) + have hwhole := add_le_add hpol hprod + change (((inputSize x + 1) ^ d + if validDeclaredInput k x.1 x.2 then + W (prepare x) + (rounds (divisor ((), x.1)) x.2 + 1) * + (W (prepare x) + R (prepare x)) else inputSize x : ℕ) : ℝ) ≤ _ + simp only [hx, ↓reduceIte, Nat.cast_add, Nat.cast_mul] + push_cast at hwhole htarget ⊢ + apply le_trans _ htarget + nlinarith + · change (((inputSize x + 1) ^ d + if validDeclaredInput k x.1 x.2 then + W (prepare x) + (rounds (divisor ((), x.1)) x.2 + 1) * + (W (prepare x) + R (prepare x)) else inputSize x : ℕ) : ℝ) ≤ _ + simp only [hx, Bool.false_eq_true, ↓reduceIte] + have hf : (((inputSize x + 1) ^ d + inputSize x : ℕ) : ℝ) ≤ p := by + apply le_trans _ hPr + exact_mod_cast (show (inputSize x + 1) ^ d + inputSize x ≤ P x by dsimp [P]; omega) + apply hf.trans (hPXY.trans (le_trans ?_ htarget)) + calc + p * (X * Y) ≤ ((Cq : ℝ) + 1) * (p * (X * Y)) := + le_mul_of_one_le_left (by positivity) (le_add_of_nonneg_left (Nat.cast_nonneg Cq)) + _ = _ := by ring + +/-- Private generic join; its leaf premises are discharged by the frozen #1337 interface below. -/ +private theorem exists_declared_contract_of_leaf (k : ℕ) (g : LeafInput → ℕ) + (cg : NativeCertificate g encLeafInput encNat) + (hcorrect : ∀ p ψ, (∀ cl ∈ ψ, cl.length ≤ k) → + ψ.vars.toFinset ⊆ Finset.range p.2 → g (p, ψ) = ψ.modelCount) + (hcap : ∀ x, g x ≤ 2 ^ x.2.numVars) + (hspace : PolyBounded (fun x => (encLeafInput x).length) cg.space) + (Cₜ dₜ Aₜ : ℕ) + (htime : ∀ x, x.2.length ≤ leafOccBound k x.1.2 * x.1.2 + 1 → + (cg.time x : ℝ) ≤ Cₜ * (((encLeafInput x).length : ℝ) + 1) ^ dₜ * + (2 : ℝ) ^ ((Aₜ : ℝ) * interpolationScale x.1.2)) : + ∃ (count : Input → ℕ) (T S : Input → ℕ) (A c e a b : ℕ), + ComputableInO count encInput encNat T S ∧ + (∀ x, count x = if validDeclaredInput k x.1 x.2 then + x.2.modelCountOn (Finset.range x.1) else 0) ∧ + (∀ x, (T x : ℝ) ≤ c * ((2 : ℝ) ^ ((A : ℝ) * interpolationScale x.1) * + (((encInput x).length : ℝ) + 1) ^ e) + c) ∧ + (∀ x, S x ≤ a * ((encInput x).length + 1) ^ b) := by + let R (x : FullInput) := ⌈((Cₜ * (leafSize k x + 1) ^ dₜ : ℕ) : ℝ) * + (2 : ℝ) ^ ((Aₜ : ℝ) * interpolationScale x.2.1)⌉₊ + obtain ⟨Cₛ, dₛ, hspace⟩ := hspace.exists_le + let Q (x : FullInput) := Cₛ * (leafSize k x + 1) ^ dₛ + have hQ : PolyBounded (fun x : FullInput => (encFullInput x).length) Q := + (PolyBounded.const Cₛ).mul (((polyBounded_leafSize k).add (.const 1)).pow dₛ) + obtain ⟨c, e, hsearch, hS⟩ := exists_computableInO_searchDeclaredWith + (computableInPolyTime_divisor) (computableInPolyTime_thresholdCompare k) + (fun p => (by decide : 1 ≤ 2).trans (two_le_thresholdBase k p)) + ((by decide : 1 ≤ 2).trans (two_le_width k)) (two_le_thresholdBase k) (le_width k) + (treeBound k) (polyBounded_depthCoeff_full k) cg.computes + (fun x _ i _ _ => hcap _) (R := R) (Q := Q) + (fun x hx i _ ha => by + obtain ⟨hclause, hlen⟩ := prefix_leaf_bounds k g x hx i ha + let ψ := ((step (thresholdBase k (x.1, x.2.1)) (width k) + (fun ψ => g ((x.1, x.2.1), ψ)))^[i] (init k x.2.2)).2.1.headD [] + have ht := htime ((x.1, x.2.1), ψ) hclause + have hlenr : ((encLeafInput ((x.1, x.2.1), ψ)).length : ℝ) + 1 ≤ + (leafSize k x : ℝ) + 1 := by + exact_mod_cast Nat.add_le_add_right hlen 1 + have hpow := pow_le_pow_left₀ (by positivity : (0 : ℝ) ≤ + ((encLeafInput ((x.1, x.2.1), ψ)).length : ℝ) + 1) hlenr dₜ + suffices hr : (cg.time ((x.1, x.2.1), ψ) : ℝ) ≤ (R x : ℝ) from Nat.cast_le.mp hr + apply (ht.trans (mul_le_mul_of_nonneg_right + (mul_le_mul_of_nonneg_left hpow (Nat.cast_nonneg Cₜ)) (by positivity))).trans + simpa only [R, Nat.cast_mul, Nat.cast_pow, Nat.cast_add, Nat.cast_one] using + (Nat.le_ceil (((Cₜ * (leafSize k x + 1) ^ dₜ : ℕ) : ℝ) * + (2 : ℝ) ^ ((Aₜ : ℝ) * interpolationScale x.2.1)))) + (fun x hx i _ ha => by + have hlen := (prefix_leaf_bounds k g x hx i ha).2 + exact (hspace ((x.1, x.2.1), ((step (thresholdBase k (x.1, x.2.1)) (width k) + (fun ψ => g ((x.1, x.2.1), ψ)))^[i] (init k x.2.2)).2.1.headD [])).trans + (Nat.mul_le_mul_left Cₛ + (Nat.pow_le_pow_left (Nat.add_le_add_right hlen 1) dₛ))) hQ + obtain ⟨d, hselected⟩ := exists_computableInO_selectedSearch k g hsearch + obtain ⟨a, b, hab⟩ := (polyBounded_selectedSpace k d hS).exists_le + obtain ⟨C, E, hT⟩ := selected_time_envelope k d c e Cₜ dₜ Aₜ + refine ⟨_, _, _, Aₜ + 16, C, E, a, b, hselected, ?_, hT, hab⟩ + intro x + exact searchDeclaredWith_eq_ite_modelCountOn + ((by decide : 1 ≤ 2).trans (two_le_thresholdBase k ((), x.1))) + ((by decide : 1 ≤ 2).trans (two_le_width k)) (two_le_thresholdBase k ((), x.1)) + (le_width k) (treeBound k ((), x.1)) (fun ψ hw _ hsub => hcorrect _ ψ hw hsub) x.2 + +/-- The accepted full declared-count telescope, conditional privately only on the remaining +concrete branch evaluator obligations. No leaf, prefix, clock or final-guard premise remains. -/ +private theorem exists_declared_contract (k N₀_branch : ℕ) {branchEval : BranchEvalInput → ℕ} + (cBranch : NativeCertificate branchEval encBranchEvalInput encNat) + (hbranch : ∀ n' eqs', checkBranchFeasible N₀_branch (n', eqs') = true → + branchEval (prepareBranchEvalInput (n', eqs')) = HeavyBranchFold.rootCount n' eqs') + (hs_br : PolyBounded (fun x => (encBranchEvalInput x).length) cBranch.space) + (hbr_time : BranchPolylogTimeBound N₀_branch cBranch) : + ∃ (count : Input → ℕ) (T S : Input → ℕ) (A c e a b : ℕ), + ComputableInO count encInput encNat T S ∧ + (∀ x, count x = if validDeclaredInput k x.1 x.2 then + x.2.modelCountOn (Finset.range x.1) else 0) ∧ + (∀ x, (T x : ℝ) ≤ c * ((2 : ℝ) ^ ((A : ℝ) * interpolationScale x.1) * + (((encInput x).length : ℝ) + 1) ^ e) + c) ∧ + (∀ x, S x ≤ a * ((encInput x).length + 1) ^ b) := by + have hbound : ∀ n' eqs', checkBranchFeasible N₀_branch (n', eqs') = true → + branchEval (prepareBranchEvalInput (n', eqs')) ≤ 2 ^ n' := by + intro n' eqs' hf + rw [hbranch n' eqs' hf] + exact HeavyBranchFold.rootCount_le_two_pow n' eqs' + obtain ⟨N₀_leaf, N₀_top, Cₜ, dₜ, Aₜ, _, ht⟩ := + exists_branchedSparseCNF_time_bound k N₀_branch cBranch hbound hs_br hbr_time + exact exists_declared_contract_of_leaf k + (branchedSparseCNFLeafCounter k N₀_leaf N₀_top N₀_branch branchEval) + (branchedSparseCNFLeafCertificate k N₀_leaf N₀_top N₀_branch cBranch hbound) + (fun p ψ hw hsub => branchedSparseCNFLeafCounter_eq_modelCount hbranch p.1 p.2 ψ hw hsub) + (branchedSparseCNFLeafCounter_le_two_pow_numVars k N₀_leaf N₀_top N₀_branch branchEval) + (polyBounded_branchedSparseCNFLeafCertificate_space k N₀_leaf N₀_top N₀_branch + cBranch hbound hs_br) Cₜ dₜ Aₜ (fun x hx => (ht x hx).2) + +/-- Reuse the existing dense-relabeling bridge; arbitrary raw variable labels are never assumed +already dense. The same remaining concrete branch premises stay explicit and private. -/ +private theorem consequences_of_branch_contract (N₀_branch : ℕ) + {branchEval : BranchEvalInput → ℕ} + (cBranch : NativeCertificate branchEval encBranchEvalInput encNat) + (hbranch : ∀ n' eqs', checkBranchFeasible N₀_branch (n', eqs') = true → + branchEval (prepareBranchEvalInput (n', eqs')) = HeavyBranchFold.rootCount n' eqs') + (hs_br : PolyBounded (fun x => (encBranchEvalInput x).length) cBranch.space) + (hbr_time : BranchPolylogTimeBound N₀_branch cBranch) : + (∀ k, satExponent k = 0) ∧ ¬ETH ∧ ¬SETH := + CountingNativeEndpointConsequencesPrep.consequences_of_declared_contract + (fun k => exists_declared_contract k N₀_branch cBranch hbranch hs_br hbr_time) + +end Cslib.Complexity.CountingNativeEndpointPrep + +/-! ## Concrete bounded-incidence resources -/ + +namespace Cslib.Complexity.CountingNativeEndpointPrep + +open Cslib.Logic.PL.CNF Cslib.GenericRAM Turing.MultiTapeTM +open SubexponentialSAT SubexponentialSAT.SparsePolyCounter + +/-- Specialize the reviewed declared-count contract to the published native bounded-incidence +resources. Its local exactness premise is discharged by the public endpoint below. No restriction +is added to the external inputs or to the global polynomial workspace bound. -/ +private theorem exists_declared_contract_of_boundedIncidence (k N₀_branch : ℕ) + (hbranch : ∀ n' eqs', checkBranchFeasible N₀_branch (n', eqs') = true → + evalBoundedIncidenceBranch (prepareBranchEvalInput (n', eqs')) = + HeavyBranchFold.rootCount n' eqs') : + ∃ (count : Input → ℕ) (T S : Input → ℕ) (A c e a b : ℕ), + ComputableInO count encInput encNat T S ∧ + (∀ x, count x = if validDeclaredInput k x.1 x.2 then + x.2.modelCountOn (Finset.range x.1) else 0) ∧ + (∀ x, (T x : ℝ) ≤ c * ((2 : ℝ) ^ ((A : ℝ) * interpolationScale x.1) * + (((encInput x).length : ℝ) + 1) ^ e) + c) ∧ + (∀ x, S x ≤ a * ((encInput x).length + 1) ^ b) := + exists_declared_contract k N₀_branch boundedIncidenceBranchCertificate hbranch + polyBounded_boundedIncidenceBranchCertificate_space + (branchPolylogTimeBound_boundedIncidenceBranchCertificate N₀_branch) + +end Cslib.Complexity.CountingNativeEndpointPrep + +/-! ## Unconditional native endpoint -/ + +namespace Cslib.Complexity.CountingNativeEndpoint + +open Cslib.Logic.PL Cslib.Logic.PL.CNF Turing.MultiTapeTM +open SubexponentialSAT SubexponentialSAT.SparsePolyCounter + +/-- For each fixed width bound, one native counter computes the exact guarded declared-variable +model count on every unary-size/CNF input. Both resource functions and all constants are fixed +before the input; time uses the interpolation scale and workspace is polynomial in the original +external encoded input length. -/ +public theorem exists_declaredCounter (k : ℕ) : + ∃ (count : ℕ × CNF ℕ → ℕ) (T S : ℕ × CNF ℕ → ℕ) (A c e a b : ℕ), + ComputableInO count (encPair encUnary encCNF) encNat T S ∧ + (∀ x, count x = if validDeclaredInput k x.1 x.2 then + x.2.modelCountOn (Finset.range x.1) else 0) ∧ + (∀ x, (T x : ℝ) ≤ c * ((2 : ℝ) ^ ((A : ℝ) * interpolationScale x.1) * + (((encPair encUnary encCNF x).length : ℝ) + 1) ^ e) + c) ∧ + (∀ x, S x ≤ a * ((encPair encUnary encCNF x).length + 1) ^ b) := + CountingNativeEndpointPrep.exists_declared_contract_of_boundedIncidence k 0 + (fun _ _ hfeas => evalBoundedIncidenceBranch_eq_rootCount hfeas) + +/-- Every fixed-width `k`-SAT problem is decidable in subexponential time in its number of +occurring variables, with the CNF encoded in the native model. Arbitrary variable labels are +handled by the existing dense-relabeling bridge. -/ +public theorem decidableInSubexpTime_KSAT (k : ℕ) : + DecidableInSubexpTime (KSAT k) encCNF CNF.numVars := by + obtain ⟨count, T, S, A, c, e, a, b, hc, hspec, hT, hS⟩ := exists_declaredCounter k + exact CountingNativeEndpointConsequencesPrep.KSAT_of_declared_contract hc hspec hT hS + +/-- The SAT exponent vanishes for every fixed clause width. -/ +public theorem satExponent_eq_zero (k : ℕ) : satExponent k = 0 := + satExponent_eq_zero_of_decidableInSubexpTime (decidableInSubexpTime_KSAT k) + +/-- The native counting construction refutes the Exponential Time Hypothesis. -/ +public theorem not_ETH : ¬ETH := + not_ETH_of_decidableInSubexpTime (decidableInSubexpTime_KSAT 3) + +/-- The native counting construction refutes the Strong Exponential Time Hypothesis. -/ +public theorem not_SETH : ¬SETH := + not_SETH_of_forall_decidableInSubexpTime decidableInSubexpTime_KSAT + +end Cslib.Complexity.CountingNativeEndpoint diff --git a/ROADMAP.md b/ROADMAP.md index 0d66d66b4..462de43b8 100644 --- a/ROADMAP.md +++ b/ROADMAP.md @@ -438,11 +438,14 @@ still to read them for the mathematics and write proofs against Complexitylib's adapted code keeps its Apache 2.0 attribution. The rewrites state no license and are only read and credited. -- **Native sparse-formula counting** ([#1226](https://github.com/cslib-community/complexitylib/issues/1226)): - `CNF.GreedyContext` certifies the existing greedy parity search uniformly from a supplied counter - on encoded `(context, rows)`, retaining and charging the context through both loops. Theorem 2.2 - counting and Tanner initialization remain separate prerequisites; the complete native counting - endpoint is still open. This conditional interface does not establish their algorithms or rates. +- **Native declared-variable counting** ([#1226](https://github.com/cslib-community/complexitylib/issues/1226)): + `CountingNativeEndpoint.exists_declaredCounter` supplies one native counter for each fixed width, + exact on every valid declared-size/CNF input and zero otherwise. It has + `2^{O_k(interpolationScale N)} * (L + 1)^{O_k(1)}` time and independent polynomial workspace in the + original external encoded length `L`, with no supplier premises. The module derives + subexponential-time `k`-SAT, zero SAT exponents, `¬ETH`, and `¬SETH`. This is the Sections 3–6 and + Appendices A–B interpolation-scale bound, not the sharper Appendix D runtime. Integration, + validation, and the curated formal abstract are tracked in #1226. ## Documentation and repository From fbe4d9d76fc32909b175a3ae22dbadedb63a5383 Mon Sep 17 00:00:00 2001 From: Samuel Giuseppe Schlesinger Date: Tue, 27 Oct 2026 11:21:44 -0400 Subject: [PATCH 04/12] feat(abstracts): bridge the unconditional native SAT endpoint MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Prepare #1338 against immutable native endpoint ec16665a461d6c0664b158b42ba75190bb4926e6. Replace the four pending Prop contracts with proved theorem statements and an acyclic direct bridge. The exact counting telescope is byte-identical modulo whitespace to the reviewed draft contract; all core definitions and the two-foundation allowlist remain unchanged. Preserve supplier credit and Samuel’s selected title. Validation: warning-as-error Lean checks of bridge, abstract and tests using independent copied artifacts with matching toolchain/dependency pins; audit 23 roots/140 dependencies; one uniform counter witness tested on empty, unused-variable, contradictory and invalid inputs. Existing native-definition controls pass. Renderer tests 23/23, staged four-theorem manifest and unchanged live 19/29 catalogue checks, mk_all, hygiene and changed-file checks pass. Source dependency integration, final outside review, catalogue promotion and #1227 follow-through remain held; no native implementation or ROADMAP edit. --- .../Abstracts/SubexponentialSATTests.lean | 14 +++- abstracts/ComplexityAbstracts.lean | 1 + .../SubexponentialSATAbstract.lean | 68 +++++++++--------- .../SubexponentialSATBridge.lean | 72 +++++++++++++++++++ abstracts/drafts/SubexponentialSAT.md | 35 ++++----- 5 files changed, 137 insertions(+), 53 deletions(-) create mode 100644 abstracts/ComplexityAbstracts/SubexponentialSATBridge.lean diff --git a/ComplexityTests/Abstracts/SubexponentialSATTests.lean b/ComplexityTests/Abstracts/SubexponentialSATTests.lean index 27946e529..cf6f95ce0 100644 --- a/ComplexityTests/Abstracts/SubexponentialSATTests.lean +++ b/ComplexityTests/Abstracts/SubexponentialSATTests.lean @@ -9,11 +9,11 @@ import Complexity.Computability.Complexity.FineGrained import Complexity.Computability.Complexity.FineGrained.CountingScale import Complexity.Logics.Propositional.CNF.ModelCount.Declared -/-! # Semantic checks for the pending subexponential SAT abstract +/-! # Semantic checks for the subexponential SAT abstract These checks identify the displayed definitions with the existing library interfaces and exercise -declared unused variables, empty cases and invalid inputs. They prove no counting algorithm or -refutation headline. The implementation imports are confined to this test module, outside the +declared unused variables, empty cases and invalid inputs. They also exercise the exact counter +theorem on valid, invalid and unused-variable inputs. The implementation imports stay outside the abstract's audited statement surface. -/ @@ -75,4 +75,12 @@ example : validDeclaredInput 1 1 [[(1, true)]] = false := by decide example : (encInput (3, [])).length = 7 := by decide example : numVars [[(100, true), (100, false)]] = 1 := by decide +-- One witness handles all these inputs: empty, unused-variable, contradictory and invalid. +example : ∃ count : Input → ℕ, + count (0, []) = 1 ∧ count (3, [[(0, true)]]) = 4 ∧ + count (1, [[(0, true)], [(0, false)]]) = 0 ∧ + count (1, [[(1, true)]]) = 0 ∧ count (1, [[(0, true), (0, true)]]) = 0 := by + obtain ⟨count, _, _, _, _, _, _, _, _, hcount, _, _⟩ := exact_count 1 + refine ⟨count, ?_, ?_, ?_, ?_, ?_⟩ <;> rw [hcount] <;> decide + end ComplexityTests.Abstracts.SubexponentialSATTests diff --git a/abstracts/ComplexityAbstracts.lean b/abstracts/ComplexityAbstracts.lean index 43940059b..465ab0653 100644 --- a/abstracts/ComplexityAbstracts.lean +++ b/abstracts/ComplexityAbstracts.lean @@ -41,6 +41,7 @@ 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 index 753019a4a..8ca030069 100644 --- a/abstracts/ComplexityAbstracts/SubexponentialSATAbstract.lean +++ b/abstracts/ComplexityAbstracts/SubexponentialSATAbstract.lean @@ -4,10 +4,11 @@ Released under Apache 2.0 license as described in the file LICENSE. Authors: OpenAI, Samuel Schlesinger, Anton Kovsharov -/ --- upstream: local-only (formal abstract draft; endpoint pending) +-- 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 @@ -15,30 +16,30 @@ import Mathlib.Data.Fintype.Pi /-! # Draft: OpenAI: the Exponential Time Hypothesis is false -**Unproved contracts, not headline theorems.** This draft prepares the formal abstract requested -in #1226. `ExactCounting`, `ETHRefutation`, `SETHRefutation`, and `ZeroSATExponents` below are -propositions describing the intended results; this file supplies no proof of any of them. There -is no bridge yet, and this draft is not selected in the public catalogue. In particular, a passing -`#check_abstract` checks the dependency boundary of these definitions, not their truth. +**Integration draft; catalogue publication pending.** The four theorems below are proved through +`SubexponentialSATBridge` from the unconditional native counting endpoint. This branch prepares +the formal abstract requested in #1226; dependency integration and outside review remain +publication prerequisites, and this draft is not selected in the public catalogue. -The intended primary result is one deterministic machine for each fixed clause width, counting -exactly over the declared variables. Its target running time is exponential in a constant times +The primary result is one deterministic machine for each fixed clause width, counting +exactly over the declared 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 original encoded -input length. Its target work space, including a separate charge for the encoded output, is +input length. Its work space, including a separate charge for the encoded output, is polynomial in that same external 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, and no private endpoint -preparation is imported. The native endpoint, its proof bridge, and outside source review must -be completed before these contracts can become catalogue theorems. +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. Once a bridge exists, Lean will check its proofs against these statements. +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 @@ -51,8 +52,8 @@ allowlisted. Once a bridge exists, Lean will check its proofs against these stat 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. This draft -does not claim authorship of those implementations. Construction provenance will be recorded in -the bridge when the unconditional endpoint is available. +does not claim authorship of those implementations. Construction provenance is recorded in +`SubexponentialSATBridge`. -/ namespace ComplexityAbstracts.SubexponentialSATAbstract @@ -146,7 +147,7 @@ def DecidableInExpTime {α : Type} (A : Set α) (enc : α ↪ List Bool) /-! ## The exponential time hypotheses The decision parameter is the number of distinct occurring variables, not the declared count -or the largest label. The intended bridge must therefore use the native dense-relabeling +or the largest label. The bridge therefore uses the native dense-relabeling correspondence. Zero infimum exponent alone does not assert a polynomial-time algorithm. -/ @@ -166,17 +167,16 @@ def ETH : Prop := def SETH : Prop := ∀ ε : ℝ, 0 < ε → ∃ k : ℕ, ¬DecidableInExpTime (KSAT k) encCNF numVars (1 - ε) -/-! ## Intended headline contracts — proofs pending +/-! ## Exact counting and the exponential time hypotheses -All declarations in this section are definitions of propositions, not theorems. The primary -contract fixes the counter, time and space functions, constants and native machine for each `k` -before every input. It includes `k = 0, 1`, `n = 0`, empty formulas and empty clauses. Invalid -width or variable-range inputs return zero. In particular, a valid empty formula returns `2^n`, -including one assignment when `n = 0`; unused declared variables remain free choices. +The primary theorem fixes the counter, time and space functions, constants and native machine +for each `k` before every input. It includes `k = 0, 1`, `n = 0`, empty formulas and empty clauses. +Invalid width or variable-range inputs return zero. In particular, a valid empty formula returns +`2^n`, including one assignment when `n = 0`; unused declared variables remain free choices. 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 future proof uses width `max 2 k` internally while retaining the +exponent of Theorem 1.1. The proof uses width `max 2 k` internally while retaining the original width guard, one inner support normalization and one outer declared-variable correction. Those proof details do not weaken the total external contract. -/ @@ -185,31 +185,33 @@ Those proof details do not weaken the total external contract. noncomputable def interpolationScale (n : ℕ) : ℝ := n * Real.log (Real.log ((n : ℝ) + 16)) ^ 2 / Real.sqrt (Real.log ((n : ℝ) + 16)) -/-- Pending primary claim: one exact native counter per fixed width, with interpolation-scale +/-- One exact native counter per fixed width, with interpolation-scale time and polynomial space in the length of the original declared input. -/ -def ExactCounting : Prop := +theorem exact_count : ∀ k : ℕ, ∃ (count : Input → ℕ) (T S : Input → ℕ) (A c e a b : ℕ), Turing.MultiTapeTM.ComputableInO count encInput ComplexityTests.Abstracts.Encoding.encNat T S ∧ (∀ x, count x = if validDeclaredInput k x.1 x.2 then modelCountOn x.2 x.1 else 0) ∧ (∀ x, (T x : ℝ) ≤ c * ((2 : ℝ) ^ ((A : ℝ) * interpolationScale x.1) * (((encInput x).length : ℝ) + 1) ^ e) + c) ∧ - (∀ x, S x ≤ a * ((encInput x).length + 1) ^ b) + (∀ x, S x ≤ a * ((encInput x).length + 1) ^ b) := + SubexponentialSATBridge.exact_count -/-- Pending headline: the exponential time hypothesis is false. -/ -def ETHRefutation : Prop := ¬ETH +/-- The exponential time hypothesis is false. -/ +theorem not_eth : ¬ETH := SubexponentialSATBridge.not_eth -/-- Pending headline: the strong exponential time hypothesis is false. -/ -def SETHRefutation : Prop := ¬SETH +/-- The strong exponential time hypothesis is false. -/ +theorem not_seth : ¬SETH := SubexponentialSATBridge.not_seth -/-- Pending headline: every fixed-width SAT exponent is zero. -/ -def ZeroSATExponents : Prop := ∀ k, satExponent k = 0 +/-- 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`: -23 root declarations, 138 dependencies checked +23 root declarations, 140 dependencies checked -/ #guard_msgs (whitespace := lax) in #check_abstract ComplexityAbstracts.SubexponentialSATAbstract allowing [ diff --git a/abstracts/ComplexityAbstracts/SubexponentialSATBridge.lean b/abstracts/ComplexityAbstracts/SubexponentialSATBridge.lean new file mode 100644 index 000000000..82b52b0d3 --- /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 + +/-! # 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, declared-range 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. All resource charges refer to the +original external encoding. + +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 complete native counter contract on the abstract's underlying list representation. -/ +theorem exact_count (k : ℕ) : + ∃ (count : ℕ × List (List (ℕ × Bool)) → ℕ) + (T S : ℕ × List (List (ℕ × Bool)) → ℕ) (A c e a b : ℕ), + ComputableInO count (encPair encUnary encCNF) encNat T S ∧ + (∀ x, count x = if CNF.validDeclaredInput k x.1 x.2 then + CNF.modelCountOn x.2 (Finset.range x.1) else 0) ∧ + (∀ x, (T x : ℝ) ≤ c * + ((2 : ℝ) ^ ((A : ℝ) * SubexponentialSAT.interpolationScale x.1) * + (((encPair encUnary encCNF x).length : ℝ) + 1) ^ e) + c) ∧ + (∀ x, S x ≤ a * ((encPair encUnary encCNF x).length + 1) ^ b) := + CountingNativeEndpoint.exists_declaredCounter 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/drafts/SubexponentialSAT.md b/abstracts/drafts/SubexponentialSAT.md index 851676f3b..b9242cba5 100644 --- a/abstracts/drafts/SubexponentialSAT.md +++ b/abstracts/drafts/SubexponentialSAT.md @@ -3,13 +3,15 @@ This is staging material for [#1226](https://github.com/cslib-community/complexitylib/issues/1226), not an entry in the selected catalogue. Samuel selected the title below in [#587](https://github.com/cslib-community/complexitylib/issues/587#issuecomment-6445129935). The -[draft abstract](../ComplexityAbstracts/SubexponentialSATAbstract.lean) defines the intended -contracts as propositions; it does not prove them. Its audit verifies only their dependency -boundary. No PDF for these claims is published. +[integration draft](../ComplexityAbstracts/SubexponentialSATAbstract.lean) now states the four +theorems through [its bridge](../ComplexityAbstracts/SubexponentialSATBridge.lean), consuming the +unconditional native endpoint. Its audit verifies the statement dependency boundary; Lean checks +the proofs. No PDF for these claims is published. -The proposed entry below is for use **after** the unconditional native endpoint and bridge are -checked and independently reviewed. The proposed theorem names are deliberately absent today; -the catalogue validator must reject selecting the draft propositions as headline theorems. +The proposed entry below is for use **after** the source dependencies and endpoint have landed, +the bridge has been validated on that source, and outside review and the required final checks +are complete. The theorem names now exist in this integration preparation, but the live +catalogue and the #1227 note remain unchanged. ```json { @@ -28,25 +30,24 @@ the catalogue validator must reject selecting the draft propositions as headline } ``` -Proposed README selection row, pending the endpoint: +Proposed README selection row, pending integration and review: | Result | Model and scope | | --- | --- | | [OpenAI: the Exponential Time Hypothesis is false](../ComplexityAbstracts/SubexponentialSATAbstract.lean) | One fixed native machine per width, exact declared-variable counts, and interpolation-scale time with polynomial overhead and polynomial space in the original external encoded input length; all SAT exponents zero and ETH/SETH false. §§3–6 and Proposition 6.4, not the sharper Theorem 1.1 / Appendix D bound. | -Before promotion, discharge the four concrete branch obligations recorded in #1226: the native -branch certificate, feasible-branch exactness, global polynomial branch space, and the branch -polylogarithmic time bound. Then prove the unconditional native endpoint, add the bridge with -construction provenance, and replace the four pending proposition definitions by the four -proved theorem statements, displaying the full exact-count telescope. Recheck the guard and -native-definition correspondence tests, add the entry to `catalogue.json`, move the row into -the README selection (adjusting its relative link), and build and inspect the generated PDFs. -Delete this staging file in that same promotion. Only then can the #1227 note change from +The endpoint checkpoint discharges the native branch certificate, feasible-branch exactness, +global polynomial branch space and branch polylogarithmic time obligations; the bridge imports +its public theorems, with no supplier assumptions. Before promotion, integrate the pending source +dependencies and endpoint, validate this bridge on the landed source, and obtain outside review +and the required final checks. Then add the entry to `catalogue.json`, move the row into the README +selection (adjusting its relative link), and build and inspect the generated PDFs. Delete this +staging file in that same promotion. Only then can the #1227 note change from “claimed” to “proved in this library”, linking the new abstract; whether the conditional entry remains is Samuel's decision. Source: OpenAI, *The Exponential Time Hypothesis is False*, revised 25 October 2026, [Proposition 6.4, pp. 43–44](https://github.com/openai/math/blob/7ef5c0cc5ca4b0e072b7a050fca09ab24bc6fa3a/preprints/The-Exponential-Time-Hypothesis-is-False-October-25-2026/paper.pdf). The draft uses the accepted native join's original-input accounting and declared-range semantics, -including small sizes and width lifting. It does not import the private join or introduce a -conditional replacement headline. +including small sizes and width lifting. The bridge imports the public unconditional endpoint, +not the earlier private join, and introduces no conditional replacement headline. From 3fc0471381bd5b16844705530f25bd4104e55e54 Mon Sep 17 00:00:00 2001 From: Samuel Giuseppe Schlesinger Date: Tue, 27 Oct 2026 11:58:30 -0400 Subject: [PATCH 05/12] feat(abstracts): promote the proved native SAT counting endpoint --- .../SubexponentialSATAbstract.lean | 12 ++--- abstracts/README.md | 5 +- abstracts/catalogue.json | 18 ++++++- abstracts/drafts/SubexponentialSAT.md | 53 ------------------- 4 files changed, 25 insertions(+), 63 deletions(-) delete mode 100644 abstracts/drafts/SubexponentialSAT.md diff --git a/abstracts/ComplexityAbstracts/SubexponentialSATAbstract.lean b/abstracts/ComplexityAbstracts/SubexponentialSATAbstract.lean index 8ca030069..f24cf5379 100644 --- a/abstracts/ComplexityAbstracts/SubexponentialSATAbstract.lean +++ b/abstracts/ComplexityAbstracts/SubexponentialSATAbstract.lean @@ -14,12 +14,10 @@ import Mathlib.Analysis.SpecialFunctions.Pow.Real import Mathlib.Analysis.SpecialFunctions.Sqrt import Mathlib.Data.Fintype.Pi -/-! # Draft: OpenAI: the Exponential Time Hypothesis is false +/-! # OpenAI: the Exponential Time Hypothesis is false -**Integration draft; catalogue publication pending.** The four theorems below are proved through -`SubexponentialSATBridge` from the unconditional native counting endpoint. This branch prepares -the formal abstract requested in #1226; dependency integration and outside review remain -publication prerequisites, and this draft is not selected in the public catalogue. +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, counting exactly over the declared variables. Its running time is exponential in a constant times @@ -51,8 +49,8 @@ of the definitions and theorem statements, not their English interpretation. 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. This draft -does not claim authorship of those implementations. Construction provenance is recorded in +machine and encoding foundations include Christian Reitwiessner's contributions. +Construction provenance is recorded in `SubexponentialSATBridge`. -/ diff --git a/abstracts/README.md b/abstracts/README.md index cb15a97f6..fbb126590 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 declared-variable counts, and interpolation-scale time with polynomial overhead and polynomial space in the original external encoded input 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..a7e359774 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, declared-variable counts, unary declared size 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, with polynomial time overhead and polynomial workspace charged to the original external input length. Includes all fixed widths and sizes, and rejects invalid declared inputs. 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", diff --git a/abstracts/drafts/SubexponentialSAT.md b/abstracts/drafts/SubexponentialSAT.md deleted file mode 100644 index b9242cba5..000000000 --- a/abstracts/drafts/SubexponentialSAT.md +++ /dev/null @@ -1,53 +0,0 @@ -# Pending catalogue proposal: subexponential SAT - -This is staging material for [#1226](https://github.com/cslib-community/complexitylib/issues/1226), -not an entry in the selected catalogue. Samuel selected the title below in -[#587](https://github.com/cslib-community/complexitylib/issues/587#issuecomment-6445129935). The -[integration draft](../ComplexityAbstracts/SubexponentialSATAbstract.lean) now states the four -theorems through [its bridge](../ComplexityAbstracts/SubexponentialSATBridge.lean), consuming the -unconditional native endpoint. Its audit verifies the statement dependency boundary; Lean checks -the proofs. No PDF for these claims is published. - -The proposed entry below is for use **after** the source dependencies and endpoint have landed, -the bridge has been validated on that source, and outside review and the required final checks -are complete. The theorem names now exist in this integration preparation, but the live -catalogue and the #1227 note remain unchanged. - -```json -{ - "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, declared-variable counts, unary declared size 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, with polynomial time overhead and polynomial workspace charged to the original external input length. Includes all fixed widths and sizes, and rejects invalid declared inputs. This does not establish the sharper Theorem 1.1 / Appendix D bound.", - "foundations": ["ComplexityAbstracts.Encoding"] -} -``` - -Proposed README selection row, pending integration and review: - -| Result | Model and scope | -| --- | --- | -| [OpenAI: the Exponential Time Hypothesis is false](../ComplexityAbstracts/SubexponentialSATAbstract.lean) | One fixed native machine per width, exact declared-variable counts, and interpolation-scale time with polynomial overhead and polynomial space in the original external encoded input length; all SAT exponents zero and ETH/SETH false. §§3–6 and Proposition 6.4, not the sharper Theorem 1.1 / Appendix D bound. | - -The endpoint checkpoint discharges the native branch certificate, feasible-branch exactness, -global polynomial branch space and branch polylogarithmic time obligations; the bridge imports -its public theorems, with no supplier assumptions. Before promotion, integrate the pending source -dependencies and endpoint, validate this bridge on the landed source, and obtain outside review -and the required final checks. Then add the entry to `catalogue.json`, move the row into the README -selection (adjusting its relative link), and build and inspect the generated PDFs. Delete this -staging file in that same promotion. Only then can the #1227 note change from -“claimed” to “proved in this library”, linking the new abstract; whether the conditional entry -remains is Samuel's decision. - -Source: OpenAI, *The Exponential Time Hypothesis is False*, revised 25 October 2026, -[Proposition 6.4, pp. 43–44](https://github.com/openai/math/blob/7ef5c0cc5ca4b0e072b7a050fca09ab24bc6fa3a/preprints/The-Exponential-Time-Hypothesis-is-False-October-25-2026/paper.pdf). -The draft uses the accepted native join's original-input accounting and declared-range semantics, -including small sizes and width lifting. The bridge imports the public unconditional endpoint, -not the earlier private join, and introduces no conditional replacement headline. From 4cbd3e02eb1fdbfb767883c1c00d4cde5731ad7f Mon Sep 17 00:00:00 2001 From: Samuel Giuseppe Schlesinger Date: Tue, 27 Oct 2026 11:59:03 -0400 Subject: [PATCH 06/12] style(FineGrained): wrap native endpoint lines --- .../Complexity/FineGrained/CountingNativeEndpoint.lean | 9 ++++++--- 1 file changed, 6 insertions(+), 3 deletions(-) diff --git a/Complexity/Computability/Complexity/FineGrained/CountingNativeEndpoint.lean b/Complexity/Computability/Complexity/FineGrained/CountingNativeEndpoint.lean index 77215c30f..4eac114d4 100644 --- a/Complexity/Computability/Complexity/FineGrained/CountingNativeEndpoint.lean +++ b/Complexity/Computability/Complexity/FineGrained/CountingNativeEndpoint.lean @@ -83,7 +83,8 @@ private abbrev encFullInput := encPair encUnit encInput private def inputSize (x : Input) : ℕ := (encInput x).length private def width (k : ℕ) : ℕ := max 2 k private def divisor (p : Context) : ℕ := BranchedSparseCNFCounter.leafSearchDivisor p.2 -private def thresholdBase (k : ℕ) (p : Context) : ℕ := BranchedSparseCNFCounter.leafThresholdBase k p.2 +private def thresholdBase (k : ℕ) (p : Context) : ℕ := + BranchedSparseCNFCounter.leafThresholdBase k p.2 private def depthCoeff (k : ℕ) (p : Context) : ℕ := countingDepthCoeff (width k) (thresholdBase k p) private def prepare (x : Input) : FullInput := ((), x) @@ -142,7 +143,8 @@ private theorem computableInPolyTime_prepare : unfold prepare fun_prop -private theorem length_prepare (x : Input) : (encFullInput (prepare x)).length = inputSize x + 1 := by +private theorem length_prepare (x : Input) : + (encFullInput (prepare x)).length = inputSize x + 1 := by simp [encFullInput, prepare, inputSize, encUnit_apply] private theorem length_leaf_input (N : ℕ) (ψ : CNF ℕ) : @@ -499,7 +501,8 @@ private theorem selected_time_envelope (k d c e Cₜ dₜ Aₜ : ℕ) : have hP : PolyBounded inputSize P := (((((PolyBounded.self.add (.const 1)).pow d).add (hW.comp computableInPolyTime_prepare.polyBounded_length)).add - (hU.comp computableInPolyTime_prepare.polyBounded_length)).add (.const 1)).add PolyBounded.self + (hU.comp computableInPolyTime_prepare.polyBounded_length)).add (.const 1)).add + PolyBounded.self obtain ⟨Cₚ, E, hP⟩ := hP.exists_le obtain ⟨Cq, _, hq⟩ := exists_clamped_rounds_le_interpolationScale refine ⟨(Cq + 1) * Cₚ, E, fun x => ?_⟩ From 31a267f414c7eb353e35ae819a20498f3031b3da Mon Sep 17 00:00:00 2001 From: Samuel Giuseppe Schlesinger Date: Tue, 27 Oct 2026 12:12:22 -0400 Subject: [PATCH 07/12] doc(FineGrained): point to the native counting endpoint --- Complexity/Computability/Complexity/FineGrained.lean | 5 +++++ 1 file changed, 5 insertions(+) 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`, From b038f18593efddc2164d758974053c70f8568b47 Mon Sep 17 00:00:00 2001 From: Samuel Giuseppe Schlesinger Date: Tue, 27 Oct 2026 12:33:13 -0400 Subject: [PATCH 08/12] doc(Circuit): fix sibling module link for site publication --- .../Computability/Circuit/Monotone/Clique/Asymptotic.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) 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. From c215ae6eea1cccb7c5b07add57e0cf85323db9a2 Mon Sep 17 00:00:00 2001 From: Christian Reitwiessner Date: Tue, 27 Oct 2026 16:46:33 +0000 Subject: [PATCH 09/12] doc(abstracts): readable exact_count for the ETH abstract (#1338) State the counter on the plain formula, with exact `modelCount` over the occurring variables on every width-`k` formula and resources folded into `ComputableInO`. Replace `modelCountOn`, `validDeclaredInput`, `Input` and `encInput` in the abstract by `modelCount` and `HasWidth`; transfer through `CountingNativeEndpoint.exists_modelCounter`. Update the tests, catalogue scope and README row accordingly. Co-Authored-By: Claude Opus 5.5 (cherry picked from commit 4dd5ade550e005719619abac9c765b3f5755850f) --- .../Abstracts/SubexponentialSATTests.lean | 54 +++++------- .../SubexponentialSATAbstract.lean | 85 ++++++++----------- .../SubexponentialSATBridge.lean | 28 +++--- abstracts/README.md | 2 +- abstracts/catalogue.json | 2 +- 5 files changed, 71 insertions(+), 100 deletions(-) diff --git a/ComplexityTests/Abstracts/SubexponentialSATTests.lean b/ComplexityTests/Abstracts/SubexponentialSATTests.lean index cf6f95ce0..9eef948f5 100644 --- a/ComplexityTests/Abstracts/SubexponentialSATTests.lean +++ b/ComplexityTests/Abstracts/SubexponentialSATTests.lean @@ -7,14 +7,13 @@ Authors: Samuel Schlesinger import ComplexityAbstracts.SubexponentialSATAbstract import Complexity.Computability.Complexity.FineGrained import Complexity.Computability.Complexity.FineGrained.CountingScale -import Complexity.Logics.Propositional.CNF.ModelCount.Declared +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 -declared unused variables, empty cases and invalid inputs. They also exercise the exact counter -theorem on valid, invalid and unused-variable inputs. The implementation imports stay outside the -abstract's audited statement surface. +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 @@ -27,17 +26,12 @@ example (φ : Formula) : Satisfiable φ ↔ Cslib.Logic.PL.CNF.Satisfiable φ := example (φ : Formula) : numVars φ = Cslib.Logic.PL.CNF.numVars φ := rfl -example (φ : Formula) (n : ℕ) : - modelCountOn φ n = Cslib.Logic.PL.CNF.modelCountOn φ (Finset.range n) := rfl +example (φ : Formula) : modelCount φ = Cslib.Logic.PL.CNF.modelCount φ := rfl -example (k n : ℕ) (φ : Formula) : - validDeclaredInput k n φ = Cslib.Logic.PL.CNF.validDeclaredInput k n φ := rfl +example (k : ℕ) (φ : Formula) : HasWidth k φ ↔ ∀ c ∈ φ, c.length ≤ k := Iff.rfl example : encCNF = Cslib.Complexity.encCNF := rfl -example : encInput = Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encUnary - Cslib.Complexity.encCNF := rfl - example {α : Type} (A : Set α) (enc : α ↪ List Bool) (T : α → ℝ) : DecidableInTimeO A enc T ↔ Cslib.Complexity.DecidableInTimeO A enc T := Iff.rfl @@ -55,32 +49,22 @@ example : SETH ↔ Cslib.Complexity.SETH := Iff.rfl example (n : ℕ) : interpolationScale n = Cslib.Complexity.SubexponentialSAT.interpolationScale n := rfl --- Empty formulas retain all declared free variables; the empty assignment is counted once. -example : modelCountOn [] 0 = 1 := by decide -example : modelCountOn [] 3 = 8 := by decide - --- An empty clause is unsatisfiable, while a single positive literal leaves two variables free. -example : modelCountOn [[]] 3 = 0 := by decide -example : modelCountOn [[(0, true)]] 3 = 4 := by decide -example : modelCountOn [[(0, true)], [(0, false)]] 3 = 0 := by decide - --- Both halves of validity matter, including repetition in the clause-width convention. -example : validDeclaredInput 0 0 [] = true := by decide -example : validDeclaredInput 0 0 [[]] = true := by decide -example : validDeclaredInput 1 1 [[(0, true)]] = true := by decide -example : validDeclaredInput 1 1 [[(0, true), (0, true)]] = false := by decide -example : validDeclaredInput 1 1 [[(1, true)]] = false := by decide +-- 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 --- The declared unary header survives even on an empty formula. -example : (encInput (3, [])).length = 7 := 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 handles all these inputs: empty, unused-variable, contradictory and invalid. -example : ∃ count : Input → ℕ, - count (0, []) = 1 ∧ count (3, [[(0, true)]]) = 4 ∧ - count (1, [[(0, true)], [(0, false)]]) = 0 ∧ - count (1, [[(1, true)]]) = 0 ∧ count (1, [[(0, true), (0, true)]]) = 0 := by - obtain ⟨count, _, _, _, _, _, _, _, _, hcount, _, _⟩ := exact_count 1 - refine ⟨count, ?_, ?_, ?_, ?_, ?_⟩ <;> rw [hcount] <;> 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/SubexponentialSATAbstract.lean b/abstracts/ComplexityAbstracts/SubexponentialSATAbstract.lean index f24cf5379..8510a513c 100644 --- a/abstracts/ComplexityAbstracts/SubexponentialSATAbstract.lean +++ b/abstracts/ComplexityAbstracts/SubexponentialSATAbstract.lean @@ -19,11 +19,12 @@ import Mathlib.Data.Fintype.Pi 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, counting -exactly over the declared 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 original encoded -input length. Its work space, including a separate charge for the encoded output, is -polynomial in that same external length. This is the interpolation-scale route of Sections 3–6 and +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; @@ -56,7 +57,7 @@ Construction provenance is recorded in namespace ComplexityAbstracts.SubexponentialSATAbstract -/-! ## Formulas and declared-variable counting +/-! ## Formulas and model counting A literal `(v, b)` asserts that variable `v` has Boolean value `b`. Clauses are disjunctions and formulas are conjunctions; repeated literals and clauses are permitted. A width bound @@ -79,27 +80,20 @@ def vars (φ : Formula) : List ℕ := φ.flatten.map Prod.fst /-- The number of distinct occurring variables, independent of their numeric labels. -/ def numVars (φ : Formula) : ℕ := (vars φ).toFinset.card -/-- Count satisfying assignments on the declared range `{0, …, n - 1}`, extending by `false` -outside it. Valid inputs below require every occurring variable to lie in that range. -/ -def modelCountOn (φ : Formula) (n : ℕ) : ℕ := - (Finset.univ.filter fun σ : (Finset.range n) → Bool => - eval φ (fun v => if h : v ∈ Finset.range n then σ ⟨v, h⟩ else false) = true).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 -/-- The input has clauses of width at most `k`, with every variable strictly below `n`. -/ -def validDeclaredInput (k n : ℕ) (φ : Formula) : Bool := - (φ.all fun clause => decide (clause.length ≤ k)) && - ((vars φ).all fun v => decide (v < n)) - -/-- A declared counting instance consists of its variable count and formula. -/ -abbrev Input := ℕ × Formula +/-- Every clause of `φ` has at most `k` literals. -/ +def HasWidth (k : ℕ) (φ : Formula) : Prop := ∀ clause ∈ φ, clause.length ≤ k /-! ## Representation details -The external input is `encPair encUnary encCNF (n, φ)`. Its length is -`2 * n + 1 + (encCNF φ).length`, so even an empty formula retains the cost of its declared -variables. 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. +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 @@ -109,10 +103,6 @@ def encCNF : Formula ↪ List Bool := (ComplexityTests.Abstracts.Encoding.encPair ComplexityTests.Abstracts.Encoding.encNat ComplexityTests.Abstracts.Encoding.encBool)) -/-- Frame the unary declared-variable count, then append the encoded formula. -/ -def encInput : Input ↪ List Bool := - ComplexityTests.Abstracts.Encoding.encPair ComplexityTests.Abstracts.Encoding.encUnary encCNF - /-! ## Deterministic machine and resource conventions The upstream model is a deterministic binary multi-tape Turing machine with finitely many @@ -144,9 +134,9 @@ def DecidableInExpTime {α : Type} (A : Set α) (enc : α ↪ List Bool) /-! ## The exponential time hypotheses -The decision parameter is the number of distinct occurring variables, not the declared count -or the largest label. The bridge therefore uses the native dense-relabeling -correspondence. Zero infimum exponent alone does not assert a polynomial-time algorithm. +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. -/ @@ -167,33 +157,30 @@ def SETH : Prop := /-! ## Exact counting and the exponential time hypotheses -The primary theorem fixes the counter, time and space functions, constants and native machine -for each `k` before every input. It includes `k = 0, 1`, `n = 0`, empty formulas and empty clauses. -Invalid width or variable-range inputs return zero. In particular, a valid empty formula returns -`2^n`, including one assignment when `n = 0`; unused declared variables remain free choices. +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 uses width `max 2 k` internally while retaining the -original width guard, one inner support normalization and one outer declared-variable correction. -Those proof details do not weaken the total external contract. +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)) -/-- One exact native counter per fixed width, with interpolation-scale -time and polynomial space in the length of the original declared input. -/ -theorem exact_count : - ∀ k : ℕ, ∃ (count : Input → ℕ) (T S : Input → ℕ) (A c e a b : ℕ), - Turing.MultiTapeTM.ComputableInO count encInput - ComplexityTests.Abstracts.Encoding.encNat T S ∧ - (∀ x, count x = if validDeclaredInput k x.1 x.2 then modelCountOn x.2 x.1 else 0) ∧ - (∀ x, (T x : ℝ) ≤ c * ((2 : ℝ) ^ ((A : ℝ) * interpolationScale x.1) * - (((encInput x).length : ℝ) + 1) ^ e) + c) ∧ - (∀ x, S x ≤ a * ((encInput x).length + 1) ^ b) := - SubexponentialSATBridge.exact_count +/-- For each fixed width `k`, one machine counts the satisfying assignments of every width-`k` +formula in time `2 ^ (A · n (log log n)² / √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 @@ -209,7 +196,7 @@ end ComplexityAbstracts.SubexponentialSATAbstract /-- info: abstract audit passed for `ComplexityAbstracts.SubexponentialSATAbstract`: -23 root declarations, 140 dependencies checked +21 root declarations, 135 dependencies checked -/ #guard_msgs (whitespace := lax) in #check_abstract ComplexityAbstracts.SubexponentialSATAbstract allowing [ diff --git a/abstracts/ComplexityAbstracts/SubexponentialSATBridge.lean b/abstracts/ComplexityAbstracts/SubexponentialSATBridge.lean index 82b52b0d3..4d6a9e070 100644 --- a/abstracts/ComplexityAbstracts/SubexponentialSATBridge.lean +++ b/abstracts/ComplexityAbstracts/SubexponentialSATBridge.lean @@ -7,11 +7,12 @@ 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, declared-range count, encoding combinators, fine-grained +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 @@ -25,8 +26,9 @@ bounded-incidence evaluator with its exactness and independent native time/works 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. All resource charges refer to the -original external encoding. +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 @@ -46,18 +48,16 @@ namespace ComplexityAbstracts.SubexponentialSATBridge open Cslib.Complexity Cslib.Logic.PL Turing.MultiTapeTM -/-- The complete native counter contract on the abstract's underlying list representation. -/ +/-- The bounded-width model counter on the abstract's underlying list representation. -/ theorem exact_count (k : ℕ) : - ∃ (count : ℕ × List (List (ℕ × Bool)) → ℕ) - (T S : ℕ × List (List (ℕ × Bool)) → ℕ) (A c e a b : ℕ), - ComputableInO count (encPair encUnary encCNF) encNat T S ∧ - (∀ x, count x = if CNF.validDeclaredInput k x.1 x.2 then - CNF.modelCountOn x.2 (Finset.range x.1) else 0) ∧ - (∀ x, (T x : ℝ) ≤ c * - ((2 : ℝ) ^ ((A : ℝ) * SubexponentialSAT.interpolationScale x.1) * - (((encPair encUnary encCNF x).length : ℝ) + 1) ^ e) + c) ∧ - (∀ x, S x ≤ a * ((encPair encUnary encCNF x).length + 1) ^ b) := - CountingNativeEndpoint.exists_declaredCounter 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 diff --git a/abstracts/README.md b/abstracts/README.md index fbb126590..3570835c9 100644 --- a/abstracts/README.md +++ b/abstracts/README.md @@ -49,7 +49,7 @@ 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. | -| [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 declared-variable counts, and interpolation-scale time with polynomial overhead and polynomial space in the original external encoded input length; all SAT exponents zero and ETH/SETH false. §§3–6 and Proposition 6.4, not the sharper Theorem 1.1 / Appendix D bound. | +| [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. | diff --git a/abstracts/catalogue.json b/abstracts/catalogue.json index a7e359774..7767a945b 100644 --- a/abstracts/catalogue.json +++ b/abstracts/catalogue.json @@ -241,7 +241,7 @@ "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, declared-variable counts, unary declared size 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, with polynomial time overhead and polynomial workspace charged to the original external input length. Includes all fixed widths and sizes, and rejects invalid declared inputs. This does not establish the sharper Theorem 1.1 / Appendix D bound.", + "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" ] From e9995c02c81d1959c135d43a26eef9219241ed46 Mon Sep 17 00:00:00 2001 From: Samuel Giuseppe Schlesinger Date: Tue, 27 Oct 2026 13:05:28 -0400 Subject: [PATCH 10/12] doc(abstracts): use renderer-safe square-root notation --- abstracts/ComplexityAbstracts/SubexponentialSATAbstract.lean | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/abstracts/ComplexityAbstracts/SubexponentialSATAbstract.lean b/abstracts/ComplexityAbstracts/SubexponentialSATAbstract.lean index 8510a513c..7939eb3c4 100644 --- a/abstracts/ComplexityAbstracts/SubexponentialSATAbstract.lean +++ b/abstracts/ComplexityAbstracts/SubexponentialSATAbstract.lean @@ -172,8 +172,8 @@ 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)² / √log n) · poly(L)` and space `poly(L)`, where `n` is the -number of variables and `L` the encoding length. -/ +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 φ) ∧ From 5e896c20e2c0f7737763ac4487ea34429fefebb9 Mon Sep 17 00:00:00 2001 From: Christian Reitwiessner Date: Tue, 27 Oct 2026 17:08:56 +0000 Subject: [PATCH 11/12] doc(abstracts): name literal components in the ETH abstract (#1338) Introduce `Literal` with `Literal.var` and `Literal.positive`, and the `Clause` abbreviation, so that `eval` and `vars` no longer use `.1`, `.2` and `Prod.fst`. All are abbreviations of the existing pair representation, so the displayed definitions stay definitionally equal to the library and the encoding is unchanged. Co-Authored-By: Claude Opus 5.5 (cherry picked from commit 090f36fe09a5c084c6dcb6ad24bfd67c286e196d) --- .../Abstracts/SubexponentialSATTests.lean | 2 ++ .../SubexponentialSATAbstract.lean | 31 +++++++++++++------ 2 files changed, 24 insertions(+), 9 deletions(-) diff --git a/ComplexityTests/Abstracts/SubexponentialSATTests.lean b/ComplexityTests/Abstracts/SubexponentialSATTests.lean index 9eef948f5..6e889b072 100644 --- a/ComplexityTests/Abstracts/SubexponentialSATTests.lean +++ b/ComplexityTests/Abstracts/SubexponentialSATTests.lean @@ -20,6 +20,8 @@ namespace ComplexityTests.Abstracts.SubexponentialSATTests open ComplexityAbstracts.SubexponentialSATAbstract +example (l : Literal) : l = (l.var, l.positive) := rfl + example (φ : Formula) (σ : ℕ → Bool) : eval φ σ = Cslib.Logic.PL.CNF.eval σ φ := rfl example (φ : Formula) : Satisfiable φ ↔ Cslib.Logic.PL.CNF.Satisfiable φ := Iff.rfl diff --git a/abstracts/ComplexityAbstracts/SubexponentialSATAbstract.lean b/abstracts/ComplexityAbstracts/SubexponentialSATAbstract.lean index 7939eb3c4..ee100402a 100644 --- a/abstracts/ComplexityAbstracts/SubexponentialSATAbstract.lean +++ b/abstracts/ComplexityAbstracts/SubexponentialSATAbstract.lean @@ -59,23 +59,36 @@ namespace ComplexityAbstracts.SubexponentialSATAbstract /-! ## Formulas and model counting -A literal `(v, b)` asserts that variable `v` has Boolean value `b`. Clauses are disjunctions -and formulas are conjunctions; repeated literals and clauses are permitted. A width bound -counts literal occurrences, including repetitions. +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 CNF formula is a list of clauses, each a list of variable/polarity pairs. -/ -abbrev Formula := List (List (ℕ × Bool)) +/-- A literal: the variable `var`, positive or negated. It is the pair `(var, positive)`. -/ +abbrev Literal := ℕ × Bool -/-- Evaluate a formula: every clause must contain a literal of the assigned polarity. -/ +/-- 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.1 == literal.2 + φ.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 Prod.fst +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 @@ -196,7 +209,7 @@ end ComplexityAbstracts.SubexponentialSATAbstract /-- info: abstract audit passed for `ComplexityAbstracts.SubexponentialSATAbstract`: -21 root declarations, 135 dependencies checked +25 root declarations, 139 dependencies checked -/ #guard_msgs (whitespace := lax) in #check_abstract ComplexityAbstracts.SubexponentialSATAbstract allowing [ From b75a280810977c3b04af888cd0d718b728617206 Mon Sep 17 00:00:00 2001 From: Samuel Giuseppe Schlesinger Date: Tue, 27 Oct 2026 13:12:14 -0400 Subject: [PATCH 12/12] test(abstracts): retain semantic controls without redundant literal eta example --- ComplexityTests/Abstracts/SubexponentialSATTests.lean | 2 -- 1 file changed, 2 deletions(-) diff --git a/ComplexityTests/Abstracts/SubexponentialSATTests.lean b/ComplexityTests/Abstracts/SubexponentialSATTests.lean index 6e889b072..9eef948f5 100644 --- a/ComplexityTests/Abstracts/SubexponentialSATTests.lean +++ b/ComplexityTests/Abstracts/SubexponentialSATTests.lean @@ -20,8 +20,6 @@ namespace ComplexityTests.Abstracts.SubexponentialSATTests open ComplexityAbstracts.SubexponentialSATAbstract -example (l : Literal) : l = (l.var, l.positive) := rfl - example (φ : Formula) (σ : ℕ → Bool) : eval φ σ = Cslib.Logic.PL.CNF.eval σ φ := rfl example (φ : Formula) : Satisfiable φ ↔ Cslib.Logic.PL.CNF.Satisfiable φ := Iff.rfl