feat: lp tactic, strict-Farkas / slack-variable extension (deferred)

Deferred future work — tracks the strict-inequality fragment that v1 (Stages 1–4a) explicitly rejects.

Problem statement

The uniform v1 strictness rule in the staged plan (https://github.com/kim-em/soplex/issues/40) allows strict (in)equalities only in goal position, where the refutation is non-strict. Strict in any of the following positions is rejected with a clear error:

• Hypotheses: (h : a < b) ⊢ goal. The Farkas refutation of ¬goal could need to combine h with a strict coefficient, which checkInfeasible_sound (over closed non-strict polyhedra) doesn't support.
• Universal guards: ∀ y, a < y → …. Same issue — strict in the guard contributes a strict row to the sup-LP, beyond checkInfeasible_sound's scope.
• Existential body conjuncts: ∃ x, 0 < x ∧ x < 1. The feasibility LP for the witness can return a boundary point that violates the strict constraint.

Goals like

example (h : 0 < x) (h' : x < 1) : 2 * x < 2
example : ∃ x : Rat, 0 < x ∧ x < 1
∀ y : Rat, 0 < y → y < 1 → y < 2

are well within the spirit of lp but are explicitly out of v1's fragment.

What would be needed

The standard fix is the slack-variable trick:

1. Introduce a fresh variable δ ≥ 0.
2. Encode each strict row aᵢ · x < bᵢ as aᵢ · x + δ ≤ bᵢ.
3. Maximise δ.
4. Accept iff the certified optimum satisfies δ > 0 (checked by decide +kernel on the closed rational).

This converts a strict-feasibility / strict-Farkas problem into a non-strict optimisation problem solvable by SoPlex's existing certificate machinery.

The encoding extends naturally to mixed strict/non-strict systems: only the strict rows get the + δ slack; non-strict rows are unchanged.

Where the slack-variable trick lives in the stage hierarchy

• For Stage 1 leaf inequality LPs: when hypotheses contain strict rows, the refutation system becomes a strict feasibility problem. Use the slack encoding on hypothesis rows.
• For Stage 2 existential body: when body conjuncts are strict, the witness-search LP becomes a strict feasibility problem. Use slack on body rows; the witness is recovered from the primal's non-δ components.
• For Stage 3 universal elimination: when universal guards or bodies are strict, the sup-LP becomes a mixed strict/non-strict optimisation. Use slack on the strict pieces.

Each stage's slack-extension reuses the same primitive but plumbs it through the stage's specific LP shape.

Soundness

The reduction is sound: a strict system is satisfiable iff the corresponding slack system has a feasible point with δ > 0. The certificate machinery already handles the slack system as a plain non-strict LP; the only new piece is the decide +kernel check that δ > 0 on the returned primal.

Scope and tradeoffs

Less heavy than the parametric-witness extension (https://github.com/kim-em/soplex/issues/48). Mostly a re-plumbing of existing primitives. The main implementation work:

• Recognise strict rows in the extractor (currently rejected).
• Insert the slack variable into the LP problem matrix.
• Add the δ > 0 post-check to the certificate dispatch.
• Update each stage's variable-ownership policy to allow strict in the corresponding positions.

Probably a smaller issue than any of Stages 1–4a once those are in.

Out of scope for this issue

• All of Stages 1–4a (already in their own issues).
• Parametric witnesses (separate deferred issue: https://github.com/kim-em/soplex/issues/48).
• Performance optimisations specific to slack-extended LPs.

Status

Deferred. Not actively being worked on. Open for tracking. Will be revisited once v1 (Stages 1–4a) is in real use and the strict-fragment limitation is encountered.

🤖 Prepared with Claude Code

Start with the existing extractor, certificate machinery, and Stage 1–3 LP paths described in the issue. Trace where strict rows are rejected and how variable ownership is enforced; done means the shared slack encoding, certified δ > 0 check, and corresponding strictness handling work across the named stages.