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

[kim-em]

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 (#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 (#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: feat: lp tactic, parametric witnesses via symbolic QE (deferred) #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

[kim-em]

Status update (post-release sweep): the hypothesis and goal positions have landed — strict hypotheses are relaxed or used via the strict-aware Farkas certificate (leanprover/lp-tactic#16, leanprover/lp-tactic#19, leanprover/lp-tactic#22), and strict / ≠ goals prove. What remains of this issue is exactly the quantifier positions: strict atoms in existential bodies and strict universal guards/bodies are still rejected (verified against leanprover/lp ea9a0d57: ∃ x : Rat, 0 < x ∧ x < 1 and strict ∀-guards both error). The focused implementation issue for that remainder is leanprover/lp-tactic#32.

🤖 Prepared with Claude Code