[Critical] Fix reduction result recovery and reference validation contracts

.claude/CLAUDE.md

@@ -165,8 +165,11 @@ Max<V>, Min<V>, Sum<W>, Or, And, Extremum<V>, ExtremumSense
 - Problems parameterized by graph type `G` and optionally weight type `W` (problem-dependent)
 - `BruteForce::solve()` returns `Result<Option<P::Solution>, SolveError>`; `None` means exhaustive search proved infeasibility
 - `BruteForce::find_all_witnesses()` is a reference-testing helper for collecting every optimal or satisfying solution
-- `ReductionResult` provides `target_problem()` and `extract_solution()` for witness/config workflows; `AggregateReductionResult` provides `extract_value()` for aggregate/value workflows
-- Every direct `extract_solution()` must call `validate_target_solution()` once before decoding; composed extractors delegate validation to the first direct decoder.
+- `ReductionResult` provides `target_problem()` and `extract_solution()` for witness/config workflows; `AggregateReductionResult` provides `extract_value()` for aggregate/value workflows. Neither requires a rule-category tag. When both are registered, completed-result recovery borrows both mappings from the same constructed reduction.
+- Register a completed-value mapping with `#[aggregate_reduction]` on its concrete `AggregateReductionResult` implementation. Use `#[aggregate_reduction(identity)]` or `#[aggregate_reduction(ilp_feasibility)]` on an empty impl for identity or ILP-feasibility maps; the shorthand reuses the witness result's source, target, and target accessor. Generic implementations use `register_aggregate_reduction!(ResultType)` for each concrete result type. These register implementations, not rule categories. Read resolved edges through `reduction_entries()`, not raw inventory entries.
+- Reduction chains expose solution and aggregate-value mappings and recover completed results through `ReductionChain::extract_result()`. Every witness reduction preserves existence: source feasibility implies target feasibility. Established target or intermediate infeasibility propagates to the source without a value map or witness extraction. Shared library recovery checks each mapped value against the extracted witness; callers establish optimality or infeasibility under their solver's numerical contract. A missing required mapping or failed witness extraction is an error, not proof of infeasibility. Counting and universal aggregates use `AggregateReductionChain::extract_value()` without a representative witness.
+- Every direct `extract_solution()` must validate once before decoding, using `validate_target_solution()` or `validate_target_witness(target, solution, certifies_source, message)`. The latter evaluates once, applies the rule's feasibility predicate or value-map threshold, and returns a typed `ExtractionError` with the rule's rejection reason; composed extractors delegate validation to the first direct decoder.
+- Decision-equivalence rules map completed `Or` values identically. Decision-to-optimization rules own their feasibility/threshold map; reject target configurations that do not certify YES instead of returning an invalid source witness. Optimization rules decode optimal witnesses and evaluate the source; register a value map only when mathematically defined. Counting and universal rules map completed folds without witnesses. Follow [result mappings](../docs/src/design.md#result-mappings); no mandatory rule-category tags.
 - Decode only the reduction's defined mathematical mapping. Reject malformed structure with `ExtractionError`; never panic, truncate, clamp, invent defaults, or add recovery branches. Explicit mathematical alternatives and sentinels are allowed. Test successful decoding and every rejected representation.
 - CLI-facing dynamic formatting uses aggregate wrapper names directly (for example `Max(2)`, `Min(None)`, `Or(true)`, or `Sum(56)`)
 - Graph types: SimpleGraph, PlanarGraph, BipartiteGraph, UnitDiskGraph, KingsSubgraph, TriangularSubgraph
@@ -210,7 +213,7 @@ Reduction graph nodes use variant key-value pairs from `Problem::variant()`:
 - Each primitive reduction is determined by the exact `(source_variant, target_variant)` endpoint pair
 - Reduction edges carry `EdgeCapabilities { witness, aggregate, turing }`; graph search defaults to witness mode, aggregate mode is available through `ReductionMode::Aggregate`, and Turing (multi-query) mode via `ReductionMode::Turing`
 - `#[reduction]` requires one `transform = exact`, `transform = upper_bound`, or `transform = unavailable` declaration and currently registers witness/config reductions; aggregate-only and Turing edges require manual `ReductionEntry` registration
-- `Decision<P> → P` is an aggregate-only edge (solve optimization, compare to bound); `P → Decision<P>` is a Turing edge (binary search over decision bound)
+- `Decision<P> → P` supports both mappings: compare the exact optimum to the bound, and recover a witness only if it meets the bound. `P → Decision<P>` is a Turing edge (binary search over decision bound).
 
 ### Extension Points
 - New models register dynamic load/serialize metadata through `declare_variants!` and, when finite enumeration exists, register it separately through `register_brute_force!`; neither belongs in CLI match arms

Cargo.toml

@@ -30,7 +30,7 @@ thiserror = "2.0.20"
 num-bigint = "0.4.8"
 num-rational = "0.4.2"
 num-traits = "0.2.19"
-good_lp = { version = "=1.14.2", default-features = false, features = ["highs"] }
+highs = "2.4.0"
 inventory = "0.3.24"
 rand = "0.10.2"
 criterion = { version = "0.8.2", optional = true }