refactor(abstracts): clarify theorem statements and shared foundations

.agents/skills/lean-abstract/SKILL.md

@@ -47,6 +47,9 @@ This requirement applies transitively: an alias or wrapper around an internal de
 - **Prefer ordinary types and quantifiers**: Prefer functions, `List`, `Fin n → α`, quantifiers, membership, and equalities over custom interfaces, typeclasses, or implementation-specific dependent records.
 - **Use `Fin n → α` for homogeneous tuples**: For more than two homogeneous components, prefer `Fin n → α` over nested cross products, with short descriptive aliases for indices.
 - **Explicit encodings**: When a theorem depends on a binary encoding (such as `encCNF` or binary tree encodings), either spell out the encoding combinators (`frame`, `encodePair`, `encodeList`, `Nat.bits`) directly in the abstract or explicitly allow the foundational encoding module. When packaging an encoding function `encodeX : X → List Bool` into an embedding `def encX : X ↪ List Bool := ⟨encodeX, encodeX_injective⟩`, declare `theorem encodeX_injective : Function.Injective encodeX := Bridge.encodeX_injective` as a local `theorem` before `def encX`: `#check_abstract` traverses the `value?` of non-theorem `def`s and stops at `theorem` proof boundaries, and `scripts/abstract_to_tex.py` elides undocumented `*_injective` helper theorems following a definition block (and only those).
+- **Share foundations, keep semantics visible**: Use the small audited `ComplexityAbstracts.Encoding` and `ComplexityAbstracts.Computation` modules for common serialization and polynomial-time conventions. Keep complexity-class, game and problem definitions in each abstract. Import every used foundation explicitly, allow it in `#check_abstract`, and list the complete foundation import closure in the catalogue entry's `foundations`. The renderer includes these definitions in each standalone PDF and once at the end of the combined catalogue.
+- **Lead with the mathematics**: Put encoding and machine representation details in a `## Representation details` module-doc section. The renderer moves that section and its following declarations to an appendix, ending at the next level-two section. Do not put headline or selected supporting theorems there. Explain every resource-significant convention in the main text, including unary versus binary sizes, uniformity and clock semantics. Moving a definition does not excuse hiding its meaning.
+- **Migrate clients to canonical names**: Extract shared definitions without deprecated aliases and update all in-repository clients, following `AGENTS.md`.
 - **State plain machine bounds where possible**: `Complexitylib` uses `ComputableTidilyInPolyTime` internally for compositional closure (`@[fun_prop]`), and proves it equivalent to plain upstream `Turing.MultiTapeTM.ComputableInTimeAndSpaceOfLength` with `Cslib.PolynomiallyBounded`. Using the plain upstream notion in the abstract lets a reader verify the theorem statement without needing to inspect tidy-machine invariants.
 
 ---
@@ -78,7 +81,7 @@ Start each conceptual block's docstring (`/-- ... -/` or `/-! ... -/`) with a co
 
 - Explain unfamiliar `Mathlib` or `Cslib` predicates (e.g., `Nat.bits`, `Function.Embedding`, `Turing.MultiTapeTM.ComputableInTimeAndSpaceOfLength`) by their mathematical meaning before naming the Lean symbol.
 - State totality, halting, and answer-preservation guarantees explicitly when describing reductions or verifiers.
-- In the module docstring (`/-! # ... -/`), explain that a reader only needs to inspect the definitions and theorem statements in `*Abstract.lean` to verify that the formalization proves the intended mathematical claim; Lean verifies the proofs through `*Bridge.lean` and `#check_abstract` audits the dependency boundary.
+- In the module docstring (`/-! # ... -/`), explain that a reader only needs to inspect the definitions and theorem statements in `*Abstract.lean` and its displayed shared foundations to verify that the formalization proves the intended mathematical claim; Lean verifies the proofs through `*Bridge.lean` and `#check_abstract` audits the dependency boundary.
 
 ---
 
@@ -117,9 +120,9 @@ Start each conceptual block's docstring (`/-- ... -/` or `/-! ... -/`) with a co
 
 Consult these concrete implementations in `abstracts/ComplexityAbstracts/`:
 
-- **Pattern A (Unfolded types, zero `Complexity.*` dependencies)**:
+- **Pattern A (Unfolded types, shared audited foundations)**:
   [CookLevinAbstract.lean](../../../abstracts/ComplexityAbstracts/CookLevinAbstract.lean) and [CookLevinBridge.lean](../../../abstracts/ComplexityAbstracts/CookLevinBridge.lean) (`SAT` and `ExactThreeSAT` are `NP`-complete, `UNSAT` is `coNP`-complete).
