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

Open

OAI.MetricKMedian.Preparation.nearby_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 nearby_assignments (F : T → Finset I) (y : I → ℝ) (s : T → X) (i : I → X)
    (V : T → ℝ) {M δ g γ B T₁ v p₀ : ℝ} {Δ : ℕ}
    (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 ≤ δ) (hT₁ : 0 ≤ T₁)
    (hg : 0 ≤ g) (hγ : 0 ≤ γ) (hunit : g*(Δ:ℝ)=1)
    (hp₀ : 0 < p₀) (hp₀1 : p₀ ≤ 1) (hp : ∀ t, p₀ ≤ G.p t)
    (j : X) (t : T) (Fj : Finset I) (hmj : ∑ a ∈ Fj, y a=1)
    (hvj : ∑ a ∈ Fj, y a*dist j (i a)=v)
    (hD : dist j (s t) ≤ M*v) (hL : 0 < G.c t → G.L t ≤ T₁*v)
    (hR : G.c t=0 → ∀ a ∈ F t, dist (s t) (i a) ≤ T₁*v) :
    ∃ 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)) ≤
        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.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.client_assignments 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 nearby_assignments (F : T → Finset I) (y : I → ℝ) (s : T → X) (i : I → X)
    (V : T → ℝ) {M δ g γ B T₁ v p₀ : ℝ} {Δ : ℕ}
    (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 ≤ δ) (hT₁ : 0 ≤ T₁)
    (hg : 0 ≤ g) (hγ : 0 ≤ γ) (hunit : g*(Δ:ℝ)=1)
    (hp₀ : 0 < p₀) (hp₀1 : p₀ ≤ 1) (hp : ∀ t, p₀ ≤ G.p t)
    (j : X) (t : T) (Fj : Finset I) (hmj : ∑ a ∈ Fj, y a=1)
    (hvj : ∑ a ∈ Fj, y a*dist j (i a)=v)
    (hD : dist j (s t) ≤ M*v) (hL : 0 < G.c t → G.L t ≤ T₁*v)
    (hR : G.c t=0 → ∀ a ∈ F t, dist (s t) (i a) ≤ T₁*v) :
    ∃ 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)) ≤
        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