docs: verify reduction #841 — NAE 3-SAT → Set Splitting

[isPANN]

Summary

• Formal Typst proof of NAE 3-SAT → Set Splitting reduction (Lovász 1973 / Garey & Johnson SP4)
• Constructor verification script: 41,107 checks, 0 failures (7 mandatory sections, exhaustive n=3, sampled n=4,5)
• Adversary verification script: 19,832 checks, 0 failures (independent implementation, 3 hypothesis property-based strategies)
• Cross-comparison: 900 instances, 0 disagreements, 0 feasibility mismatches

Verification Report

=== Verification Report: NAE 3-SAT → Set Splitting (#841) ===

Typst proof: docs/paper/proposed-reductions-841.typ
  - Construction: ✓ (3 steps: universe, complementarity, clause subsets)
  - Correctness: ✓ (⟹ + ⟸)
  - Extraction: ✓
  - Overhead: ✓ (universe_size = 2n, num_subsets = n + m)
  - YES example: ✓ (4 vars, 3 clauses, σ=(1,0,1,0))
  - NO example: ✓ (3 vars, 8 clauses = all sign patterns, every σ has all-true clause)

Constructor: verify_nae3sat_setsplitting.py
  - Checks: 41,107 passed, 0 failed
  - Sections: 1(sympy) 2(exhaustive) 3(extraction) 4(overhead) 5(structural) 6(YES) 7(NO)
  - Forward: exhaustive n=3, sampled n=4,5
  - Backward: exhaustive n=3, sampled n=4,5
  - Gap analysis: all claims covered

Adversary: adversary_nae3sat_setsplitting.py
  - Checks: 19,832 passed, 0 failed
  - Property-based: 3 hypothesis strategies (2,500 examples)
  - Forward: exhaustive n ≤ 5
  - Backward: exhaustive n ≤ 5
  - Bugs found: none

Cross-comparison:
  - Instances compared: 900
  - Structural agreement: 900/900
  - Feasibility agreement: 900/900

Bugs found: none
Iterations: 2 rounds (fixed NO example scratch work, fixed clause-matching index)

Verdict: VERIFIED

Test plan

• Typst compiles without errors
• Constructor script: python3 docs/paper/verify-reductions/verify_nae3sat_setsplitting.py → 0 failures
• Adversary script: python3 docs/paper/verify-reductions/adversary_nae3sat_setsplitting.py → 0 failures
• Cross-comparison: python3 docs/paper/verify-reductions/cross_compare_nae3sat_setsplitting.py → 0 disagreements

Closes #841

🤖 Generated with Claude Code

[codecov]

Codecov Report

✅ All modified and coverable lines are covered by tests.
✅ Project coverage is 98.03%. Comparing base (423506c) to head (e489546).
⚠️ Report is 1 commits behind head on main.

Additional details and impacted files

@@           Coverage Diff           @@
##             main     #983   +/-   ##
=======================================
  Coverage   98.03%   98.03%           
=======================================
  Files         784      784           
  Lines       82310    82310           
=======================================
  Hits        80695    80695           
  Misses       1615     1615           

☔ View full report in Codecov by Sentry.
📢 Have feedback on the report? Share it here.

🚀 New features to boost your workflow:

• ❄️ Test Analytics: Detect flaky tests, report on failures, and find test suite problems.