From 83529d57ea3c95bd49c090d9739f4707a9c25774 Mon Sep 17 00:00:00 2001
From: Christian Reitwiessner <chris-ai1@catch.exinto.de>
Date: Tue, 27 Oct 2026 17:13:14 +0000
Subject: [PATCH 1/5] doc(abstracts): make vars the set of occurring variables
 in the ETH abstract (#1338)
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

Every use of `vars` in the abstract went through `.toFinset`. Define `vars φ`
directly as the `Finset` of occurring variables, so `numVars φ = (vars φ).card`
and model counting ranges over assignments `vars φ → Bool`. The definitions
remain definitionally equal to the library; a test checks
`vars φ = (CNF.vars φ).toFinset` by `rfl`.

Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
---
 .../Abstracts/SubexponentialSATTests.lean        |  2 ++
 .../SubexponentialSATAbstract.lean               | 16 ++++++++--------
 2 files changed, 10 insertions(+), 8 deletions(-)

diff --git a/ComplexityTests/Abstracts/SubexponentialSATTests.lean b/ComplexityTests/Abstracts/SubexponentialSATTests.lean
index 9eef948f5..5c4681f56 100644
--- a/ComplexityTests/Abstracts/SubexponentialSATTests.lean
+++ b/ComplexityTests/Abstracts/SubexponentialSATTests.lean
@@ -24,6 +24,8 @@ example (φ : Formula) (σ : ℕ → Bool) : eval φ σ = Cslib.Logic.PL.CNF.eva
 
 example (φ : Formula) : Satisfiable φ ↔ Cslib.Logic.PL.CNF.Satisfiable φ := Iff.rfl
 
+example (φ : Formula) : vars φ = (Cslib.Logic.PL.CNF.vars φ).toFinset := rfl
+
 example (φ : Formula) : numVars φ = Cslib.Logic.PL.CNF.numVars φ := rfl
 
 example (φ : Formula) : modelCount φ = Cslib.Logic.PL.CNF.modelCount φ := rfl
diff --git a/abstracts/ComplexityAbstracts/SubexponentialSATAbstract.lean b/abstracts/ComplexityAbstracts/SubexponentialSATAbstract.lean
index ee100402a..b79f7823b 100644
--- a/abstracts/ComplexityAbstracts/SubexponentialSATAbstract.lean
+++ b/abstracts/ComplexityAbstracts/SubexponentialSATAbstract.lean
@@ -87,17 +87,17 @@ def eval (φ : Formula) (σ : ℕ → Bool) : Bool :=
 /-- A formula is satisfiable when some total Boolean assignment makes it true. -/
 def Satisfiable (φ : Formula) : Prop := ∃ σ : ℕ → Bool, eval φ σ = true
 
-/-- Variables in occurrence order, retaining repetitions. -/
-def vars (φ : Formula) : List ℕ := φ.flatten.map Literal.var
+/-- The variables occurring in `φ`. -/
+def vars (φ : Formula) : Finset ℕ := (φ.flatten.map Literal.var).toFinset
 
-/-- The number of distinct occurring variables, independent of their numeric labels. -/
-def numVars (φ : Formula) : ℕ := (vars φ).toFinset.card
+/-- The number of variables occurring in `φ`, independent of their numeric labels. -/
+def numVars (φ : Formula) : ℕ := (vars φ).card
 
-/-- The number of satisfying assignments of `φ`: assignments of its distinct variables, each
-variable counted once, that make `φ` true. -/
+/-- The number of satisfying assignments of `φ`: assignments `vars φ → Bool` that make `φ` true
+when every other variable is set to `false`. -/
 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
+  (Finset.univ.filter fun σ : vars φ → Bool =>
+    eval φ (fun v => if h : v ∈ vars φ then σ ⟨v, h⟩ else false) = true).card
 
 /-- Every clause of `φ` has at most `k` literals. -/
 def HasWidth (k : ℕ) (φ : Formula) : Prop := ∀ clause ∈ φ, clause.length ≤ k

From aa8dabc1e89bf9e1be9b01c69fee5f9bef1fbb1a Mon Sep 17 00:00:00 2001
From: Christian Reitwiessner <chris-ai1@catch.exinto.de>
Date: Tue, 27 Oct 2026 17:20:24 +0000
Subject: [PATCH 2/5] doc(abstracts): state the exact CNF encoding length in
 the ETH abstract (#1338)

Add `length_encCNF`: the encoding of a formula has exactly one bit per clause
plus `10 + 8 * Nat.size v` bits per literal occurrence with variable `v`. This
shows that the polynomial factor in `exact_count` is polynomial in the number
of literals and the binary length of the variable labels. The proof is in the
bridge, by induction over clauses and literals; tests check small instances.

Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
---
 .../Abstracts/SubexponentialSATTests.lean     |  6 +++++
 .../SubexponentialSATAbstract.lean            | 15 ++++++++---
 .../SubexponentialSATBridge.lean              | 26 +++++++++++++++++--
 3 files changed, 42 insertions(+), 5 deletions(-)

diff --git a/ComplexityTests/Abstracts/SubexponentialSATTests.lean b/ComplexityTests/Abstracts/SubexponentialSATTests.lean
index 5c4681f56..2c575c460 100644
--- a/ComplexityTests/Abstracts/SubexponentialSATTests.lean
+++ b/ComplexityTests/Abstracts/SubexponentialSATTests.lean
@@ -55,6 +55,12 @@ example (n : ℕ) :
 example : modelCount [] = 1 := by decide
 example : modelCount [[]] = 0 := by decide
 
+-- The encoding length formula on small inputs: one clause bit plus `10 + 8 · Nat.size v` per
+-- literal occurrence.
+example : (encCNF [[(2, true)]]).length = 27 := by decide
+example : (encCNF [[(0, false)], []]).length = 12 := by decide
+example : (encCNF [[(2, true)]]).length = 1 + (10 + 8 * Nat.size 2) := length_encCNF _
+
 -- 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
diff --git a/abstracts/ComplexityAbstracts/SubexponentialSATAbstract.lean b/abstracts/ComplexityAbstracts/SubexponentialSATAbstract.lean
index b79f7823b..c0551f029 100644
--- a/abstracts/ComplexityAbstracts/SubexponentialSATAbstract.lean
+++ b/abstracts/ComplexityAbstracts/SubexponentialSATAbstract.lean
@@ -16,8 +16,9 @@ import Mathlib.Data.Fintype.Pi
 
 /-! # OpenAI: the Exponential Time Hypothesis is false
 
-The four theorems below are proved through `SubexponentialSATBridge` from the unconditional
-native counting endpoint.
+The four complexity theorems below are proved through `SubexponentialSATBridge` from the
+unconditional native counting endpoint. A fifth theorem, `length_encCNF`, gives the exact length
+of the input encoding.
 
 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
@@ -116,6 +117,14 @@ def encCNF : Formula ↪ List Bool :=
     (ComplexityTests.Abstracts.Encoding.encPair ComplexityTests.Abstracts.Encoding.encNat
       ComplexityTests.Abstracts.Encoding.encBool))
 
+/-- **The encoding is concise.** Its length is exactly one bit per clause, plus `10 + 8 · b` bits
+for each literal occurrence, where `b = Nat.size v` is the number of binary digits of its variable
+`v`. Thus the input length is linear in the number of literals and logarithmic in the variable
+labels, as for a reasonable encoding in the sense of Garey and Johnson. -/
+theorem length_encCNF (φ : Formula) :
+    (encCNF φ).length = φ.length + (φ.flatten.map fun l => 10 + 8 * Nat.size l.var).sum :=
+  SubexponentialSATBridge.length_encCNF φ
+
 /-! ## Deterministic machine and resource conventions
 
 The upstream model is a deterministic binary multi-tape Turing machine with finitely many
@@ -209,7 +218,7 @@ end ComplexityAbstracts.SubexponentialSATAbstract
 
 /--
 info: abstract audit passed for `ComplexityAbstracts.SubexponentialSATAbstract`:
-25 root declarations, 139 dependencies checked
+26 root declarations, 143 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 4d6a9e070..e97c74630 100644
--- a/abstracts/ComplexityAbstracts/SubexponentialSATBridge.lean
+++ b/abstracts/ComplexityAbstracts/SubexponentialSATBridge.lean
@@ -14,7 +14,7 @@ import Complexity.Computability.Complexity.FineGrained.CountingNativeModelCount
 Transfer the unconditional native counting endpoint to the abstract. Its list-of-list CNF
 representation, Boolean evaluation, model count, encoding combinators, fine-grained
 classes and interpolation scale are definitionally equal to the definitions displayed in
-`SubexponentialSATAbstract.lean`. Thus these four transfers require no semantic weakening,
+`SubexponentialSATAbstract.lean`. Thus these 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.
 
@@ -33,7 +33,7 @@ dense relabeling, with all resource charges referring to `encCNF φ`.
 The native endpoint's dense-relabeling argument supplies the decision consequences for formulas
 with arbitrary natural labels and the occurring-variable parameter. Its SAT exponent and
 ETH/SETH results are transferred directly here. No branch-certificate or exactness premise
-remains in any of the four theorems.
+remains in any of the four complexity 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
@@ -59,6 +59,28 @@ theorem exact_count (k : ℕ) :
         (fun φ => ((encCNF φ).length + 1) ^ b) :=
   CountingNativeEndpoint.exists_modelCounter k
 
+/-- The exact length of the CNF encoding: one bit per clause, plus `10 + 8 · Nat.size v` bits for
+each literal occurrence with variable `v`. -/
+theorem length_encCNF (φ : List (List (ℕ × Bool))) :
+    (encCNF φ).length = φ.length + (φ.flatten.map fun l => 10 + 8 * Nat.size l.1).sum := by
+  have hc (c : List (ℕ × Bool)) : 2 * (encList (encPair encNat encBool) c).length =
+      (c.map fun l => 10 + 8 * Nat.size l.1).sum := by
+    induction c with
+    | nil => rfl
+    | cons l c ih =>
+      have hl : (encPair encNat encBool l).length = 2 * Nat.size l.1 + 2 := by
+        rw [length_encPair, encNat_apply, Nat.size_eq_bits_len]; rfl
+      rw [encList_cons, List.length_append, length_frame, hl, List.map_cons, List.sum_cons, ← ih]
+      ring
+  induction φ with
+  | nil => rfl
+  | cons c φ ih =>
+    change (encList _ (c :: φ)).length = _
+    change (encList _ φ).length = _ at ih
+    rw [encList_cons, List.length_append, length_frame, ih, List.flatten_cons, List.map_append,
+      List.sum_append, ← hc c, List.length_cons]
+    ring
+
 /-- The native counter refutes the library's Exponential Time Hypothesis. -/
 theorem not_eth : ¬ETH := CountingNativeEndpoint.not_ETH
 

From 4df26d396c474c29c7588dd5fbd45669fd54bccc Mon Sep 17 00:00:00 2001
From: Christian Reitwiessner <chris-ai1@catch.exinto.de>
Date: Tue, 27 Oct 2026 17:44:09 +0000
Subject: [PATCH 3/5] doc(abstracts): open the shared encoding namespace in the
 ETH abstract (#1338)

Write `encList (encList (encPair encNat encBool))` and `encNat` instead of the
fully qualified `ComplexityTests.Abstracts.Encoding.*` names. Only references
are shortened; the audit and all statements are unchanged.

Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
---
 .../ComplexityAbstracts/SubexponentialSATAbstract.lean    | 8 ++++----
 1 file changed, 4 insertions(+), 4 deletions(-)

diff --git a/abstracts/ComplexityAbstracts/SubexponentialSATAbstract.lean b/abstracts/ComplexityAbstracts/SubexponentialSATAbstract.lean
index c0551f029..8789fd067 100644
--- a/abstracts/ComplexityAbstracts/SubexponentialSATAbstract.lean
+++ b/abstracts/ComplexityAbstracts/SubexponentialSATAbstract.lean
@@ -58,6 +58,8 @@ Construction provenance is recorded in
 
 namespace ComplexityAbstracts.SubexponentialSATAbstract
 
+open ComplexityTests.Abstracts.Encoding
+
 /-! ## Formulas and model counting
 
 A literal is a variable or its negation. Clauses are disjunctions of literals and formulas are
@@ -113,9 +115,7 @@ encoded by the empty word. The shared foundation spells out all framing and list
 /-- 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))
