design: ReductionResult should declare value mapping, not just solution mapping

[isPANN]

Problem

The current framework only declares how to convert a target solution back to a source solution (extract_solution), but does not declare the relationship between the target's optimal value and the source's feasibility.

For example, the Partition → BinPacking reduction is correct iff "optimal bins ≤ 2 ↔ Partition is feasible", but this "≤ 2" threshold is buried inside reduce_to() logic. The framework cannot see it, and automated soundness testing cannot verify it.

This matters because:

• Or→Min/Max reductions implicitly embed a decision threshold inside an optimization target
• The target's real semantic type is Or (feasible/infeasible), but the framework treats it as Min/Max
• Automated NO-instance testing (solve(source) vs solve(target)) cannot detect unsoundness for targets where evaluate always returns Some (e.g., BinPacking — every packing uses some number of bins)

Scope

Among the 5 unsound reductions in #1006, all 5 happen to be detectable because their targets either have Or values or support Min(None). But the gap exists for rules like Partition→BinPacking, where a future soundness bug of the same kind would go undetected by automated testing.

Proposed Solution

Add extract_value to the ReductionResult trait:

trait ReductionResult {
    fn target_problem(&self) -> &Target;
    fn extract_solution(&self, target_config: &[usize]) -> Vec<usize>;  // existing
    fn extract_value(&self, target_value: Target::Value) -> Source::Value; // new
}

Each reduction must explicitly declare how the target's aggregate value maps back to the source's value. Examples:

Reduction	Implementation
Or→Or (most rules)	extract_value(Or(b)) = Or(b) (trivial, default impl)
Partition→BinPacking	extract_value(Min(Some(k))) = Or(k <= 2)
Partition→SWCP	extract_value(Min(Some(_))) = Or(true), Min(None) = Or(false)
Min→Min	extract_value(Min(v)) = Min(f(v))

Benefits

• Hidden thresholds become explicit — BinPacking reduction must write k <= 2, cannot hide it
• Uniform soundness testing — all reductions can be tested with one pattern: assert_eq!(solve(source), reduction.extract_value(solve(target)))
• Framework semantics complete — a reduction declares both "how solutions map" and "how values map"

Cost

• All existing reductions need a new method (Or→Or cases can use a default impl)
• Trait bounds become slightly more complex

Context

Discovered while building the verify-rules skill (#1006 follow-up). The NO-instance soundness check works for Or→Or and Or→Min-with-None targets, but fails for Or→Min-always-Some targets due to this missing value mapping.