[RemyDegenne]

This PR adds Lagrange duality for convex programs with finitely many convex inequality constraints under Slater's condition, in LMLExplore/Analysis/Convex/LagrangeDuality.lean (new file, 254 lines). The setting is a convex set C in any real vector space (no topology needed), F convex on C, and constraints h : ι → V → ℝ with [Fintype ι], each convex on C. It targets the Lagrange duality bullet of EValues Layer 1.4 ("Nulls generated by constraints and the dual formula for KL_inf"): ⨅ x ∈ C, (∀ i, h i x ≤ 0) → F x = max_{π ≥ 0} ⨅ x ∈ C, F x + ∑ i, π i * h i x, with the maximum attained [Lue69, Chapter 8], proved by separating in ι → ℝ with one extra coordinate via Mathlib's geometric_hahn_banach_open.

Main declarations:

• LMLExplore.exists_forall_le_add_sum_mul_of_slater: for every lower bound p of F on the feasible set, some multiplier π : ι → ℝ≥0 has p ≤ F x + ∑ i, π i * h i x for all x ∈ C. This is the core result; the others follow from it.
• LMLExplore.exists_iInf_eq_iInf_add_of_slater: strong duality with an attained dual optimum, for a primal value that is bounded below. This is the interface of Suggested.lean's iInf_eq_iSup_iInf_add_of_slater, renamed to say what it states: it is an ∃ π statement. Its redundant Convex ℝ C hypothesis is dropped because ConvexOn implies it.
• LMLExplore.iSup_iInf_add_le_iInf: weak duality in EReal, with no hypotheses.
• LMLExplore.iInf_eq_iSup_iInf_add_of_slater: the README's max form in EReal, with no boundedness hypothesis (the primal value may be ⊥). The ⨆ form is stated in EReal because in ℝ it is false: an unbounded Lagrangian has junk infimum 0, which can exceed a negative primal value.
• IsMinOn.exists_mul_eq_zero_and_isMinOn_add_sum_mul_of_slater: complementary slackness. A minimizer of the program minimizes the Lagrangian of some multiplier over C, and π i * h i x = 0 for every i.

