From eb391585ee86a5bda3a8f10d7d04c97440661731 Mon Sep 17 00:00:00 2001 From: Samuel Giuseppe Schlesinger Date: Fri, 30 Oct 2026 17:14:48 -0400 Subject: [PATCH] doc(fine-grained): note that ETH- and SETH-conditional results are vacuous MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit The library proves `¬ETH` and `¬SETH` (`Cslib.Complexity.CountingNativeEndpoint.not_ETH`, `not_SETH`), but the module docstrings of the ETH-conditional lower bounds (graph problems, Bipartite Permutation Independent Set, Partial MCSP, linear-size reductions) and of `OVH_of_SETH` still present them as hardness results without saying that their premise is refuted. Add one short paragraph to each module stating that the conditional statements hold vacuously and naming which parts (the reductions, size bounds and equivalences) remain unconditional. This follows the note already on the Partial MCSP catalogue entry (#1227) and in `FineGrained.lean`. Documentation only: no statement, definition or abstract changes. From the misformalization audit by auditor-claude-e6cf7b0d-1. Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_015DLg8kwPs8yi7ePPdtoNvG --- .../Computability/Complexity/FineGrained/GraphProblems.lean | 4 ++++ .../Complexity/FineGrained/OrthogonalVectors.lean | 5 +++++ .../Complexity/FineGrained/PermutationIndependentSet.lean | 4 ++++ .../Computability/Complexity/FineGrained/Reduction.lean | 3 +++ Complexity/Computability/MCSP/PartialETH.lean | 5 +++++ 5 files changed, 21 insertions(+) diff --git a/Complexity/Computability/Complexity/FineGrained/GraphProblems.lean b/Complexity/Computability/Complexity/FineGrained/GraphProblems.lean index b39118544..3714cce73 100644 --- a/Complexity/Computability/Complexity/FineGrained/GraphProblems.lean +++ b/Complexity/Computability/Complexity/FineGrained/GraphProblems.lean @@ -53,6 +53,10 @@ vertices and edges, so the lower bounds for them imply the lower bounds for the to a polynomial in the length of the encoded instance, and a lower bound says: for some `δ > 0`, no decider runs within time `2 ^ (δ μ)` times a polynomial. +**The hypothesis is refuted.** `Cslib.Complexity.CountingNativeEndpoint.not_ETH` proves that `ETH` +is false, so the `ETH`-conditional lower bounds below hold vacuously. They are kept as conditional +statements; the reductions and size bounds behind them are unconditional. + ## Main results * `Cslib.Complexity.ETH.not_decidableInSubexpTime_ThreeColoring`: no `2 ^ o(|V| + |E|)` algorithm diff --git a/Complexity/Computability/Complexity/FineGrained/OrthogonalVectors.lean b/Complexity/Computability/Complexity/FineGrained/OrthogonalVectors.lean index d2755b7df..12adefce9 100644 --- a/Complexity/Computability/Complexity/FineGrained/OrthogonalVectors.lean +++ b/Complexity/Computability/Complexity/FineGrained/OrthogonalVectors.lean @@ -49,6 +49,11 @@ The orthogonal vectors hypothesis is stated with a polynomial factor in the dime dimension `c log N`, which follows from the strong exponential time hypothesis with the sparsification lemma, is not proved here. +**The hypothesis is refuted.** `Cslib.Complexity.CountingNativeEndpoint.not_SETH` proves that +`SETH` is false, so `Cslib.Complexity.OVH_of_SETH` holds vacuously and gives no evidence for `OVH`, +which this library neither proves nor refutes. The reduction from a fast `OV` decider to a fast +`SAT` decider is unconditional. + ## Main definitions * `Cslib.Complexity.OV.clauseVector`, `Cslib.Complexity.OV.halfVectors`: the vectors of the diff --git a/Complexity/Computability/Complexity/FineGrained/PermutationIndependentSet.lean b/Complexity/Computability/Complexity/FineGrained/PermutationIndependentSet.lean index d9da2fc8f..fbc95a6e9 100644 --- a/Complexity/Computability/Complexity/FineGrained/PermutationIndependentSet.lean +++ b/Complexity/Computability/Complexity/FineGrained/PermutationIndependentSet.lean @@ -77,6 +77,10 @@ using a library proof based on monotone threshold enumeration (`Tuple.sort` and and querying a purported $2^{o(n \log n)}$ decider for `BipartitePermutationIndependentSet` decides `ThreeColoring` in time $2^{o(N)}$, contradicting `ETH`. +**The hypothesis is refuted.** `Cslib.Complexity.CountingNativeEndpoint.not_ETH` proves that `ETH` +is false, so the `ETH`-conditional lower bound of this module holds vacuously. It is kept as a +conditional statement; the Turing reduction from `ThreeColoring` behind it is unconditional. + ## Main definitions * `Cslib.Complexity.BipartitePermutationGraph`: instance $(n, E)$ of parameter $n$ and directed diff --git a/Complexity/Computability/Complexity/FineGrained/Reduction.lean b/Complexity/Computability/Complexity/FineGrained/Reduction.lean index fffcc1b5e..0ef3adee6 100644 --- a/Complexity/Computability/Complexity/FineGrained/Reduction.lean +++ b/Complexity/Computability/Complexity/FineGrained/Reduction.lean @@ -38,6 +38,9 @@ clauses shows that the target problem is not decidable in subexponential time in stronger: a lower bound for a measure gives one for every measure at most linear in it (`Cslib.Complexity.DecidableInSubexpTime.mono_measure`). +`Cslib.Complexity.CountingNativeEndpoint.not_ETH` proves that `ETH` is false, so lower bounds +obtained this way hold vacuously. The transfer theorems are unconditional. + ## Main results * `Cslib.Complexity.DecidableInExpTime.mono_measure`, diff --git a/Complexity/Computability/MCSP/PartialETH.lean b/Complexity/Computability/MCSP/PartialETH.lean index 14c850b4c..198767ee7 100644 --- a/Complexity/Computability/MCSP/PartialETH.lean +++ b/Complexity/Computability/MCSP/PartialETH.lean @@ -78,6 +78,11 @@ subexponential time $2^{o(m \log m)} = N^{o(\log \log N)}$ (`¬DecidableInSubexp \iff \mathrm{ilangoInstance}\, G \in \mathrm{PartialMCSP.BinaryGate} \iff \mathrm{ilangoInstance}\, G \in \mathrm{PartialMCSP.MonotoneReadOnce}.$$ +**The hypothesis is refuted.** `Cslib.Complexity.CountingNativeEndpoint.not_ETH` proves that `ETH` +is false, so the `ETH`-conditional lower bounds of this module hold vacuously. They are kept as +conditional statements, as is the Partial MCSP catalogue entry; the reduction and the equivalences +above are unconditional. + ## Main definitions * `Cslib.PartialMCSP.MonotoneReadOnce`: partial-function MCSP restricted to read-once positive