docs: verify reduction #841 — NAESatisfiability → SetSplitting

[zazabap]

Summary

Mathematical verification of the NAESatisfiability → SetSplitting reduction (#841) using the /verify-reduction skill.

Typst proof: docs/paper/proposed-reductions-841.typ

• Construction: universe (2n elements) + complementarity subsets + clause subsets
• Correctness: ⟹ (NAE assignment → partition) + ⟸ (partition → NAE assignment)
• Extraction: read positive element's partition side
• Overhead: universe_size = 2*num_vars, num_subsets = num_vars + num_clauses
• Example: 3 vars, 2 clauses, fully worked

Python verification: docs/paper/verify-reductions/verify_naesatisfiability_setsplitting.py

• 12,132 checks, 0 failures
• Forward + backward exhaustive n ≤ 4
• Solution extraction verified with complementarity check

Lean lemmas: docs/paper/verify-reductions/lean/ReductionProofs/NaesatSetsplitting.lean

• 2 overhead lemmas proved

Test plan

• python3 docs/paper/verify-reductions/verify_naesatisfiability_setsplitting.py passes (12,132/0)
• PDF compiles without errors
• Lean builds (trivial rfl lemmas)

🤖 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 (a469322).

Additional details and impacted files

@@           Coverage Diff           @@
##             main     #977   +/-   ##
=======================================
  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.

[zazabap]

Closing: does not meet the stricter verify-reduction skill requirements. Will redo with the updated skill.