diff --git a/.github/scripts/certification_smoke.py b/.github/scripts/certification_smoke.py
new file mode 100644
index 0000000..5ec8ea9
--- /dev/null
+++ b/.github/scripts/certification_smoke.py
@@ -0,0 +1,57 @@
+"""Hard certification smoke test for CI (the `certification-hard` lane).
+
+Unlike the unit lane -- which skips gracefully when Kissat/drat-trim are absent -- this
+script REQUIRES them and fails red if the certification path does not actually execute:
+
+  1. Kissat and drat-trim must be on PATH (else exit 1).
+  2. A CDCL UNSAT verdict must be replayed and accepted by drat-trim (a real DRAT check).
+  3. A CDCL SAT verdict must be replayed against the formula (a real model check).
+
+Both instances are plain 3-CNF with no frame structure, so they are decided by the CDCL
+engine + certification, not by a self-certifying frame -- this exercises exactly the path
+the unit lane is allowed to skip. Exit 0 only if both certifications ran and passed.
+"""
+
+import shutil
+import sys
+from pathlib import Path
+
+sys.path.insert(0, str(Path(__file__).resolve().parents[2]))
+
+from backend.cnf_utils import CNFFormula                # noqa: E402
+from backend.metasolver import _certified_cdcl          # noqa: E402
+
+
+def _fail(msg: str) -> None:
+    print(f"CERTIFICATION LANE FAILED: {msg}")
+    sys.exit(1)
+
+
+def main() -> None:
+    for tool in ("kissat", "drat-trim"):
+        if shutil.which(tool) is None:
+            _fail(f"{tool} is not on PATH; the certification lane requires it")
+
+    # All 8 clauses over 3 variables exclude all 8 assignments -> UNSAT, and it carries
+    # no 2-SAT / parity / counting structure, so it is refuted by CDCL + a DRAT proof.
+    unsat = CNFFormula(3, [[a, b, c] for a in (1, -1) for b in (2, -2) for c in (3, -3)])
+    status, _t, verified = _certified_cdcl(unsat, "kissat", 10.0)
+    if status != "UNSAT":
+        _fail(f"expected UNSAT on the 8-clause formula, got {status}")
+    if not verified:
+        _fail("UNSAT verdict was NOT DRAT-certified (drat-trim did not run/accept)")
+    print("ok: CDCL UNSAT replayed and accepted by drat-trim")
+
+    sat = CNFFormula(3, [[1, 2, 3], [-1, -2, 3], [1, -2, -3]])
+    status, _t, verified = _certified_cdcl(sat, "kissat", 10.0)
+    if status != "SAT":
+        _fail(f"expected SAT on the satisfiable formula, got {status}")
+    if not verified:
+        _fail("SAT model was NOT verified against the formula (model replay failed)")
+    print("ok: CDCL SAT model replayed against the formula")
+
+    print("CERTIFICATION LANE PASSED: DRAT UNSAT + model-replay SAT both executed.")
+
+
+if __name__ == "__main__":
+    main()
diff --git a/.github/workflows/tests.yml b/.github/workflows/tests.yml
index 9b89d48..10904be 100644
--- a/.github/workflows/tests.yml
+++ b/.github/workflows/tests.yml
@@ -6,6 +6,9 @@ on:
   pull_request:
 
 jobs:
+  # Lane 1 -- unit-fast: portable, may skip solver-dependent tests if the external
+  # binaries are unavailable (shutil.which -> None). Green does not by itself assert
+  # that external certification executed; that is lane 2's job.
   unit-fast:
     runs-on: ubuntu-latest
     strategy:
@@ -24,16 +27,29 @@ jobs:
         run: |
           python -m pip install --upgrade pip
           pip install -r backend/requirements.txt
+
+      # Best-effort: install the external solvers so the @requires_kissat
+      # integration tests run too. If a package is unavailable the tests skip
+      # gracefully (shutil.which -> None), so this lane stays green either way.
+      - name: Install SAT solvers (best effort)
+        run: sudo apt-get update && sudo apt-get install -y kissat drat-trim cadical || true
           pip install -e .[dev]
 
       - name: Run test suite
         run: python -m pytest backend/tests/ -q
 
+  # Lane 2 -- certification-hard: Kissat + drat-trim are MANDATORY. This lane fails
+  # red if the external certification path does not actually execute -- it is the
+  # lane that stands behind the repo's headline claim (verify, don't trust).
   certification-hard:
     runs-on: ubuntu-latest
     steps:
       - uses: actions/checkout@v4
 
+      - name: Set up Python
+        uses: actions/setup-python@v5
+        with:
+          python-version: "3.12"
       - name: Set up Python 3.11
         uses: actions/setup-python@v5
         with:
@@ -43,6 +59,22 @@ jobs:
         run: |
           python -m pip install --upgrade pip
           pip install -r backend/requirements.txt
+
+      # Mandatory, NOT best-effort: no "|| true". If these are unavailable the lane
+      # must fail rather than silently skip the certification it is guarding.
+      - name: Install Kissat + drat-trim (mandatory)
+        run: sudo apt-get update && sudo apt-get install -y kissat drat-trim
+
+      - name: Assert the external tools are present
+        run: |
+          command -v kissat
+          command -v drat-trim
+
+      - name: Certification smoke (real DRAT UNSAT + model-replay SAT)
+        run: python .github/scripts/certification_smoke.py
+
+      - name: Certification-relevant tests must run (not skip)
+        run: python -m pytest backend/tests/test_integration.py backend/tests/test_kissat_wrapper.py -q
           pip install -e .[dev]
 
       - name: Build SAT/proof tools
