Phase 4l: certificates on firm footing (multi-seed guarantees + graph certification)

.claude/CLAUDE.md

@@ -58,4 +58,13 @@ inference-time descent** into distribution-free reliability certificates. Read
   a wash where geometry already wins (arith-IRED +0.007 4/5) and slightly worse on fixed-bowl cells.
   Aggregation is feature-set-aware (`feature_set_of`, canonical tables default `feature_set="base"`)
   so richer never pollutes T1/T2/T4. JAX for spectrum/connectivity lives in `curvature.py` (inv. 1).
+- Phase 4l certificates on firm footing ✅ (T6/T7): put the guarantees on a 5-seed footing.
+  `run_halting_sweep.py` + `aggregate.{halting_rows,aggregate_halting_cell}` → **T6**: arith halting
+  saves 57.1%±1.7% (was single-seed 57.8%), graph 80.8%±5.2%, both risk ≤ α, within-budget 5/5.
+  `[sweep] include_ood=true` + OOD aggregation block → **T7**: guarantee breaks under shift over 5
+  seeds (arith ID risk 0.077→OOD 0.764, 0/5; graph 0.010→0.168, 4/5). Full-fold graph cert run: LTT
+  certifies 1.1% cov at α=0.1 but **22.5% at α=0.15 / 48.5% at α=0.20, validity holds at every α** —
+  the "certifies zero" was an operating-point artifact of graph's ~30% error floor, not a broken
+  certificate. Aggregation dedups halting rows by seed (drops the stale Phase-4b H1 config-hash row);
+  `plotting._selective_row`/`_halting_row` prefer arithmetic so full-fold graph rows don't flip F2/F4/F6.
 - Next: E3/E4 (a 3rd/4th task to characterize *when* geometry beats softmax) · Modal · scale-up.

analysis/aggregate.py

@@ -93,6 +93,18 @@ def aggregate_cell(rows_for_k: list[dict]) -> dict:
     dadd = [m["delta_aurc_geom_adds"] for m in ms] if has_add else []
     add_mean, add_std = _ms([d[0] for d in dadd]) if has_add else (float("nan"), float("nan"))
     add_ci = sum(1 for d in dadd if d[1] > 0.0)
+    # OOD stress (Phase 4l): the ID-calibrated threshold applied to the shifted fold. Only rows run
+    # with include_ood carry these; pre-4l / selective-sweep rows fall through (has_ood=False).
+    has_ood = all("ood_ltt" in m and "accuracy_ood" in m for m in ms)
+    _nan = (float("nan"), float("nan"))
+    if has_ood:
+        acc_ood = _ms([m["accuracy_ood"] for m in ms])
+        risk_ood = _ms([m["ood_ltt"]["selective_risk"] for m in ms])
+        cov_ood = _ms([m["ood_ltt"]["coverage"] for m in ms])
+        ood_within = sum(1 for m in ms if m["ood_ltt"].get("risk_within_budget"))
+    else:
+        acc_ood = risk_ood = cov_ood = _nan
+        ood_within = 0
     return {
         "task": rows_for_k[0].get("task"),
         "k_restarts": _k(rows_for_k[0]),
@@ -126,6 +138,12 @@ def aggregate_cell(rows_for_k: list[dict]) -> dict:
         "ltt_coverage": _ms([m["ltt"]["coverage"] for m in ms]),
         "ltt_selective_risk": _ms([m["ltt"]["selective_risk"] for m in ms]),
         "ltt_abstain_rate": _ms([m["ltt"]["abstain_rate"] for m in ms]),
+        # OOD stress (Phase 4l); NaN + has_ood=False when the cell has no include_ood rows.
+        "has_ood": has_ood,
+        "accuracy_ood": acc_ood,
+        "ood_selective_risk": risk_ood,
+        "ood_coverage": cov_ood,
+        "seeds_ood_within_budget": ood_within,
     }
 
 
@@ -172,3 +190,60 @@ def _key(cell: list[dict]) -> tuple:
         return (has_add, len(cell), max(r.get("timestamp", "") for r in cell))
 
     return aggregate_cell(max(cells, key=_key))
