Definitions bundle OAIQ037K050 of the split of OpenAI, The approximation threshold for metric k-median (result family 125)

import Mathlib
import Definitions.Def_OAIQ037K043
import Definitions.Def_OAIQ037K044
import Definitions.Def_OAIQ037K045
import Definitions.Def_OAIQ037K046

section
-- module Solutions.OAIQ037_KM.KMedian_Compression_GaussianListCompiler
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.Gaussian.ListOperation
open Binary Binary.PolyProgram Function

noncomputable def pivotProgram : PolyProgram er Nat.bits pivot :=
  (ratNonzero.listFindIdx 0).congr _ (fun _ => rfl)

noncomputable def basisProgram : PolyProgram eslots er basis := by
  let tl := listTail eu ()
  let zero : PolyProgram eu Ratio.encode (fun _ : Unit => (0:ℚ)) := constant eu Ratio.encode 0
  let zeros := tl.comp (zero.listMap ())
  let nonnil := (((constant eslots Ratio.encode 1).fanout zeros).comp (listCons Ratio.encode))
  exact (ite (listIsEmpty eu) nonnil (constant eslots er [])).congr _ (fun _ => rfl)
end MetricKMedian.Gaussian.ListOperation
end

end OAI
end

section
-- module Solutions.OAIQ037_KM.KMedian_Compression_IntegerKernelProgram
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.Gaussian.IntegerProgram
open Binary Binary.PolyProgram

noncomputable def rationalProgram : PolyProgram Input.encode ListOperation.Input.encode Input.rational := by
  let cast := (ratOfInt.listMap 0).listMap []
  let raw := (cast.second ListOperation.eslots)
  exact raw.recode Input.raw (fun _ => rfl) (fun I => by
    change ListOperation.edata (List.replicate I.n (),castRows (List.ofFn (fun i => List.ofFn (I.V i)))) = _
    rw [castRows_ofFn]
    simp only [ListOperation.Input.encode,ListOperation.Input.raw,Input.rational,values_tabulate])

end MetricKMedian.Gaussian.IntegerProgram
end

end OAI
end

section
-- module Solutions.OAIQ037_KM.KMedian_Compression_AffineListCompiler
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.IntegerLaw.ListOperation
open Binary Binary.PolyProgram Function

noncomputable def entriesProgram : PolyProgram ed ees entries := by
  let zz := encodePair Signed.encode er
  let zip := (snd es (encodePair er em)).comp (listZip Signed.encode er 0 [])
  exact (zip.comp (((listIndices zz (0,[])).fanout (identity (encodeList zz))).comp (listZip Nat.bits zz 0 (0,[])))).congr _ (fun _ => rfl)

end MetricKMedian.IntegerLaw.ListOperation
end

end OAI
end

section
-- module Solutions.OAIQ037_KM.KMedian_Optimization_SimplexListProgram
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.LPBinary
open Finset

namespace Program
open Binary Binary.PolyProgram
noncomputable def upperProgram : PolyProgram (encodePair Ratio.encode er) er (fun x : ℚ × Row => upper x.2 x.1) :=
  (listFilterWith ratLE 0 0).congr _ (fun _ => rfl)
noncomputable def positivePart : PolyProgram Ratio.encode Ratio.encode (fun q => max 0 q) :=
  (((constant Ratio.encode Ratio.encode 0).fanout (identity Ratio.encode)).comp ratMax).congr _ (fun _ => rfl)
end Program
end MetricKMedian.LPBinary
end

end OAI
end

section
-- module Solutions.OAIQ037_KM.KMedian_Optimization_TruncatedListCompiler
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.LPBinary.Program
open Binary Binary.PolyProgram Function

noncomputable def truncateRowProgram : PolyProgram (encodePair Ratio.encode er) er (fun x : ℚ × Row => Truncated.row x.2 x.1) := by
  let t := snd Ratio.encode Ratio.encode
  let test := (t.fanout (constant (encodePair Ratio.encode Ratio.encode) Ratio.encode 1)).comp ratLE
  let coord := ite test (fst Ratio.encode Ratio.encode) t
  exact (coord.listMapWith 0 0).congr _ (fun x => by simp only [Function.comp_apply,decide_eq_true_eq,Truncated.row])

noncomputable def truncateMatrixProgram : PolyProgram (encodePair ers Ratio.encode) ers (fun x : Rows × ℚ => Truncated.matrix x.1 x.2) :=
  ((exchange ers Ratio.encode).comp (truncateRowProgram.listMapWith [] [])).congr _ (fun _ => rfl)

