analyze_lp_evidence performs additional solves in private models and returns an immutable historical LpEvidence. It does not change a model, persistent session, or earlier result. Complete describes completion of the requested analysis; it is not an original optimization result. Available means independently checked numerical evidence, never an exact certificate or proof of an infinite feasible trajectory.

This implements the auxiliary-model approach in the O3 design. It calls the public linear solve primitive with an explicit HiGHS route; it never invokes vendor ray getters or changes a live backend. Original Continuous linear models and Numerical guarantees are admitted. Fixed integer variables, semis, active indicators/globals, Native, Exact/Certified policies, and caller primal starts are rejected without relaxation. Inactive metadata is preserved and structurally validated. Source matrix values and bounds must fit the existing numerical adapter's admitted ranges.

Models and checks

The feasible-base model copies the source feasible set to a distinct owner, with zero objective and offset. A candidate is checked in its private model and again against the original source. Original slots are mapped explicitly, including deleted slots, and all active values must be finite. A source feasibility solve with a zero objective cannot be unbounded. A purported infeasible outcome accompanied by an independently feasible assignment is rejected, regardless of the backend's solution flag.

The recession model minimizes the original objective's normalized improving slope: c*d for minimization, -c*d for maximization. Each direction component lies in [-1,1]; finite lower bounds require nonnegative direction, finite upper bounds require nonpositive direction. Two finite sides force zero. Row recession bounds are derived similarly, with zero replacing each finite endpoint. This LP is bounded and always has the zero direction. Infeasible or unbounded outcomes are inconsistent backend evidence. A nonzero candidate is normalized by its positive infinity norm, then rechecked against original variable and row directions. Publication requires a checked source base point and slope strictly below -minimum_improvement. Original objective offsets play no role in the direction objective.

The Farkas model introduces one nonnegative variable for every finite row and variable bound side. Lower-side variables have positive sign and upper-side variables negative sign. They satisfy A^T*(p-q)+a-b=0 and a total multiplier sum at most one. Every multiplier is also bounded above by one, a redundant bound that makes the normalized box explicit. The objective maximizes L*p-U*q+l*a-u*b. Zero is feasible and the objective is bounded; impossible statuses are rejected. Constant contradictory rows work even when the source has no variables.

The original checker derives signed row multipliers y=p-q, normalizes them by their maximum absolute value, and independently recomputes z=-A^T*y. The auxiliary bound multipliers are not trusted for original attribution. Positive y or z selects a finite lower side; negative selects a finite upper side. Exactly zero selects no side and contributes zero. A nonzero multiplier requiring an infinite endpoint fails validation. The checker recomputes stationarity from the published double multipliers and requires a strictly positive total finite-side contribution above minimum_contradiction. Source objective sense and offset are irrelevant to this contradiction.

Compensated long-double accumulation retains cancellation terms through row sums, transpose products, and total contradiction contributions. Nonfinite results and conversions that erase nonzero values are rejected. Reported margins and slopes retain their signs. The checks have explicit, finite nonnegative tolerances; finite-precision stationarity/recession remains numerical evidence even when a residual prints as zero.

If an original point passes the declared primal tolerance while a positive Farkas margin passes its declared contradiction tolerance, both groups become Rejected/InconsistentEvidence. Diagnostic residuals, margins, and the original point remain inspectable, but neither conclusion remains available. The deterministic regression deliberately exercises this overlap.

Ownership, phases, and budgets

PrimalRay prepares feasible-base and recession phases. Farkas prepares only its multiplier LP. Both and Automatic prepare all three possible phases, before any backend call; this ensures late malformed or oversized transformations cannot consume partial backend work. Automatic runs feasibility then either recession or Farkas, at most two calls. Both normally uses three, or two when infeasibility makes a primal direction unnecessary. Every prepared but unused stage is explicitly not attempted.

The artifact owns the complete original snapshot, tolerances, original-coordinate diagnostic vectors, and each prepared private auxiliary snapshot. A stage records the exact private model, source-column/finite-side map, attempted flag, owning auxiliary_result, and independent auxiliary validation. Every auxiliary objective, bound, and gap belongs to that private model. None is relabeled as a source objective/bound/gap. Passive accessors perform no solver work. Checked source access rejects foreign, deleted, absent, or out-of-range handles. Accepted-direction and Farkas accessors require available evidence. Raw diagnostic records remain inspectable after rejection and may contain information that was examined but not accepted.

One monotonic allowance starts before snapshot copying. Every solve receives only remaining time and the shared cancellation token. Checks run before and after transformations, backend return, candidate checks, publication, and temporary source cleanup. Node limit zero stops immediately; positive node limits are passed to LP solves, which consume no branch-and-bound nodes. The max_auxiliary_solves cap and attempted_calls count public auxiliary solve invocations, including local empty/constant decisions; they do not measure hidden vendor runs. This quota and deterministic coordinator work limits are separate. A backend phase limit stops later phases. A timely checked direction or contradiction from that limited phase may remain available alongside Interrupted and its exact stop status. A whole-operation time/cancel/work/resource failure conservatively removes all group availability and retains only diagnostics/provenance. Allocation/error handling clears availability before allocating error messages.

Auxiliary variable, row, and nonzero caps are checked with overflow-safe arithmetic before constructing their models. The retained-slot cap counts logical source/private entities, terms, maps, result slots, and evidence entries, plus original string/metadata elements. It is an aggregate storage guard, not a byte-accurate peak-memory limit. Temporary model canonicalization and backend internals have their own allocation behavior. The work cap counts coordinator element visits, excluding backend internals; it is not a solver-node count or a CPU-time surrogate. Source copy, canonicalization, propagation, factorization, and destruction are cooperative operations that may overshoot a deadline. Final availability is checked after temporary cleanup; forced process preemption is not promised.

Validation

test/optimize/lp_evidence.cpp checks real HiGHS rays and contradictions with lower/upper/free/fixed/ranged entities, both objective senses, offset invariance, zero-variable contradictory rows, feasible bounded models without evidence, infeasible models with improving directions but no base point, tombstones, source destruction, resource/option admission, and missing backend.

test/optimize/lp_evidence_coordinator.cpp uses a separately compiled GECODE_OPTIMIZE_TEST_LP_EVIDENCE object and a deterministic finite-grid oracle. Production contains no injected callbacks. It rejects bad owners/revisions/masks/dimensions, nonfinite or mismatched scalars, unknown statuses, impossible normalized statuses, and false infeasibility beside a valid point. It checks original recession failure after normalization, an incorrectly selected infinite bound, preservation of a 1+1e16-1e16 contradiction margin, tolerance overlap, phase/cleanup cancellation, and allocation failure after otherwise accepted evidence. Both new test sources explicitly undefine NDEBUG so Release test consumers retain their checks.

The additive C/Python bindings preserve separate evidence groups and owning raw auxiliary-stage children. Rays from vendor getters, exact certificates, sensitivity/ranging, and basis reuse between sources remain separate extensions.