Repository navigation
feat(pcp): certify the four-clause MAX-E3LIN to E3SAT reduction #1798
Description
Prerequisite for #886 and the Håstad endpoint in ROADMAP.md. This bounded milestone constructs the system-level four-clause reduction; it does not prove small-soundness Label Cover, Håstad hardness, or perfect completeness for the noisy Long Code test. Those objectives remain open on #886.
Use the existing CSP Bool V representation: a constraint (b, [x,y,z]) means σ x ^^ σ y ^^ σ z = b. Reuse CSP.eval/CSP.Satisfiable, CNF, CNF.countUnsat, CNF.unsatVal and the plain polynomial-time calculus. No parallel equation-system representation is needed. The all-three-scope hypothesis is explicit; repeated variables are permitted, while distinct scopes should produce CNF.IsExactThreeDistinct.
Acceptance: an executable full-system reduction; exactly four output clauses per input equation; exact equality between the number of falsified output clauses and violated input equations for every assignment; preservation of satisfiability and an explicit quarter-factor unsatisfied-fraction/gap transfer; a plain ComputableInPolyTime certificate over explicit encodings; concrete satisfiable and inconsistent systems, including empty and repeated-variable cases; full six validation gates, abstract-impact assessment, and outside-author-fleet API/correctness review before integration.
Primary source checked: J. Håstad, Some Optimal Inapproximability Results, JACM 48(4), 2001, proof of Theorem 6.1, p. 831 (PDF page 34): https://www.cs.umd.edu/~gasarch/TOPICS/pcp/hastadopt.pdf . Paraphrase: replace a three-literal parity equation by four 3-clauses; a violated equation loses exactly one of them. Source notation uses sign multiplication; Lean uses Bool XOR with true for bit one. The reduction proves the elementary gadget step, not the source hardness theorem. The withdrawn xorThreeCNF noted in #392 was dead code; this deliverable includes its full-system consumer and efficiency/gap guarantees.
Owner/session: worker-codex-pcp-20261030-65g7glwh (WORKER). Branch: feat/e3lin-e3sat-20261030. Private Extra-drive lane pcp; provisioned checkout path will be recorded when READY arrives.
Activity
SamuelSchlesinger commentedon Oct 30, 2026
worker-codex-pcp-20261030-65g7glwh— active. I claim the bounded system-level XOR-to-E3CNF reduction and its exact loss/size/runtime guarantees on branchfeat/e3lin-e3sat-20261030, private Extra-drive lanepcp. I have checked existing issues/PRs and the source locator in the issue. Next: implement in the provisioned checkout after readiness; preserve #886's broader repetition and hardness objective.SamuelSchlesinger commentedon Oct 30, 2026
Reuse refinement:
Constraint/CSP.toCNFBoundedalready implements the forbidden-pattern compiler andCslib.Complexity.CSP.computableInPolyTime_toCNFBounded_of_finitealready certifies its runtime. This task will reuse both, adding exact falsified-clause counting and the parity-specific four-clause/gap specialization. The small compiler/encoding certificate block will move unchanged fromFineGrained/CountingCSPintoComputability/PolyTime/CSP/ToCNF, preserving declaration names; its two consumers are the existing counting module and this PCP reduction. This avoids pulling the subexponential counting endpoint into the approximation theory.SamuelSchlesinger commentedon Oct 30, 2026
worker-codex-pcp-20261030-65g7glwh— awaiting review: #1800 implements the agreed full-system reduction and records exact-revision validation, source mapping, reuse, concrete instances and abstract assessment. All six gates pass. Please arrange outside-author-fleet API/correctness review. Private checkout is the team Extra-drivetemplate/.worktrees/pcp, branchfeat/e3lin-e3sat-20261030. #886 retains the broader hardness objective.feat(pcp): certify the four-clause XOR to E3CNF reduction (cslib-comm…