OAI.MetricKMedian.Preparation.client_assignments: intermediate lemma from OpenAI, The approximation threshold for metric k-median (result family 125)

Open

OAI.MetricKMedian.Preparation.client_assignments

by dbenbenn · Oct 27, 2026 · Mathlib 0df444a (Lean v4.33.1)

openai-math

An intermediate lemma of the split of OpenAI's proof of OAI.MetricKMedian.main_finite_work, carved from OpenAI's openai/math development for this platform. The statement and its proof are OpenAI's (OpenAI, The approximation threshold for metric k-median (result family 125), OpenAI Math Release, September 24, 2026, result family 125, github.com/openai/math, Apache License 2.0), ported to Lean 4.33.1 and Mathlib 0df444a.

The statement, as published (namespace OAI.MetricKMedian.Preparation, with open Finset SupplierStars):

theorem client_assignments (F : T → Finset I) (y : I → ℝ) (s : T → X) (i : I → X)
    (V : T → ℝ) {M δ T₁ g γ B v : ℝ} {Δ : ℕ}
    (G : BundleGeometry F y s i V M δ)
    (L : CoupledLaw (targets G.A) flag (weight y G.P G.A G.c γ) G.P y G.p G.c g γ B Δ)
    (hy : ∀ a, 0 ≤ y a) (hM : 0 < M) (hδ : 0 < δ) (hδ1 : δ ≤ 1/4)
    (hT : 0 < T₁) (hθ : 1/(M*δ) ≤ 1/8) (hα : M/(δ*T₁) ≤ 1/4)
    (hg : 0 < g) (hγ : 0 ≤ γ) (hunit : g*(Δ:ℝ)=1)
    (j : X) (t : T) (Fj : Finset I) (hmj : ∑ a ∈ Fj, y a=1)
    (hms : ∑ a ∈ F t, y a=1) (hvj : ∑ a ∈ Fj, y a*dist j (i a)=v)
    (hnearest : ∀ a ∈ F t, ∀ b ∉ F t, dist (s t) (i a) ≤ dist (s t) (i b))
    (hV : V t ≤ v) (hD : dist j (s t) ≤ M*v) :
    let p₀ := 1-1/(M*δ)
    ∃ r : (L.Ω × (T → Finset I)) → Physical I T → ℝ,
      (∀ z, 0 < (L.ν.joint L.κ).weight z →
        (∀ a, 0 ≤ r z a ∧ r z a ≤ physicalOpen L z a) ∧ (∑ a, r z a)=1) ∧
      (L.ν.joint L.κ).expect (fun z => ∑ a, r z a*
        (Sum.elim (fun a => dist j (i a)) (fun ti => dist j (i ti.2)) a)) ≤
        max (farFactor δ p₀ (M/(δ*T₁)) (M/T₁) γ)
          (nearFactor p₀ (M+(1+δ)*T₁) γ g)*v

Definitions. The statement is written with OAI.MetricKMedian.FiniteLaw.expect and OAI.MetricKMedian.FiniteLaw (definitions bundle OAIQ035K004 of this split); OAI.MetricKMedian.Preparation.BundleGeometry, OAI.MetricKMedian.Preparation.Physical, OAI.MetricKMedian.Preparation.farFactor, OAI.MetricKMedian.Preparation.nearFactor, OAI.MetricKMedian.Preparation.SupplierStars.Star, OAI.MetricKMedian.Preparation.SupplierStars.targets and OAI.MetricKMedian.Preparation.SupplierStars.weight (definitions bundle OAIQ035K010 of this split); OAI.MetricKMedian.FiniteLaw.joint (definitions bundle OAIQ035K016 of this split); OAI.MetricKMedian.Preparation.SupplierStars.flag (definitions bundle OAIQ035K024 of this split); OAI.MetricKMedian.Preparation.CoupledLaw (definitions bundle OAIQ035K025 of this split); OAI.MetricKMedian.Preparation.physicalOpen (definitions bundle OAIQ035K036 of this split).

Used by. The proof of OAI.MetricKMedian.Preparation.selected_preparation_outcome of this split imports it.

Preamble

import Mathlib
import Definitions.Def_OAIQ035K016
import Definitions.Def_OAIQ035K036

Formal statement

section

set_option linter.all false
set_option linter.unusedVariables false
set_option linter.unusedTactic false
set_option linter.unreachableTactic false

namespace OAI

section
section
namespace MetricKMedian.Preparation
open Finset SupplierStars
attribute [instance] CoupledLaw.finite
variable {I T X : Type} [Fintype I] [DecidableEq I] [Fintype T] [DecidableEq T]
  [PseudoMetricSpace X]

theorem client_assignments (F : T → Finset I) (y : I → ℝ) (s : T → X) (i : I → X)
    (V : T → ℝ) {M δ T₁ g γ B v : ℝ} {Δ : ℕ}
    (G : BundleGeometry F y s i V M δ)
    (L : CoupledLaw (targets G.A) flag (weight y G.P G.A G.c γ) G.P y G.p G.c g γ B Δ)
    (hy : ∀ a, 0 ≤ y a) (hM : 0 < M) (hδ : 0 < δ) (hδ1 : δ ≤ 1/4)
    (hT : 0 < T₁) (hθ : 1/(M*δ) ≤ 1/8) (hα : M/(δ*T₁) ≤ 1/4)
    (hg : 0 < g) (hγ : 0 ≤ γ) (hunit : g*(Δ:ℝ)=1)
    (j : X) (t : T) (Fj : Finset I) (hmj : ∑ a ∈ Fj, y a=1)
    (hms : ∑ a ∈ F t, y a=1) (hvj : ∑ a ∈ Fj, y a*dist j (i a)=v)
    (hnearest : ∀ a ∈ F t, ∀ b ∉ F t, dist (s t) (i a) ≤ dist (s t) (i b))
    (hV : V t ≤ v) (hD : dist j (s t) ≤ M*v) :
    let p₀ := 1-1/(M*δ)
    ∃ r : (L.Ω × (T → Finset I)) → Physical I T → ℝ,
      (∀ z, 0 < (L.ν.joint L.κ).weight z →
        (∀ a, 0 ≤ r z a ∧ r z a ≤ physicalOpen L z a) ∧ (∑ a, r z a)=1) ∧
      (L.ν.joint L.κ).expect (fun z => ∑ a, r z a*
        (Sum.elim (fun a => dist j (i a)) (fun ti => dist j (i ti.2)) a)) ≤
        max (farFactor δ p₀ (M/(δ*T₁)) (M/T₁) γ)
          (nearFactor p₀ (M+(1+δ)*T₁) γ g)*v := by
  sorry

end MetricKMedian.Preparation
end
end

end OAI
end

Source

OpenAI, The approximation threshold for metric k-median (result family 125), OpenAI Math Release, September 24, 2026, https://github.com/openai/math (result family 125; paper: https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/preprints/The-Approximation-Threshold-for-Metric-k-Median-September-24-2026/main.pdf; Apache License 2.0)

View graph