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

import Mathlib
import Definitions.Def_OAIQ037K048
import Definitions.Def_OAIQ037K049
import Definitions.Def_OAIQ037K050

section
-- module Solutions.OAIQ037_KM.KMedian_Binary_NumericParserProgram
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.InputParser
open Binary Binary.PolyProgram Binary.Automatic Binary.Automatic.Poly
@[fun_prop] theorem take_poly {α : Type} [Coding α] [Inhabited α] : Poly (fun x : List α × ℕ => x.1.take x.2) := ⟨listTake enc default⟩
@[fun_prop] theorem drop_poly {α : Type} [Coding α] [Inhabited α] : Poly (fun x : List α × ℕ => x.1.drop x.2) := ⟨listDrop enc default⟩
@[fun_prop] theorem value_poly : Poly Word.value := ⟨BooleanLists.valueProgram⟩
@[fun_prop] theorem signed_poly : Poly (fun x : Bool × ℕ => Signed.value x.1 x.2) := ⟨intFromParts⟩
@[fun_prop] theorem mkRat_poly : Poly (fun x : ℤ × ℕ => mkRat x.1 x.2) := ⟨mkRational⟩
@[fun_prop] theorem width_poly : Poly width := by unfold width; apply list_findIdx <;> fun_prop
def natRead (xs : List Bool) : ℕ × List Bool :=
  (Word.value ((xs.drop (width xs+1)).take (width xs)),xs.drop (width xs+1+width xs))
@[fun_prop] theorem natRead_poly : Poly natRead := by
  have hd : Poly (fun xs : List Bool => xs.drop (width xs+1)) :=
    Poly.comp (f:=fun x : List Bool × ℕ => x.1.drop x.2) drop_poly (g:=fun xs : List Bool => (xs,width xs+1)) (by fun_prop)
  have ht : Poly (fun xs : List Bool => (xs.drop (width xs+1)).take (width xs)) :=
    Poly.comp (f:=fun x : List Bool × ℕ => x.1.take x.2) take_poly (pair hd width_poly)
  exact pair (Poly.comp value_poly ht) (Poly.comp (f:=fun x : List Bool × ℕ => x.1.drop x.2) drop_poly (g:=fun xs : List Bool => (xs,width xs+1+width xs)) (by fun_prop))
 theorem prefix_width (n : ℕ) (xs : List Bool) : width (List.replicate n true++false::xs)=n := by
  induction n with
  | zero => simp [width,List.findIdx_cons]
  | succ n ih => simp only [List.replicate_succ,List.cons_append,width,List.findIdx_cons,Bool.not_true,Bool.false_eq_true,↓reduceIte]; exact congrArg Nat.succ ih
def ratRead (xs : List Bool) : ℚ × List Bool :=
  let a := natRead xs.tail
  let b := natRead a.2
  (mkRat (Signed.value (xs.head?.getD false) a.1) b.1,b.2)
@[fun_prop] theorem ratRead_poly : Poly ratRead := by unfold ratRead; fun_prop
end MetricKMedian.InputParser
end

end OAI
end

section
-- module Solutions.OAIQ037_KM.KMedian_Binary_SequentialParserProgram
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.InputParser
open Binary Binary.PolyProgram Binary.Automatic Binary.Automatic.Poly Polynomial
section Generic
variable {α : Type} [Coding α] [Inhabited α] (read : List Bool → α × List Bool)
 omit [Inhabited α] in
 theorem parseStep_poly (h : Poly read) : Poly (parseStep read) := by
  unfold parseStep
  have hh : Poly (fun x : State (α:=α) × Unit => read x.1.1) := Poly.comp h (by fun_prop)
  have ha : Poly (fun x : State (α:=α) × Unit => (read x.1.1).1 :: x.1.2) :=
    Poly.comp (f:=fun y : α × List α => y.1::y.2) list_cons (g:=fun x : State (α:=α) × Unit => ((read x.1.1).1,x.1.2)) (by fun_prop)
  exact pair (by fun_prop) ha
