docs: verify reduction #841 — NAESatisfiability → SetSplitting

[zazabap]

Summary

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

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

• 4-step construction: universe (2n elements) + complementarity + clause subsets
• Independent ⟹/⟸ correctness proofs
• YES example: n=3, m=2, α=(T,T,T) — fully worked, all subsets non-monochromatic
• NO example: n=3, all 8 clauses — proven NAE-unsatisfiable (every assignment makes one clause all-true)

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

• 35,322 checks, 0 failures
• All 7 mandatory sections (sympy, exhaustive n≤5, extraction, overhead, structural, YES, NO)
• Exhaustive forward + backward for n ≤ 5

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

• 2 non-trivial lemmas: complement symmetry of NAE satisfaction
• 5 overhead/concrete lemmas, 0 sorry

Self-review: 2 iterations — scratch work in YES example caught and removed.

Test plan

• python3 docs/paper/verify-reductions/verify_naesatisfiability_setsplitting.py — 35,322 PASS
• PDF compiles without errors
• Zero hand-waving language in Typst proof
• Both YES and NO examples present and fully worked

🤖 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 (983555d).
⚠️ Report is 1 commits behind head on main.

Additional details and impacted files

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