-- **Pattern B (Fresh `inductive` syntax + polymorphic `Presentation` / `Laws`, zero `Complexity.*` dependencies)**:
+- **Pattern B (Fresh `inductive` syntax + polymorphic `Presentation` / `Laws`, shared audited foundations)**:
   [TQBFAbstract.lean](../../../abstracts/ComplexityAbstracts/TQBFAbstract.lean) and [TQBFBridge.lean](../../../abstracts/ComplexityAbstracts/TQBFBridge.lean) (`TQBF` is `PSPACE`-complete).
 - **Pattern A reusing another bridge**:
   [SubsetSumAbstract.lean](../../../abstracts/ComplexityAbstracts/SubsetSumAbstract.lean) and [SubsetSumBridge.lean](../../../abstracts/ComplexityAbstracts/SubsetSumBridge.lean) (`SubsetSum` is `NP`-complete with numbers in binary; the bridge reuses the plain `NP` transfer lemmas of `CookLevinBridge`).

ComplexityTests.lean

@@ -2,6 +2,7 @@ import ComplexityTests.AWPPAmplification
 import ComplexityTests.AWPPLowness
 import ComplexityTests.Abstracts.All
 import ComplexityTests.Abstracts.CheckTests
+import ComplexityTests.Abstracts.InputLayouts
 import ComplexityTests.AdaptivePPT
 import ComplexityTests.Advice
 import ComplexityTests.AffineController

ComplexityTests/Abstracts/InputLayouts.lean

@@ -0,0 +1,53 @@
+/-
+Copyright (c) 2026 Samuel Schlesinger. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Samuel Schlesinger
+-/
+
+-- upstream: local-only (formal abstract regression tests)
+
+import ComplexityAbstracts.FormulaBoundsAbstract
+import ComplexityAbstracts.USTCONAbstract
+
+/-! # Input layout checks for the Andreev and undirected-connectivity abstracts -/
+
+namespace ComplexityTests.Abstracts.InputLayouts
+
+open FormulaBoundsAbstract
+
+-- Coordinate zero is the least significant address bit.
+example : tableIndex 3 ![true, true, false] = 3 := by decide
+
+-- The first bit of the second block follows the four table bits and the first block.
+example (x : Fin 10 → Bool) : blockInput (b := 2) (m := 3) x 1 0 = x 7 :=
+  blockInput_eq (b := 2) (m := 3) x 1 0 7 rfl
+
+-- Block parities are (true, false), so the answer is table entry one.
+example : andreev 2 2 ![false, true, false, false, true, false, true, true] = true := by
+  decide
+
+-- Empty addresses and empty blocks both select the first table entry.
+example (x : Fin 1 → Bool) : andreev 0 3 x = x 0 := rfl
+
+example (x : Fin 4 → Bool) : andreev 2 0 x = x 0 := rfl
+
+private def singleton : USTCONAbstract.Instance :=
+  ⟨1, ⟨⟨fun _ _ => false, by simp⟩, 0, 0⟩⟩
+
+private def edgeWithIsolatedVertex : USTCONAbstract.Instance :=
+  ⟨3, ⟨⟨fun a b => decide (a.val + b.val = 1), by decide⟩, 0, 2⟩⟩
+
+-- The smallest valid instance has a one-bit matrix and coincident endpoints.
+example : USTCONAbstract.encode singleton = [true, false, false, false, false] := by decide
+
+example : singleton ∈ USTCONAbstract.USTCON := SimpleGraph.Reachable.refl _
+
+-- Vertices zero and one are adjacent; vertex two is isolated. Headers name endpoints zero and two.
+example : USTCONAbstract.encode edgeWithIsolatedVertex =
+    [true, true, true, false, false, true, true, false,
+      false, true, false, true, false, false, false, false, false] := by decide
+
+-- An endpoint rules out a zero-vertex instance.
+example (I : USTCONAbstract.Instance) : 0 < I.vertexCount := Fin.pos I.source
+
+end ComplexityTests.Abstracts.InputLayouts

abstracts/ComplexityAbstracts.lean

@@ -1,12 +1,14 @@
 import ComplexityAbstracts.BarringtonAbstract
 import ComplexityAbstracts.BarringtonBridge
 import ComplexityAbstracts.Check
+import ComplexityAbstracts.Computation
 import ComplexityAbstracts.ConstantDepthAbstract
 import ComplexityAbstracts.ConstantDepthBridge
 import ComplexityAbstracts.CookLevinAbstract
 import ComplexityAbstracts.CookLevinBridge
 import ComplexityAbstracts.CryptographyAbstract
 import ComplexityAbstracts.CryptographyBridge
+import ComplexityAbstracts.Encoding
 import ComplexityAbstracts.FaginAbstract
 import ComplexityAbstracts.FaginBridge
 import ComplexityAbstracts.FormulaBoundsAbstract

abstracts/ComplexityAbstracts/BarringtonAbstract.lean