+  encList (encList (encPair encNat encBool))
 
 /-- **The encoding is concise.** Its length is exactly one bit per clause, plus `10 + 8 · b` bits
 for each literal occurrence, where `b = Nat.size v` is the number of binary digits of its variable
@@ -199,7 +199,7 @@ 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
+      Turing.MultiTapeTM.ComputableInO count encCNF encNat
         (fun φ => ⌈(2 : ℝ) ^ (A * interpolationScale (numVars φ))⌉₊ * ((encCNF φ).length + 1) ^ e)
         (fun φ => ((encCNF φ).length + 1) ^ b) :=
   SubexponentialSATBridge.exact_count k

From 0e9292b78edd58ef06f6d9e84b6e74dda558e5a7 Mon Sep 17 00:00:00 2001
From: Christian Reitwiessner <chris-ai1@catch.exinto.de>
Date: Tue, 27 Oct 2026 17:48:30 +0000
Subject: [PATCH 4/5] doc(abstracts): display ComputableInO in the ETH abstract
 (#1338)

Display `ComputableInO` locally over upstream `ComputableInTimeAndSpace`, as
the abstract already does for `DecidableInTimeO`, and use it in `exact_count`.
The abstract no longer imports or allowlists `MultiTape.ResourceBounds`; its
only allowlisted module is the shared `Encoding` foundation. A test checks
agreement with the library predicate by `Iff.rfl`.

Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
---
 .../Abstracts/SubexponentialSATTests.lean     |  6 +++
 .../SubexponentialSATAbstract.lean            | 43 ++++++++++---------
 2 files changed, 29 insertions(+), 20 deletions(-)

diff --git a/ComplexityTests/Abstracts/SubexponentialSATTests.lean b/ComplexityTests/Abstracts/SubexponentialSATTests.lean
index 2c575c460..f16df06fd 100644
--- a/ComplexityTests/Abstracts/SubexponentialSATTests.lean
+++ b/ComplexityTests/Abstracts/SubexponentialSATTests.lean
@@ -6,6 +6,7 @@ Authors: Samuel Schlesinger
 
 import ComplexityAbstracts.SubexponentialSATAbstract
 import Complexity.Computability.Complexity.FineGrained
+import Complexity.Computability.Machines.Turing.MultiTape.ResourceBounds
 import Complexity.Computability.Complexity.FineGrained.CountingScale
 import Complexity.Logics.Propositional.CNF.ModelCount
 
@@ -34,6 +35,11 @@ example (k : ℕ) (φ : Formula) : HasWidth k φ ↔ ∀ c ∈ φ, c.length ≤
 
 example : encCNF = Cslib.Complexity.encCNF := rfl
 
+example {α β : Type} (f : α → β) (encIn : α ↪ List Bool) (encOut : β ↪ List Bool)
+    (T S : α → ℕ) :
+    ComputableInO f encIn encOut T S ↔ Turing.MultiTapeTM.ComputableInO f encIn encOut T S :=
+  Iff.rfl
+
 example {α : Type} (A : Set α) (enc : α ↪ List Bool) (T : α → ℝ) :
     DecidableInTimeO A enc T ↔ Cslib.Complexity.DecidableInTimeO A enc T := Iff.rfl
 
diff --git a/abstracts/ComplexityAbstracts/SubexponentialSATAbstract.lean b/abstracts/ComplexityAbstracts/SubexponentialSATAbstract.lean
index 8789fd067..9d35c72ea 100644
--- a/abstracts/ComplexityAbstracts/SubexponentialSATAbstract.lean
+++ b/abstracts/ComplexityAbstracts/SubexponentialSATAbstract.lean
@@ -9,7 +9,7 @@ Authors: OpenAI, Samuel Schlesinger, Anton Kovsharov
 import ComplexityAbstracts.Check
 import ComplexityAbstracts.Encoding
 import ComplexityAbstracts.SubexponentialSATBridge
-import Complexity.Computability.Machines.Turing.MultiTape.ResourceBounds
+import Cslib.Computability.Machines.Turing.MultiTape.Deterministic
 import Mathlib.Analysis.SpecialFunctions.Pow.Real
 import Mathlib.Analysis.SpecialFunctions.Sqrt
 import Mathlib.Data.Fintype.Pi
@@ -34,12 +34,12 @@ agreement with the canonical definitions. Machinery is existential. The bridge i
 public unconditional endpoint, whose native counter and consequences prove the displayed
 statements without any branch-certificate or exactness hypothesis.
 
-**What a reader inspects.** Read the definitions below, the displayed `Encoding` foundation,
-and the one additional allowed module, `MultiTape.ResourceBounds`. The latter contributes only
-the plain native `ComputableInO` resource convention, explained below, over upstream deterministic
-machines. No CNF implementation, complexity-class definition or counting construction is
-allowlisted. Lean checks the bridge proofs; `#check_abstract` audits the dependency boundary
-of the definitions and theorem statements, not their English interpretation.
+**What a reader inspects.** Read the definitions below and the displayed `Encoding` foundation.
+The machine model is upstream cslib's deterministic multi-tape Turing machine; no library
+module beyond `Encoding` is allowlisted, so no CNF implementation, complexity-class definition or
+counting construction enters the statements. Lean checks the bridge proofs; `#check_abstract`
+audits the dependency boundary of the definitions and theorem statements, not their English
+interpretation.
 
 ## References and credit
 
@@ -133,17 +133,21 @@ and symbol operations. The input tape is read-only, and output is write-only. Ti
 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.
+Upstream `ComputableInTimeAndSpace f encIn encOut t s` asserts one such machine that, on every
+input `x`, halts with `encOut (f x)` within `t x` steps and `s x` work cells.
+`DecidableInTimeAndSpace` is the case of the exact Boolean membership bit. The finite machine and
+all bounds precede the inputs. Time and space are independent budgets; a time bound does not
+supply polynomial space.
 -/
 
+/-- `f` is computable within time `O(T x)` and space `O(S x)`, with the encoded output also of
+length `O(S x)`: output is charged even though its tape is not a work tape. -/
+def ComputableInO {α β : Type} (f : α → β) (encIn : α ↪ List Bool) (encOut : β ↪ List Bool)
+    (T S : α → ℕ) : Prop :=
+  ∃ c, Turing.MultiTapeTM.ComputableInTimeAndSpace f encIn encOut
+      (fun x => c * (T x + 1)) (fun x => c * (S x + 1)) ∧
+    ∀ x, (encOut (f x)).length ≤ c * (S x + 1)
+
 /-- 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) ∧