end MetricKMedian.LPBinary.Program
end

end OAI
end

section
-- module Solutions.OAIQ037_KM.KMedian_Optimization_LPBinaryStart
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.LPBinary
open Binary Binary.PolyProgram Function

namespace Program
noncomputable def rawGradProgram (r : ℕ) : PolyProgram ei Nat.bits (rawGrad r) := by
  let ds := fst ers Nat.bits
  let n := (ds.comp (listHead er [])).comp (listLength Ratio.encode 0)
  let m := ds.comp (listLength er [])
  let mh := (m.fanout (rawPenaltyProgram r)).comp natMul
  exact ((n.fanout ((mh.fanout mh).comp natMul)).comp natMul).congr _ (fun x => by dsimp only [Function.comp_apply,rawGrad]; rw [pow_two])
noncomputable def rawRateProgram (r : ℕ) : PolyProgram ei Ratio.encode (rawRate r) := by
  let grad := (rawGradProgram r).comp ratOfNat
  let den := ((constant ei Ratio.encode (2*(r:ℚ))).fanout grad).comp ratMul
  exact (den.comp ratInv).congr _ (fun x => by simp only [Function.comp_apply,rawRate,one_div])
noncomputable def rawStepsProgram (r : ℕ) : PolyProgram ei Nat.bits (rawSteps r) := by
  let k := snd ers Nat.bits
  let kk := (k.fanout k).comp natMul
  let g := ((constant ei Nat.bits (8*r^2)).fanout (rawGradProgram r)).comp natMul
  exact ((g.fanout kk).comp natMul).congr _ (fun _ => by dsimp only [Function.comp_apply,rawSteps]; simp only [pow_two])
noncomputable def rawContextProgram (r : ℕ) : PolyProgram ei ec (rawContext r) :=
  ((fst ers Nat.bits).fanout (((rawPenaltyProgram r).comp ratOfNat).fanout (((snd ers Nat.bits).comp ratOfNat).fanout (rawRateProgram r)))).congr _ (fun _ => rfl)
noncomputable def rawInitialProgram : PolyProgram ei er rawInitial := by
  let ids := ((fst ers Nat.bits).comp (listHead er [])).comp (listIndices Ratio.encode 0)
  let k := (snd ers Nat.bits).comp ratOfNat
  let test := (snd Ratio.encode Nat.bits).comp natZero
  let coord := ite test (constant (encodePair Ratio.encode Nat.bits) Ratio.encode 0) (fst Ratio.encode Nat.bits)
  exact ((k.fanout ids).comp (coord.listMapWith 0 0)).congr _ (fun x => by simp only [Function.comp_apply,rawInitial,decide_eq_true_eq])
noncomputable def startProgram (r : ℕ) : PolyProgram Input.encode es (start r) :=
  (inputRaw.comp ((rawContextProgram r).fanout rawInitialProgram)).congr _ (fun _ => rfl)
noncomputable def stepsProgram (r : ℕ) : PolyProgram Input.encode Nat.bits (fun I => rawSteps r I.raw) :=
  (inputRaw.comp (rawStepsProgram r)).congr _ (fun _ => rfl)
end Program

end MetricKMedian.LPBinary
end

end OAI
end

section
-- module Solutions.OAIQ037_KM.KMedian_Optimization_LPBinaryTrajectory
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.LPBinary
open Binary Binary.PolyProgram Polynomial Function

noncomputable def statePolynomial (r : ℕ) : Polynomial ℕ :=
  2*(Program.startProgram r).sizeBound+1+X*(2*(3*heightPolynomial r+10)+1)

 theorem state_size (r : ℕ) (hr : 0 < r) (I : Input) (t : ℕ) (ht : t ≤ rawSteps r I.raw) :
    (es (update^[t] (start r I))).length ≤ (statePolynomial r).eval I.encode.length := by
  rw [update_iterate]
  have hc : (ec (rawContext r I.raw)).length ≤ (Program.startProgram r).sizeBound.eval I.encode.length := by
    have hh := (Program.startProgram r).length_bound I
    change (encodePair ec er (rawContext r I.raw,rawInitial I.raw)).length ≤ (Program.startProgram r).sizeBound.eval I.encode.length at hh
    rw [encodePair_length] at hh
    dsimp only at hh
    omega
  have hy := iterate_size I r hr t (by rwa [rawSteps_eq] at ht)
  change (encodePair ec er (rawContext r I.raw,I.iterate r t)).length ≤ _
  rw [encodePair_length]
  dsimp only
  simp only [statePolynomial,eval_add,eval_mul,eval_ofNat,eval_X,eval_one,heightPolynomial_eval]
  omega

