docs: verify reduction #198 — MinimumVertexCover → HamiltonianCircuit

[zazabap]

Summary

Mathematical verification of the classic Garey & Johnson Theorem 3.4 gadget reduction (VC → HC). This is a complex construction with 12-vertex/14-edge cover-testing widgets, chain links between widgets, and K selector vertices.

• Typst proof: Full construction (4 steps), bidirectional correctness, solution extraction, overhead table, YES example (P3, K=1), NO example (K3, K=1)
• Constructor: 5,782 checks, 0 failures — widget structure (14 edges, cross-edge positions, boundary degrees), exhaustive n ≤ 4
• Adversary: 5,937 checks, 0 failures — independent implementation with hypothesis PBT, traversal pattern verification
• Cross-comparison: 244 instances, 0 disagreements (vertex counts, edge counts, VC feasibility all agree)

Bug found during iteration

First run: 15 failures on graphs with isolated vertices where K > number of non-isolated vertices. The G&J construction requires K ≤ n' (non-isolated vertices) because selectors need vertex chains to traverse. Fixed by adding this as an explicit prerequisite. This is the same edge-case limitation noted in the standard G&J treatment.

Verification Report

Constructor: 5,782 passed, 0 failed
  - Widget 14-edge invariant verified for all widgets across all graphs n ≤ 4
  - Cross edges at positions (3,1), (3,1), (6,4), (6,4) verified
  - Interior vertices have 0 external edges
  - Selector-chain connectivity verified
  - Forward+backward: 160 graph-K instances, all agree

Adversary: 5,937 passed, 0 failed  
  - Independent gadget construction from Typst spec
  - 3 traversal patterns (Pattern U, u-only, v-only) verified
  - hypothesis: 2,290 graph-K pairs
  - Bugs found: none

Cross-comparison: 244 agree, 0 disagree
Iterations: 2 rounds (isolated vertex fix)
Verdict: VERIFIED

Closes #198

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

Additional details and impacted files

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