diff --git a/.gitignore b/.gitignore
index 984b352..9764ecb 100644
--- a/.gitignore
+++ b/.gitignore
@@ -37,3 +37,9 @@ __pycache__/
 
 # regenerable benchmark outputs (produced by docs/ladder/scripts/*.py)
 docs/ladder/scripts/*_results.json
+
+# Python packaging artifacts
+*.egg-info/
+build/
+dist/
+__pycache__/
diff --git a/CITATION.cff b/CITATION.cff
index 095475e..faade8b 100644
--- a/CITATION.cff
+++ b/CITATION.cff
@@ -1,4 +1,23 @@
 cff-version: 1.2.0
+message: "If you use this software or its research notes, please cite it as below."
+title: "λSAT — certified λ-logic SAT middleware and a research harness for frame-structured SAT hardness"
+abstract: >-
+  A headless, certified Boolean-satisfiability middleware: it decides formulas via
+  three sound, engine-independent frames (implication/2-SAT, parity/GF(2),
+  counting/cardinality) and their coupling, falling back to a DRAT-certified CDCL
+  engine only when no frame applies. Every verdict is independently checked (SAT by
+  model replay, UNSAT by a sound frame refutation or a drat-trim proof). On top sits
+  a research program on the intrinsic geometry of SAT hardness — a hyperbolic
+  instance-manifold, a game-theoretic dispatcher, and an explicit proven/measured/
+  speculative claim ledger.
+type: software
+authors:
+  - family-names: "Vilela Franco"
+    given-names: "Jesús"
+repository-code: "https://github.com/jesusvilela/lambda-sat-solver"
+url: "https://github.com/jesusvilela/lambda-sat-solver"
+license: MIT
+version: "0.1.0"
 message: "If you use this software, please cite it using the metadata from this file."
 title: "lambda-sat-solver: Certified SAT middleware and frame-structured hardness research harness"
 authors:
@@ -17,8 +36,40 @@ keywords:
   - SAT
   - satisfiability
   - certified solving
+  - DRAT proof checking
+  - computational complexity
+  - resolution width
+  - Nullstellensatz degree
+  - lambda calculus
+references:
+  - type: article
+    authors:
+      - family-names: "Ben-Sasson"
+        given-names: "Eli"
+      - family-names: "Wigderson"
+        given-names: "Avi"
+    title: "Short proofs are narrow — resolution made simple"
+    year: 2001
+  - type: article
+    authors:
+      - family-names: "Clegg"
+        given-names: "Matthew"
+      - family-names: "Edmonds"
+        given-names: "Jeffery"
+      - family-names: "Impagliazzo"
+        given-names: "Russell"
+    title: "Using the Groebner basis algorithm to find proofs of unsatisfiability"
+    year: 1996
+  - type: article
+    authors:
+      - family-names: "Gomes"
+        given-names: "Carla P."
+      - family-names: "Selman"
+        given-names: "Bart"
+    title: "Heavy-tailed phenomena in satisfiability and constraint satisfaction problems"
+    year: 2000
   - DRAT
   - CDCL
   - proof checking
   - SAT hardness
-  - portfolio solving
\ No newline at end of file
+  - portfolio solving
diff --git a/CONTRIBUTING.md b/CONTRIBUTING.md
index f603b10..e0fa6e8 100644
--- a/CONTRIBUTING.md
+++ b/CONTRIBUTING.md
@@ -1,5 +1,45 @@
 # Contributing
 
+Thanks for your interest. This repository has an unusual constitution, and contributions
+are judged by it. Read [`docs/CHARTER.md`](docs/CHARTER.md) first — it is the standard
+everything here is held to.
+
+## The one rule that matters: a name is not a proof
+
+Every claim must be labelled **proven**, **measured**, or **speculative**, and bound to
+something checkable — a theorem, a test, or a reproducible measurement. A pull request that
+adds a capability claim without a test or a reproduction is not ready, however elegant.
+
+- **Soundness is non-negotiable.** The frames and the certified paths must never emit a
+  wrong `SAT`/`UNSAT`. New frame logic needs a differential test against a trusted oracle
+  (brute force on small cases) and must *punt* (`CDCL_NEEDED`) rather than guess.
+- **Measure before you optimize.** Performance claims need a before/after measurement in a
+  script under `docs/ladder/scripts/`. Honest negatives are welcome and are recorded, not
+  hidden.
+- **Certification stays intact.** Anything that produces a verdict must keep it checkable:
+  SAT by model replay, UNSAT by a sound frame refutation or a DRAT proof.
+
+## Getting set up
+
+```bash
+pip install -e ".[dev,bench]"       # editable install + test/bench deps
+# external tools for full certification: install Kissat + drat-trim (see BACKEND_README.md)
+python -m pytest backend/tests -q   # the full suite must stay green
+```
+
+## Before opening a pull request
+
+1. `python -m pytest backend/tests -q` passes locally.
+2. New behaviour has a test; new/changed claims are labelled and reproducible.
+3. If you touched a benchmark claim, update [`REPRODUCIBILITY.md`](REPRODUCIBILITY.md) and
+   re-run the named command.
+4. Keep the voice honest and scoped — claims are bounded to the mix/axis they were measured
+   on, not generalized.
+
+## Style
+
+Match the surrounding code: its naming, comment density, and idiom. New research notes go
+under `docs/ladder/` and are linked from its index with a one-line, honest summary.
 Contributions are welcome, but this repository has a strict claim discipline.
 
 ## Core rule
@@ -43,4 +83,4 @@ python -m backend.cli examples/simple_unsat.cnf --mode strict
 
 ## Style
 
-Keep the public surface readable for a skeptical stranger. The poetic layer is allowed, but the first-contact path must make the executable claim clear before the metaphor.
\ No newline at end of file
+Keep the public surface readable for a skeptical stranger. The poetic layer is allowed, but the first-contact path must make the executable claim clear before the metaphor.
diff --git a/README.md b/README.md
index 41338b9..2bfb5de 100644
--- a/README.md
+++ b/README.md
@@ -101,6 +101,13 @@ flowchart TD
 ```
 
 - **frame router** (`frame_solver.py`) — the three frames + their coupling, refute-first.
+- **metasolver** (`metasolver.py`) — reverts the dynamical description into a dispatch. On a
+  *counting-and-parity-inclusive mix* (not the competition set) it wins on PAR-2 over Kissat,
+  CaDiCaL and CryptoMiniSat — because it is instant where they blow up on counting, and
+  comparable elsewhere. A structural result on a specific mix, not a generally faster solver.
+- **meta-metasolver** (`metametasolver.py`) — the minimax mixed strategy; on the heavy-tailed
+  random-3SAT band it *out-searches CMS in wall-clock* (parallel, at a `k×` CPU cost, no CMS
+  in the pool). Single-thread on few cores, this advantage shrinks — see the honest scope.
 - **metasolver** (`metasolver.py`) — description-driven dispatch. On the included
   competition-style mix, its aggregate win comes from routing structured islands before
   CDCL, not from a claim of general CDCL dominance.
@@ -112,6 +119,10 @@ flowchart TD
 - **the view from outside** — `dynamics.py` (laws/relations/motions), `fabric.py` +
   `fabric_model.py` (the hyperbolic instance-manifold), `observer.py` (the adjudicator).
 
+> Every number here is a *measured* claim on a small, fixed, synthetic mix — regenerate it
+> with one command and read the scope in [`REPRODUCIBILITY.md`](REPRODUCIBILITY.md). This is
+> a certified middleware and a research harness, **not** a claim of a generally faster SAT
+> solver.
 For exact measured/proven/speculative status, read [`PUBLIC_RESEARCH_CLAIMS.md`](PUBLIC_RESEARCH_CLAIMS.md)
 and [`REPRODUCIBILITY.md`](REPRODUCIBILITY.md) before citing benchmark numbers.
 
@@ -169,6 +180,8 @@ assert r.certified                              # every verdict carries its proo
 ```
 backend/
   frame_solver.py      three sound frames + coupling (the router)
+  metasolver.py        description-driven dispatch  (beats CMS on the mix)
+  metametasolver.py    fractal portfolio           (out-searches CMS on the tail, parallel)
   metasolver.py        description-driven dispatch  (scoped benchmark mix)
   metametasolver.py    fractal portfolio           (scoped heavy-tail benchmark)
   acaf.py              adaptive actor-critic policy (cores-sized mixed strategy)
diff --git a/REPRODUCIBILITY.md b/REPRODUCIBILITY.md
index cdcfd61..d0582a2 100644
--- a/REPRODUCIBILITY.md
+++ b/REPRODUCIBILITY.md
@@ -1,5 +1,66 @@
 # Reproducibility
 
+Every benchmark claim in this repository is a **repo-internal measured claim** on a stated
+mix, timeout, and environment — not an external competition result. This file gives the
+exact command, environment, and expected shape of each so you can regenerate it. Numbers
+are **hardware-sensitive** (wall-clock, core count); regenerate on your machine rather than
+trusting the absolute seconds.
+
+## Environment (as measured)
+
+| component | version |
+|---|---|
+| Python | 3.11 / 3.12 (CI matrix) |
+| numpy | 2.4.6 |
+| Kissat | 4.0.4 |
+| CaDiCaL | 3.0.0 |
+| CryptoMiniSat (`pycryptosat`) | 5.14.7 |
+| drat-trim | (DRAT proof checker) |
+| dev container | 4 vCPU (the portfolio/parallel numbers are core-bound — see below) |
+
+```bash
+pip install -e ".[dev,bench]"
+# external, non-pip: install Kissat + drat-trim (see BACKEND_README.md)
+python -m pytest backend/tests -q        # 650 tests; the soundness/certification floor
+```
+
+## The measured claims, and how to regenerate each
+
+Each row: the command, the timeout, and what the output should show. Instance lists are
+fixed in the harness (deterministic seeds); the JSON outputs are git-ignored so you can
+diff your run against the table.
+
+| claim | command | timeout | expected shape |
+|---|---|---|---|
+| **frame-aware middleware vs raw CDCL** | `python -m docs.ladder.scripts.sota_benchmark` | 20 s | middleware 40/40, PAR-2 ~0.05 s; Kissat 35/40 ~5.4 s; CaDiCaL 36/40 ~4.3 s; 40/40 certified; 26/40 frame-decided |
+| **vs CryptoMiniSat (four-way)** | `python -m docs.ladder.scripts.metasolver_benchmark` | 20 s | CMS 38/40, PAR-2 ~2.7 s; metasolver 40/40, PAR-2 ~0.05 s; CMS times out on php10/php12 (counting), metasolver instant there |
+| **out-search CMS on random-3SAT** | `python -m docs.ladder.scripts.metametasolver_benchmark` | 30 s | on the n=220–280 hard band, the fractal portfolio beats CMS wall-clock on the majority of instances (PAR-2 ~1.6×); loses trivial instances to launch overhead; CPU cost ≈ breadth× |
+| **NS degree vs width incomparable** | `python -m pytest backend/tests/test_ladder_contracts.py -k incomparable -q` | — | PHP (width 2, NS 4); Tseitin K4 (width 4, NS 3) — neither dominates |
+| **hard certification actually runs** | `python .github/scripts/certification_smoke.py` | — | "CERTIFICATION LANE PASSED": a CDCL UNSAT DRAT-checked and a CDCL SAT model-replayed |
+
+## How to interpret a discrepancy
+
+- **Solved-count differs.** Almost always a timeout/hardware difference. Solved-count is
+  robust; PAR-2 seconds are not — re-read them relative to *your* Kissat baseline, not ours.
+- **The portfolio does not beat CMS on your box.** Expected on ≤2 cores: the meta-metasolver
+  is a *parallel* mixed strategy; with few cores its arms contend and the wall-clock win
+  shrinks or vanishes. It is the `k×`-CPU-for-wall-clock trade, stated in
+  [`docs/ladder/GAME_THEORY_NOTE.md`](docs/ladder/GAME_THEORY_NOTE.md). The single-thread
+  claims (frames, metasolver on counting/parity) are core-independent.
+- **A frame verdict disagrees with a trusted solver.** That would be a **soundness bug** —
+  the one class we treat as critical. Please report it (see `SECURITY.md`) with the formula.
+
+## Scope of the claims (read this before quoting a number)
+
+These are measured on a **small, fixed, synthetic competition-style mix** (random-3SAT,
+Tseitin, XORSAT, pigeonhole, mixed), not the SAT Competition benchmark set. The honest
+one-line reading:
+
+> On a mix that includes the counting and parity fragments, the frame-aware middleware
+> dominates raw CDCL and CryptoMiniSat on PAR-2 because it is instant where they blow up
+> (counting) and comparable elsewhere; on the unstructured tail a parallel portfolio can
+> out-search CMS at a CPU cost. This is a *structural* result on a *specific mix* — not a
+> claim of a generally faster SAT solver.
 This repository has two separable surfaces:
 
 1. **Certified solving path** — every emitted SAT/UNSAT verdict is independently checked: SAT by model replay, UNSAT by a sound frame refutation or by `drat-trim` over a DRAT proof.
@@ -74,4 +135,4 @@ Before citing or announcing a result, check `PUBLIC_RESEARCH_CLAIMS.md` and `doc
 
 - **proven** means theorem-backed or sound-by-construction;
 - **measured** means benchmarked under stated scope;
-- **speculative** means a lens or research direction and is not load-bearing.
\ No newline at end of file
+- **speculative** means a lens or research direction and is not load-bearing.
diff --git a/SECURITY.md b/SECURITY.md
index c1efad6..9dd0cf3 100644
--- a/SECURITY.md
+++ b/SECURITY.md
@@ -1,3 +1,39 @@
+# Security policy
+
+This is a research library and CLI, not a network service. Its security surface is
+unusual and worth stating plainly: the project's core promise is **soundness** — that a
+verdict it certifies is correct. The most serious class of defect here is therefore not a
+memory-safety bug but a **soundness bug**: a formula reported `SAT`/`UNSAT` (with
+`certified = True`) whose verdict is wrong.
+
+## Trusted computing base
+
+By design, the external SAT solver (Kissat) is **not trusted**. Every verdict is
+re-checked by a small, independent core:
+
+- SAT — the model is replayed against the original formula (`cnf_utils.verify_model`);
+- UNSAT via a frame — sound by construction (2-SAT SCC, GF(2) refutation, counting bound);
+- UNSAT via CDCL — the DRAT proof is replayed by `drat-trim` (LRAT optional).
+
+A bug in Kissat, CaDiCaL, or CryptoMiniSat that produced a wrong answer would be **caught**
+by this core, not trusted. A soundness-relevant bug is therefore one in the trusted core
+itself (parser, Tseitin transform, model checker, the frame refutations, or the proof-checker
+invocation).
+
+## Reporting a vulnerability
+
+Please report privately rather than in a public issue:
+
+- Use **GitHub Security Advisories** ("Report a vulnerability") on this repository, or
+- email the maintainer via the address on the GitHub profile of the repository owner.
+
+Please include a minimal reproducing formula and the observed vs expected verdict. A
+witnessed soundness violation (a certified-but-wrong verdict) will be treated as the
+highest priority.
+
+## Supported versions
+
+The project is pre-1.0; fixes land on the default branch. Pin a commit for reproducibility.
 # Security Policy
 
 Please do **not** report security issues through public GitHub issues, discussions, or pull requests.
@@ -22,4 +58,4 @@ Please include:
 
 ## Operational safety
 
-For untrusted inputs, prefer the Docker container or another sandbox. Do not run untrusted CNF/proof corpora with elevated privileges. External solver binaries are outside this project's trusted computing base; this project verifies SAT/UNSAT verdicts, but it does not make external solver processes memory-safe.
\ No newline at end of file
+For untrusted inputs, prefer the Docker container or another sandbox. Do not run untrusted CNF/proof corpora with elevated privileges. External solver binaries are outside this project's trusted computing base; this project verifies SAT/UNSAT verdicts, but it does not make external solver processes memory-safe.
diff --git a/backend/cli.py b/backend/cli.py
index 91bb715..fbd4886 100644
--- a/backend/cli.py
+++ b/backend/cli.py
@@ -194,10 +194,13 @@ async def main():
         sys.exit(1)
 
 
+def cli_main():
+    """Synchronous console-script entry point (see pyproject.toml)."""
 def main_cli():
     """Synchronous console-script entry point for pyproject.toml."""
     asyncio.run(main())
 
 
 if __name__ == '__main__':
+    cli_main()
     main_cli()
diff --git a/docs/_config.yml b/docs/_config.yml
new file mode 100644
index 0000000..76a8717
--- /dev/null
+++ b/docs/_config.yml
@@ -0,0 +1,13 @@
+# Minimal GitHub Pages config — austere by intent (plain Markdown, no theatre).
+# Serve from /docs on the default branch: Settings → Pages → Source: main /docs.
+title: λSAT
+description: >-
+  Certified frame-first SAT middleware — structured regions before CDCL,
+  certified verdicts after every path.
+theme: jekyll-theme-minimal
+show_downloads: false
+
+# Keep the research subtrees out of the built site index (still browsable on GitHub).
+exclude:
+  - vdis/
+  - __pycache__/
diff --git a/docs/assets/architecture.mmd b/docs/assets/architecture.mmd
new file mode 100644
index 0000000..b638e47
--- /dev/null
+++ b/docs/assets/architecture.mmd
@@ -0,0 +1,19 @@
+%% λSAT architecture — the certified frame-first router.
+%% Source of truth for the diagram; renders on github.com and via mermaid-cli.
+flowchart TD
+    F([formula]) --> R{router}
+    R -->|"binary clauses"| IMP["implication frame (2-SAT)<br/>SCC contradiction / assignment"]
+    R -->|"XOR structure"| PAR["parity frame (GF(2))<br/>Gaussian refutation / model"]
+    R -->|"pigeonhole shape"| CNT["counting frame (ℤ)<br/>k &gt; m magnitude contradiction"]
+    R -->|"none of the above"| CDCL["CDCL fallback (Kissat)"]
+
+    IMP --> OBS([observer — certify])
+    PAR --> OBS
+    CNT --> OBS
+    CDCL -->|"UNSAT: DRAT replay<br/>SAT: model replay"| OBS
+    OBS --> V([certified verdict])
+
+    classDef frame fill:#eef,stroke:#557;
+    classDef fallback fill:#fee,stroke:#755;
+    class IMP,PAR,CNT frame;
+    class CDCL fallback;
diff --git a/docs/benchmark-capsule.md b/docs/benchmark-capsule.md
new file mode 100644
index 0000000..e721fe5
--- /dev/null
+++ b/docs/benchmark-capsule.md
@@ -0,0 +1,75 @@
+---
+title: "Benchmark capsule"
+---
+
+# Benchmark capsule
+
+Every number here is a **measured** claim on a small, fixed, synthetic mix — **not** the SAT
+Competition set, and **not** a claim of general CDCL dominance. Numbers are hardware-sensitive
+(wall-clock, core count); regenerate on your machine. Commands and pinned versions:
+[REPRODUCIBILITY.md](https://github.com/jesusvilela/lambda-sat-solver/blob/main/REPRODUCIBILITY.md).
+
+## Setup
+
+| | |
+|---|---|
+| **engines** | Kissat 4.0.4 · CaDiCaL 3.0.0 · CryptoMiniSat 5.14.7 (pycryptosat) |
+| **families** | random-3SAT (α≈4.26) · Tseitin/XOR · XORSAT · pigeonhole (PHP) · mixed |
+| **timeout** | 20 s (main mix) · 30 s (random-3SAT tail study) |
+| **hardware** | 4 vCPU dev container (portfolio numbers are core-bound) |
+| **metric** | solved-count and PAR-2 (timeout counts as 2×) |
+| **certification** | every middleware verdict: SAT model-replayed, UNSAT frame-sound or DRAT |
+
+## Main mix — frame-aware middleware vs raw CDCL and CMS
+
+`python -m docs.ladder.scripts.metasolver_benchmark` · 40 instances · 20 s
+
+| family | n | Kissat | CaDiCaL | CryptoMiniSat | **middleware** |
+|---|---|---|---|---|---|
+| random-3SAT | 9 | 9/9 · 0.12 s | 9/9 · 0.13 s | 9/9 · 0.18 s | 9/9 · 0.23 s |
+| Tseitin (parity) | 9 | 5/9 · 18.98 s | 5/9 · 18.83 s | 9/9 · 0.95 s | **9/9 · 0.00 s** |
+| XORSAT | 12 | 12/12 · 0.00 s | 12/12 · 0.00 s | 12/12 · 0.00 s | 12/12 · 0.00 s |
+| PHP (counting) | 4 | 3/4 · 10.77 s | 4/4 · 0.12 s | **2/4 · 24.51 s** | **4/4 · 0.00 s** |
+| mixed | 6 | 6/6 · 0.00 s | 6/6 · 0.00 s | 6/6 · 0.00 s | 6/6 · 0.01 s |
+| **total** | 40 | 35/40 · 5.38 s | 36/40 · 4.28 s | 38/40 · 2.71 s | **40/40 · 0.05 s** |
+
+CryptoMiniSat is the strongest baseline (38/40): its Gaussian engine **owns parity** (9/9
+Tseitin, where the raw CDCL engines get 5/9). It carries **no counting engine**, so
+pigeonhole is exponential for it (php10/php12 time out) while the counting frame is instant.
+
+## Random-3SAT tail — the honest tunnel
+
+`python -m docs.ladder.scripts.metametasolver_benchmark` · n=220–280 · 30 s
+
+| solver | solved | PAR-2 (wall) |
+|---|---|---|
+| single Kissat (1 core) | 15/16 | ~5.3 s |
+| CryptoMiniSat (1 core) | 14/16 | 10.01 s |
+| fractal portfolio (~nproc cores) | 15/16 | 6.22 s — beats CMS wall-clock on 13/16 |
+
+The portfolio's advantage over CMS is a **parallel, mixed-strategy** effect (heavy-tailed
+runtime collapsed by diversified seeds), paid for in `k×` CPU. On few cores it shrinks. It is
+**not** a smarter search, and it does **not** beat a single strong Kissat by much on this box.
+
+## What improves
+
+- **Counting**: instant certified refutation where CDCL and CMS are exponential (PHP).
+- **Parity**: instant certified verdict; even CMS's Gaussian engine is matched or beaten in
+  wall-clock by the direct GF(2) refutation.
+- **Aggregate PAR-2 on this mix**: dominated by the structured families the frames own.
+
+## What does **not** improve
+
+- **Random-3SAT**: no exposed frame; the middleware falls to CDCL and is only *comparable* —
+  CMS is competitive-to-faster there. This is CDCL's territory and stays that way.
+- **Single-thread on obfuscated structure**: if the XOR/counting structure is hidden from the
+  cheap detectors, the frame does not fire.
+- **Trivial instances under certification**: the DRAT proof of a trivial CDCL UNSAT can cost
+  more than the solve — an uncertified solver returns faster. That is the price of proof, and
+  it is intentional.
+
+## One-line reading
+
+> On a mix that includes the counting and parity fragments, certified frame routing decides
+> the structured islands instantly and provably, and hands the unstructured tail to CDCL. The
+> advantage is structural and scoped — not a generally faster SAT solver.
diff --git a/docs/index.md b/docs/index.md
new file mode 100644
index 0000000..b462440
--- /dev/null
+++ b/docs/index.md
@@ -0,0 +1,151 @@
+---
+title: "λSAT — Certified Frame-First SAT Middleware"
+description: "Structured regions before CDCL. Certified verdicts after every path."
+---
+
+# λSAT
+
+### Certified frame-first SAT middleware
+
+*Structured regions before CDCL. Certified verdicts after every path.*
+
+λSAT is a certified SAT middleware. **It does not try to replace CDCL.** It first checks
+whether a formula belongs to one of several structured regions with sound algebraic
+certificates — implication, parity, or counting — and falls back to CDCL otherwise. Every
+emitted verdict is independently checked.
+
+That is the whole recognizer. The geometry comes later, and only as a map.
+
+---
+
+## 1 · The question
+
+Modern SAT solvers are extremely strong, but a solver's *output* is not by itself an
+*explanation*. λSAT asks a smaller, answerable question:
+
+> Can some structured SAT regions be recognized and certified **before** search, while the
+> unstructured tail is handed honestly to CDCL?
+
+This deliberately avoids the dangerous claim of "a new solver that beats SOTA."
+
+---
+
+## 2 · Certification — the trusted computing base
+
+This is the part that matters most.
+
+- **SAT** is checked by **model replay** against the original formula.
+- **UNSAT** is checked by either a **sound frame refutation** (self-certifying) or an
+  **independent DRAT proof replay** (`drat-trim`).
+- **Kissat, CaDiCaL, CryptoMiniSat are tools, not trusted authorities.**
+
+The middleware can be wrong only if a *checker or a frame* is wrong — never merely because
+an external solver said so. A wrong answer from the engine is **caught, not believed.**
+
+```
+formula
+  │
+  ▼
+router ── implication? ─ yes ─▶ 2-SAT frame ─────┐
+  │        parity?      ─ yes ─▶ GF(2) frame ─────┤
+  │        counting?    ─ yes ─▶ counting frame ──┤ sound by construction
+  │                                               │
+  └── none of the above ─────▶ CDCL (Kissat) ─────┤ DRAT / model replay
+                                                  ▼
+                                          certified verdict
+```
+
+---
+
+## 3 · The three frames
+
+Each structured region has one sound, engine-independent frame, with an input condition, a
+certificate, and an honest failure mode (it *punts* to CDCL rather than guessing).
+
+| frame | structure | certificate |
+|---|---|---|
+| **implication** | 2-SAT / implication graph | SCC contradiction, or an assignment |
+| **parity** | GF(2) / XOR structure | linear-algebra refutation or model |
+| **counting** | pigeonhole / cardinality | an arithmetic (magnitude) contradiction |
+| **fallback** | general SAT | CDCL + model replay / DRAT |
+
+The contribution is **not** replacing CDCL. It is **deciding structured islands before
+CDCL, and certifying every emitted verdict.**
+
+---
+
+## 4 · What the benchmark claims — and doesn't
+
+The benchmark claim is **scoped to the included mix** (a small, fixed, synthetic set:
+2-SAT, Tseitin/XOR, pigeonhole, random-3SAT, mixed). It does **not** imply general CDCL
+dominance.
+
+| family | why hard for CDCL | λSAT route | result shape |
+|---|---|---|---|
+| 2-SAT / implication | implication closure | implication frame | instant · certified |
+| Tseitin / XOR | parity obstruction | GF(2) frame | instant · certified |
+| PHP / counting | cardinality obstruction | counting frame | instant · certified |
+| random-3SAT | no exposed frame | CDCL / portfolio | **CDCL remains central** |
+
+Numbers (PAR-2, per-family) live in the [benchmark capsule](benchmark-capsule.md), not on
+this page — the headline is the *routing and certification*, not a speed record.
+
+---
+
+## 5 · What it does **not** claim
+
+- It does **not** solve SAT hardness.
+- It does **not** dominate CDCL on arbitrary SAT.
+- It does **not** claim CryptoMiniSat is weak on XOR (CMS owns parity; the frame merely
+  re-derives it with a certificate).
+- It does **not** make external solvers trusted.
+- The hyperbolic / fabric layer is a **research map**, not part of the minimal certification
+  claim.
+
+---
+
+## 6 · Reproduce
+
+```bash
+git clone https://github.com/jesusvilela/lambda-sat-solver
+cd lambda-sat-solver
+pip install -e ".[dev]"
+python -m pytest backend/tests/ -q          # the soundness / certification floor
+```
+
+The certified strict path (requires Kissat + `drat-trim`):
+
+```bash
+python -m backend.cli examples/simple_sat.cnf   --mode strict     # SAT, model-replayed
+python -m backend.cli examples/simple_unsat.cnf --mode strict     # UNSAT, checked
+```
+
+Full environment, pinned versions, and per-benchmark commands:
+[REPRODUCIBILITY.md](https://github.com/jesusvilela/lambda-sat-solver/blob/main/REPRODUCIBILITY.md).
+
+---
+
+## 7 · The research ladder (a map, not a proof)
+
+Only after the engineering is clear: the research layer studies *where SAT hardness lives* —
+resolution width, Nullstellensatz degree, parity, counting, symmetry, and heavy-tailed
+search. Honestly:
+
+- resolution width and Nullstellensatz degree are **incomparable** (neither dominates);
+- cheap graph-structural scalars **failed** to carry random-3SAT hardness;
+- the geometry is used as a **routing / modeling lens**, not as proof by metaphor.
+
+Index: [`docs/ladder/`](ladder/). Claim discipline: [`docs/CHARTER.md`](CHARTER.md).
+
+---
+
+## Links
+
+- [Repository](https://github.com/jesusvilela/lambda-sat-solver)
+- [Technical note](technical-note.md) · [Benchmark capsule](benchmark-capsule.md)
+- [Reproducibility](https://github.com/jesusvilela/lambda-sat-solver/blob/main/REPRODUCIBILITY.md)
+  · [Claim ledger](https://github.com/jesusvilela/lambda-sat-solver/blob/main/PUBLIC_RESEARCH_CLAIMS.md)
+- [Security policy](https://github.com/jesusvilela/lambda-sat-solver/blob/main/SECURITY.md)
+  · [Citation](https://github.com/jesusvilela/lambda-sat-solver/blob/main/CITATION.cff)
+
+*Route when structure is sufficient. Search when it is not. Verify either way.*
diff --git a/docs/ladder/README.md b/docs/ladder/README.md
index 71652a4..3ef7790 100644
--- a/docs/ladder/README.md
+++ b/docs/ladder/README.md
@@ -10,6 +10,10 @@ and every rung says so.
 - **Two genuine hardness carriers, theorem-backed.** `min_refutation_width`
   (Ben-Sasson–Wigderson: width lower-bounds resolution size) and
   `nullstellensatz_degree` (Clegg–Edmonds–Impagliazzo: PC degree lower-bounds
+  PC size). They are related but **incomparable** — neither dominates: PHP(3→2)
+  has NS 4 > width 2, while Tseitin K4 has NS 3 < width 4 (measured, both
+  directions; test `test_ns_and_width_are_incomparable`). Both are exact and
+  exponential — the right object is genuinely expensive.
   PC size). They are exact, expensive, and **incomparable**: PHP(3→2) separates
   one way (NS 4 > width 2), while Tseitin K4 separates the other way
   (NS 3 < width 4). The right object is genuinely stratified, not one scalar.
@@ -32,6 +36,9 @@ and every rung says so.
 ## What's proven vs open
 
 - **Proven / measured:** the two size lower bounds (BSW, CEI) as theorems the
+  carriers compute against; the Rung-1 negative on our own instances; NS and
+  width **incomparable** (PHP 4>2, Tseitin K4 3<4); the char-2 collapse of the
+  naive symmetry channel.
   carriers compute against; the Rung-1 negative on our own instances; width and
   Nullstellensatz degree as distinct, mutually non-dominating carriers; the
   char-2 collapse of the naive symmetry channel.
diff --git a/docs/technical-note.md b/docs/technical-note.md
new file mode 100644
index 0000000..a762d5d
--- /dev/null
+++ b/docs/technical-note.md
@@ -0,0 +1,116 @@
+---
+title: "Structured Islands Before CDCL — A Certified SAT Middleware"
+---
+
+# Structured Islands Before CDCL
+
+### A certified SAT middleware
+
+*A narrow, reviewable note: here is the executable claim, here is the certification
+boundary, here is where CDCL remains sovereign.*
+
+## Abstract
+
+λSAT is a headless SAT middleware that decides *structured* formulas before search and
+hands the rest to CDCL. A router tries three sound, engine-independent frames —
+implication (2-SAT), parity (GF(2)/XOR), and counting (pigeonhole/cardinality) — and their
+cross-frame coupling; a formula that lives in one is decided with a certificate and no
+search. Anything else returns `CDCL_NEEDED` and is solved by Kissat. **Every emitted verdict
+is independently checked**: SAT by model replay, UNSAT by a sound frame refutation or a
+`drat-trim` DRAT proof. The external solver is never a trusted authority. The benchmark
+claim is scoped to a small synthetic mix that includes the counting and parity fragments;
+it is a statement about *certified frame routing*, not about generally out-searching CDCL.
+
+## 1 · Motivation
+
+SAT solvers are powerful, and getting a formula *solved* is rarely the problem. The problem
+addressed here is narrower: some formulas carry structure whose contradiction is decidable
+by a short algebraic argument **before** any search, and that argument is its own
+certificate. λSAT separates that structured decision from unstructured search, and — the
+non-negotiable part — verifies whatever it emits.
+
+## 2 · Architecture
+
+```
+formula → router → { implication | parity | counting | coupling } → verdict → observer
+                        └───────────── else: CDCL_NEEDED ──────────→ Kissat → observer
+```
+
+The router is refute-first (cheap near-linear refutation before any model reconstruction).
+The observer is the certification stage: it accepts a verdict only with a checkable
+certificate. `strict` mode requires the external tools to be present at startup and turns an
+uncertified fallback verdict into an error; `dev`/`research` modes degrade to best-effort.
+
+## 3 · The three frames
+
+Each frame has an **input condition**, a **certificate**, and a **failure mode** (it must
+punt, never guess).
+
+- **Implication (2-SAT).** Condition: binary clauses. Certificate: a strongly-connected
+  component placing a variable and its negation together (a sound UNSAT), or a satisfying
+  assignment. Failure: no binary contradiction → punt.
+- **Parity (GF(2)).** Condition: recoverable XOR constraints. Certificate: Gaussian
+  elimination reaching `0 = 1` (UNSAT), or a reconstructed, re-verified model. Failure:
+  parity does not cover the formula / underdetermined → punt.
+- **Counting (ℤ).** Condition: pigeonhole-shaped `k` disjoint at-least-one clauses covered
+  by `m < k` at-most-one cliques. Certificate: the magnitude contradiction `k > m`. Failure:
+  structure absent → punt.
+
+The **coupling** exchanges entailed literals across frames to a fixpoint (Nelson–Oppen), so
+an instance no single frame decides can still be decided soundly; it too only emits UNSAT via
+a channel refutation or SAT via a verified model.
+
+## 4 · Certification boundary
+
+| | trusted | not trusted |
+|---|---|---|
+| components | DIMACS parser · Tseitin transform · model checker · the three frame refutations · the DRAT-checker invocation | Kissat · CaDiCaL · CryptoMiniSat |
+
+- **SAT** → the assignment is replayed against the original clauses.
+- **UNSAT via a frame** → sound by construction (no external checker).
+- **UNSAT via CDCL** → the DRAT proof is replayed by `drat-trim` (LRAT optional).
+
+A CI lane (`certification-hard`) makes Kissat + `drat-trim` mandatory and fails red unless a
+real DRAT UNSAT check and a real model-replay SAT check both execute.
+
+## 5 · Benchmark capsule
+
+Full detail in the [benchmark capsule](benchmark-capsule.md). In one paragraph: on a fixed
+synthetic mix (random-3SAT, Tseitin, XORSAT, pigeonhole, mixed; 20 s timeout), the
+frame-aware middleware decides the structured families instantly and certified, while raw
+CDCL and CryptoMiniSat spend seconds or time out on the parity/counting families. On the
+unstructured random-3SAT tail the middleware falls to CDCL and is **comparable**, not
+better. The aggregate PAR-2 advantage is therefore a *structural* effect of the mix, not a
+faster search.
+
+## 6 · Interpretation
+
+- **Frame-decidable islands** vs the **CDCL tunnel** — a formula either exposes an algebraic
+  obstruction (decide + certify) or it does not (search).
+- A parallel, seed-diversified **portfolio** helps only on the heavy-tailed tail, and only by
+  spending cores for wall-clock; it is a mixed strategy, not a smarter search.
+- **No-Free-Lunch holds.** There is no general dominance here, and none is claimed.
+
+## 7 · Limitations
+
+- The benchmark mix is **not** the SAT Competition set.
+- Frames fire **only** when structure is exposed; obfuscated structure is missed.
+- Random-3SAT is, and remains, **CDCL territory**.
+- Strict-mode UNSAT via the fallback still requires external proof tooling (`drat-trim`).
+
+## 8 · Reproduction
+
+```bash
+pip install -e ".[dev]"
+python -m pytest backend/tests/ -q
+python .github/scripts/certification_smoke.py     # forces a real DRAT + model-replay check
+```
+
+Pinned versions, per-benchmark commands, and how to read a discrepancy:
+[REPRODUCIBILITY.md](https://github.com/jesusvilela/lambda-sat-solver/blob/main/REPRODUCIBILITY.md).
+
+## 9 · Conclusion
+
+λSAT is a claim-discipline artifact as much as a solver: **route when structure is
+sufficient, search when it is not, verify either way.** The interesting object is the
+certified boundary between the two — not a speed record.
diff --git a/pyproject.toml b/pyproject.toml
index 7ce5d89..36957e8 100644
--- a/pyproject.toml
+++ b/pyproject.toml
@@ -1,10 +1,43 @@
 [build-system]
+requires = ["setuptools>=61.0", "wheel"]
 requires = ["setuptools>=68", "wheel"]
 build-backend = "setuptools.build_meta"
 
 [project]
 name = "lambda-sat-solver"
 version = "0.1.0"
+description = "Certified λ-logic SAT middleware and a research harness for frame-structured SAT hardness"
+readme = "README.md"
+requires-python = ">=3.11"
+license = { file = "LICENSE" }
+authors = [{ name = "Jesús Vilela Franco" }]
+keywords = [
+    "SAT", "satisfiability", "solver", "certified", "DRAT", "proof-checking",
+    "Kissat", "CryptoMiniSat", "computational-complexity", "lambda-calculus",
+]
+classifiers = [
+    "Development Status :: 4 - Beta",
+    "Intended Audience :: Science/Research",
+    "License :: OSI Approved :: MIT License",
+    "Programming Language :: Python :: 3.11",
+    "Programming Language :: Python :: 3.12",
+    "Topic :: Scientific/Engineering :: Mathematics",
+]
+dependencies = [
+    "numpy>=1.24.0",
+    "pydantic>=2.0.0",
+    # CryptoMiniSat baseline used by backend/cms_wrapper.py and the benchmarks.
+    # It is a *competitor* the metasolver is measured against, not part of the
+    # certified solve path; kept as a core dep so the test suite runs as shipped.
+    "pycryptosat>=5.11.0",
+]
+
+[project.optional-dependencies]
+dev = ["pytest>=7.4.0", "pytest-asyncio>=0.21.0"]
+bench = ["pycryptosat>=5.11.0"]
+
+[project.scripts]
+lambda-sat = "backend.cli:cli_main"
 description = "Certified SAT middleware and frame-structured SAT hardness research harness"
 readme = "README.md"
 requires-python = ">=3.11"
@@ -50,6 +83,17 @@ Homepage = "https://github.com/jesusvilela/lambda-sat-solver"
 Repository = "https://github.com/jesusvilela/lambda-sat-solver"
 Issues = "https://github.com/jesusvilela/lambda-sat-solver/issues"
 
+# External, non-pip tools are required for full certification (not installable via
+# pip): the Kissat SAT solver and the drat-trim DRAT checker (LRAT optional).
+# The three sound frames are self-certifying and need neither. See BACKEND_README.md.
+
+[tool.setuptools.packages.find]
+where = ["."]
+include = ["backend*"]
+exclude = ["backend.tests*"]
+
+[tool.pytest.ini_options]
+testpaths = ["backend/tests"]
 [project.scripts]
 lambda-sat = "backend.cli:main_cli"
 
@@ -58,4 +102,4 @@ include = ["backend*"]
 
 [tool.pytest.ini_options]
 testpaths = ["backend/tests"]
-pythonpath = ["."]
\ No newline at end of file
+pythonpath = ["."]