end MetricKMedian.LPBinary
end

end OAI
end

section
-- module Solutions.OAIQ037_KM.KMedian_Programs_NearestListProgram
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.LPBinary
open Binary Binary.PolyProgram Function Finset

namespace Nearest

noncomputable def entriesProgram : PolyProgram (encodePair er er) ees (fun x : Row × Row => entries x.1 x.2) := by
  let ez := encodePair Ratio.encode Ratio.encode
  let zip := listZip Ratio.encode Ratio.encode 0 0
  let ids := listIndices ez (0,0)
  exact (zip.comp ((ids.fanout (identity (encodeList ez))).comp (listZip Nat.bits ez 0 (0,0)))).congr _ (fun _ => rfl)
noncomputable def beforeProgram : PolyProgram (encodePair ee ee) encodeBool (fun x : Entry × Entry => before x.1 x.2) := by
  let a := fst ee ee
  let b := snd ee ee
  let idx := fst Nat.bits (encodePair Ratio.encode Ratio.encode)
  let dist := (snd Nat.bits (encodePair Ratio.encode Ratio.encode)).comp (snd Ratio.encode Ratio.encode)
  let dst := (a.comp dist).fanout (b.comp dist)
  let ilt := ((a.comp idx).fanout (b.comp idx)).comp natLT
  exact (((dst.comp ratLT).fanout (((dst.comp ratEQ).fanout ilt).comp boolAnd)).comp boolOr).congr _ (fun _ => by simp only [Function.comp_apply,before,Bool.decide_or,Bool.decide_and])
end Nearest
end MetricKMedian.LPBinary
end

end OAI
end

section
-- module Solutions.OAIQ037_KM.KMedian_Optimization_ApproximationListProgram
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.LPBinary
open Binary Binary.PolyProgram Function Finset
namespace Repair

noncomputable def openingProgram : PolyProgram (encodePair er Ratio.encode) er (fun x : Row × ℚ => opening x.1 x.2) := by
  let y := snd Ratio.encode Ratio.encode
  let den := ((constant (encodePair Ratio.encode Ratio.encode) Ratio.encode 1).fanout (fst Ratio.encode Ratio.encode)).comp ratSub
  let val := (y.fanout den).comp ratDiv
  let coord := ((constant (encodePair Ratio.encode Ratio.encode) Ratio.encode 1).fanout val).comp Program.ratMin
  exact ((exchange er Ratio.encode).comp (coord.listMapWith 0 0)).congr _ (fun _ => rfl)
noncomputable def weightsProgram : PolyProgram (encodePair er er) er (fun x : Row × Row => weights x.1 x.2) := by
  let test := ((fst Ratio.encode Ratio.encode).fanout (constant (encodePair Ratio.encode Ratio.encode) Ratio.encode 1)).comp ratLE
  let coord := ite test (constant (encodePair Ratio.encode Ratio.encode) Ratio.encode 0) (snd Ratio.encode Ratio.encode)
  exact ((listZip Ratio.encode Ratio.encode 0 0).comp (coord.listMap (0,0))).congr _ (fun _ => by simp only [Function.comp_apply,weights,decide_eq_true_eq])
noncomputable def lossProgram (r : ℕ) : PolyProgram ei Ratio.encode (fun x : Rows × ℕ => TruncatedLP.loss r x.2) :=
  (((constant ei Ratio.encode (1+1/(r:ℚ))).fanout ((Program.rawPenaltyProgram r).comp ratOfNat)).comp ratDiv).congr _ (fun _ => rfl)
end Repair
end MetricKMedian.LPBinary
end

end OAI
end

section
-- module Solutions.OAIQ037_KM.KMedian_Optimization_FractionalListChecks
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.LPBinary.Repair
open Binary Binary.PolyProgram Function Finset

