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

Open

OAI.MetricKMedian.RationalBatchData.proposal_count_tail

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); in Lean it is the declaration OAI.MetricKMedian.RationalBatchData.proposal_count_tail of lean/OAI/Combinatorics/KMedian/KMedian/Rounding/RationalProposalCount.lean at commit adc7f12, ported to Lean 4.33.1 and Mathlib 0df444a.

The statement, as published (namespace OAI.MetricKMedian.RationalBatchData, with open Finset FixedBatch PhysicalPotential):

theorem proposal_count_tail (A : Finset (CopyState.Copy (F := F) Δ)) (G : A → Finset A)
    (g β p φ : ℚ) (hp0 : 0 ≤ p) (hφ0 : 0 ≤ φ) (hupper : (1+φ)*p ≤ 1)
    (enum : Fin n ≃ HeavyAction (graph G) (heavySet (graphMass G g) β))
    (hg : 0 < (g:ℝ)) (hg1 : (g:ℝ) ≤ 1) (hp : 0 < (p:ℝ))
    (hφ : 0 < (φ:ℝ)) (hφ1 : (φ:ℝ) ≤ 1) (hβ : 0 < (β:ℝ))
    (hunit : (g:ℝ)*(Δ:ℝ)=1) (hG : ∀ i, (G i).card=Δ)
    (hsmall : 8*(p:ℝ)*(Δ:ℝ) ≤ (φ:ℝ)*(g:ℝ)) :
    (proposal G Δ g β p φ hp0 hφ0 hupper enum).real.prob
      (fun Z => mass (g:ℝ) A+4/((g:ℝ)*(β:ℝ)) <
        mass (g:ℝ) (transition A G (heavySet (graphMass G g) β) Z)) ≤
      96*(Δ:ℝ)^2*(β:ℝ)/((p:ℝ)*(φ:ℝ)^2*(g:ℝ))

Definitions. The statement is written with OAI.MetricKMedian.CopyState.Copy and OAI.MetricKMedian.PhysicalPotential.mass (definitions bundle OAIQ037K003 of this split); OAI.MetricKMedian.FixedBatch.HeavyAction, OAI.MetricKMedian.FixedBatch.instDecidableEqHeavyAction and OAI.MetricKMedian.FixedBatch.instFintypeHeavyAction (definitions bundle OAIQ037K004 of this split); OAI.MetricKMedian.RationalBatchData.heavySet (definitions bundle OAIQ037K005 of this split); OAI.MetricKMedian.FiniteLaw.prob (definitions bundle OAIQ037K016 of this split); OAI.MetricKMedian.RationalBatchData.graph and OAI.MetricKMedian.RationalBatchData.graphMass (definitions bundle OAIQ037K017 of this split); OAI.MetricKMedian.RationalBatchData.transition (definitions bundle OAIQ037K030 of this split); OAI.MetricKMedian.SparseIntegerLaw.real (definitions bundle OAIQ037K037 of this split); OAI.MetricKMedian.RationalBatchData.proposal (definitions bundle OAIQ037K044 of this split).

Used by. The proof of OAI.MetricKMedian.RationalPhysicalKernel.histories_count_tail of this split imports it.

Preamble

import Mathlib
import Definitions.Def_OAIQ037K044

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.RationalBatchData
open Finset FixedBatch PhysicalPotential
variable {F : Type} [DecidableEq F] {Δ n : ℕ}

theorem proposal_count_tail (A : Finset (CopyState.Copy (F := F) Δ)) (G : A → Finset A)
    (g β p φ : ℚ) (hp0 : 0 ≤ p) (hφ0 : 0 ≤ φ) (hupper : (1+φ)*p ≤ 1)
    (enum : Fin n ≃ HeavyAction (graph G) (heavySet (graphMass G g) β))
    (hg : 0 < (g:ℝ)) (hg1 : (g:ℝ) ≤ 1) (hp : 0 < (p:ℝ))
    (hφ : 0 < (φ:ℝ)) (hφ1 : (φ:ℝ) ≤ 1) (hβ : 0 < (β:ℝ))
    (hunit : (g:ℝ)*(Δ:ℝ)=1) (hG : ∀ i, (G i).card=Δ)
    (hsmall : 8*(p:ℝ)*(Δ:ℝ) ≤ (φ:ℝ)*(g:ℝ)) :
    (proposal G Δ g β p φ hp0 hφ0 hupper enum).real.prob
      (fun Z => mass (g:ℝ) A+4/((g:ℝ)*(β:ℝ)) <
        mass (g:ℝ) (transition A G (heavySet (graphMass G g) β) Z)) ≤
      96*(Δ:ℝ)^2*(β:ℝ)/((p:ℝ)*(φ:ℝ)^2*(g:ℝ)) := by
  sorry

end MetricKMedian.RationalBatchData
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); Lean: https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/lean/OAI/Combinatorics/KMedian/KMedian/Rounding/RationalProposalCount.lean (declaration OAI.MetricKMedian.RationalBatchData.proposal_count_tail)

View graph