+
+
+def halting_rows(rows: list[dict] | None = None, task: str | None = None) -> list[dict]:
+    """Latest ``split=='halting'`` row per ``(config_hash, seed)``, optionally one ``task``.
+
+    The halting rows are excluded from ``selective_rows`` (different split); this is their
+    multi-seed counterpart for the adaptive-halting (CRC) guarantee (Phase 4l).
+    """
+    if rows is None:
+        rows = read_all()
+    latest: dict[tuple[str, int], dict] = {}
+    for r in rows:
+        if r.get("split") == "halting" and (task is None or r.get("task") == task):
+            latest[(r["config_hash"], r["seed"])] = r  # later rows win
+    return list(latest.values())
+
+
+def halting_tasks_present(rows: list[dict] | None = None) -> list[str]:
+    """Sorted distinct task names among halting rows."""
+    return sorted({r.get("task") for r in halting_rows(rows)} - {None})
+
+
+def aggregate_halting_cell(rows_for_task: list[dict]) -> dict:
+    """Aggregate per-seed halting rows into the multi-seed CRC verdict (compute saved + risk).
+
+    Dedups to the latest row per seed by timestamp — so a stale single-seed run under an older
+    config schema (e.g. the original Phase-4b H1 seed-0 row, whose config_hash has since drifted)
+    does not double-count against the current seed sweep.
+    """
+    by_seed: dict[int, dict] = {}
+    for r in sorted(rows_for_task, key=lambda r: r.get("timestamp", "")):
+        by_seed[r["seed"]] = r
+    rows_for_task = list(by_seed.values())
+    ms = [r["metrics"] for r in rows_for_task]
+    n = len(ms)
+    taus = [m["tau_hat"] for m in ms if m.get("tau_hat") is not None]
+    return {
+        "task": rows_for_task[0].get("task"),
+        "n_seeds": n,
+        "seeds": sorted(r["seed"] for r in rows_for_task),
+        "run_ids": [r["run_id"] for r in rows_for_task],
+        "alpha": ms[0].get("alpha"),
+        "tau_hat": _ms(taus) if taus else (float("nan"), float("nan")),
+        "n_tau_feasible": len(taus),
+        "compute_saved": _ms([m["compute_saved"] for m in ms]),
+        "halting_risk": _ms([m["halting_risk"] for m in ms]),
+        "full_accuracy": _ms([m["full_accuracy"] for m in ms]),
+        "accuracy_drop": _ms([m["accuracy_drop"] for m in ms]),
+        "seeds_within_budget": sum(1 for m in ms if m.get("risk_within_budget")),
+        "seeds_risk_monotone": sum(1 for m in ms if m.get("risk_monotone_in_tau")),
+    }
+
+
+def aggregate_halting(rows: list[dict] | None = None) -> dict[str, dict]:
+    """``{task: aggregate_halting_cell(...)}`` for every task with halting rows."""
+    return {t: aggregate_halting_cell(halting_rows(rows, task=t))
+            for t in halting_tasks_present(rows)}

analysis/make_tables.py