variable (P : PolyProgram enc enc read) (hrest : ∀ xs, (read xs).2.length≤xs.length)
def parse (x : List Unit × List Bool) : List α × List Bool :=
  let s := x.1.foldl (fun b a => parseStep read (b,a)) (x.2,[])
  (s.2.reverse,s.1)
end Generic
end MetricKMedian.InputParser
end

end OAI
end

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 coefficientsProgram : PolyProgram ef er (fun x : ℕ × Row => coefficients x.2 x.1) := by
  let p := fst Nat.bits er
  let row := snd Nat.bits er
  let inp := row.fanout p
  let denom := inp.comp (listGetD Ratio.encode 0)
  let rem := inp.comp (listEraseIdx Ratio.encode 0)
  let divide : PolyProgram (encodePair Ratio.encode Ratio.encode) Ratio.encode (fun x : ℚ × ℚ => x.2/x.1) :=
    ((exchange Ratio.encode Ratio.encode).comp ratDiv).congr _ (fun _ => rfl)
  exact ((denom.fanout rem).comp (divide.listMapWith 0 0)).congr _ (fun _ => rfl)

noncomputable def reduceProgram : PolyProgram (encodePair (encodePair er Nat.bits) er) er
    (fun x : (Row × ℕ) × Row => reduce x.1.1 x.1.2 x.2) := by
  let ec := encodePair er Nat.bits
  let cp := fst ec er
  let c := cp.comp (fst er Nat.bits)
  let p := cp.comp (snd er Nat.bits)
  let row := snd ec er
  let inp := row.fanout p
  let rem := inp.comp (listEraseIdx Ratio.encode 0)
  let val := inp.comp (listGetD Ratio.encode 0)
  let zp := (rem.fanout c).comp (listZip Ratio.encode Ratio.encode 0 0)
  let term : PolyProgram (encodePair Ratio.encode (encodePair Ratio.encode Ratio.encode)) Ratio.encode
      (fun x : ℚ × (ℚ × ℚ) => x.2.1-x.2.2*x.1) := by
    let pair := snd Ratio.encode (encodePair Ratio.encode Ratio.encode)
    let a := pair.comp (fst Ratio.encode Ratio.encode)
    let b := pair.comp (snd Ratio.encode Ratio.encode)
    let d := fst Ratio.encode (encodePair Ratio.encode Ratio.encode)
    exact ((a.fanout ((b.fanout d).comp ratMul)).comp ratSub).congr _ (fun _ => rfl)
  exact ((val.fanout zp).comp (term.listMapWith (0,0) 0)).congr _ (fun _ => rfl)

noncomputable def residualProgram : PolyProgram (encodePair ef ers) ers
    (fun x : (ℕ × Row) × Rows => residual x.1.2 x.1.1 x.2) := by
  let frame := fst ef ers
  let p := frame.comp (fst Nat.bits er)
  let c := frame.comp coefficientsProgram
  let rows := snd ef ers
  let start := (c.fanout p).fanout rows
  exact (start.comp (reduceProgram.listMapWith [] [])).congr _ (fun _ => rfl)

noncomputable def liftProgram : PolyProgram (encodePair ef er) er
    (fun x : (ℕ × Row) × Row => lift x.1.2 x.1.1 x.2) := by
  let frame := fst ef er
  let p := frame.comp (fst Nat.bits er)
  let c := frame.comp coefficientsProgram
  let z := snd ef er
  let terms := (c.fanout z).comp (listZipWith Ratio.encode Ratio.encode 0 0 ratMul)
  let value := (terms.comp ratSum).comp ratNeg
  exact (((z.fanout p).fanout value).comp (listInsertAt Ratio.encode 0)).congr _ (fun _ => rfl)

end MetricKMedian.Gaussian.ListOperation
end

end OAI
end

