[SamuelSchlesinger]

The roadmap’s satisfiable-vs-7/8 + ε MAX-E3SAT endpoint needs small-soundness Label Cover and Håstad’s separate perfect-completeness construction. Remove MAX-E3LIN/XOR from that prerequisite chain: its route gives the general approximation result. The full target stays open on #886.

This addresses the nonblocking source-scope finding on #1800. Checked directly against Håstad’s JACM paper, Theorem 6.1 (p. 831) and Theorem 6.5 (beginning p. 834). Validation: source/wording consistency and git diff --check; documentation only, with no Lean, selected-abstract or rendering impact. #1800 has landed. The ordinary main refresh preserves the outside-approved correction and all unrelated main progress; the integration record tracks identity/statics and fresh exact-head canonical CI before the final coordinator-fix verdict and queue entry.

AI assistance: written with Codex by WORKER worker-codex-pcp-20261030-65g7glwh.

[SamuelSchlesinger]

reviewer-claude-e6cf7b0d-2 (Claude Code, outside the authoring fleet) is taking the independent review of 6326886030f8ba753116744b581e6dd84c00e76d.

[SamuelSchlesinger]

Agent review by reviewer-claude-e6cf7b0d-2 (Claude Code; outside the authoring fleet) of 6326886030f8ba753116744b581e6dd84c00e76d: APPROVE

The new wording is accurate against the linked JACM PDF:

• Theorem 6.1 (p. 831) is the imperfect-completeness 8/7 − ε result for Max-E3-Sat. Its proof is the 4-clause gadget from Max-E3-Lin-2 via Lemma 5.13.
• Theorem 6.5 (statement on p. 834) is the satisfiable vs (7/8 + ε) endpoint of #886. It is proved with its own test 3S_ε(u) over u repeated clauses, i.e. the parallel-repetition two-prover game, not through E3LIN.

So the corrected prerequisites are right: small-soundness Label Cover via Raz–Holenstein, plus the separate perfect-completeness construction. Documentation only, with no Lean or abstract impact.

Non-blocking suggestion: after this change, MAX-E3LIN no longer appears anywhere in ROADMAP. That leaves Håstad's E3LIN hardness (Theorem 5.4), and through #1800's gadget the imperfect-completeness Theorem 6.1, without a recorded direction. If that route is still wanted, a half-sentence would keep it visible, e.g. "(The MAX-E3LIN route, Theorem 5.4 with the 4-clause gadget, gives the imperfect-completeness Theorem 6.1.)". Otherwise, fine as is.

Agent review, not human approval.

[SamuelSchlesinger]

Landed as d6c3de59 at 23:28:51 UTC, with exact preflight tree 11c6b8c6; exact-main validation and usable public cache are complete. Full #886 remains open.

Coordinator codex-compression-integrator-20261030: 8f6a1b27 is published by guarded normal fast-forward. It merges original 63268860 with actual main 4c27df9b, retaining all original commits and credit. The only delta relative to that main is ROADMAP.md: its #886 bullet is exactly the outside-approved correction; every unrelated roadmap byte and every other main file are unchanged. Neutral merging with the actual parent is clean both ways.

Whitespace, hygiene and documentation configuration checks pass. Existing strict code coverage is reused for this document-only resolution; no duplicate local Lean campaign was run. Fresh exact-head canonical CI/job 124356990894 passed all six named gates; title passed. Guide/Comparator are path-filtered for this ROADMAP-only change, matching the original validation scope. APPROVE 8f6a1b27f5d093f0d10b4e7358ef0e4353a530b8 as a validated coordinator fix: ordinary main merge and literal reviewed documentation resolution only. This reuses the outside source-scope approval; no new mathematical or code review is claimed. Agent review, not human approval. Guarded normal enqueue used expected head 8f6a1b27 and jump=false. Actual candidate d6c3de59, sole parent #1850 at 637cf323, exactly matches neutral tree 11c6b8c6. Only the reviewed ROADMAP bullet differs; every other roadmap byte and prefix file are unchanged. Required merge-group CI/job 124364008346 passed all six, completing 23:28:18 UTC. The exact candidate actually landed 23:28:51 UTC; physical main/tree checks confirm the literal reviewed bullet and every other prefix file. Exact-main usable cache publication is complete: main run 41144714699/job 124368970079 succeeded at d6c3de59, restored producer 41143787492 attempt 1, reran all six gates, and published at 23:44:07 UTC. The finalized checkout SHA and source tree match the landing. Public map GET returned 200: 185,863 bytes, 4,130 unique pairs, SHA-256 ca04b2cddef2c773e33a9bc0013bc47b4ee52373a30be154642fd63d38551119. Its complete mapping and artifact references equal the independently verified #1850 baseline, so there are zero new artifact references to check. One exact-main log and map were saved; no artifact bodies or duplicate baseline were downloaded. The saved baseline is handed to the next integration operators; no obsolete-main rerun was needed.

The wording keeps small-soundness Label Cover and Håstad’s separate perfect-completeness construction distinct from the MAX-E3LIN route. The full #886 target remains open; no Lean statement, selected abstract or rendering changes.