Consumer and dependency edge: the Layer 1.4 dual formula iInf_klDiv_constraintNull_eq (KL_inf = max_{π ∈ Π_g} E_Q log(1 + ∑ π_i g_i)). The README proves its ≤ direction by "apply[ing] Lagrange duality on the probability measures P with klDiv Q P < ∞ and the g i integrable". This PR depends on neither open EValues PR (#384 Layer 0.1, #385 Layer 2.1) and touches only LMLExplore/.

What remains of Layer 1.4 after this PR: constraintNull and the bets Π g, the complete class [LRR26, Theorem 3.1], the optimal bets, and the KL_inf dual formula itself, which consumes this file.

The proof follows the proof of strong duality under Slater's condition in Boyd–Vandenberghe, Convex Optimization (2004), §5.3.2. It separates the open convex set {(t, u) | ∃ x ∈ C, F x < t ∧ ∀ i, h i x < u i} from (p, 0); upward closedness makes the coefficients nonpositive, and Slater's point makes the first coefficient negative. The file cites [BV04, §5.3.2, §5.5.2] and [Lue69, Chapter 8]. No Mathlib infrastructure is vendored. Searches of the pinned Mathlib, Tau Ceti, Statlib, LML and LMLExplore/ for Slater, Lagrangian and strong duality found nothing; the only related material is the planned, unimplemented cone-program duality mentioned in the docstring of Mathlib's Analysis/Convex/Cone/Basic.lean.

Roadmap: EValues

🤖 Prepared with Claude Code

[RemyDegenne]

AI review — approved

Each rubric is judged independently by multiple review agents; the PR merges only once every rubric is green — any rubric that is not green (changes requested, blocked, errored, stale, or not yet run) blocks the merge. See the rubrics.

⚠️ This review ran from a rubrics checkout that differs from the published rubrics (out of date, pinned, or locally edited), so its findings may reflect different rules.

	rubric	state	judge	summary
✅	correctness	approved	claude/claude-opus-5-5	Weak duality, the Slater multiplier lemma, strong duality in both the ∃π/ℝ form (matching Suggested.lean's interface minus the hC hypothesis, which ConvexOn already implies) and the EReal ⨆ form, complementary slackness and the Prod/Pi linear-map expansion are all faithfully stated. Edge cases (empty ι, primal value ⊥, empty C, junk infima in ℝ) are handled correctly.
✅	reuse	approved	claude/claude-opus-5-5	Mathlib and LMLExplore contain no Slater, strong-duality or convex Lagrangian results; the proofs reuse Mathlib's Hahn–Banach separation (geometric_hahn_banach_open_point) and strict-epigraph convexity lemmas. The LinearMap.prod_pi_apply_eq_sum_univ helper has no Mathlib equivalent and is used twice, and the public theorems state different forms rather than forming a parallel API.
✅	scope	approved	claude/claude-opus-5-5	Directly implements the EValues Layer 1.4 Lagrange duality bullet (README.md:408-413, Suggested.lean:129-136) in the roadmap's designated LMLExplore/Analysis/Convex/ home, consumed by the KL_inf dual formula's ≤ direction (README.md:420). Single coherent topic; the LinearAlgebra/Pi.lean helper is a proximate prerequisite used only by the new proof.
✅	attribution	approved	claude/claude-opus-5-5	The file credits its central informal sources (Boyd–Vandenberghe §5.3.2 for the Slater separation proof it follows, §5.5.2 for complementary slackness, and Luenberger Chapter 8) in its module docstring with full bibliographic text. Mathlib's geometric_hahn_banach_open_point is an ordinary dependency, nothing is vendored, and the roadmap is credited only in the PR description.
✅	api-design	approved	claude/claude-opus-5-5	The public surface (core multiplier lemma, attained strong duality matching the roadmap's interface, EReal weak and strong duality, complementary slackness) fits the Layer 1.4 consumer, and the earlier private coordinate lemma is now public as LinearMap.prod_pi_apply_eq_sum_univ in LMLExplore/LinearAlgebra/Pi.lean. The remaining private helpers are specific to this proof, and no definitions or annotations are missing.
✅	generality	approved	claude/claude-opus-5-5	All public results follow from the single core lemma exists_forall_le_add_sum_mul_of_slater, with no unused or overly strong hypotheses: weak duality carries no module assumptions and the redundant Convex ℝ C is dropped. The helper LinearMap.prod_pi_apply_eq_sum_univ is stated over any semiring and module and has no Mathlib equivalent (grep finds only LinearMap.pi_apply_eq_sum_univ).
✅	placement	approved	claude/claude-opus-5-5	The Lagrange duality file sits in LMLExplore/Analysis/Convex/, where the EValues README places it, and the general LinearMap.prod_pi_apply_eq_sum_univ helper sits in LMLExplore/LinearAlgebra/Pi.lean, the path matching Mathlib's pi_apply_eq_sum_univ. All imports are specific and used.
✅	naming	approved	claude/claude-opus-5-5	Every public name describes its conclusion in standard Mathlib terms. The _eq/_le suffixes match what is proved, IsMinOn. and LinearMap. are the right dot-notation namespaces (the latter mirrors Mathlib's LinearMap.pi_apply_eq_sum_univ), and no notation is introduced.
✅	documentation	approved	claude/claude-opus-5-5	Both new files open with module docstrings that say what the material is and what it feeds, and every public theorem's docstring matches its statement without overclaiming or any roadmap/process narrative. The Mathlib declarations the docstrings name (geometric_hahn_banach_open_point, LinearMap.pi_apply_eq_sum_univ) exist.
✅	proof-quality	approved	claude/claude-opus-5-5	The brittle non-terminal simp from the prior round is now a simp only followed by linarith, and the remaining proofs are robust and commented where long. I withdraw the earlier finding about hslater being rebuilt because it is cosmetic.

♻️ = approved on an earlier commit, re-run before merge.

_{Reviewing this diff at head 39e4ef8. rubrics @ 7d59664. CLI @ 7d59664. Review spend: $2.11.}