@@ -199,7 +203,7 @@ 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 encNat
+      ComputableInO count encCNF encNat
         (fun φ => ⌈(2 : ℝ) ^ (A * interpolationScale (numVars φ))⌉₊ * ((encCNF φ).length + 1) ^ e)
         (fun φ => ((encCNF φ).length + 1) ^ b) :=
   SubexponentialSATBridge.exact_count k
@@ -218,10 +222,9 @@ end ComplexityAbstracts.SubexponentialSATAbstract
 
 /--
 info: abstract audit passed for `ComplexityAbstracts.SubexponentialSATAbstract`:
-26 root declarations, 143 dependencies checked
+27 root declarations, 143 dependencies checked
 -/
 #guard_msgs (whitespace := lax) in
 #check_abstract ComplexityAbstracts.SubexponentialSATAbstract allowing [
-  ComplexityAbstracts.Encoding,
-  Complexity.Computability.Machines.Turing.MultiTape.ResourceBounds
+  ComplexityAbstracts.Encoding
 ]

From 7e600f5487eece294abd34a50c39027e13565306 Mon Sep 17 00:00:00 2001
From: Christian Reitwiessner <chris-ai1@catch.exinto.de>
Date: Tue, 27 Oct 2026 23:08:50 +0000
Subject: [PATCH 5/5] doc(abstracts): display length_encCNF in the rendered ETH
 abstract