@@ -14,6 +14,7 @@
 try:  # sibling import when run as a script (analysis/ on sys.path)
     from aggregate import (
         aggregate_by_k,
+        aggregate_halting,
         feature_set_of,
         headline_cell,
         objective_of,
@@ -23,6 +24,7 @@
 except ImportError:  # pragma: no cover
     from analysis.aggregate import (
         aggregate_by_k,
+        aggregate_halting,
         feature_set_of,
         headline_cell,
         objective_of,
@@ -193,6 +195,59 @@ def _t5(rows: list[dict]) -> str:
         "tab:richer", f"run_ids={all_ids}")
 
 
+def _t6(rows: list[dict]) -> str:
+    """Adaptive halting (CRC guarantee) over seeds — H1 on a multi-seed footing (Phase 4l).
+
+    Per task: the CRC-chosen agreement threshold, compute saved, halting risk vs the budget alpha,
+    end-task accuracy drop, and how many seeds keep the risk within budget — all mean$\\pm$std.
+    """
+    cells = aggregate_halting(rows)
+    body, all_ids = [], []
+    for task, a in cells.items():
+        body.append([
+            _esc(task), f"${a['alpha']}$", _pm(a["tau_hat"], 2), _pm(a["compute_saved"], 3),
+            _pm(a["halting_risk"], 3), _pm(a["accuracy_drop"], 3),
+            f"{a['seeds_within_budget']}/{a['n_seeds']}",
+        ])
+        all_ids += a["run_ids"]
+    header = ["task", r"$\alpha$", r"$\hat\tau$", "compute saved", "halting risk",
+              "acc drop", "seeds $\\le\\alpha$"]
+    return _tabular(
+        header, body, "lcccccc",
+        "Adaptive halting (CRC), mean$\\pm$std over seeds: the basin-agreement threshold "
+        "$\\hat\\tau$ is calibrated on a disjoint fold so the halting risk (disagreement with the "
+        "full-budget answer) stays within the budget $\\alpha$. ``compute saved`` is the fraction "
+        "of descent steps skipped; ``seeds $\\le\\alpha$`` counts seeds with test risk in budget.",
+        "tab:halting", f"run_ids={all_ids}")
+
+
+def _t7(rows: list[dict]) -> str:
+    """OOD stress over seeds — the guarantee holds ID and breaks under shift (Phase 4l).
+
+    Per task: ID vs OOD accuracy, and the ID-calibrated LTT threshold's selective risk on the ID
+    fold vs the shifted fold, with a count of seeds where OOD risk stays within budget.
+    """
+    body, all_ids = [], []
+    for task in tasks_present(rows):
+        a = headline_cell(rows, task=task)
+        if not a.get("has_ood"):
+            continue
+        body.append([
+            _esc(task), _pm(a["accuracy_id"], 2), _pm(a["accuracy_ood"], 2),
+            _pm(a["ltt_selective_risk"], 3), _pm(a["ood_selective_risk"], 3),
+            f"{a['seeds_ood_within_budget']}/{a['n_seeds']}",
+        ])
+        all_ids += a["run_ids"]
+    header = ["task", "acc ID", "acc OOD", "sel.\\ risk ID", "sel.\\ risk OOD", "seeds OOD ok"]
+    return _tabular(
+        header, body, "lccccc",
+        "OOD stress (mean$\\pm$std over seeds): the ID-calibrated selective-prediction threshold "
+        "applied to a shifted fold. The selective-risk guarantee holds in-distribution but breaks "
+        "under shift (OOD risk exceeds the budget), motivating abstention; ``seeds OOD ok`` counts "
+        "seeds whose OOD risk still stays within budget.",
+        "tab:oodstress", f"run_ids={all_ids}")
+
+
 def _t3(rows: list[dict]) -> str:
     sel = selective_rows(rows)
     env = sel[-1]["env"] if sel else {}
@@ -235,6 +290,12 @@ def _has_body(tex: str) -> bool:
     t5 = _t5(rows)                                  # only when richer-geometry rows exist
     if _has_body(t5):
         outputs["T5_richer_geometry.tex"] = t5
+    t6 = _t6(rows)                                  # only when split='halting' rows exist
+    if _has_body(t6):
+        outputs["T6_halting.tex"] = t6
+    t7 = _t7(rows)                                  # only when include_ood rows exist
+    if _has_body(t7):
+        outputs["T7_ood_stress.tex"] = t7
     for name, tex in outputs.items():
         (TABLE_DIR / name).write_text(tex)
         print(f"[tables] wrote {TABLE_DIR / name}")

configs/experiments/graph_halting.toml

@@ -0,0 +1,36 @@
+# Adaptive-halting experiment on graph shortest-path (Phase 4l — a 2nd task for the CRC guarantee).
+# Same task/inference/train as the graph selective E2 config, but per-step decoding is recorded so
+# the basin-agreement halting threshold can be CRC-calibrated. Folds kept modest to bound decode
+# memory on CPU (mirrors arithmetic_halting).
+[run]
+task = "graph_planning"
+seed = 0
+notes = "graph adaptive-halting run"
+
+[task.graph_planning]
+n_nodes = 7
+ood_n_nodes = 10
+edge_prob = 0.4
+max_len = 4
+
+[model]
+latent_dim = 32
+hidden_dim = 128
+context_dim = 64
+
+[inference]
+k_restarts = 12
+steps = 50
+
+[train]
+epochs = 25             # graph needs more epochs than arithmetic to reach the 70-85% regime
+n_train = 8000
+n_neg = 4
+
+[eval]
+n_eval = 800            # test fold (per-step decode kept small)
+
+[conformal]
+alpha = 0.1             # halting error budget: E[early answer != full answer] <= alpha
+delta = 0.05
+n_calib = 800           # calibration fold

configs/sweeps/arith_halting_seeds.toml

@@ -0,0 +1,9 @@
+# Phase 4l: 5-seed adaptive-halting (CRC) on arithmetic — the multi-seed version of the H1 headline
+# (~58% compute saved at halting risk <= alpha), which was single-seed. Uses run_halting_sweep.py
+# (each cell trains, CRC-calibrates, appends a split="halting" row). aggregate.aggregate_halting +
+# make_tables T6 summarise the compute-saved / halting-risk mean±std.
+[sweep]
+base = "configs/experiments/arithmetic_halting.toml"
+
+[sweep.grid]
+"run.seed" = [0, 1, 2, 3, 4]

configs/sweeps/arith_ood_seeds.toml

@@ -0,0 +1,9 @@
+# Phase 4l: 5-seed FULL-FOLD arithmetic selective prediction with include_ood=true, so the OOD
+# stress result (F6: ID risk vs OOD risk under the ID-calibrated threshold) gets a multi-seed
+# mean±std instead of a single seed. Matches graph_cert_seeds so T7 is 5-seed on both tasks.
+[sweep]
+base = "configs/experiments/arithmetic_selective.toml"
+include_ood = true
+
+[sweep.grid]
+"run.seed" = [0, 1, 2, 3, 4]

configs/sweeps/graph_cert_seeds.toml

@@ -0,0 +1,10 @@
+# Phase 4l THE CERT RUN: 5-seed FULL-FOLD graph selective prediction (n_calib=1500), so LTT
+# abstention can actually certify nonzero coverage on graph — the reduced-fold seed sweeps
+# (n_calib=800) certify zero. include_ood=true also yields 5-seed graph OOD stress (T7). No n_calib
+# override: it inherits graph_selective.toml's full folds. Heaviest cell set in the project.
+[sweep]
+base = "configs/experiments/graph_selective.toml"
+include_ood = true
+
+[sweep.grid]
+"run.seed" = [0, 1, 2, 3, 4]

configs/sweeps/graph_halting_seeds.toml

@@ -0,0 +1,8 @@
+# Phase 4l: 5-seed adaptive-halting (CRC) on graph shortest-path — a 2nd task for the halting
+# guarantee (secondary to the arithmetic headline). Uses run_halting_sweep.py -> split="halting"
+# rows -> aggregate_halting -> T6.
+[sweep]
+base = "configs/experiments/graph_halting.toml"
+
+[sweep.grid]
+"run.seed" = [0, 1, 2, 3, 4]

docs/DECISIONS.md

@@ -2,6 +2,24 @@
 
 Short, dated, append-only. Newest first.
 
+## 2026-07-30 — Phase 4l: certificates on firm footing (multi-seed guarantees + graph certification)
+**Finding/decision:** put the project's core contribution — the distribution-free certificates — on a
+5-seed footing. (1) **Halting:** new `experiments/run_halting_sweep.py` + `aggregate.halting_rows`/
+`aggregate_halting_cell` (split="halting" was excluded from `selective_rows`). Arith saves
+57.1%±1.7% (single-seed H1 was 57.8%), graph 80.8%±5.2%; both risk ≤ α, within budget 5/5 (T6).
+(2) **OOD:** `[sweep] include_ood=true` in `run_sweep` + an OOD aggregation block; the selective
+guarantee breaks under shift over 5 seeds (arith ID 0.077 → OOD 0.764, 0/5; graph 0.010 → 0.168,
+4/5) (T7). (3) **Graph certification:** a full-fold run (n_calib=1500) certifies only 1.1% coverage
+at α=0.1 but 22.5% at α=0.15 and 48.5% at α=0.20, with achieved risk ≤ target at every α — so the
+old "certifies zero coverage" note was an **operating-point artifact** of graph's ~30% error floor,
+not a broken certificate. **Bugs fixed:** (a) halting aggregation dedups by seed (the stale Phase-4b
+H1 seed-0 row survived under a drifted config_hash, giving n=6); (b) `plotting._selective_row` and
+`_halting_row` now prefer arithmetic, since the new full-fold (n_test=1500) graph rows would
+otherwise tie/flip the arithmetic figures F2/F4/F6 to graph. **Why record it:** every guarantee
+number the paper states is now multi-seed, and the graph certificate is shown valid at its honest α.
+**Reversible?** Additive runner + aggregation + a sweep flag; default `include_ood=False` preserves
+all prior sweeps.
+
 ## 2026-07-29 — Phase 4k: the graph redundancy is a task property, not thin features
 **Finding/decision:** the 4j redundancy verdict rested on a thin curvature description (only
 `λmax`/`tr(H)`), so we added two opt-in richer feature groups — the **full Hessian spectrum**

docs/EXPERIMENTS.md

@@ -232,6 +232,52 @@ contribute there, even with the richest geometry we can extract. The base rows r
 numbers exactly, confirming richer geometry is purely additive and non-breaking (default stays the
 canonical 14 features; aggregation is feature-set-aware so richer never pollutes T1/T2/T4).
 
+### Certificates on firm footing — multi-seed guarantees + graph certification (Phase 4l → T6/T7)
+
+The certificates are the contribution, but three of their numbers were single-seed or vacuous. This
+phase puts all three on a 5-seed footing (new `run_halting_sweep.py`; `[sweep] include_ood=true`;
+objective/feature-set-style aggregation for halting + OOD; full-fold graph cert run). Additive — no
+change to the geometry features or the falsification test.
+
+**Adaptive halting (CRC), 5 seeds — T6.** The H1 headline replicates and extends:
+
+| task | τ̂ | compute saved | halting risk (≤ α=0.1) | seeds ≤ α |
+|------|-----|---------------|------------------------|-----------|
+| arithmetic | $0.917$ | $0.571 \pm 0.017$ | $0.012 \pm 0.005$ | $5/5$ |
+| graph | $0.85\pm0.03$ | $\mathbf{0.808 \pm 0.052}$ | $0.065 \pm 0.032$ | $5/5$ |
+
+The single-seed 57.8% arithmetic number is now $57.1\%\pm1.7\%$ over 5 seeds (within budget every
+seed); on graph the CRC halt saves **~81%** of compute at risk $0.065 \le 0.1$ — the halting
+guarantee holds on both tasks across seeds.
+
+**OOD stress, 5 seeds — T7.** The ID-calibrated selective threshold applied to the shifted fold:
+
+| task | acc ID | acc OOD | sel. risk ID | sel. risk OOD | seeds OOD ≤ α |
+|------|--------|---------|--------------|---------------|---------------|
+| arithmetic | $0.83$ | $0.21$ | $0.077$ | $\mathbf{0.764}$ | $0/5$ |
+| graph | $0.70$ | $0.33$ | $0.010$ | $0.168$ | $4/5$ |
+
+The guarantee holds ID and **breaks under shift** on both tasks (arithmetic catastrophically:
+$0.077\to0.764$; graph mildly: $0.010\to0.168$) — 5-seed confirmation of F6, and the argument for
+treating an abstention as a routing signal.
+
+**Graph certification — the certificate is valid on graph, at its honest operating point.** At the
+full fold ($n_\text{calib}=1500$) the graph LTT abstention still certifies almost nothing at
+α=0.1 (coverage $0.011$), because graph's ~30% base error leaves no confident slice with true error
+below 10%. But sweeping α (from the same `coverage_validity` block; mean over 5 seeds):
+
+| α | certified coverage | achieved risk |
+|-----|--------------------|---------------|
+| $0.10$ | $0.011$ | $0.010$ |
+| $0.15$ | $0.225$ | $0.078$ |
+| $0.20$ | $0.485$ | $0.157$ |
+| $0.30$ | $0.895$ | $0.263$ |
+
+Achieved risk sits **at or below target at every α** — validity holds; the earlier "certifies zero
+coverage" was an α=0.1 operating-point artifact, not a broken certificate. Graph certifies **22.5%
+coverage at α=0.15** and **48.5% at α=0.20**, versus arithmetic's 74% at α=0.10 — the honest cost of
+a harder task's higher error floor, not a failure. (F3 shows the arithmetic α-sweep on the diagonal.)
+
 ## Operating regime
 
 Tune each task's difficulty so base accuracy is **70–85%**. Fully-solved tasks saturate AURC and

docs/SESSION_HANDOFF.md

@@ -2,7 +2,7 @@
 
 **Start here.** Rolling state of the project between sessions.
 
-## Current state (2026-07-29)
+## Current state (2026-07-30)
 
 - **Phase 0 (skeleton): ✅** repo tree, `uv`/`pyproject.toml`, `Makefile`, CI, config system
   (`edc.config`), deterministic seeding (`edc.seeding`), append-only ledger (`edc.ledger`),
@@ -99,9 +99,21 @@
   geometry already wins (arith-IRED +0.007, 4/5, unchanged) and slightly worse on the fixed-bowl
   basin-center cells (extra features add noise). Aggregation is feature-set-aware (`feature_set_of`;
   `headline_cell`/`by_k` default `feature_set="base"`) so richer never pollutes T1/T2/T4. 109 tests.
-- **Open question / next:** a 3rd/4th task (E3/E4, e.g. logic/Sudoku) to characterize *when* geometry
-  beats softmax now that feature poverty is ruled out; harden honesty gaps (multi-seed halting/OOD,
-  MC-dropout baseline, a full-fold graph run that actually certifies); Modal; scale-up.
+- **Phase 4l (certificates on firm footing — multi-seed guarantees + graph certification): ✅** put
+  the project's core contribution (the certificates) on a 5-seed footing. New
+  `experiments/run_halting_sweep.py` + `aggregate.{halting_rows, aggregate_halting_cell}` → **T6**:
+  arith halting saves **57.1%±1.7%** (was single-seed 57.8%), graph **80.8%±5.2%**, both halting risk
+  ≤ α, within budget 5/5. `[sweep] include_ood=true` (run_sweep) + an OOD aggregation block → **T7**:
+  the selective guarantee breaks under shift over 5 seeds (arith ID sel-risk 0.077 → OOD 0.764, 0/5;
+  graph 0.010 → 0.168, 4/5). Full-fold graph cert run (`graph_cert_seeds.toml`, n_calib=1500): LTT
+  certifies only **1.1% coverage at α=0.1** but **22.5% at α=0.15, 48.5% at α=0.20; validity holds at
+  every α** — the old "certifies zero" was an operating-point artifact of graph's ~30% error floor,
+  not a broken certificate. Fixed a stale-row bug (halting dedups by seed, dropping the Phase-4b H1
+  row under a drifted config_hash) and made `plotting._selective_row`/`_halting_row` prefer arithmetic
+  so the new full-fold (n_test=1500) graph rows don't flip F2/F4/F6. 115 tests.
+- **Open question / next:** a 3rd/4th task (E3/E4, e.g. logic/parity) to characterize *when* geometry
+  beats softmax now that feature poverty is ruled out; a deep-ensemble baseline (the one remaining
+  deferred baseline); Modal; scale-up.
 
 ## What is real vs stub