[Refactor] Treat each reduction as one construction and witness-mapping lifecycle

[isPANN]

A reduction must be maintained as one complete algorithm: construct the target instance and recover the source answer from a correct target result. Preserve the existing typed witness API, make each executed step own one construction, and keep brute-force witness selection out of models and reductions.

Related: #1145. This issue covers reduction lifecycle, reverse APIs, result interpretation, and the relocation of SolutionAggregate. Other numerical, enumeration-domain, and model-domain work in #1145 remains separate.

Mathematical contract

The ordinary witness workflow remains:

source.reduce_to() -> executed result
executed result.target_problem() -> solve target
executed result.extract_solution(qualifying target witness) -> source witness

Keep Problem::evaluate, ReduceTo, and typed ReductionResult method signatures. Preserve ReduceToAggregate and AggregateReductionResult::extract_value for genuine mathematical value mappings, including aggregate-only Sum uses. Do not redesign Max, Min, or the value system.

For each affected rule, state:

1. Its instance domain, including whether infeasible source instances are supported.
2. Whether extraction needs a feasible or optimal target witness, and any threshold or other mathematical conditions.
3. The source guarantee for every qualifying target witness, including every tied optimum.
4. How a completed target result represents source infeasibility, unless source feasibility is an explicit promise.

A witness mapping alone does not establish a complete-solving capability. For example:

Rule	Target result	Source answer
MVC -> MIS	Maximum independent set	Complement gives minimum vertex cover
SAT -> MIS	Maximum independent-set size k for m source clauses	k=m: recover satisfying assignment; k<m: UNSAT
Binary ILP -> QUBO	Optimal assignment and energy	Apply the proved energy relation: recover source optimum or conclude source infeasibility
Decision<P> -> P	Optimum and witness	Compare the bound; recover a witness when the bound is met
P -> Decision<P>	Multiple threshold-query results	Recover an optimum value under the decision-search algorithm's domain

An unconstrained QUBO has an optimum even when a source constrained problem is infeasible. Thus “every target optimum unconditionally yields a source feasible witness” is not the contract for penalty reductions over all instances. The complete mathematical result interpretation must be specified and proved. Its thresholds and value relationships belong to the reduction; solver completion executes them.

Extraction itself performs the mapping under its premises. It does not check solver optimality, repair output, revalidate source feasibility, or guarantee correctness for manually supplied witnesses outside the contract. Backend failures/timeouts are errors, never mathematical NO. Preserve genuine transport and representation failures.

Witness/aggregate describe recovery capabilities; Turing describes a query procedure. They are not three mutually exclusive mathematical categories. Exact witness recovery does not imply counting or approximation preservation. This issue does not introduce a general Turing execution framework.

Current local evidence

These observations concern the current local working tree associated with #1145, not necessarily main:

• ReductionChain::execute invokes separate witness and aggregate constructors. For #[reduction(aggregate = custom)], both generated constructors call reduce_to. Deterministic construction produces equivalent results, but repeats work/storage and uses parallel arrays rather than one owned execution.
• Chain, JSON, and ExecutedPath already share the private map_solution traversal. Preserve it. Current Rust source has no extract_solution_any or checked/unchecked extraction family.
• DynAggregateReductionResult::source_has_solution evaluates and maps a value, then queries the global variant registry and calls VariantEntry::value_has_solution. It can panic for an unregistered source.
• SolutionAggregate is defined in src/types.rs. Its candidate-versus-total operation serves brute-force selection. Unrelated rule bounds, the variant predicate, and DynProblem::evaluate_dyn also depend on it; the latter two use self-comparison as a feasibility predicate.
• Three map_config_back_internal forwarding paths in KSG/triangular mapping only add error conversion at their outer entry.
• One-hot extraction branches remain in coloring, TSP, multiway-cut, and inverse-kinematics QUBO rules. Their necessity must be checked against the actual qualifying-witness premise.
• MVC -> EnsembleComputation uses evaluation to obtain the meaningful program prefix needed for mapping. Necessary decoding must not be deleted mechanically.
• Canonical instructions contain conflicting external-extraction validation guidance.