Review follow-up on #1352: move `length_encCNF` from the appendix section
`Representation details` into a new `Input size` section before
`exact_count`, list it as a supporting theorem of the `subexponential-sat`
catalogue entry so the PDF shows it, and cite Garey and Johnson by key.

Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
---
 .../SubexponentialSATAbstract.lean            | 25 +++++++++++++------
 abstracts/catalogue.json                      |  3 +++
 2 files changed, 20 insertions(+), 8 deletions(-)

diff --git a/abstracts/ComplexityAbstracts/SubexponentialSATAbstract.lean b/abstracts/ComplexityAbstracts/SubexponentialSATAbstract.lean
index 9d35c72ea..987c50b2f 100644
--- a/abstracts/ComplexityAbstracts/SubexponentialSATAbstract.lean
+++ b/abstracts/ComplexityAbstracts/SubexponentialSATAbstract.lean
@@ -48,6 +48,8 @@ interpretation.
   `openai/math@7ef5c0cc5ca4b0e072b7a050fca09ab24bc6fa3a`.
 * [R. Impagliazzo and R. Paturi, *On the complexity of k-SAT*][ImpagliazzoPaturi2001]: the
   exponential-time hypotheses and the infimum exponent.
+* [M. R. Garey and D. S. Johnson, *Computers and Intractability*][GareyJohnson1979]: reasonable
+  encodings.
 
 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