@@ -32,7 +32,10 @@ Lean checks the bridge proof and `#check_abstract` audits the statement boundary
 namespace ComplexityTests.Abstracts.BarringtonAbstract
 
 /-- A nonuniform NC¹ language has a polynomial-size De Morgan circuit at each input length,
-with depth at most a constant times `floor(log₂ n)+1`. Every gate, constants included, costs one. -/
+with depth at most a constant times `floor(log₂ n)+1`. Every gate, constants included, costs one.
+Here `L : Language Bool` is a set of finite bit strings. `L.slice n x` tests whether the word
+`List.ofFn x` belongs to `L`; `single` makes that Boolean the sole circuit output, and `Computes`
+requires agreement on every input. -/
 def InNC1 (L : Language Bool) : Prop :=
   ∃ (c : ℕ) (size : ℕ → ℕ), Cslib.PolynomiallyBounded size ∧ ∀ n,
     ∃ C : Cslib.Circuits.Circuit Cslib.Circuits.Boolean.signature n 1,
@@ -43,7 +46,8 @@ def InNC1 (L : Language Bool) : Prop :=
 /-- A width-five permutation program reads one input bit per instruction, selects one of two
 permutations, and multiplies the selected permutations in instruction order. The elementary
 `MonoidProgram` model is explicitly allowed; it is a list of `(position, selection function)`
-instructions. Its length is polynomial and its final permutation is tested against a set. -/
+instructions. Its length is polynomial. Both the program and the acceptance set may depend on
+input length; acceptance tests the entire final permutation. -/
 def HasWidthFivePrograms (L : Language Bool) : Prop :=
   ∃ size : ℕ → ℕ, Cslib.PolynomiallyBounded size ∧ ∀ n,
     ∃ (P : Cslib.BranchingPrograms.MonoidProgram (Fin n) Bool (Equiv.Perm (Fin 5)))

abstracts/ComplexityAbstracts/BarringtonBridge.lean

@@ -13,7 +13,10 @@ import Complexity.Computability.Circuit.Boolean.BarringtonClass
 namespace ComplexityTests.Abstracts.BarringtonBridge
 
 /-- A nonuniform NC¹ language has a polynomial-size De Morgan circuit at each input length,
-with depth at most a constant times `floor(log₂ n)+1`. Every gate, constants included, costs one. -/
+with depth at most a constant times `floor(log₂ n)+1`. Every gate, constants included, costs one.
+Here `L : Language Bool` is a set of finite bit strings. `L.slice n x` tests whether the word
+`List.ofFn x` belongs to `L`; `single` makes that Boolean the sole circuit output, and `Computes`
+requires agreement on every input. -/
 def InNC1 (L : Language Bool) : Prop :=
   ∃ (c : ℕ) (size : ℕ → ℕ), Cslib.PolynomiallyBounded size ∧ ∀ n,
     ∃ C : Cslib.Circuits.Circuit Cslib.Circuits.Boolean.signature n 1,
@@ -24,7 +27,8 @@ def InNC1 (L : Language Bool) : Prop :=
 /-- A width-five permutation program reads one input bit per instruction, selects one of two
 permutations, and multiplies the selected permutations in instruction order. The elementary
 `MonoidProgram` model is explicitly allowed; it is a list of `(position, selection function)`
-instructions. Its length is polynomial and its final permutation is tested against a set. -/
+instructions. Its length is polynomial. Both the program and the acceptance set may depend on
+input length; acceptance tests the entire final permutation. -/
 def HasWidthFivePrograms (L : Language Bool) : Prop :=
   ∃ size : ℕ → ℕ, Cslib.PolynomiallyBounded size ∧ ∀ n,
     ∃ (P : Cslib.BranchingPrograms.MonoidProgram (Fin n) Bool (Equiv.Perm (Fin 5)))

abstracts/ComplexityAbstracts/Computation.lean

