Move numerical backend lowering out of exact reduction contracts

[isPANN]

Problem and root cause

Numeric storage conversion is registered as mathematical reduction, and its precision guarantees are inferred from individual coefficients.

src/rules/ilp_casts.rs, qubo_casts.rs, maximumsetpacking_casts.rs, and spinglass_casts.rs use i64_to_exact_f64(). Preserving each input coefficient does not preserve sums, constraints, or objective ordering. Fixed ILP pipelines currently route through ILP<*, i64> -> ILP<*, f64>, placing a backend representation conversion in the mathematical reduction graph.

The helper also rejects all integers outside [-2^53+1, 2^53-1], although 2^53 and many larger i64 values are exactly representable. This scalar test is both overly restrictive for transport and insufficient to certify an optimization reduction.

Reproducible counterexample

Build a binary integer ILP with constraints:

• x0 = x1
• x2 = x3
• x0 + x2 = 1

Maximize:

2^52*x0 + 2^52*x1 + 2^52*x2 + (2^52 + 1)*x3

All coefficients are individually representable in f64. The feasible source objectives are:

The current ILP CLI route has returned the first assignment with status optimal. The source witness is feasible, but source optimality is false.

Required refactor

1. Terminate fixed integer ILP pipelines at ILP<bool, i64> or ILP<i64, i64>.
2. Move required HiGHS numeric lowering into the existing ILP backend implementation. Delete the corresponding cast reduction registrations and superseded reduction implementation. Backend transport is not an equivalence edge.
3. Retain the original integer model for post-solve feasibility and objective evaluation. Validate the decoded assignment against it before extraction, and validate the final source witness at the solver boundary.
4. Apply Separate witness feasibility and source solve conclusions at shared boundaries #1141's outcome semantics: numerical backend optimality generally establishes at most a validated Feasible source result, not exact Optimal. Numerical infeasibility alone does not establish source infeasibility. Propagate unresolved outcomes to decision consumers.
5. Audit every production caller of i64_to_exact_f64(). Separate:
   • exact arithmetic: keep integers/rationals through the computation;
   • lossless scalar transport: test actual representability, including sparse exactly representable integers above 2^53; check range before float-to-integer conversion, avoiding saturating round-trip traps near i64::MAX;
   • numerical backend lowering: document its numerical contract and do not promote its result to an exact proof;
   • mathematical reductions: retain a numeric edge only with a problem-level argument preserving feasibility and required objective order. Remove unsound edges instead of treating coefficient checks as proof.
6. Remove the misleading universal MAX_EXACT_F64_INTEGER gate. Do not narrow a mathematical model just to match an unrelated backend.
7. Preserve deterministic solver selection. Registry presence means an implementation is registered; runtime representation failures remain explicit errors. No instance-ranking system, fallback, or solver-difficulty cutoff is required.

A sound partial scalar embedding such as integer coordinates into exact rational arithmetic is different from a floating-point evaluation pipeline. Audit each edge's actual operations rather than deleting every cross-numeric edge mechanically. The reduction attribute transform = exact describes parameter counts; it is not a certificate of numerical equivalence.

References

• MathOpt HiGHS adapter: backend claims and result status are handled explicitly.
• HiGHS tolerances: zero MIP gaps do not remove floating-point feasibility/optimality tolerances.
• CP-SAT model definition: integer arithmetic domains and floating-objective scaling guarantees are explicit.

Acceptance tests

• The counterexample above cannot be reported as exact Optimal unless source optimality is independently established.
• Integer ILP target and source feasibility are checked after backend decoding.
• Lossless scalar conversion accepts 2^53 and rejects 2^53+1; boundary checks cover i64::MIN/MAX without saturating conversions.
• An exact reduction chain cannot acquire an unsound optimization equivalence from a coefficient-only cast.
• Numerical infeasibility does not become an exact negative decision.
• Normal fixed ILP routes continue to execute, with truthful result statuses.
• Audit findings for other cast edges are resolved within their mathematical contract, not hidden by larger thresholds.

Run focused numeric/ILP tests and make check with relevant features. No new solver framework, certificate system, or arbitrary-precision migration of every model is required.

Related: #1141 (result and witness contracts), #1146 (exact CVP arithmetic), #1092 (separate mathematical domain restrictions in reduction routes). Coordinate the result-contract change with #1141 before exposing the revised ILP pipelines.