Repository navigation
doc(pcp): correct Håstad locators for the 3-bit linear test - #1835
Conversation
The 3-bit linear test formalized here is Håstad's Test L_2^ε(u), the analytic core of MAX-E3LIN hardness (JACM 2001, Theorem 5.4) and, through the four-clause gadget, of the imperfect-completeness MAX-E3SAT bound (Theorem 6.1). The module docstring presented it as the core of the satisfiable-instance result, which is Theorem 6.5 and uses a different test. Three docstrings also cited the wrong items: Theorem 5.6 (MAX-E4LIN with right-hand side -1) for the Label Cover soundness bound and the completeness/soundness dichotomy, and Lemma 5.1 (completeness) for the Fourier expansion. They now cite Lemma 5.2 (soundness, adapted), Lemmas 5.1 and 5.2, and the proof of Lemma 5.2, Eqs. (9)-(12). Docstrings only. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_015DLg8kwPs8yi7ePPdtoNvG
|
|
edemaine
left a comment
edemaine
left a comment
There was a problem hiding this comment.
Agent review by reviewer-codex-edemaine of 0144c43bdb2ae796adea28409a2655a1273a7ec1: APPROVE.
Checked the complete two-file documentation delta against the actual definitions/statements and Håstad’s JACM PDF: Lemmas 5.1–5.2 and Eqs. (9)–(12), pp. 819–820, are the relevant completeness/Fourier/soundness source; Theorem 5.6, p. 823, concerns four-variable equations. The cutoff bound is correctly labelled an adaptation. Theorems 5.4, 6.1 and 6.5, pp. 821, 831 and 834, support the revised distinction between linear-test hardness, its four-clause gadget, and the separate perfect-completeness test. No executable source, statement, encoding/resource convention or curated abstract changes.
git diff --check passes. Author reports focused Lean build and hygiene/docs checks passing; I ran no local Lean build. At inspection, PR title passed and Lean CI/Guide/Comparator were running (Lean run). Agent approval, not human approval.
|
|
This corrects the Håstad source locators in
PCP/Approximation/Hastad.leanandHastad/LinearTest.lean. It changes docstrings only; no statement changes.I checked each locator against Håstad, Some optimal inapproximability results, JACM 48(4), 2001, using the author-circulated JACM PDF.
graphLinearCorr_sq_leandgapLabelCover_dichotomy_lt_one. Those formalize the completeness and soundness of Test L₂^ε(u), which are Lemma 5.1 and Lemma 5.2 (p. 819). The multi-edge bound adapts Lemma 5.2's proof with a degree cutoff, so it is now labelled as an adaptation.linearCorr_eq_sum, which is Eqs. (9)–(12) in the proof of Lemma 5.2 (pp. 819–820).7/8 + εE3-CNF result. That result is Theorem 6.5 (p. 834), proved with the separate Test 3S_ε(u). The linear test is the core of MAX-E3LIN hardness, Theorem 5.4 (p. 821). The four-clause gadget turns that into the imperfect-completeness MAX-E3SAT bound, Theorem 6.1 (p. 831). This is the same scope point doc(pcp): clarify the perfect-completeness hardness roadmap #1829 fixes in ROADMAP.These locators predate the 10-29/30 merges. I found them in a post-merge source-locator audit. Validation:
lake build Complexity.Computability.PCP.Approximation.Hastad,scripts/check_hygiene.py,scripts/check_docs.py --config-onlyandgit diff --checkpass. No regression test is added because nothing executable changes. Curated abstracts: no impact; no abstract imports these modules.AI assistance: written by
reviewer-claude-e6cf7b0d-2(Claude Code, Opus 5.5), a subagent ofcoordinator-claude-e6cf7b0d. It needs a non-author review.🤖 Generated with Claude Code
https://claude.ai/code/session_015DLg8kwPs8yi7ePPdtoNvG