@@ -0,0 +1,45 @@
+/-
+Copyright (c) 2026 Samuel Schlesinger. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Samuel Schlesinger
+-/
+
+-- upstream: local-only (formal abstract foundations)
+
+import ComplexityAbstracts.Check
+import ComplexityAbstracts.Encoding
+import Cslib.Computability.Machines.Turing.MultiTape.Deterministic
+import Cslib.Foundations.Data.Nat.PolynomialBound
+
+/-! # Polynomial-time functions and verifiers
+
+One deterministic binary multi-tape Turing machine, with finitely many states, computes the
+function on every encoded input. Its time and work space are polynomially bounded in input bit
+length. Input is read-only and output is write-only. The machine is uniform: its code and its
+bounds are fixed before the input is chosen. No condition is imposed on words outside an
+encoding's image.
+
+A verifier receives an instance and a certificate. Its running time is polynomial in their
+combined encoded length, not just the instance length. The pair encoding has length
+`2 * |enc x| + 1 + |w|`, so it gives the usual polynomial bound in `|enc x| + |w|`.
+-/
+
+namespace ComplexityTests.Abstracts.Computation
+
+/-- Total polynomial-time computation on encoded inputs, with explicit time and space bounds. -/
+def PolyTime {α β : Type} (f : α → β) (a : α ↪ List Bool) (b : β ↪ List Bool) : Prop :=
+  ∃ t s : ℕ → ℕ, Cslib.PolynomiallyBounded t ∧ Cslib.PolynomiallyBounded s ∧
+    Turing.MultiTapeTM.ComputableInTimeAndSpaceOfLength f a b t s
+
+/-- One total polynomial-time deterministic verifier, on an instance and a binary certificate. -/
+def PolyTimeVerifier {α : Type} (enc : α ↪ List Bool) (V : α × List Bool → Bool) : Prop :=
+  PolyTime V (Encoding.encPair enc Encoding.encBits) Encoding.encBool
+
+end ComplexityTests.Abstracts.Computation
+
+/--
+info: abstract audit passed for `ComplexityTests.Abstracts.Computation`:
+2 root declarations, 33 dependencies checked
+-/
+#guard_msgs (whitespace := lax) in
+#check_abstract ComplexityTests.Abstracts.Computation allowing [ComplexityAbstracts.Encoding]

abstracts/ComplexityAbstracts/ConstantDepthAbstract.lean

@@ -44,7 +44,9 @@ abbrev ACBasis := Cslib.Circuits.Boolean.Unbounded.signature
 def meaning : Cslib.Circuits.Interpretation ACBasis Bool :=
   Cslib.Circuits.Boolean.Unbounded.interpretation
 
-/-- Charge one for AND/OR, including their nullary constant cases; negations are free. -/
+/-- Depth charges one for AND/OR, including their nullary constant cases, and zero for NOT.
+This weight affects depth only: `C.size` counts every operation gate, including NOT and
+constants. -/
 def andOrCost : Cslib.Circuits.Boolean.Unbounded.Op → ℕ
   | .not => 0
   | .and _ | .or _ => 1
@@ -57,7 +59,7 @@ def modularMeaning (p : ℕ) :
 
 /-- **Håstad.** A parity circuit of AND/OR depth at most `d` needs `2^s` gates whenever
 `s ≥ 2` and `17s(16s+1)^(d-2) ≤ n`. Subtraction is in naturals. This gives the sharp exponent
-`1/(d-1)` for every fixed `d ≥ 2`; negations cost zero in the depth bound. -/
+`1/(d-1)` for every fixed `d ≥ 2`. Negations cost zero in depth and one gate in size. -/
 theorem hastad {n d s : ℕ} (C : Cslib.Circuits.Circuit ACBasis n 1)
     (correct : ∀ x, C.eval meaning x 0 = parity n x) (hs : 2 ≤ s)
     (depth : C.depthWith andOrCost ≤ d) (budget : 17 * s * (16 * s + 1) ^ (d - 2) ≤ n) :

abstracts/ComplexityAbstracts/ConstantDepthBridge.lean

@@ -25,7 +25,9 @@ abbrev ACBasis := Cslib.Circuits.Boolean.Unbounded.signature
 def meaning : Cslib.Circuits.Interpretation ACBasis Bool :=
   Cslib.Circuits.Boolean.Unbounded.interpretation
 
-/-- Charge one for AND/OR, including their nullary constant cases; negations are free. -/
+/-- Depth charges one for AND/OR, including their nullary constant cases, and zero for NOT.
+This weight affects depth only: `C.size` counts every operation gate, including NOT and
+constants. -/
 def andOrCost : Cslib.Circuits.Boolean.Unbounded.Op → ℕ
   | .not => 0
   | .and _ | .or _ => 1
@@ -38,7 +40,7 @@ def modularMeaning (p : ℕ) :
 
 /-- **Håstad.** A parity circuit of AND/OR depth at most `d` needs `2^s` gates whenever
 `s ≥ 2` and `17s(16s+1)^(d-2) ≤ n`. Subtraction is in naturals. This gives the sharp exponent
-`1/(d-1)` for every fixed `d ≥ 2`; negations cost zero in the depth bound. -/
+`1/(d-1)` for every fixed `d ≥ 2`. Negations cost zero in depth and one gate in size. -/
 theorem hastad {n d s : ℕ} (C : Cslib.Circuits.Circuit ACBasis n 1)
     (correct : ∀ x, C.eval meaning x 0 = parity n x) (hs : 2 ≤ s)
     (depth : C.depthWith andOrCost ≤ d) (budget : 17 * s * (16 * s + 1) ^ (d - 2) ≤ n) :