section
-- module Solutions.OAIQ037_KM.KMedian_Compression_GaussianListMachine
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 downProgram : PolyProgram ed (encodeLoop eState er) down := by
  let dat := fst edata efs
  let slots := dat.comp (fst eslots ers)
  let rows := dat.comp (snd eslots ers)
  let frames := snd edata efs
  let row := rows.comp (listHead er [])
  let p := row.comp pivotProgram
  let frame := p.fanout row
  let tl := rows.comp (listTail er [])
  let recRows := (frame.fanout tl).comp residualProgram
  let recSlots := slots.comp (listTail eu ())
  let recFrames := (frame.fanout frames).comp (listCons ef)
  let recurse := (((recSlots.fanout recRows).fanout recFrames).comp (injectLeft eUp ed)).comp (injectRight eState er)
  let skip := (((slots.fanout tl).fanout frames).comp (injectLeft eUp ed)).comp (injectRight eState er)
  let test := (p.fanout (row.comp (listLength Ratio.encode 0))).comp natLT
  let pivotCase := ite test skip recurse
  let zeroCase := (((constant ed er []).fanout frames).comp (injectRight eUp ed)).comp (injectRight eState er)
  let noCols := ite (slots.comp (listIsEmpty eu)) pivotCase zeroCase
  let baseCase := (((slots.comp basisProgram).fanout frames).comp (injectRight eUp ed)).comp (injectRight eState er)
  exact (ite (rows.comp (listIsEmpty er)) noCols baseCase).congr _ (fun x => by
    simp only [down,Function.comp_def,decide_eq_true_eq])

noncomputable def upProgram : PolyProgram eUp (encodeLoop eState er) up := by
  let z := fst er efs
  let frames := snd er efs
  let frame := frames.comp (listHead ef (0,[]))
  let new := (frame.fanout z).comp liftProgram
  let tl := frames.comp (listTail ef (0,[]))
  let recur := ((new.fanout tl).comp (injectRight eUp ed)).comp (injectRight eState er)
  let done := z.comp (injectLeft eState er)
  exact (ite (frames.comp (listIsEmpty ef)) recur done).congr _ (fun _ => rfl)

noncomputable def bodyProgram : PolyProgram eState (encodeLoop eState er) body :=
  sumElim ed eUp downProgram upProgram (([],[]),[]) ([],[])
end MetricKMedian.Gaussian.ListOperation
end

end OAI
end

section
-- module Solutions.OAIQ037_KM.KMedian_Compression_GaussianBinaryProgram
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 Polynomial

noncomputable def kernelProgram : PolyProgram Input.encode er Input.result :=
  loopFrom startProgram bodyProgram Input.result (2*X+2) statePolynomial (fun I => by
    obtain ⟨t,ht,hrun⟩ := full_run I.encode.length I.encode.length
      (residualHeight I.encode.length I.encode.length I.encode.length)
      (returnHeight I.encode.length I.encode.length I.encode.length)
      I.rows I.cols I.data I.underdetermined (input_audit I)
    refine ⟨t,?_,?_⟩
    · have hr := (input_bounds I).1
      simp only [eval_add,eval_mul,eval_ofNat,eval_X]
      omega
    · simpa only [statePolynomial_eval,Input.result] using hrun)

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 kernelProgram : PolyProgram Input.encode er Input.result :=
  ((rationalProgram.comp ListOperation.kernelProgram).comp IntegerList.numeratorsProgram).congr _ (fun I => by
    simp only [Function.comp_apply,ListOperation.Input.result,ListOperation.kernelList,IntegerList.numerators_ofFn]
    unfold Input.result computedIntegerKernel
    simp only [Vector.getElem_ofFn]
    rfl)
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 activeProgram : PolyProgram ed ees active := by
  let num := (snd Nat.bits (encodePair Signed.encode er)).comp (fst Signed.encode er)
  let test := ((num.fanout (constant ee Signed.encode 0)).comp intEQ).comp boolNot
  exact (entriesProgram.comp (test.listFilter (0,(0,[])))).congr _ (fun x => by
    simp only [Function.comp_apply,active]
    congr 1
    funext e
    simp)

