Definitions bundle OAIQ037K078 of the split of OpenAI, The approximation threshold for metric k-median (result family 125)
DefinitionOAIQ037K078A definitions bundle of the split of OpenAI's proof of OAI.MetricKMedian.main_finite_work, carved from OpenAI's openai/math development (OpenAI, The approximation threshold for metric k-median (result family 125), OpenAI Math Release, September 24, 2026, result family 125, github.com/openai/math at commit adc7f12, Apache License 2.0) and ported to Lean 4.33.1 and Mathlib 0df444a. The declarations and their proofs are OpenAI's.
Contents. It holds 2 declarations of OpenAI's Lean: 2 theorems.
Sources. They come from these modules of lean/OAI/Combinatorics/KMedian, in whole or in part: KMedian_Programs_FinalSelectionProgram, KMedian_Reduction_LocalCompletionProgram.
Imports. It imports the published bundle Def_MetricKMedian; the bundles OAIQ037K075 and OAIQ037K076 of this split.
Imported by (directly, in this split): the bundle OAIQ037K079.
import Mathlib
import Definitions.Def_MetricKMedian
import Definitions.Def_OAIQ037K075
import Definitions.Def_OAIQ037K076
section
-- module Solutions.OAIQ037_KM.KMedian_Programs_FinalSelectionProgram
set_option linter.all false
set_option linter.unusedVariables false
set_option linter.unusedTactic false
set_option linter.unreachableTactic false
namespace OAI
section
namespace MetricKMedian.Reduction.Program
open Finset Preparation Binary Binary.PolyProgram Binary.Automatic Binary.Automatic.Poly
open SparseGraph.ListOperation (Row Table setView)
open InstanceProgram (Raw view)
open Completion.Rational.BestProgram (card card_view)
theorem selectData_view (I : Instance) (L : List (Finset (Fin I.n))) :
selectData (view I,L.map setView)=setView (selectList I L) := by
unfold selectData
rw [selectRaw_view]
simp only [InstanceProgram.fallbackData,InstanceProgram.singletonData_view,selectList]
cases SparseSelect.best (feasible I) (rationalCost I) L <;> rfl
end MetricKMedian.Reduction.Program
end
end OAI
end
section
-- module Solutions.OAIQ037_KM.KMedian_Reduction_LocalCompletionProgram
set_option linter.all false
set_option linter.unusedVariables false
set_option linter.unusedTactic false
set_option linter.unreachableTactic false
namespace OAI
section
namespace MetricKMedian.Reduction.Program
open Finset Binary Binary.PolyProgram Binary.Automatic Binary.Automatic.Poly
open SparseGraph.ListOperation (Row Table setView indices)
open InstanceProgram (Raw view)
open MetricKMedian.MaskProgram
open Preparation.RationalNearest.MaskProgram (erase erase_view insert insert_view)
open Enumeration
theorem getDist_view (I : Instance) (i j : Fin I.n) : getDist (view I,(i.val,j.val))=I.distance i j := by
simp only [getDist,view,List.getElem?_ofFn,dite_eq_left (Fin.isLt _),Option.getD_some,Fin.eta]
end MetricKMedian.Reduction.Program
end
end OAI
end