SOTA plan v3: implementation lanes (2026-10-14)

docs/SOTA_PLAN.md v3 is the specification. This file says who builds what, in parallel, without collisions.

The constraint that shapes everything

One GPU lane. The heavy-job flock serialises every GPU job on this shared box (/apps/CLAUDE.md rule 2). Queue: pool round 0 (chain4) -> chain5 (valid n=8 + repair round) -> chain6 (miniF2F-test anchor n=64 @40k). Later GPU jobs are appended as chainN.sh scripts that each wait for the previous chain's bash PID.
Frozen files. Files imported by a live chain (.tmp/audit_2026-10-14/frozen_files.txt, plus all of align/verify/) are edited only on branches and merged after the last chain that imports them has exited.
Everything else runs in parallel. Each code lane is one agent in its own git worktree and branch, owning a disjoint set of files. Lanes merge into master one at a time, after the full CPU suite passes on the merged tree.
Disk. /home is a shared 50 GB volume that filled on 2026-10-14. All caches, toolchains and scratch go under /apps (set CARGO_HOME, RUSTUP_HOME, OPAMROOT, ELAN_HOME, TMPDIR, TORCHINDUCTOR_CACHE_DIR, HF_HOME explicitly).

Lanes

Lane	Branch	Plan items	Owns	Merge gate
V1 verifier freeze	`phase0/verifier`	0a.1: deferred code-verification findings U08-1/2/3/5/8 (lexer desync, axiom-walk fail-open, sandbox wiring, orphaned REPLs) + red-team fixes; ceiling test	`align/verify/*`, `tests/test_lean`, `docs/LEAN_VERIFIER.md`	after chain6 exits; frozen hash recorded
V2 generation harness	`phase0/genharness`	class-B trajectory ledger, U12-2 (lean_gen SIGTERM exit code), U12-3 (orphan reaping), U07-1/2/4 (inference engine), un-merged LoRA adapter serving option (0b.1)	`extras/vllm_rollout/`, `scripts/p2/pipeline_gen_verify.py`, `align/inference/`	after chain6 exits
S statistics + registration	`phase0/stats`	0a.6: SOTA analysis in eval_report (unbiased pass@k from n=64, paired sign-flip, problem bootstrap, McNemar secondary, Holm, MDE calculator, test-look log), pre-registration document + hash	`scripts/p2/eval_report.py`, new `align/eval/paired.py`, `docs/PREREG_SOTA.md`, tests	any time
D data supply + decontamination	`phase0/supply`	0a.4 + 0a.5: candidate-set ingestion (streamed, to `/apps`), problem schema, MinHash + normalised-text decontam, elaborated-type hash tool (Lean, run later in the GPU-free window), membership-check and classifier code (features computed on GPU later)	new `scripts/p2/supply/**`, new `align/data/decontam.py`, tests	any time
T training	`phase0/training`	U03-2 global token-mean option (config flag, default unchanged), LoRA export fidelity tooling, K-contrast driver (A/A, K1/K2/K4/K6 configs), Kimina-Distill-8B download + config check	`align/train/train_module.py`, `align/train/sft_loss.py`, `configs/p2_*`, new `scripts/p2/contrasts.py`, tests	any time
B bug-finding benchmark	`paper2/bench`	Phase 5 Part A on CPU: Rust + Charon + Aeneas toolchain under `/apps`, separate Lean 4.31 env, RustSec / fix-commit / mutant ground-truth builder, bounded-checker harness (Kani, proptest, cargo-fuzz)	new top-level `bugfind/`	any time
R RL wiring [v3.1]	`phase0/rl-lean`	Phase 0b.1: Qwen3 LoRA policy + Lean reward + un-merged adapter publication + resume; positive-only / signed / CISPO / Dr.GRPO loss modes; global token-count normalisation; budget ledger	new `scripts/p2/rl_lean.py`, `configs/p2_rl_lean.toml`, tests	any time (GPU probe after chain6)
MV math verifier [v3.1]	`phase0/mathverify`	Codex-found false accepts in the math-answer checker (U08-17..24, 29)	`align/verify/{equiv,expr,extract,normalize}.py`, tests	after chain6 (align/verify is frozen)
N notes	`notes/phase0`	0307 Aeneas semantics, 0209 variance components + equivalence tests, 0210 data selection + contamination, 0107 Leanstral-variant subsection	`notes/`, `notebooks/`	any time

Decisions (all taken 2026-10-19 by the project owner)

License: Apache-2.0 for code, models and data we release (open-source research); data rows keep their source licenses (Nemotron rows CC-BY-SA-4.0, shipped separately). See LICENSE and NOTICE.
Pre-registration sota-v1 REGISTERED, time-stamped with OpenTimestamps (docs/evidence/prereg/); Amendment A1 (MDE recompute from the n = 64 anchor) scheduled before any contrast or candidate result.
Pre-registration choices signed off: dev pass@8 from n = 32; headline = Holm p < 0.05 AND beyond the K0 97.5th percentile; Holm families {K1, K2, K4, K6} and {K5}; priors K2 0-3 pp, K4 0-2 pp, K6 0-1 pp (conditional 0-2 pp).
Host guard rules are permanent (/apps/development/rlhf/CLAUDE.md).