noncomputable def activeRowsProgram : PolyProgram ed em activeRows := by
  let ones := activeProgram.comp ((constant ee Signed.encode 1).listMap (0,(0,[])))
  let ids := (fst es (encodePair er em)).comp (listIndices Gaussian.ListOperation.eu ())
  let a := fst Nat.bits ee
  let row := (snd Nat.bits ee).comp ((snd Nat.bits (encodePair Signed.encode er)).comp (snd Signed.encode er))
  let coord := (row.fanout a).comp (listGetD Signed.encode 0)
  let col := (exchange ees Nat.bits).comp (coord.listMapWith (0,(0,[])) 0)
  let cols := (activeProgram.fanout ids).comp (col.listMapWith 0 [])
  exact ((ones.fanout cols).comp (listCons er)).congr _ (fun _ => rfl)

noncomputable def activeDataProgram : PolyProgram ed Gaussian.IntegerProgram.ed activeData :=
  (((activeProgram.comp ((constant ee Gaussian.ListOperation.eu ()).listMap (0,(0,[])))).fanout activeRowsProgram)).congr _ (fun _ => rfl)

noncomputable def kernelInputProgram : PolyProgram Input.encode Gaussian.IntegerProgram.Input.encode Input.kernel :=
  activeDataProgram.recode Input.raw (fun _ => rfl) (fun I => by rw [activeData_raw])

noncomputable def extendProgram : PolyProgram (encodePair (encodeList ez) Nat.bits) Signed.encode
    (fun x : List (ℕ × ℤ) × ℕ => extend x.1 x.2) := by
  let a := fst Nat.bits ez
  let b := (snd Nat.bits ez).comp (fst Nat.bits Signed.encode)
  let test := (b.fanout a).comp natEQ
  let filtered := (exchange (encodeList ez) Nat.bits).comp (test.listFilterWith (0,0) 0)
  exact ((filtered.comp ((snd Nat.bits Signed.encode).listMap (0,0))).comp IntegerList.sumProgram).congr _ (fun _ => rfl)

noncomputable def fullProgram : PolyProgram (encodePair ed er) er (fun x : Data × Row => full x.1 x.2) := by
  let x := fst ed er
  let z := snd ed er
  let ids := ((x.comp activeProgram).comp ((fst Nat.bits (encodePair Signed.encode er)).listMap (0,(0,[]))))
  let zs := (ids.fanout z).comp (listZip Nat.bits Signed.encode 0 0)
  let out := ((x.comp (snd es (encodePair er em))).comp (fst er em)).comp (listIndices Signed.encode 0)
  exact ((zs.fanout out).comp (extendProgram.listMapWith 0 0)).congr _ (fun _ => rfl)

noncomputable def affineKernelProgram : PolyProgram Input.encode er (fun I => List.ofFn (computedAffineKernel I.μ I.v)) := by
  let raw : PolyProgram Input.encode ed Input.raw := (identity ed).recode Input.raw (fun _ => rfl) (fun _ => rfl)
  let kern := kernelInputProgram.comp Gaussian.IntegerProgram.kernelProgram
  exact ((raw.fanout kern).comp fullProgram).congr _ (fun I => full_raw I)

end MetricKMedian.IntegerLaw.ListOperation
end

end OAI
end

section
-- module Solutions.OAIQ037_KM.KMedian_Rounding_SignedListOperations
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.RoundingList
open Binary Binary.Automatic Binary.Automatic.Poly RationalWeightedStep Finset

attribute [fun_prop] square_poly

theorem square_list {n : ℕ} (p : Vector ℚ n) :
    square p.toList=List.ofFn (fun z : Fin (n*n) => ((finProdFinEquiv.symm z).1.val,(finProdFinEquiv.symm z).2.val)) := by
  simp only [square,indices,Vector.length_toList,range_finRange,List.flatMap_def,List.map_map,Function.comp_def]
  rw [← List.ofFn_eq_map]
  conv => lhs; arg 1; arg 1; intro i; rw [← List.ofFn_eq_map]
  exact ofFn_product _

namespace Signed

theorem valid_list {n : ℕ} (β : Fin n → ℚ) (p : Vector ℚ n) (z : Fin (n*n)) :
    valid (List.ofFn β) p.toList ((finProdFinEquiv.symm z).1.val,(finProdFinEquiv.symm z).2.val)=
      decide (z∈RationalSignedStep.pairs β p) := by
  simp only [valid,frac,get_point,Gaussian.ListOperation.get_ofFn,← Bool.decide_and]
  apply Bool.eq_iff_iff.mpr
  simp only [decide_eq_true_eq,RationalSignedStep.pairs,mem_filter,mem_univ,true_and,RationalWeightedStep.fractional,Fin.val_ne_iff]
  tauto