noncomputable def boundedProgram : PolyProgram Ratio.encode encodeBool bounded := by
  let lo := ((constant Ratio.encode Ratio.encode 0).fanout (identity Ratio.encode)).comp ratLE
  let hi := ((identity Ratio.encode).fanout (constant Ratio.encode Ratio.encode 1)).comp ratLE
  exact ((lo.fanout hi).comp boolAnd).congr _ (fun q => by simp only [Function.comp_apply,id_eq,bounded,Bool.decide_and])
noncomputable def dominatedProgram : PolyProgram (encodePair er er) encodeBool (fun x : Row × Row => dominated x.1 x.2) := by
  let lo := ((constant (encodePair Ratio.encode Ratio.encode) Ratio.encode 0).fanout (fst Ratio.encode Ratio.encode)).comp ratLE
  let test := (lo.fanout ratLE).comp boolAnd
  exact ((listZip Ratio.encode Ratio.encode 0 0).comp (test.listAll (0,0))).congr _ (fun _ => by simp only [Function.comp_def,dominated,Bool.decide_and])
end MetricKMedian.LPBinary.Repair
end

end OAI
end

section
-- module Solutions.OAIQ037_KM.KMedian_Programs_ScaleListProgram
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.LPBinary
open Binary Binary.PolyProgram Function Finset
namespace Input

noncomputable def scaleProgram : PolyProgram (encodePair Input.encode Ratio.encode) Input.encode (fun x : Input × ℚ => x.1.scale x.2) := by
  let coord := (exchange Ratio.encode Ratio.encode).comp ratDiv
  let matrix := (coord.listMapWith 0 0).listMapWith [] []
  let I := fst Input.encode Ratio.encode
  let B := snd Input.encode Ratio.encode
  let ds := I.comp (Program.inputRaw.comp (fst ers Nat.bits))
  let k := I.comp (Program.inputRaw.comp (snd ers Nat.bits))
  let raw := ((B.fanout ds).comp matrix).fanout k
  exact raw.recode id (fun _ => rfl) (fun x => by
    dsimp only [Function.comp_apply,id_eq]
    change ei ((x.1.rows.map (fun ds => ds.map (fun d => d/x.2))),x.1.k)=ei ((x.1.scale x.2).raw)
    rw [Input.raw,scale_rows]
    rfl)
end Input
end MetricKMedian.LPBinary
end

end OAI
end

section
-- module Solutions.OAIQ037_KM.KMedian_Optimization_FractionalSelectProgram
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.LPBinary
open Binary Binary.PolyProgram Function Finset
namespace Input
noncomputable def zeroOutputProgram : PolyProgram Input.encode Repair.eo Input.zeroOutput := by
  let rows := Program.inputRaw.comp (fst ers Nat.bits)
  let rowZero := (constant Ratio.encode Ratio.encode 0).listMap 0
  let mat := rows.comp (rowZero.listMap [])
  let row := (rows.comp (listHead er [])).comp rowZero
  exact (row.fanout mat).congr _ (fun I => by
    change (((I.rows.head?.getD []).map (fun _ => (0:ℚ))),I.rows.map (fun ds => ds.map (fun _ => (0:ℚ))))=I.zeroOutput
    have hi : I.rows.head?.getD []=List.ofFn (I.distance ⟨0,I.mpos⟩) := by
      dsimp only [Input.rows]
      rw [List.head?_eq_getElem?]
      simp only [List.getElem?_ofFn, I.mpos, dite_eq_left, Option.getD_some]
    rw [hi]
    simp only [Input.rows,List.map_ofFn,Function.comp_def,Input.zeroOutput,List.ofFn_const])
end Input
namespace Scale

theorem feasible_mem (r : ℕ) (hr : 0 < r) (I : Input) (hd : ∀ j i, 0 ≤ I.distance j i) (B : ℚ) :
    B ∈ feasible r I ↔ B ∈ TruncatedLP.feasibleScales I.distance r I.k hr I.kpos hd := by
  simp only [feasible,List.mem_filter,Input.rows,guesses_mem,candidate_eq r hr I hd,
    Repair.valid_encodeData,decide_eq_true_eq,TruncatedLP.feasibleScales,mem_filter]

theorem selected_eq (r : ℕ) (hr : 0 < r) (I : Input) (hd : ∀ j i, 0 ≤ I.distance j i) :
    selected r I=Repair.encodeData (TruncatedLP.selectFractional I.distance r I.k hr I.kpos hd) := by
  have hm (B : ℚ) : Repair.value (candidate r I B) I.rows=(TruncatedLP.scaledCandidate I.distance r I.k hr I.kpos hd B).value I.distance := by
    rw [candidate_eq r hr I hd,Input.rows,Repair.value_encodeData]
  unfold selected selectedScale
  simp only [hm]
  rw [argmin_eq _ _ _ (feasible_mem r hr I hd),candidate_eq r hr I hd]
  rfl

