docs: presentation & navigation for newcomers (Phase 4)

README.md

@@ -1,5 +1,20 @@
 # Arda
 
+[![proof-lean](https://github.com/DrMurphyIsIn/Arda/actions/workflows/proof-lean.yml/badge.svg)](https://github.com/DrMurphyIsIn/Arda/actions/workflows/proof-lean.yml)
+[![proof-verify](https://github.com/DrMurphyIsIn/Arda/actions/workflows/proof-verify.yml/badge.svg)](https://github.com/DrMurphyIsIn/Arda/actions/workflows/proof-verify.yml)
+[![telperion-lean-e2e](https://github.com/DrMurphyIsIn/Arda/actions/workflows/telperion-lean-e2e.yml/badge.svg)](https://github.com/DrMurphyIsIn/Arda/actions/workflows/telperion-lean-e2e.yml)
+
+> **TL;DR** — A Lean 4 / Mathlib formalization of the machine-checkable core of a
+> 42-year-old extremal-graph-theory problem (the Brualdi–Goldwasser tree maximizer,
+> `per(L(T))/∏deg`), the reusable certificate engine — [**Telperion**](telperion/) —
+> that generated it, and a second front in proof complexity. Everything is checked
+> by the Lean kernel with **no `sorry`, no added axioms**, and an *executable* honesty
+> ledger. **The conjecture is not claimed proved.** New here? Start at
+> **[STATUS.md](STATUS.md)** for the proven-vs-open map, then see
+> [Verifying the claims](#verifying-the-claims) to re-run the kernel checks yourself.
+> Want to use the engine on your own problem? See
+> [`telperion/docs/GETTING_STARTED.md`](telperion/docs/GETTING_STARTED.md).
+
 This repository is a working research program, kept honest in public form:
 machine-checked progress on a 42-year-old open problem in extremal graph
 theory, the general-purpose proof engine that campaign forged, and — most

telperion/CONTRIBUTING.md

@@ -0,0 +1,99 @@
+# Contributing to Telperion
+
+Telperion is an **untrusted generator over a trusted kernel**: contributions may
+be as clever or as hacky as you like internally, because the Lean kernel re-checks
+the output. What the review process protects is not the generator's cleverness but
+its **honesty** — that every emitted theorem is non-vacuous, byte-reproducible, and
+means what it says. This guide is about clearing those gates.
+
+New here? Read [`docs/ARCHITECTURE.md`](docs/ARCHITECTURE.md) first (the pipeline
+and the engine/research-lab boundary), then [`docs/GETTING_STARTED.md`](docs/GETTING_STARTED.md).
+
+## Setup
+
+```bash
+pip install -e "telperion[dev]"     # sympy + pytest + numpy + networkx
+cd telperion
+python -m pytest tests -q           # the suite should be green before you start
+```
+
+Keep the **engine core (`src/telperion/`) sympy-only**. numpy/networkx belong to
+the `bg/` research lab and the `[bg]` extra; cvxpy belongs to the `[sdp]` finders.
+`tests/test_core_boundary.py` enforces this and will fail if the core imports them.
+
+## Adding a certificate shape (an emitter)
+
+1. **Write the emitter** — a new `src/telperion/emit_<shape>.py` whose class
+   subclasses `Emitter` (in `workflow.py`) and implements
+   `emit_body(family, profile) → (text, n_theorems)`. Certify in **exact
+   arithmetic** (`fractions.Fraction` / sympy); no floats on the certificate path.
+2. **Register it** — add the import to `src/telperion/__init__.py` (in the right
+   tier group). If it introduces a new certificate *kind*, register that kind in
+   `certify.py`.
+3. **Declare a sensitivity stance** — add an entry to the `REGISTRY` in
+   `src/telperion/emitter_sensitivity.py`. This is mandatory:
+   `tests/test_certificate_sensitivity.py::test_every_emitter_is_classified`
+   fails until you do. Choose honestly:
+   - **`CERTIFICATE_SENSITIVE`** — the emitted theorem carries a corruptible
+     witness (a specific numeric/algebraic identity). You must also add a
+     negative-control adapter under `negctrl_adapters/` that forges the witness
+     and confirms the kernel rejects it.
+   - **`STRUCTURALLY_NONVACUOUS`** — the theorem is positivity / decidability /
+     finite-cover / hypothesis-gated glue with no corruptible witness; the
+     built-in structural non-vacuity check suffices. Write a one-line note saying
+     *why* (see the existing entries — e.g. `HalfPlaneDiskEmitter` — as a model).
+4. **Add a worked example** — a `examples/<shape>/generate.py` that certifies →
+   emits → writes `lean/<Shape>.lean`, and supports `--check` (drift/byte-stability).
+   Include a `lakefile.toml` + `lean-toolchain` pinned to `leanprover/lean4:v4.32.0`,
+   matching every other example.
+5. **List it in the manifest** — add a `[[check]]` block to `telperion.toml`
+   (`name`, `script`, `group`). An unlisted `generate.py` is a hard CI failure
+   (the manifest-completeness gate). Pick the group by regeneration cost:
+   `quick` (seconds), `heavy` (minutes), `audit` (adversarial/large), `sdp`
+   (needs cvxpy).
+
+## Before you open a PR
+
+Run what CI runs:
+
+```bash
+cd telperion
+python -m pytest tests -q                         # unit tests (incl. the sensitivity gate)
+PYTHONPATH=src python -m telperion.cli verify --group quick   # regen drift + byte-stability
+python examples/<shape>/generate.py --check       # your example is byte-stable
+```
+
+And **verify the emitted Lean actually compiles** — the whole point:
+
+```bash
+cd examples/<shape>/lean && lake exe cache get && lake build
+```
+
+If you cannot run Lean locally, the CI `telperion-lean-e2e` job compiles emitted
+Lean for you; do not merge on a red Lean job.
+
+## CI gates your PR must pass
+
+| Workflow | What it checks |
+|---|---|
+| `telperion-test` | pytest across sympy versions + `verify --group quick` (drift + byte-stability). |
+| `telperion-lean-e2e` | regenerate emitted Lean and `lake build` it against pinned Mathlib. |
+| `telperion-casestudy` / `telperion-audit` | `verify --group heavy` / `--group audit` re-certification. |
+| `telperion-production` | frozen-artifact compile + regeneration diff. |
+| `telperion-comparator` | independent second check (whitelisted axioms only). |
+
+## House rules
+
+- **Honesty flags are load-bearing.** Keep `conjecture1_proved = False`; label
+  ranges, open pieces, and negative results as such. Preserve failed-route
+  `*_nogo*` modules with their reasons — they are part of the record.
+- **No floats on the certificate path.** Exact arithmetic only.
+- **Don't hand-edit emitted `.lean` files.** They are regenerated; edit the
+  generator and re-run.
+
+## Licensing
+
+The Telperion engine (`src/`, CLI, MCP server) is **BUSL-1.1**; emitted
+certificates and the `examples/` artifacts are Apache-2.0 (they are yours). See
+[`../LICENSING.md`](../LICENSING.md). By contributing you agree your changes are
+licensed on the same split terms.

telperion/README.md

@@ -4,6 +4,11 @@
 claims into kernel-checked Mathlib proofs by exact-arithmetic witness, not by
 trust.**
 
+> **New to Telperion?** → [Getting Started](docs/GETTING_STARTED.md) (install →
+> generate → verify a proof locally) · [Architecture](docs/ARCHITECTURE.md) (how it
+> works; engine vs. research lab) · [Contributing](CONTRIBUTING.md) (add a
+> certificate shape).
+
 You describe your problem as a parameterized *family* of statements. Telperion
 certifies each instance in exact rational arithmetic, then emits Lean 4 that
 Mathlib's kernel re-proves from scratch. **The generator is untrusted by

telperion/docs/ARCHITECTURE.md

@@ -0,0 +1,108 @@
+# Telperion architecture
+
+Telperion is a **certificate generator with an untrusted-generator / trusted-kernel
+trust model**: it may use any heuristic, search, or SDP solver to *find* a
+certificate, but the output is Lean that Mathlib's kernel re-proves from scratch.
+Nothing Telperion does needs to be trusted — a wrong certificate is a compile
+error, never a false theorem. This document maps the code onto that model.
+
+## The one boundary that matters: engine vs. research lab
+
+The package has two clearly separated parts, and the separation is **enforced by
+a test** (`tests/test_core_boundary.py`), not just convention:
+
+| | Path | What it is | Depends on |
+|---|---|---|---|
+| **Engine** | `src/telperion/` (everything except `bg/`) | The reusable, problem-agnostic tool: the pipeline, ~78 certificate emitters, the CLI, the MCP server, the self-verification layer. | sympy only (core) |
+| **Research lab** | `src/telperion/bg/` | The Brualdi–Goldwasser–specific research code (spectral helpers, tree search / MAP-Elites, Ehrhart probes). *Not* part of the reusable engine. | `[bg]` extra (numpy, networkx) |
+
+The core engine never imports `bg/`. If you want to use Telperion on your own
+problem, you only ever touch the engine; the `bg/` lab is one large worked
+example that happens to live in the same repository.
+
+## The pipeline
+
+Every emitted file goes through the same four stages:
+
+```
+define ─▶ certify() ─▶ validate ─▶ emit() ─▶ lake build (Lean kernel) ─▶ freeze()
+ family    exact cert    sanity       Lean          re-proves              byte-stable
+ spec      per instance  gates       output         from scratch           artifact
+```
+
+- **`family.py`** — an `InequalityFamily` is a parameterized grid of instances
+  (name, symbols, grid axes, constants, and the target per grid point). This is
+  the only thing *you* write.
+- **`certify.py`** — certifies each instance in **exact `fractions.Fraction` /
+  sympy** arithmetic. No floats on the certificate path.
+- **`workflow.py`** — `emit()` renders the certified family to Lean. All emitters
+  subclass the single `Emitter` base class here (interface: `emit_body(family,
+  profile) → (text, n_theorems)`); `LeanProfile` (in `lean.py`) carries
+  everything about the target Lean project the output must respect.
+- **`provenance.py`** — stamps the input-hash header, and `freeze()` writes the
+  byte-stable artifact + manifest that the regeneration-diff gate compares against.
+- **`lean.py`** — the Lean rendering (`file_shell`, the tactic skeletons; the
+  tactic contract is documented in [`TACTIC_CONTRACT.md`](TACTIC_CONTRACT.md)).
+
+## The certificate emitters
+
+~78 `emit_*.py` modules, each producing one *shape* of certificate. They are
+discovered by explicit imports in `src/telperion/__init__.py` (grouped by tier),
+and every family generator is listed in the top-level `telperion.toml` manifest
+(the source of truth for what CI regenerates and checks). Broadly:
+
+- **General / textbook** — direct Pólya positivity, SOS (rational, Artin
+  denominators), the Positivstellensatz family (Handelman, Putinar,
+  Nullstellensatz + infeasibility/refutation), Chvátal–Gomory rounding, Sturm,
+  Bernstein, exact identities, p-adic valuations, brackets, finite case analysis.
+- **Analytic / RH** — zero-free-region atoms, half-plane–disk (Borel–Carathéodory),
+  Jensen zero-count, transcendental enclosures.
+- **Brualdi–Goldwasser** — tight-cap enclosure, affine-parameter endpoint,
+  recursion/cavity closure, per-size dominance, curvature-boundary, integrality
+  gate (23-adic), and more.
+- **Proof complexity** — SOS refutation, pseudo-expectation duality, XOR moment
+  PSD, cone/Farkas infeasibility.
+
+Under the positivity shapes sits an **automatic certificate search** (the Pólya
+engine plus optional SDP finders under the `[sdp]` extra), so for many statements
+you never construct the certificate by hand.
+
+## The self-verification layer
+
+The Lean kernel catches *false* theorems. It cannot catch a theorem that is
+true-but-**vacuous** (e.g. a reflexive `X = X` that proves nothing). Telperion
+adds a layer specifically for that gap:
+
+- **`nonvacuity.py`** — refuses reflexive/trivial statements at emit time
+  (structural), and, for `CERTIFICATE_SENSITIVE` emitters, checks that corrupting
+  the certificate actually breaks the claim (semantic).
+- **`emitter_sensitivity.py`** — a registry forcing every emitter to declare a
+  stance: `CERTIFICATE_SENSITIVE` (carries a corruptible witness → needs a
+  kernel-gated negative-control adapter) or `STRUCTURALLY_NONVACUOUS`
+  (positivity / decidable / hypothesis-gated glue → no adapter needed). A new
+  emitter that declares neither **fails the test suite** until it does.
+- **`negctrl_adapters/`** — the per-emitter negative controls: forge the
+  certificate, confirm the kernel rejects the forgery.
+- **`comparator.py`** — the independent second check (whitelisted axioms only);
+  see [`COMPARATOR.md`](COMPARATOR.md).
+- **`circularity.py`, `coverage.py`, `faithfulness.py`, `metacircular.py`** —
+  non-circularity witnesses, coverage profiling, seeded-exact-point faithfulness,
+  and the audit calculus pointed at itself (which documents the one irreducible
+  trusted floor: whether a formal statement *means* the informal claim is
+  undecidable — Löb/Gödel).
+
+## Interfaces
+
+- **CLI** (`cli.py`, console script `telperion`) — `certify`, `emit`, `diff`,
+  `verify --group <quick|heavy|audit|sdp>`, `prove`, and the diagnosis helpers.
+- **MCP server** (`mcp_server.py`, console script `telperion-mcp`, `[mcp]` extra)
+  — exposes the same certify→emit pipeline as ~15 tools to LLM/RL agents, with no
+  emit-without-certify path. Registered as a Claude plugin under
+  `claude-plugin/`.
+
+## Where to look next
+
+- Use it end-to-end: [`GETTING_STARTED.md`](GETTING_STARTED.md).
+- Add a new certificate shape: [`../CONTRIBUTING.md`](../CONTRIBUTING.md).
+- The trust model in prose: [`METHODOLOGY.md`](METHODOLOGY.md).
+- The exact Mathlib tactic bindings: [`TACTIC_CONTRACT.md`](TACTIC_CONTRACT.md).

telperion/docs/GETTING_STARTED.md

@@ -0,0 +1,122 @@
+# Getting started with Telperion
+
+Telperion turns a *family of mathematical statements* into **Lean 4 proofs that
+Mathlib's kernel re-checks from scratch**. You describe the family; Telperion
+certifies each instance in exact rational arithmetic, emits Lean, and the Lean
+kernel is the sole thing you have to trust. This guide takes you from a clean
+machine to **an emitted certificate you have verified locally end-to-end**.
+
+There are two halves, and you can stop after the first:
+
+1. **Generate** — pure Python (sympy only). Fast, no Lean required.
+2. **Verify** — compile the emitted Lean against a pinned Mathlib. This is the
+   step that actually makes it a proof, and it is the part newcomers most often
+   skip because the toolchain setup is not obvious. It is written out in full below.
+
+## 1. Install the Python package
+
+Telperion requires **Python ≥ 3.11**. From the repository root:
+
+```bash
+pip install -e telperion            # the engine (sympy-only core)
+```
+
+Optional extras, installed as needed:
+
+```bash
+pip install -e "telperion[dev]"     # pytest + numpy + networkx (run the test suite)
+pip install -e "telperion[sdp]"     # cvxpy — the SDP certificate finders
+pip install -e "telperion[bg]"      # numpy + networkx — the Brualdi–Goldwasser research lab
+pip install -e "telperion[mcp]"     # expose Telperion to LLM agents over MCP
+```
+
+This installs two console commands: `telperion` (the CLI) and `telperion-mcp`
+(the MCP server). Check it works:
+
+```bash
+telperion --help
+```
+
+## 2. Generate a certificate (no Lean needed)
+
+Every example is a self-contained `generate.py`. The simplest non-research one
+proves Bernoulli's inequality `(1 + x)^k − 1 − kx ≥ 0`:
+
+```bash
+cd telperion
+python examples/bernoulli/generate.py
+# → wrote Bernoulli (5 theorems); input hash 3aa1dbc9…
+```
+
+That wrote `examples/bernoulli/lean/BernoulliSolution.lean` — real Lean, one
+theorem per instance, each with a proof term. You can read it; you do **not**
+have to trust the generator that wrote it, because the next step makes the Lean
+kernel re-prove every line.
+
+Re-running `generate.py --check` instead of writing verifies the output is
+**byte-identical** to what's committed (this is the drift gate CI runs):
+
+```bash
+python examples/bernoulli/generate.py --check
+# → check: OK (regeneration matches frozen output byte-for-byte)
+```
+
+## 3. Verify the emitted Lean locally (the step that matters)
+
+Compiling the emitted Lean needs **Lean 4 `v4.32.0`** (the pin every example
+shares) and a **pre-built Mathlib cache** — do *not* let it compile Mathlib from
+source, which takes hours.
+
+**3a. Install elan** (the Lean toolchain manager). `lake` will read each
+example's `lean-toolchain` file and fetch the exact pinned Lean automatically:
+
+```bash
+curl https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh -sSf | sh
+# restart your shell, or: source ~/.elan/env
+```
+
+**3b. Fetch the prebuilt Mathlib oleans, then build:**
+
+```bash
+cd telperion/examples/bernoulli/lean
+lake exe cache get      # downloads the prebuilt Mathlib cache (minutes, not hours)
+lake build              # the Lean kernel re-checks every emitted theorem
+```
+
+A clean exit from `lake build` means the kernel accepted every proof. That is
+the whole guarantee: **a wrong certificate is a compile error, never a false
+theorem.** Try it — edit a numeric constant in `BernoulliSolution.lean` and
+re-run `lake build`; the kernel rejects it.
+
+Every example under `telperion/examples/*/lean/` follows this identical
+`lake exe cache get && lake build` pattern.
+
+### Optional: independent second check (the Comparator)
+
+For an even stronger check — that the emitted proof proves *exactly* the stated
+theorem using only whitelisted axioms — Telperion integrates
+`leanprover/comparator` (from `openai/ten-proofs`) and the independent `nanoda`
+Rust kernel. See [`COMPARATOR.md`](COMPARATOR.md). This is what the
+`telperion-comparator` CI job runs; it is not required for local use.
+
+## 4. Use it on your own problem
+
+The end-to-end API is `certify → validate → emit`, then `lake build` in your own
+Lean project. The five-minute in-memory example and the full list of certificate
+shapes are in the [Telperion README](../README.md); the internals and the
+engine/research-lab boundary are in [`ARCHITECTURE.md`](ARCHITECTURE.md); how to
+add a new certificate shape is in [`../CONTRIBUTING.md`](../CONTRIBUTING.md).
+
+## Troubleshooting
+
+- **`lake build` starts compiling Mathlib from source** — you skipped
+  `lake exe cache get`, or your Lean version doesn't match the cache. Confirm
+  `lean-toolchain` reads `leanprover/lean4:v4.32.0` and re-run the cache fetch.
+- **`telperion` command not found** — the `pip install -e telperion` didn't put
+  the console script on your `PATH`; use `python -m telperion.cli` instead.
+- **`ModuleNotFoundError: cvxpy` / `networkx`** — install the matching extra
+  (`[sdp]` for cvxpy, `[bg]`/`[dev]` for networkx). The sympy-only core never
+  needs them; only the SDP finders and the research lab do.
+
+`conjecture1_proved = False` — nothing here depends on trusting Telperion; the
+Lean kernel is the arbiter.