Agreed implementation design

One executed object per witness step

Replace parallel witness/aggregate vectors with one vector of executed records:

struct ExecutedStep {
    witness: Rc<dyn DynReductionResult>,
    aggregate: Option<Rc<dyn DynAggregateReductionResult>>,
}

For a step supporting both operations, registration calls reduce_to once and creates both trait views from the same Rc allocation. Rc::clone copies a reference, not the target or result. Optional completion operations must use that same state. This is existing runtime-boundary machinery, not a new all-purpose trait for rule authors.

Update execution records, ReduceFn, registration macros, graph paths, fixed ILP pipelines, and callers together. Preserve shared-prefix execution in ExecutedPath. Keep standalone aggregate-only execution without witness requirements. Consolidate the separate Decision<P> -> P witness/aggregate result structs into one result containing the target and bound; one runtime step must not call both constructors.

Result interpretation without registry or enumeration coupling

Delete DynAggregateReductionResult::source_has_solution and VariantEntry::value_has_solution, including generated/manual initializers. Bind required interpretation while concrete types are available at the existing runtime boundary, using the reduction's mathematical value relation. Do not introduce another global predicate table, model-name branches, JSON-shape guessing, or a universal replacement trait.

Keep the existing shared solver completion for typed/fixed ILP pipelines and bundles. Ordinary extraction does not call outcome interpretation. Composition must establish each preceding step's witness premise; graph reachability alone is not proof of complete-solving capability.

Scope SolutionAggregate to brute force

Move its definition and Max/Min/Or/Extremum implementations into src/solvers/brute_force.rs. Required cross-crate enumeration callers may use the existing solvers export facade; do not retain an alias at types::SolutionAggregate.

Keep bounds where candidate/final-value selection or brute-force APIs actually need them. Remove unrelated model/reduction bounds. Migrate self-comparison predicates in tests to assertions on their concrete mathematical values. Preserve Aggregate and value wrappers in src/types.rs.

Also migrate DynProblem::evaluate_dyn: its feasibility output must remain correct without depending on brute-force selection. Merely moving its import is insufficient. First produce the concrete bridge signatures and caller inventory, using existing value semantics where concrete types are available; no blanket public-API rewrite is authorized.

Consolidate extraction paths

• Keep _dyn, _any, and _json methods that perform necessary type erasure/transport for actual callers, including the CLI crate.
• Keep one mathematical extractor and the existing shared reverse traversal. No checked/unchecked/strict variants, flags, versioned APIs, or compatibility wrappers.
• Merge pure map_config_back_internal forwarding wrappers and use appropriate typed errors in the actual mapping.
• Remove checks excluded by proved premises. If a qualifying target optimum triggers a branch, repair the construction/mapping rather than turn the defect into an extraction rejection.
• Retain required decoding, index computations, and genuinely reachable arithmetic/representation errors. Keep display evaluation distinct from acceptance gates.

Execution plan

1. Establish the exact prerequisite baseline and changed-file inventory. The planning tree already has 819 modified tracked files, and 66 Rust files reference SolutionAggregate or its method; these are not automatically this issue's PR scope.
2. Review concrete runtime and dynamic-evaluation bridge signatures before implementation. Resolve generic type/visibility constraints without moving enumeration coupling elsewhere.
3. Atomically migrate executed ownership, registration, solver completion, and affected callers. Relocate SolutionAggregate in that migration where compilation dependencies require it.
4. Clean rule-local extraction and geometric mapping in bounded groups after proving premises. Update tests with each group.
5. Update docs/src/design.md, .claude/CLAUDE.md, canonical add/review/verify skills, and affected API diagrams/paper material. Eliminate contradictory policies.
6. Run focused tests followed by required repository checks and report actual results.

Detailed local implementation plan: docs/plans/2026-09-13-reduction-lifecycle.md (not yet committed).

Acceptance

