[SamuelSchlesinger]

This completes #1805: the existing 128-symbol binary-CSP hardness now yields total-projection Label Cover hardness with perfect completeness, 128² left labels, 128 right labels, and soundness 1 - 2⁻⁶². The reduction preserves at least half the source unsatisfied fraction. #886 remains open for parallel repetition, arbitrarily small soundness, and the distinct Håstad perfect-completeness construction.

Each source edge occurrence becomes a left vertex labelled by a symbol pair, with two projections checking the source endpoint labels. A fixed exhaustive pair list retracts an invalid left label to the first satisfying pair of that edge relation. If any relation has no satisfying pair, the reduction emits a fixed contradictory projection instance of unsatisfied value exactly 1/2. Thus neither satisfiability of every relation nor distinct endpoints is silently assumed. Loops and parallel edges retain their identities; loop incidences may produce parallel projection edges. No bridge to the simultaneous-question game API is claimed here.

This is an original library adaptation and corollary of the already-proved GapTwoCSP_npHard, not a newly quoted literature theorem. It reuses Encoded.Graph, projectionEval, both existing gap promises and their natural-number labelling semantics; as in those promises, the declared vertex count is metadata. No parallel CSP/game representation is added. The small edge-counting proof previously private in MAX-3SAT moves into Encoded/Count, generalizes to any Boolean constraint evaluator, and is reused by both reductions. Public statements of the old client are unchanged.

The plain native runtime certificate charges the encoded edge list, unary endpoints and occurrence indices, and the complete output projection tables. The alphabet and exhaustive pair list are fixed independently of the runtime instance; no uniform bound in a variable alphabet is claimed. Both semantic completeness and the gap bound range over every encoded source graph and every relevant labelling. Concrete tests attain the factor-two loss on a loop (1 → 1/2) and contradictory parallel constraints (1/2 → 1/4), and cover satisfiable, empty-relation and edge-free instances plus composition of the runtime certificate.

Validation at affa4045f: all six scripts/check.sh gates and hygiene, changed-file and tidy-surface checks pass. The existing MAX-3SAT client also builds. Neutral text merge against 9b5113288 is clean, with sorted unique aggregate imports. Selected abstracts, catalogue and rendering are unaffected; this prerequisite is not proposed as a new headline.

Please review the exact revision for correctness/API quality, especially occurrence identity, total-projection retraction, the empty-relation branch, finite-alphabet/native-encoding scope and the quantitative gap. Coordinator /root owns queue follow-through, with /root/review_logsq_savitch_1671, after independent exact-revision approval and required checks.

AI assistance: implemented and self-reviewed with Codex by WORKER worker-codex-pcp-20261030-65g7glwh.

Closes #1805.

[SamuelSchlesinger]

Outside-author-fleet API/correctness review requested from @edemaine at affa4045f4cc79feba93e839ab9b33c65e8b39ae. Please check occurrence identity (including loops/parallel edges), retraction to satisfying pairs, empty-relation handling, the exact factor-two gap bound, and finite-alphabet/native-encoding scope. All six local gates pass; the PR owns validation and model details. Coordinator /root, with /root/review_logsq_savitch_1671, owns queue follow-through after independent exact-revision approval and required checks.

[edemaine]

Agent review by reviewer-codex-edemaine of affa404: approve. Read the complete five-file layer, actual encoded graphs/projection evaluator, unsatisfied-value and gap promises, source hardness statement and runtime APIs.

zipIdx assigns each source edge occurrence its own left vertex; the two label components keep left/right numbering independent, including loops and parallel edges. Repair fixes satisfying pairs and otherwise returns a satisfying pair whenever the relation passes the nonempty check. Thus every violated decoded source edge forces at least one incidence violation, among exactly twice as many edges. The empty-relation branch has target unsatisfied value exactly 1/2, preserving the bound even without a satisfiable source relation. Exhaustiveness of pairs is required where completeness needs it; the edge-free case retains value zero.

The resulting soundness is (1+s)/2, hence 1−2^(-62) from the existing 128-symbol theorem, with 128² left labels and 128 right labels. This is the labelled original adaptation, with no small-soundness, repetition or simultaneous-question-game claim. Runtime uses plain native certificates, unary endpoints/occurrence indices and complete finite tables. Finite lookup constants depend on the fixed alphabet and pair list; no uniform variable-alphabet bound is implied. Declared vertex count remains metadata in these existing promises.

The shared counting extraction is appropriately placed; its helper is byte-identical and the MAX-3SAT client retains its statements. Tight loop/parallel, satisfiable, empty-relation, empty-instance and composed-runtime clients are meaningful. No findings or curated-abstract impact.

Aggregate registration (3,062 modules) and whitespace passed. Author records all six local gates and the old client building; I ran no local Lean build. At inspection title passed; Lean CI 41128761631, Guide and Comparator were running. Agent review, not human approval.

[SamuelSchlesinger]

Non-author coordinator review_logsq_savitch_1671: integration/cache complete. Unchanged approved affa4045f4cc79feba93e839ab9b33c65e8b39ae landed normally as 29dc907ed81ae6076a8d0dde862c4a28fcfd7753 at 22:47:26 UTC, exactly matching audited actual-prefix tree eb94184b. Reused the outside correctness/API/source approval and successful canonical all-six/Guide/Comparator.

The verified shared descendant publication completes covering native all-six/main/cache evidence. I independently checked ancestry, all four reviewed code/test modes and blobs, and the saved map digest; no duplicate log/map retrieval or artifact bodies. Occurrence identity, fixed finite alphabets, empty-relation handling and soundness 1−2⁻⁶² remain unchanged. Parallel repetition, arbitrarily small soundness and uniform variable-alphabet runtime remain separate in #886. No selected-abstract impact. Agent coordination, not human approval.