docs: verify-reduction — 5 type-incompatible reductions (math verified, needs decision variants)

[zazabap]

Summary

5 reductions that are mathematically verified but cannot be implemented as ReduceTo in the current codebase due to Value type mismatches between source and target models.

#	Source(Type) → Target(Type)	Mismatch	Checks	Resolution needed
#198	MVC(Min) → HamiltonianCircuit(Or)	Min→Or	29K	Use VertexCover(Or) from PR #976
#890	MaxCut(Max) → OLA(Min)	Max→Min	248K	Add decision MaxCut variant or use ReduceToAggregate
#888	OLA(Min) → RootedTreeArrangement(Or)	Min→Or	18K	Add decision OLA variant (one-way reduction)
#894	MVC(Min) → PartialFeedbackEdgeSet(Or)	Min→Or	721K	Use VertexCover(Or) from PR #976
#395	Partition(Or) → KthLargestMTuple(Sum)	Or→Sum	45K	Turing reduction; needs ReduceToAggregate

Each includes Typst proof + constructor Python + adversary Python + test vectors JSON.

These are split from PR #992 (the main batch of 32 implementable verified reductions).

Test plan

• Typst proofs compile to PDF
• Constructor scripts pass
• Adversary scripts pass

🤖 Generated with Claude Code

[codecov]

Codecov Report

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

Additional details and impacted files

@@            Coverage Diff             @@
##             main     #996      +/-   ##
==========================================
+ Coverage   98.03%   98.12%   +0.09%     
==========================================
  Files         784      858      +74     
  Lines       82310    89004    +6694     
==========================================
+ Hits        80695    87338    +6643     
- Misses       1615     1666      +51     

☔ 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.