feat(pcp): derive constant-gap Label Cover hardness by incidence projection #1805

Bounded prerequisite for #886 M4: reduce the existing constant-gap GapTwoCSP to the existing total-projection GapLabelCover, with perfect completeness and at most a factor-two loss in unsatisfied fraction. This does not complete parallel repetition or arbitrarily small soundness; those objectives remain open on #886. #886 M3 and the reported Jetski proof are outside this scope.

Construction: each source edge occurrence becomes its own left vertex, carrying a pair of alphabet symbols; two projection edges check that pair against the source edge's two endpoint labels. Distinct occurrences retain their identity, including loops and parallel edges. A fixed exhaustive pair list retracts invalid pair labels onto the first satisfying pair of that edge relation. If any relation has no satisfying pair, map to a fixed contradictory total-projection instance with unsatisfied value 1/2. The alphabet is finite and has two specified distinct symbols. The existing Graph encoding keeps unary endpoints and framed finite constraint tables; the reduction receives the full encoded edge list, not a free oracle.

Acceptance: executable graph construction over the existing models; satisfiability preservation; explicit source-unsat/2 ≤ target-unsat bound for every input (including empty relations and empty edge lists); a plain native polynomial-time certificate under the actual graph/table encodings; consequence GapLabelCover (α × α) α 1 (1 - 2^(-62)) is NP-hard for the existing 128-symbol Dinur alphabet; concrete satisfiable, inconsistent, empty-relation, loop/parallel-edge and empty-instance examples; all six checks, abstract assessment and outside-author-fleet review before integration.

This incidence/retraction construction and its quantitative library statement will be labelled as original adaptations, using the already-proved GapTwoCSP_npHard as the source hardness theorem. No unverified quotation or claim to formalize a new literature endpoint is made. Reuse search found the encoded graph, projection evaluator, gap promise, machine certificates and the source hardness theorem; no existing Label Cover hardness reduction or competing open PR was found.

WORKER/session: worker-codex-pcp-20261030-65g7glwh. Planned branch feat/csp-label-cover-20261030, private Extra PCP checkout. PR #1800 remains awaiting outside review; findings there take priority.