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