end Scale
end MetricKMedian.LPBinary
end

end OAI
end

section
-- module Solutions.OAIQ037_KM.KMedian_Programs_PivotListProgram
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.IntegerLaw.ListPivot
open Binary Binary.PolyProgram Function Finset

noncomputable def ratioProgram : PolyProgram ee Ratio.encode ratio :=
  ((((fst Signed.encode Signed.encode).comp ratOfInt).fanout ((snd Signed.encode Signed.encode).comp ratOfInt)).comp ratDiv).congr _ (fun _ => rfl)
noncomputable def positiveProgram : PolyProgram ee encodeBool (fun e : Entry => decide (0<e.2)) :=
  (((constant ee Signed.encode 0).fanout (snd Signed.encode Signed.encode)).comp intLT).congr _ (fun _ => rfl)

end MetricKMedian.IntegerLaw.ListPivot
end

end OAI
end

section
-- module Solutions.OAIQ037_KM.KMedian_Programs_DependentSparseProgram
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.SparseIntegerLaw.DependentProgram
open Binary Binary.PolyProgram Function BinarySparse
variable {C A : Type} (T : C → Type)

variable {T} (ec : C → List Bool) (ea : A → List Bool) (view : ∀ c, T c → A)

def Bundle.compress (d : C → ℕ) (v : ∀ c, T c → Fin (d c) → ℚ) (x : Bundle T) : Bundle T :=
  ⟨x.ctx,x.law.compressAuto (v x.ctx)⟩

noncomputable def contextProgram : PolyProgram (Bundle.encode ec ea view) ec (fun x : Bundle T => x.ctx) :=
  (fst ec (ed ea)).recode (Bundle.raw view) (fun _ => rfl) (fun _ => rfl)
noncomputable def statesProgram : PolyProgram (Bundle.encode ec ea view) (encodeList ea)
    (fun x : Bundle T => x.law.states.toList.map (view x.ctx)) :=
  ((snd ec (ed ea)).comp (snd el (encodeList ea))).recode (Bundle.raw view) (fun _ => rfl) (fun _ => rfl)
noncomputable def lawProgram : PolyProgram (Bundle.encode ec ea view) el
    (fun x : Bundle T => (x.law.law.denominator,List.ofFn x.law.law.numerator)) :=
  ((snd ec (ed ea)).comp (fst el (encodeList ea))).recode (Bundle.raw view) (fun _ => rfl) (fun _ => rfl)

end MetricKMedian.SparseIntegerLaw.DependentProgram
end

end OAI
end

section
-- module Solutions.OAIQ037_KM.KMedian_Probability_BernoulliStepProgram
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.SparseBernoulli.Program
open Binary Binary.PolyProgram Function
open SparseIntegerLaw.DependentProgram
def State.step (d : ℕ) (x : State) : State :=
  State.increment (if x.ctx.t<x.ctx.input.n then
    Bundle.compress (fun c : Context => (c.input.n+1)^d) (fun _ => features (d:=d))
      (Bundle.branch probability probability_unit endpoint x)
    else x)

end MetricKMedian.SparseBernoulli.Program
end

end OAI
end

section
-- module Solutions.OAIQ037_KM.KMedian_Probability_BernoulliRunProgram
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.SparseBernoulli.Program
open Binary Binary.PolyProgram Function Polynomial
open SparseIntegerLaw.DependentProgram
open SparseIntegerLaw.BinarySparse (el ed)