• Core typed witness APIs and Problem::evaluate are preserved.
• Each executed witness step constructs once; witness, aggregate, and completion share the result state.
• Decision conversion and common-prefix path execution obey the same ownership rule.
• Typed chain/path and CLI extraction share the mapping implementation; necessary representation bridges remain.
• No extraction registry lookup, solver-correctness validation, or superseded forwarding API remains in the affected paths.
• Complete solving handles source optima and infeasibility through proved rule relationships, including SAT -> MIS and ILP -> QUBO.
• SolutionAggregate lives with brute-force selection; model evaluation, reduction mapping, and non-enumerative solver completion do not depend on it.
• Aggregate-only Sum operations remain usable without witness selection or solver registration.
• Checks cover ILP variable projection, MVC complement, tied optima, multi-step composition, construction count, shared prefixes, unregistered mathematical operations, dynamic evaluation, and error attribution.
• Rule premises and canonical contributor guidance agree; no blanket malformed-witness rejection requirement is added.
• make check, make mcp-test, make coverage, and git diff --check pass; make paper runs when affected. Preserve >95% changed-line coverage and report the actual base. Historical checks do not validate new implementation.

Review and delivery boundaries

Implement on the current refactor/native-ilp-adapter branch and worktree. Do not create additional branches or split this work into many independent PRs. The maintainer has waived the PR file/line limit for this refactor; mathematical correctness and maintainability take priority. Do not preserve obsolete wrappers to divide the migration artificially. Exclude unrelated local changes, untracked verifier/skills, generated artifacts, and temporary audit scripts. Do not commit the entire working tree. Merge requires green CI and explicit user permission.

Definition references

• Metric reduction, Definition 3: input transformation and answer postprocessing.
• Optimization/approximation-preserving reductions: solution mappings and additional approximation guarantees.
• Counting reductions: counting guarantees are separate from witness recovery.
• Lucas, Ising formulations: energy optimization and threshold interpretation.

Implementation result

• Each runtime witness constructor returns one ExecutedStep. Witness, aggregate and optimum interpretation share the same Rc result. Decision conversion and shared-prefix execution use the same ownership model.
• Removed registry result predicates and moved SolutionAggregate into brute-force selection. Concrete dynamic evaluation works without aggregation or catalog registration; typed witness APIs are unchanged. The aggregate dynamic bridge also has no unused witness-lifetime bound.
• Typed chains, executed paths and JSON extraction use the same reverse traversal. A real MVC -> MIS -> SetPacking -> ILP test compares all of them with direct typed composition on the same witness. CLI tests exercise the shared JSON bridge and qualifying tour extraction.
• Removed three geometric forwarding wrappers, redundant one-hot extraction checks and test-helper evaluation gates. Ensemble extraction still computes the meaningful program prefix. Serialized geometric execution state retains real coordinate, tape and arithmetic errors without an implicit missing-field default.
• MultiwayCut always deletes negative edges and optimizes the nonnegative remainder. Every target optimum in signed test cases agrees with independent source enumeration.
• TravelingSalesman uses nonnegative shifted costs and an explicit optimum-energy threshold; it restores signed tour costs or source infeasibility. It preserves accepted small-cycle, loop and parallel-edge cases without narrowing the source model domain.
• Inverse kinematics retains all omitted constants and a separated energy threshold. Source infeasibility is recovered before orientation extraction, including globally incompatible allowed-pair chains.
• Both newly completed value relations are exercised through complete_reduction, in addition to rule-level all-optima checks. Mathematical premises and proofs are documented in the paper and canonical contributor guidance.

Verification

Passed: make check, make mcp-test, make paper, final Clippy, formatting and git diff --check. The added composition test also passed its focused run, and removal of unused generic bounds passed workspace/all-targets compilation.

The subsequent make coverage run tested the final state and passed at 95.52% against origin/main (5,711 changed lines; 256 missing). The threshold, exclusions and comparison base were unchanged.

Implementation and verification are complete in refactor/native-ilp-adapter. No additional branch, PR, commit, push or merge was created. The local implementation plan contains the completion evidence.