theorem active_list {n : ℕ} (β : Fin n → ℚ) (p : Vector ℚ n) :
    active (List.ofFn β) p.toList=decide (RationalSignedStep.Active β p) := by
  unfold active index
  rw [square_list]
  apply Bool.eq_iff_iff.mpr
  simp only [decide_eq_true_eq,List.findIdx_lt_length,List.mem_ofFn]
  constructor
  · rintro ⟨a,⟨z,rfl⟩,hz⟩
    exact ⟨z,by simpa only [valid_list,decide_eq_true_eq] using hz⟩
  · rintro ⟨z,hz⟩
    exact ⟨_,⟨z,rfl⟩,by simpa only [valid_list,decide_eq_true_eq] using hz⟩

theorem index_list {n : ℕ} (β : Fin n → ℚ) (p : Vector ℚ n) (h : RationalSignedStep.Active β p) :
    index (List.ofFn β) p.toList=((RationalSignedStep.pairs β p).min' h).val := by
  unfold index
  rw [square_list]
  let z := (RationalSignedStep.pairs β p).min' h
  apply (List.findIdx_eq (by simpa only [List.length_ofFn] using z.isLt)).mpr
  constructor
  · simp only [List.getElem_ofFn,valid_list,decide_eq_true_eq]
    exact min'_mem _ h
  · intro j hj
    simp only [List.getElem_ofFn,valid_list,decide_eq_false_iff_not]
    intro hm
    exact (not_le_of_gt hj) ((RationalSignedStep.pairs β p).min'_le _ hm)

theorem pair_list {n : ℕ} (β : Fin n → ℚ) (p : Vector ℚ n) (h : RationalSignedStep.Active β p) :
    pair (List.ofFn β) p.toList=((RationalSignedStep.pair β p h).val.1.val,(RationalSignedStep.pair β p h).val.2.val) := by
  simp only [pair,index_list β p h,square_list,Gaussian.ListOperation.get_ofFn,RationalSignedStep.pair]

theorem probability_list {n : ℕ} (β : Fin n → ℚ) (p : Vector ℚ n) :
    probability (List.ofFn β) p.toList=RationalSignedStep.probability β p := by
  unfold probability RationalSignedStep.probability
  rw [active_list]
  simp only [decide_eq_true_eq]
  split_ifs with h
  · simp only [ratio,pair_list β p h,Gaussian.ListOperation.get_ofFn,up_list,down_list]
  · rfl

theorem endpoint_list {n : ℕ} (β : Fin n → ℚ) (p : Vector ℚ n) (b : Fin 2) :
    endpoint (List.ofFn β) p.toList (decide (b≠0))=(RationalSignedStep.endpoint β p b).toList := by
  unfold endpoint RationalSignedStep.endpoint
  rw [active_list]
  simp only [decide_eq_true_eq]
  by_cases h : RationalSignedStep.Active β p
  · simp only [ite_eq_left h,dite_eq_left h,ratio,pair_list β p h,Gaussian.ListOperation.get_ofFn,up_list,down_list]
    by_cases hb : b=0 <;> simp [hb,move_list]
  · simp only [ite_eq_right h,dite_eq_right h]

end Signed
end MetricKMedian.RoundingList
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 leastProgram : PolyProgram ees Ratio.encode least :=
  ((((positiveProgram.listFilter (0,0)).comp (ratioProgram.listMap (0,0))).comp LPBinary.Program.minimumProgram)).congr _ (fun _ => rfl)
noncomputable def pivotProgram : PolyProgram ees Nat.bits pivot := by
  let m := fst Ratio.encode ee
  let e := snd Ratio.encode ee
  let eq := ((e.comp ratioProgram).fanout m).comp ratEQ
  let test := ((e.comp positiveProgram).fanout eq).comp boolAnd
  let tests := (leastProgram.fanout (identity ees)).comp (test.listMapWith (0,0) false)
  exact (tests.comp (listFindIdx (identity encodeBool) false)).congr _ (fun es => by
    simp only [Function.comp_def, List.findIdx_map, id_eq, pivot, Bool.decide_and])

noncomputable def updateProgram : PolyProgram (encodePair el er) el (fun x : LawData × Row => update x.1 x.2) := by
  let μ := fst el er
  let num := μ.comp (snd Signed.encode er)
  let z := snd el er
  let es := (num.fanout z).comp (listZip Signed.encode Signed.encode 0 0)
  let p := es.comp pivotProgram
  let b := (es.fanout p).comp (listGetD ee (0,0))
  let g := fst ee ee
  let e := snd ee ee
  let m1 := ((e.comp (fst Signed.encode Signed.encode)).fanout (g.comp (snd Signed.encode Signed.encode))).comp intMul
  let m2 := ((g.comp (fst Signed.encode Signed.encode)).fanout (e.comp (snd Signed.encode Signed.encode))).comp intMul
  let coord := (m1.fanout m2).comp intSub
  let nums := (b.fanout es).comp (coord.listMapWith (0,0) 0)
  let den := ((μ.comp (fst Signed.encode er)).fanout (b.comp (snd Signed.encode Signed.encode))).comp intMul
  exact (den.fanout nums).congr _ (fun _ => rfl)

end MetricKMedian.IntegerLaw.ListPivot
end

end OAI
end

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

noncomputable def scaledRowsProgram : PolyProgram eqd em scaledRows := by
  let dim := fst es (encodePair el eqm)
  let rest := snd es (encodePair el eqm)
  let rows := rest.comp (snd el eqm)
  let law := rest.comp (fst el eqm)
  let cols := (dim.fanout rows).comp (MatrixList.transposeProgram Ratio.encode Gaussian.ListOperation.eu 0 ())
  let icols := cols.comp (IntegerList.numeratorsProgram.listMap [])
  let nums := law.comp (snd Signed.encode er)
  exact ((nums.fanout icols).comp (MatrixList.transposeProgram Signed.encode Signed.encode 0 0)).congr _ (fun _ => rfl)

noncomputable def integerInputProgram : PolyProgram RationalInput.encode Input.encode RationalInput.integer := by
  let dim := fst es (encodePair el eqm)
  let law := (snd es (encodePair el eqm)).comp (fst el eqm)
  let p := dim.fanout (law.fanout scaledRowsProgram)
  exact p.recode RationalInput.raw (fun _ => rfl) (fun I => by
    change ed (List.replicate I.d (), (I.lawData, scaledRows I.raw))=_
    rw [scaledRows_raw]
    rfl)
end MetricKMedian.IntegerLaw.BinaryCompression
end

end OAI
end

section
-- module Solutions.OAIQ037_KM.KMedian_Sparse_SparseListTrim
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.BinarySparse
open Binary Binary.PolyProgram Function Finset
variable {α : Type}

noncomputable def activeProgram (ea : α → List Bool) (a0 : α) :
    PolyProgram (ed ea) (encodeList (encodePair Signed.encode ea)) activeEntries := by
  let l := fst el (encodeList ea)
  let nums := l.comp (snd Signed.encode er)
  let s := snd el (encodeList ea)
  let test := ((((fst Signed.encode ea).fanout (constant (encodePair Signed.encode ea) Signed.encode 0)).comp intEQ).comp boolNot)
  exact (((nums.fanout s).comp (listZip Signed.encode ea 0 a0)).comp (test.listFilter (0,a0))).congr _ (fun x => by
    simp only [Function.comp_def,activeEntries,decide_not])

noncomputable def trimDataProgram (ea : α → List Bool) (a0 : α) :
    PolyProgram (ed ea) (ed ea) trimData := by
  let zs := activeProgram ea a0
  let nums := zs.comp ((fst Signed.encode ea).listMap (0,a0))
  let states := zs.comp ((snd Signed.encode ea).listMap (0,a0))
  let den := (fst el (encodeList ea)).comp (fst Signed.encode er)
  exact ((den.fanout nums).fanout states).congr _ (fun _ => rfl)

end MetricKMedian.SparseIntegerLaw.BinarySparse
end

end OAI
end

section
-- module Solutions.OAIQ037_KM.KMedian_Sparse_SparseBranchProgram
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.BinarySparse
open Binary Binary.PolyProgram Function
variable {α γ : Type}

noncomputable def branchLawProgram :
    PolyProgram (encodePair el (encodeList Ratio.encode)) el branchLawData := by
  let en := encodePair el (encodeList Ratio.encode)
  let law := fst el (encodeList Ratio.encode)
  let probs := snd el (encodeList Ratio.encode)
  let D := probs.comp IntegerList.denominatorProgram
  let nums := law.comp (snd Signed.encode er)
  let zs := probs.comp IntegerList.numeratorsProgram
  let triples := D.fanout ((nums.fanout zs).comp (listZip Signed.encode Signed.encode 0 0))
  let ez := encodePair Signed.encode Signed.encode
  let z := snd Signed.encode ez
  let w := z.comp (fst Signed.encode Signed.encode)
  let a := z.comp (snd Signed.encode Signed.encode)
  let d := fst Signed.encode ez
  let p0 := (w.fanout a).comp intMul
  let p1 := (w.fanout ((d.fanout a).comp intSub)).comp intMul
  let entries := (p0.fanout p1).comp pairList
  let outputnums := triples.comp (entries.listFlatMapWith (0,0) 0)
  let den := ((law.comp (fst Signed.encode er)).fanout D).comp intMul
  exact (den.fanout outputnums).congr _ (fun _ => rfl)

end MetricKMedian.SparseIntegerLaw.BinarySparse
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)

noncomputable def compressionInputProgram (a0 : A) (d : C → ℕ) (v : ∀ c, T c → Fin (d c) → ℚ)
    (F : C × A → List ℚ) (hF : ∀ c a, F (c,view c a)=List.ofFn (v c a))
    (D : PolyProgram ec IntegerLaw.BinaryCompression.es (fun c => List.replicate (d c) ()))
    (V : PolyProgram (encodePair ec ea) IntegerLaw.BinaryCompression.eqr F) :
    PolyProgram (Bundle.encode ec ea view) IntegerLaw.BinaryCompression.RationalInput.encode
      (Bundle.compressionInput d v) := by
  let ctx := contextProgram ec ea view
  let rows := (ctx.fanout (statesProgram ec ea view)).comp (V.listMapWith a0 [])
  let work := (ctx.comp D).fanout ((lawProgram ec ea view).fanout rows)
  exact work.recode id (fun _ => rfl) (fun x => by
    change IntegerLaw.BinaryCompression.eqd (List.replicate (d x.ctx) (),
      ((x.law.law.denominator,List.ofFn x.law.law.numerator),
        (x.law.states.toList.map (view x.ctx)).map (fun a => F (x.ctx,a))))=_
    simp only [states_list,List.map_ofFn,Function.comp_def,hF]
    rfl)

noncomputable def branchProgram (a0 : A) (p : ∀ c, T c → ℚ) (hp : ∀ c a, 0 ≤ p c a ∧ p c a ≤ 1)
    (next : ∀ c, T c → Fin 2 → T c)
    (P : C × A → ℚ) (E0 E1 : C × A → A)
    (hP : ∀ c a, P (c,view c a)=p c a)
    (hE0 : ∀ c a, E0 (c,view c a)=view c (next c a 0))
    (hE1 : ∀ c a, E1 (c,view c a)=view c (next c a 1))
    (PP : PolyProgram (encodePair ec ea) Ratio.encode P)
    (PE0 : PolyProgram (encodePair ec ea) ea E0) (PE1 : PolyProgram (encodePair ec ea) ea E1) :
    PolyProgram (Bundle.encode ec ea view) (Bundle.encode ec ea view) (Bundle.branch p hp next) := by
  let c := contextProgram ec ea view
  let states := statesProgram ec ea view
  let probs := (c.fanout states).comp (PP.listMapWith a0 0)
  let law := ((lawProgram ec ea view).fanout probs).comp branchLawProgram
  let endpoints := (PE0.fanout PE1).comp pairList
  let outputstates := (c.fanout states).comp (endpoints.listFlatMapWith a0 a0)
  let work := c.fanout (law.fanout outputstates)
  exact work.recode id (fun _ => rfl) (fun x => by
    exact congrArg (encodePair ec (ed ea)) (raw_branch view p hp next P E0 E1 hP hE0 hE1 x))

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

noncomputable def incrementProgram : PolyProgram State.encode State.encode State.increment := by
  let old := fst Context.encode (SparseIntegerLaw.BinarySparse.ed er)
  let inp := old.comp ((fst qr Nat.bits).recode Context.raw (fun _ => rfl) (fun _ => rfl))
  let t := old.comp ((snd qr Nat.bits).recode Context.raw (fun _ => rfl) (fun _ => rfl))
  let inc := (t.fanout (constant _ Nat.bits 1)).comp natAdd
  let law := snd Context.encode (SparseIntegerLaw.BinarySparse.ed er)
  exact ((inp.fanout inc).fanout law).recode (Bundle.raw view) (fun _ => rfl) (fun _ => rfl)

end MetricKMedian.SparseBernoulli.Program
end

end OAI
end

section
-- module Solutions.OAIQ037_KM.KMedian_Programs_GraphRunProgram
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 Polynomial
open SparseIntegerLaw.DependentProgram SparseIntegerLaw.BinarySparse
open ListOperation (Row Table et)

theorem state_next (x : Input) (t : ℕ) : State.step (x.state t)=x.state (t+1) := by
  have he (ht : t < x.m) : update ⟨x,t⟩=(fun G S => next G S ⟨t,ht⟩) := by
    funext G S i
    by_cases h : i=⟨t,ht⟩
    · subst i; simp only [update,next,Function.update_self,ite_true]
    · have hv : i.val≠t := fun hh => h (Fin.ext hh)
      simp only [update,next,Function.update_of_ne h,ite_eq_right hv]
  unfold State.step Input.state
  by_cases ht : t < x.m
  · rw [ite_eq_left ht]
    change (⟨⟨x,t+1⟩,((run x.columns t).prod (column ⟨x,t⟩) (update ⟨x,t⟩)).compressAuto features⟩ : State)=_
    rw [run,dite_eq_left ht]
    simp only [column,dite_eq_left ht,he ht,SparseGraph.step,SparseIntegerLaw.prodCompress]
  · rw [ite_eq_right ht,run,dite_eq_right ht]
    rfl

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

end MetricKMedian.SparseGraph.Program
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 priorProgram : PolyProgram (encodePair ees ee) Ratio.encode (fun x : List Entry × Entry => prior x.1 x.2) := by
  let pred := (exchange ee ee).comp beforeProgram
  let filtered := (exchange ees ee).comp (pred.listFilterWith (0,(0,0)) (0,(0,0)))
  let cap := (snd Nat.bits (encodePair Ratio.encode Ratio.encode)).comp (fst Ratio.encode Ratio.encode)
  exact ((filtered.comp (cap.listMap (0,(0,0)))).comp ratSum).congr _ (fun _ => rfl)
noncomputable def amountProgram : PolyProgram (encodePair ees ee) Ratio.encode (fun x : List Entry × Entry => amount x.1 x.2) := by
  let cap := ((snd ees ee).comp (snd Nat.bits (encodePair Ratio.encode Ratio.encode))).comp (fst Ratio.encode Ratio.encode)
  let remain := ((constant (encodePair ees ee) Ratio.encode 1).fanout priorProgram).comp ratSub
  exact ((cap.fanout (remain.comp Program.positivePart)).comp Program.ratMin).congr _ (fun _ => rfl)
noncomputable def fillingProgram : PolyProgram (encodePair er er) er (fun x : Row × Row => filling x.1 x.2) :=
  ((entriesProgram.fanout entriesProgram).comp (amountProgram.listMapWith (0,(0,0)) 0)).congr _ (fun _ => rfl)
end Nearest
end MetricKMedian.LPBinary
end

end OAI
end