diff --git a/ComplexityTests/Abstracts/SubexponentialSATTests.lean b/ComplexityTests/Abstracts/SubexponentialSATTests.lean
index 9eef948f53..f16df06fde 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
 
@@ -24,6 +25,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
@@ -32,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
 
@@ -53,6 +61,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 ee100402a8..987c50b2fd 100644
--- a/abstracts/ComplexityAbstracts/SubexponentialSATAbstract.lean
+++ b/abstracts/ComplexityAbstracts/SubexponentialSATAbstract.lean
@@ -9,15 +9,16 @@ 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
 
 /-! # 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
@@ -33,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
 
@@ -47,6 +48,8 @@ of the definitions and theorem statements, not their English 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
@@ -57,6 +60,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
@@ -87,17 +92,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
@@ -112,9 +117,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))
 
 /-! ## Deterministic machine and resource conventions
 
@@ -124,17 +127,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) ∧
@@ -168,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
@@ -190,7 +212,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
+      ComputableInO count encCNF encNat
         (fun φ => ⌈(2 : ℝ) ^ (A * interpolationScale (numVars φ))⌉₊ * ((encCNF φ).length + 1) ^ e)
         (fun φ => ((encCNF φ).length + 1) ^ b) :=
   SubexponentialSATBridge.exact_count k
@@ -209,10 +231,9 @@ end ComplexityAbstracts.SubexponentialSATAbstract
 
 /--
 info: abstract audit passed for `ComplexityAbstracts.SubexponentialSATAbstract`:
-25 root declarations, 139 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
 ]
diff --git a/abstracts/ComplexityAbstracts/SubexponentialSATBridge.lean b/abstracts/ComplexityAbstracts/SubexponentialSATBridge.lean
index 4d6a9e0701..e97c746303 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
 
diff --git a/abstracts/catalogue.json b/abstracts/catalogue.json
index 7767a945b8..27754ded43 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": [