def Input.state (x : Input) (d t : ℕ) : State := ⟨⟨x,t⟩,run (d:=d) x.p x.feasible t⟩

 theorem state_next (x : Input) (d t : ℕ) : State.step d (x.state d t)=x.state d (t+1) := by
  have hp (ht : t<x.n) : probability ⟨x,t⟩=(fun _ => x.p ⟨t,ht⟩) := by
    funext q; simp only [probability,dite_eq_left ht]
  have he (ht : t<x.n) : endpoint ⟨x,t⟩=(fun q b => SparseBernoulli.endpoint q ⟨t,ht⟩ b) := by
    funext q b i
    simp only [endpoint,SparseBernoulli.endpoint,Fin.ext_iff]
  unfold State.step Input.state
  by_cases ht : t<x.n
  · rw [ite_eq_left ht]
    change (⟨⟨x,t+1⟩, ((run (d:=d) x.p x.feasible t).branch
      (probability ⟨x,t⟩) (probability_unit ⟨x,t⟩) (endpoint ⟨x,t⟩)).compressAuto features⟩ : State)=_
    rw [run,dite_eq_left ht]
    apply congrArg (fun μ => (⟨⟨x,t+1⟩,μ⟩ : State))
    simp only [SparseIntegerLaw.step,hp ht,he ht]
  · rw [ite_eq_right ht,run,dite_eq_right ht]
    rfl

 theorem state_iterate (x : Input) (d t : ℕ) : (State.step d)^[t] x.start=x.state d t := by
  induction t with
  | zero => rfl
  | succ t ih => rw [Function.iterate_succ_apply',ih,state_next]

noncomputable def countProgram : PolyProgram Input.encode Nat.bits Input.n :=
  (listLength Ratio.encode 0).recode (fun x => List.ofFn x.p) (fun _ => rfl) (fun x => by simp only [List.length_ofFn])

end MetricKMedian.SparseBernoulli.Program
end

end OAI
end

section
-- module Solutions.OAIQ037_KM.KMedian_Process_CountStepProgram
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.SparseCounts.Program
open Binary Binary.PolyProgram Function
open SparseIntegerLaw.DependentProgram SparseIntegerLaw.BinarySparse
open ListOperation (Row Table er et)
abbrev T (c : Context) := SparseCounts.Table c.input.n c.input.m
abbrev State := Bundle T

def column (c : Context) : SparseIntegerLaw (Fin c.input.n → ℕ) :=
  if h : c.t < c.input.m then c.input.columns ⟨c.t,h⟩ else .dirac (fun _ => 0)
def update (c : Context) (G : T c) (S : (Fin c.input.n → ℕ)) : T c :=
  fun i => if i.val=c.t then S else G i

def State.product (x : State) : State := ⟨x.ctx,x.law.prod (column x.ctx) (update x.ctx)⟩

def State.increment (x : State) : State := ⟨⟨x.ctx.input,x.ctx.t+1⟩,x.law⟩
def State.step (x : State) : State :=
  State.increment (if x.ctx.t<x.ctx.input.m then
    Bundle.compress (fun c : Context => c.input.n*c.input.m+(c.input.n*c.input.m)*(c.input.n*c.input.m))
      (fun _ => features) x.product else x)

end MetricKMedian.SparseCounts.Program
end

end OAI
end

section
-- module Solutions.OAIQ037_KM.KMedian_Process_CountRunProgram
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.SparseCounts.Program
open Binary Binary.PolyProgram Function Polynomial
open SparseIntegerLaw.DependentProgram SparseIntegerLaw.BinarySparse
open ListOperation (Row Table et)
def Input.start (x : Input) : State := ⟨⟨x,0⟩,.dirac (fun _ _ => 0)⟩

end MetricKMedian.SparseCounts.Program
end

end OAI
end

section
-- module Solutions.OAIQ037_KM.KMedian_Sparse_SparseBind
set_option linter.all false
set_option linter.unusedVariables false
set_option linter.unusedTactic false
set_option linter.unreachableTactic false

namespace OAI

namespace MetricKMedian.SparseIntegerLaw
open Finset
variable {α β : Type}

def bindCompress {d : ℕ} (μ : SparseIntegerLaw α) (κ : Fin μ.length → SparseIntegerLaw β)
    (v : β → Fin d → ℚ) : SparseIntegerLaw β :=
  (μ.bindIndexed κ).compressAuto v

end MetricKMedian.SparseIntegerLaw

end OAI
end

section
-- module Solutions.OAIQ037_KM.KMedian_Process_PhysicalBatchProgram
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.SparsePhysicalBatch.Program
open Binary Binary.PolyProgram Function
open SparseIntegerLaw.BinarySparse SparseIntegerLaw.DependentProgram
open SparseGraph.ListOperation (Row Table et)
def Input.bern (bal : Bool) (x : Input) : SparseIntegerLaw (Fin x.n → Bool) :=
  SparseBernoulli.run (d:=4) (x.bernInput bal).p (x.bernInput bal).feasible x.n
def Input.part (bal : Bool) (x : Input) : SparseIntegerLaw (Finset (Fin x.n)) :=
  (x.bern bal).map (fun ω => if bal then balanced x.Z x.C ω else unbalanced x.Z ω)
end MetricKMedian.SparsePhysicalBatch.Program
end

end OAI
end

section
-- module Solutions.OAIQ037_KM.KMedian_Sparse_SparseSupport
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.SparseIntegerLaw
open Finset
variable {α : Type}

theorem compressAuto_positive {d : ℕ} (μ : SparseIntegerLaw α) (v : α → Fin d → ℚ)
    (a : Fin (μ.compressAuto v).length) : 0 < (μ.compressAuto v).law.rational.weight a := by
  exact (⟨μ.length,μ.states,μ.law.compressAuto (fun i => v μ.states[i.val])⟩ :
    SparseIntegerLaw α).trim_positive a

end MetricKMedian.SparseIntegerLaw
end
end

end OAI
end

section
-- module Solutions.OAIQ037_KM.KMedian_Programs_GraphStepProgram
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.SparseGraph.Program
open Binary Binary.PolyProgram Function
open SparseIntegerLaw.DependentProgram SparseIntegerLaw.BinarySparse
open ListOperation (Row Table er et)
def State.step (x : State) : State :=
  State.increment (if x.ctx.t<x.ctx.input.m then
    Bundle.compress (fun c : Context => c.input.n*c.input.m+(c.input.n*c.input.m)*(c.input.n*c.input.m))
      (fun _ => features) x.product else x)

end MetricKMedian.SparseGraph.Program
end

end OAI
end

section
-- module Solutions.OAIQ037_KM.KMedian_Sparse_SparseCardinalFixed
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.SparseWeightedPartial
open RationalWeightedStep

theorem run_positive {n : ℕ} (β : Fin n → ℚ) (hβ : ∀ i, 0 < β i)
    (p : Vector ℚ n) (t : ℕ) (a : Fin (run β hβ p t).length) :
    0 < (run β hβ p t).law.rational.weight a := by
  cases t with
  | zero => change 0 < ((1:ℤ):ℚ)/1; norm_num
  | succ t =>
    exact ((run β hβ p t).branch (probability β) (probability_unit β hβ)
      (endpoint β)).compressAuto_positive features a

end MetricKMedian.SparseWeightedPartial

end
end

end OAI
end

section
-- module Solutions.OAIQ037_KM.KMedian_Sparse_SparseGridRounding
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.SparseGridRounding
open Finset
open RationalWeightedStep (point)
variable {n : ℕ}

def law (q : Fin n → ℚ) : SparseIntegerLaw (Fin n → ℕ) :=
  (SparseCardinalRounding.round (fraction q)).map (count q)

end MetricKMedian.SparseGridRounding
end
end

end OAI
end

section
-- module Solutions.OAIQ037_KM.KMedian_Programs_BundlesProgram
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.SparseBundles.Program
open Binary Binary.PolyProgram Function SparseIntegerLaw.BinarySparse
open SparseIntegerLaw.DependentProgram SparseCounts.Program
def QInput.input (x : QInput) : Input := ⟨x.n,x.m,(fun j => SparseGridRounding.law (fun i => x.q i j))⟩
end MetricKMedian.SparseBundles.Program
end

end OAI
end

section
-- module Solutions.OAIQ037_KM.KMedian_Sparse_SparseWeightedRounding
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.SparseWeightedRounding
open Finset RationalWeightedStep SparseWeightedPartial
variable {n : ℕ}

def round (β : Fin n → ℚ) (hβ : ∀ i, 0 < β i) (p : Vector ℚ n) :
    SparseIntegerLaw (Vector ℚ n) :=
  (run β hβ p n).step features RationalLastFraction.probability
    RationalLastFraction.probability_unit RationalLastFraction.endpoint

end MetricKMedian.SparseWeightedRounding
end
end

end OAI
end

section
-- module Solutions.OAIQ037_KM.KMedian_Programs_LastFractionProgram
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.RoundingProgram.WeightedRound
open Binary Binary.PolyProgram Binary.Automatic Binary.Automatic.Poly SparseIntegerLaw.BinarySparse

def result (x : Input false) : RoundingProgram.State false :=
  ⟨x.n,x.β,x.positive,SparseWeightedRounding.round x.β (x.positive rfl) x.p⟩
end MetricKMedian.RoundingProgram.WeightedRound
end

end OAI
end

section
-- module Solutions.OAIQ037_KM.KMedian_Sparse_SparseTargetSubset
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.SparseTargetSubset
open Finset RationalWeightedStep
variable {n : ℕ}

def vectors (D : Finset (Fin n)) (q : ℚ) : SparseIntegerLaw (Vector ℚ n) :=
  SparseWeightedRounding.round (fun _ => 1) (fun _ => by norm_num) (initial D q)

def law (D : Finset (Fin n)) (q : ℚ) : SparseIntegerLaw (Finset (Fin n)) :=
  (vectors D q).map SparseCardinalRounding.selected

theorem positive (D : Finset (Fin n)) (q : ℚ) (a : Fin (law D q).length) :
    0 < (law D q).law.rational.weight a := by
  exact ((SparseWeightedPartial.run (fun _ => 1) (fun _ => by norm_num) (initial D q) n).branch
    RationalLastFraction.probability RationalLastFraction.probability_unit
    RationalLastFraction.endpoint).compressAuto_positive SparseWeightedPartial.features a

end MetricKMedian.SparseTargetSubset
end
end

end OAI
end

section
-- module Solutions.OAIQ037_KM.KMedian_Programs_StarActivationProgram
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.SparseStarActivation.Program
open Binary Binary.PolyProgram Binary.Automatic Binary.Automatic.Poly SparseIntegerLaw.BinarySparse
open SparseGraph.ListOperation (Row Table setView indices)
def Input.graph (x : Input) : SparseGraph.Program.Input :=
  ⟨x.n,x.m,fun e => SparseTargetSubset.law (x.D e) (x.q e)⟩
end MetricKMedian.SparseStarActivation.Program
end

end OAI
end

section
-- module Solutions.OAIQ037_KM.KMedian_Sparse_SparseBernoulliSupport
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.SparseBernoulli
open Finset
variable {n d : ℕ}

theorem run_positive (p : Fin n → ℚ) (hp : ∀ i, 0 ≤ p i ∧ p i ≤ 1)
    (t : ℕ) (a : Fin (run (d := d) p hp t).length) :
    0 < (run (d := d) p hp t).law.rational.weight a := by
  induction t with
  | zero =>
    change 0 < (SparseIntegerLaw.dirac (fun _ : Fin n => false)).law.rational.weight a
    change (0:ℚ) < 1/1
    norm_num
  | succ t ih =>
    let inv : SparseIntegerLaw (Fin n → Bool) → Prop := fun μ =>
      ∀ a : Fin μ.length, 0 < μ.law.rational.weight a
    suffices hs : inv (run (d := d) p hp (t+1)) from hs a
    rw [run]
    split_ifs with ht
    · exact ((run (d := d) p hp t).branch (fun _ => p ⟨t,ht⟩)
        (fun _ => hp ⟨t,ht⟩) (fun q b => endpoint q ⟨t,ht⟩ b)).compressAuto_positive _
    · exact ih

end MetricKMedian.SparseBernoulli
end
end

end OAI
end

section
-- module Solutions.OAIQ037_KM.KMedian_Rounding_RationalSignedTerminal
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.RationalSignedTerminal
open Finset RationalWeightedStep RationalSignedStep
variable {n : ℕ}

def terminal (u : Fin n → ℚ) (p : Vector ℚ n)
    (hp : ∀ i, 0 ≤ point p i ∧ point p i ≤ 1) : SparseIntegerLaw (Vector ℚ n) :=
  (SparseBernoulli.run (d := 2) (point p) hp n).map (state u p)

end MetricKMedian.RationalSignedTerminal
end
end

end OAI
end

section
-- module Solutions.OAIQ037_KM.KMedian_Programs_UnitScanProgram
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.Preparation.RationalUnitInput.ScanProgram
open Finset Binary Binary.PolyProgram Binary.Automatic Binary.Automatic.Poly
open SparseGraph.ListOperation (Row Table setView indices)
open Program
variable {η τ : ℝ} (p : RationalAllParameters η τ)
def Input.sup (x : Input) : RationalSuppliers.Program.ScanInput :=
  letI := x.metric
  ⟨x.f,(x.U.representatives p.M).card,x.j,x.U.suppliers x.R p,x.U.df,x.U.dc,x.B⟩
end MetricKMedian.Preparation.RationalUnitInput.ScanProgram
end

end OAI
end