@@ -117,14 +119,6 @@ literals within clauses and the clauses within the formula. This is the native `
 def encCNF : Formula ↪ List Bool :=
   encList (encList (encPair encNat encBool))
 
-/-- **The encoding is concise.** Its length is exactly one bit per clause, plus `10 + 8 · b` bits
-for each literal occurrence, where `b = Nat.size v` is the number of binary digits of its variable
-`v`. Thus the input length is linear in the number of literals and logarithmic in the variable
-labels, as for a reasonable encoding in the sense of Garey and Johnson. -/
-theorem length_encCNF (φ : Formula) :
-    (encCNF φ).length = φ.length + (φ.flatten.map fun l => 10 + 8 * Nat.size l.var).sum :=
-  SubexponentialSATBridge.length_encCNF φ
-
 /-! ## Deterministic machine and resource conventions
 
 The upstream model is a deterministic binary multi-tape Turing machine with finitely many
@@ -181,6 +175,21 @@ def ETH : Prop :=
 def SETH : Prop :=
   ∀ ε : ℝ, 0 < ε → ∃ k : ℕ, ¬DecidableInExpTime (KSAT k) encCNF numVars (1 - ε)
 
+/-! ## Input size
+
+The polynomial factors below are polynomials in the length of `encCNF φ`, which is exactly
+determined by the formula.
+-/
+
+/-- **The encoding is concise.** Its length is exactly one bit per clause, plus `10 + 8 · b` bits
+for each literal occurrence, where `b = Nat.size v` is the number of binary digits of its variable
+`v`. Thus the input length is linear in the number of literals and logarithmic in the variable
+labels, as for a reasonable encoding in the sense of
+[Garey and Johnson][GareyJohnson1979]. -/
+theorem length_encCNF (φ : Formula) :
+    (encCNF φ).length = φ.length + (φ.flatten.map fun l => 10 + 8 * Nat.size l.var).sum :=
+  SubexponentialSATBridge.length_encCNF φ
+
 /-! ## Exact counting and the exponential time hypotheses
 
 The primary theorem fixes the counter, constants and native machine for each `k` before every
diff --git a/abstracts/catalogue.json b/abstracts/catalogue.json
index 7767a945b..27754ded4 100644
--- a/abstracts/catalogue.json
+++ b/abstracts/catalogue.json
@@ -240,6 +240,9 @@
         "ComplexityAbstracts.SubexponentialSATAbstract.not_seth",
         "ComplexityAbstracts.SubexponentialSATAbstract.satExponent_eq_zero"
       ],
+      "supporting_theorems": [
+        "ComplexityAbstracts.SubexponentialSATAbstract.length_encCNF"
+      ],
       "summary": "For each fixed clause width, one deterministic native machine exactly counts satisfying assignments in subexponential time and polynomial space. Every fixed-width SAT exponent is zero, and ETH and SETH are false. Native formalization of OpenAI's manuscript, revised 25 October 2026, by the contributors to #1226.",
       "scope": "Explicit CNF semantics, model counts over the occurring variables, and binary formula/output encodings; the interpolation-scale exponent n (log log (n + 16))² / sqrt(log(n + 16)) from §§3–6 and Proposition 6.4, where n is the number of variables, with polynomial time overhead and polynomial workspace in the encoded formula length. Includes all fixed widths and sizes; the count is exact on every formula of the given width. This does not establish the sharper Theorem 1.1 / Appendix D bound.",
       "foundations": [