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

import Mathlib
import Definitions.Def_OAIQ037K056
import Definitions.Def_OAIQ037K057
import Definitions.Def_OAIQ037K058

section
-- module Solutions.OAIQ037_KM.KMedian_Geometry_GraphRunHeight
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
open Binary
variable {n m : ℕ}

theorem denominator_height (ν : Fin m → SparseIntegerLaw (Finset (Fin n))) (N L : ℕ)
    (hN : ∀ i, (ν i).length≤N) (hL : ∀ i, (ν i).law.denominator≤(2:ℤ)^L) (t : ℕ) :
    (run ν t).law.denominator≤(2:ℤ)^(stepHeight n m N L*t) := by
  induction t with
  | zero => simp [run,SparseIntegerLaw.dirac]
  | succ t ih =>
    rw [run]
    split_ifs with ht
    · rw [dite_eq_left ht]
      let μ := run ν t
      let ρ := μ.prod (ν ⟨t,ht⟩) (fun G S => next G S ⟨t,ht⟩)
      have hc := ρ.compressAuto_denominator features 0
        (fun i a => (features_height ρ.states[i.val] a).1)
        (fun i a => (features_height ρ.states[i.val] a).2)
      simp only [zero_mul,add_zero] at hc
      have hrD : ρ.law.denominator=μ.law.denominator*(ν ⟨t,ht⟩).law.denominator := rfl
      have hrN : ρ.length ≤ (n*m+(n*m)*(n*m)+1)*N :=
        Nat.mul_le_mul (run_length ν t) (hN _)
      change (ρ.compressAuto features).law.denominator≤_
      apply hc.trans
      rw [hrD]
      calc
        _ ≤ ((2:ℤ)^(stepHeight n m N L*t)*(2:ℤ)^L)*
            (2:ℤ)^((2*(n*m+(n*m)*(n*m)+1)*(n*m+(n*m)*(n*m)+1))*
              ((n*m+(n*m)*(n*m)+1)*N+1)*((n*m+(n*m)*(n*m)+1)*N)) := by
          gcongr
          · exact (ν ⟨t,ht⟩).law.denominator_pos.le
          · exact hL _
          · norm_num
        _ = _ := by rw [← pow_add,← pow_add]; congr 1; simp only [stepHeight]; ring
    · rw [dite_eq_right ht]
      exact ih.trans (pow_le_pow_right₀ (by norm_num) (Nat.mul_le_mul_left _ (Nat.le_succ t)))
end MetricKMedian.SparseGraph
end

end OAI
end

section
-- module Solutions.OAIQ037_KM.KMedian_Process_RoundingStateCompiler
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
open Binary Binary.PolyProgram Function
open SparseIntegerLaw.BinarySparse

noncomputable def statesProgram (s : Bool) :
    PolyProgram State.encode (encodeList erow) (fun x : State s => x.μ.states.toList.map Vector.toList) :=
  ((snd erow (ed erow)).comp (snd el (encodeList erow))).recode State.raw State.encode_raw (fun _ => rfl)
noncomputable def weightsProgram (s : Bool) :
    PolyProgram State.encode erow (fun x : State s => List.ofFn x.β) :=
  (fst erow (ed erow)).recode State.raw State.encode_raw (fun _ => rfl)

end MetricKMedian.RoundingProgram
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
 theorem probability_view (c : Context) (q : T c) : rowProbability (c,view c q)=probability c q := by
  simp only [rowProbability,probability,view,List.getElem?_ofFn]
  split_ifs <;> rfl

end MetricKMedian.SparseBernoulli.Program
end

end OAI
end

section
-- module Solutions.OAIQ037_KM.KMedian_Process_BatchOrdinalCodes
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.RationalBatchData.Ordinal
open Finset FixedBatch
open SparseGraph.ListOperation (Row Table setView indices)
variable {I : Type} [LinearOrder I] {n : ℕ}
variable (r : Fin n ≃o I) (D : Actions I I) (H : Finset I)

def view : ActionList.Raw := (List.ofFn fun h => sets r (D.erase (r h)),sets r H)

 theorem sets_length (S : Finset I) : (sets r S).length=n := by rw [sets_eq,List.length_ofFn]
 theorem sets_card (S : Finset I) : ((sets r S).filter id).length=S.card := by
  exact (MetricKMedian.EncodingLists.bool_card _).trans (card_map _)

 theorem units_length : (ActionList.units (view r D H)).length=n+n*n := by
  simp [ActionList.units,view,sets_eq,List.length_flatMap,Function.comp_def]
end MetricKMedian.RationalBatchData.Ordinal
end

end OAI
end

section
-- module Solutions.OAIQ037_KM.KMedian_Process_BatchOrdinalArrays
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.RationalBatchData.Ordinal
open Finset FixedBatch
open SparseGraph.ListOperation (Row Table setView indices)
variable {I : Type} [LinearOrder I] [Fintype I] {n : ℕ}
variable (r : Fin n ≃o I) (D : Actions I I) (H : Finset I)

 theorem erase_code (e : HeavyAction D H) :
    ActionArrays.erase (view r D H) (code r D H e)=sets r ((heavy D H).erase e) := by
  cases e with
  | inl e =>
    change ActionArrays.erase (view r D H) (r.symm e.val).val=sets r (D.erase e.val)
    simp only [ActionArrays.erase,view,sets_length,ite_eq_left (r.symm e.val).isLt,
      List.getElem?_ofFn,dite_eq_left (r.symm e.val).isLt,Option.getD_some,Fin.eta,OrderIso.apply_symm_apply]
  | inr e =>
    have hc : ¬ n+(r.symm e.val.1).val*n+(r.symm e.val.2).val<n := by omega
    change ActionArrays.erase (view r D H) (n+(r.symm e.val.1).val*n+(r.symm e.val.2).val)=sets r {e.val.2}
    simp only [ActionArrays.erase,view,sets_length,ite_eq_right hc,indices,
      RoundingList.range_finRange,List.map_map,Function.comp_def]
    rw [← List.ofFn_eq_map]
    apply congrArg List.ofFn
    funext i
    rw [show ActionList.child n (n+(r.symm e.val.1).val*n+(r.symm e.val.2).val)=(r.symm e.val.2).val from child_code r D H e]
    apply Bool.eq_iff_iff.mpr
    simp only [decide_eq_true_eq,mem_map_equiv,mem_singleton,← Fin.ext_iff]
    change (i=r.symm e.val.2) ↔ r i=e.val.2
    exact r.eq_symm_apply
end MetricKMedian.RationalBatchData.Ordinal
end

end OAI
end

section
-- module Solutions.OAIQ037_KM.KMedian_Process_BatchProposalProgram
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.RationalBatchData.ProposalProgram
open Finset FixedBatch Binary Binary.PolyProgram
open SparseIntegerLaw.BinarySparse
open SparseGraph.ListOperation (Row Table setView)
variable {C : Type} (I : C → Type) [∀ c, LinearOrder (I c)] [∀ c, Fintype (I c)]

variable {I}

abbrev Input.encode (x : Input I) := Binary.Automatic.enc x.raw

end MetricKMedian.RationalBatchData.ProposalProgram
end

end OAI
end

section
-- module Solutions.OAIQ037_KM.KMedian_Process_TaperListProgram
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.Taper.ListOperation
open Binary Binary.Automatic Binary.Automatic.Poly Finset
 theorem mem_breaks {n : ℕ} (P : ℚ) (d : Fin n → ℚ) (q : ℚ) :
    q∈breaks (P,List.ofFn d) ↔ q∈Taper.breakpoints P d := by
  simp only [breaks,upper_list,List.mem_cons,List.mem_append,List.mem_map,List.mem_ofFn,
    Taper.breakpoints,mem_insert,mem_union,mem_image,mem_univ,true_and]
  aesop
 theorem aSum_list {n : ℕ} (P t : ℚ) (d : Fin n → ℚ) :
    aSum ((P,List.ofFn d),t)=Taper.A P d t := by
  simp only [aSum,List.map_ofFn,List.sum_ofFn,Taper.A,Function.comp_def]
 theorem bSum_list {n : ℕ} (P t : ℚ) (d : Fin n → ℚ) :
    bSum ((P,List.ofFn d),t)=Taper.B P d t := by
  simp only [bSum,List.map_ofFn,List.sum_ofFn,Taper.B,Function.comp_def]
 theorem mem_candidates {n : ℕ} (g P : ℚ) (d : Fin n → ℚ) (q : ℚ) :
    q∈candidateList ((g,P),List.ofFn d) ↔ q∈Taper.candidates g P d := by
  simp only [candidateList,List.mem_append,List.mem_flatMap,List.mem_map,mem_breaks,
    aSum_list,bSum_list,Taper.candidates,mem_union,mem_image,mem_product,Prod.exists]
  aesop
 theorem mass_list {n : ℕ} (g P r : ℚ) (d : Fin n → ℚ) :
    mass (((g,P),List.ofFn d),r)=rationalMass g P d r := by
  simp only [mass,List.map_ofFn,List.sum_ofFn,rationalMass,Function.comp_def]
 theorem mem_roots {n : ℕ} (g P : ℚ) (d : Fin n → ℚ) (q : ℚ) :
    q∈roots ((g,P),List.ofFn d) ↔ q∈rootCandidates g P d := by
  simp only [roots,List.mem_filter,mem_candidates,Bool.and_eq_true,decide_eq_true_eq,mass_list,
    rootCandidates,mem_filter]
 theorem radius_list {n : ℕ} (g P : ℚ) (d : Fin n → ℚ) :
    radius ((g,P),List.ofFn d)=inverseRadius g P d := by
  unfold inverseRadius
  split_ifs with h
  · apply LPBinary.foldl_max_eq
    · exact (mem_filter.mp (max'_mem (rootCandidates g P d) h)).2.1.le
    · exact (mem_roots _ _ _ _).mpr (max'_mem _ h)
    · intro q hq
      exact le_max' _ _ ((mem_roots _ _ _ _).mp hq)
  · have he : roots ((g,P),List.ofFn d)=[] := by
      apply List.eq_nil_iff_forall_not_mem.mpr
      intro q hq
      exact h ⟨q,(mem_roots _ _ _ _).mp hq⟩
    simp only [radius,he,List.foldl_nil]
end MetricKMedian.Taper.ListOperation
end

end OAI
end

section
-- module Solutions.OAIQ037_KM.KMedian_Process_TaperAllProgram
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.Taper.ListOperation
open Binary Binary.Automatic Binary.Automatic.Poly Finset

 theorem colocated_list {n : ℕ} (g : ℚ) (d : Fin n → ℚ) :
    colocated (g,List.ofFn d)=rationalColocatedMass g d := by
  simp only [colocated,List.map_ofFn,List.sum_ofFn,rationalColocatedMass,Function.comp_def]
end MetricKMedian.Taper.ListOperation
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 rawColumn (x : InputRaw × ℕ) : Data Row :=
  if x.2 < x.1.2.length then x.1.2[x.2]?.getD ((1,[1]),[])
  else ((1,[1]),[x.1.1.map (fun _ => false)])

theorem rawColumn_eq (c : Context) : rawColumn c.raw=columnRaw (column c) := by
  simp only [rawColumn,Context.raw,Input.raw,List.length_ofFn,List.getElem?_ofFn,column]
  split_ifs with h
  · rfl
  · simp only [columnRaw,SparseIntegerLaw.dirac,Vector.toList_replicate,
      List.map_replicate,List.ofFn_const,ListOperation.setView,Finset.notMem_empty,decide_false]
    rfl

theorem update_view (c : Context) (G : T c) (S : Finset (Fin c.input.n)) :
    ListOperation.nextTable ((c.t,view c G),ListOperation.setView S)=view c (update c G S) := by
  apply List.ext_getElem
  · simp only [ListOperation.nextTable,ListOperation.indices,view,ListOperation.view,List.length_map,List.length_range,List.length_ofFn]
  · intro j hj hj'
    have hjm : j < c.input.m := by simpa only [view,ListOperation.view,List.length_ofFn] using hj'
    simp only [ListOperation.nextTable,ListOperation.indices,view,ListOperation.view,ListOperation.setView,List.getElem_map,
      List.getElem_range,List.getElem_ofFn,List.getElem?_ofFn,dite_eq_left hjm,Option.getD_some,update]
    split_ifs <;> rfl

def rawProduct (x : (InputRaw × ℕ) × Data Table) : (InputRaw × ℕ) × Data Table :=
  let p := prodData (x.2,rawColumn x.1)
  (x.1,(p.1,p.2.map (fun z => ListOperation.nextTable ((x.1.2,z.1),z.2))))

theorem rawProduct_eq (x : State) :
    rawProduct (x.ctx.raw,(x.raw view).2)=((x.product).ctx.raw,((x.product).raw view).2) := by
  unfold rawProduct
  rw [rawColumn_eq]
  simp only [Bundle.raw,columnRaw,State.product,prodData,
    states_list,SparseIntegerLaw.prod,Vector.toList_ofFn,List.map_ofFn,List.flatMap_def,
    Function.comp_def,RoundingList.ofFn_product,Context.raw,update_view]
  rfl

noncomputable def productProgram : PolyProgram State.encode State.encode State.product := by
  have hc : Binary.Automatic.Poly rawColumn := by
    unfold rawColumn
    have hm : Binary.Automatic.Poly (fun x : InputRaw × ℕ => x.1.1.map (fun _ => false)) := by
      apply Binary.Automatic.Poly.list_map <;> fun_prop
    fun_prop
  have hp : Binary.Automatic.Poly rawProduct := by
    unfold rawProduct
    apply Binary.Automatic.Poly.pair
    · fun_prop
    · apply Binary.Automatic.Poly.pair
      · fun_prop
      · apply Binary.Automatic.Poly.list_map <;> fun_prop
  exact hp.program.recode (fun x => (x.ctx.raw,(x.raw view).2)) (fun _ => rfl)
    (fun x => congrArg Binary.Automatic.enc (rawProduct_eq x))

noncomputable def dimensionsProgram : PolyProgram Context.encode IntegerLaw.BinaryCompression.es
    (fun c => List.replicate (c.input.n*c.input.m+(c.input.n*c.input.m)*(c.input.n*c.input.m)) ()) :=
  (((fst ei Nat.bits).comp ListOperation.dimensions_poly.program).recode Context.raw (fun _ => rfl)
    (fun c => congrArg _ (ListOperation.dimensions_eq (fun i => columnRaw (c.input.columns i)))))
noncomputable def featuresProgram : PolyProgram (encodePair Context.encode et) IntegerLaw.BinaryCompression.eqr
    (fun x => ListOperation.featureList (x.1.input.raw.1,x.2)) := by
  let p : PolyProgram (encodePair (encodePair ei Nat.bits) et) IntegerLaw.BinaryCompression.eqr
      (fun x : (InputRaw × ℕ) × Table => ListOperation.featureList (x.1.1.1,x.2)) := by
    apply Binary.Automatic.Poly.program
    fun_prop
  exact p.recode (fun x => (x.1.raw,x.2)) (fun _ => rfl) (fun _ => rfl)

noncomputable def compressProgram : PolyProgram State.encode State.encode
    (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)) :=
  SparseIntegerLaw.DependentProgram.compressProgram Context.encode et view [] _ (fun _ => features)
    (fun x => ListOperation.featureList (x.1.input.raw.1,x.2))
    (fun _ G => ListOperation.featureList_view G) dimensionsProgram featuresProgram

noncomputable def incrementProgram : PolyProgram State.encode State.encode State.increment := by
  let old := fst Context.encode (ed et)
  let inp := old.comp ((fst ei Nat.bits).recode Context.raw (fun _ => rfl) (fun _ => rfl))
  let t := old.comp ((snd ei Nat.bits).recode Context.raw (fun _ => rfl) (fun _ => rfl))
  let inc := (t.fanout (constant _ Nat.bits 1)).comp natAdd
  let law := snd Context.encode (ed et)
  exact ((inp.fanout inc).fanout law).recode (Bundle.raw view) (fun _ => rfl) (fun _ => rfl)
noncomputable def activeProgram : PolyProgram State.encode encodeBool
    (fun x : State => decide (x.ctx.t<x.ctx.input.m)) := by
  let raw : PolyProgram (encodePair ei Nat.bits) encodeBool
      (fun x : InputRaw × ℕ => decide (x.2<x.1.2.length)) := Binary.Automatic.Poly.program (by fun_prop)
  let ctx : PolyProgram Context.encode encodeBool (fun c => decide (c.t < c.input.m)) := raw.recode Context.raw (fun _ => rfl)
    (fun c => by simp only [Context.raw,Input.raw,List.length_ofFn])
  exact (contextProgram Context.encode et view).comp ctx
noncomputable def stepProgram : PolyProgram State.encode State.encode State.step :=
  ((PolyProgram.ite activeProgram (identity State.encode) (productProgram.comp compressProgram)).comp incrementProgram).congr _
    (fun x => by simp only [State.step,Function.comp_def,decide_eq_true_eq,id_eq])
end MetricKMedian.SparseGraph.Program
end

end OAI
end

section
-- module Solutions.OAIQ037_KM.KMedian_Programs_CardinalRoundProgram
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.SparseCardinalRounding.Program
open Binary Binary.PolyProgram Function SparseIntegerLaw.BinarySparse

noncomputable def inputProgram : PolyProgram encodeInput RoundingProgram.Input.encode weightedInput := by
  have hm : Binary.Automatic.Poly (fun q : List ℚ => q.map (fun _ => (1:ℚ))) := by
    apply Binary.Automatic.Poly.list_map <;> fun_prop
  let p : PolyProgram qr (encodePair qr qr) (fun q : List ℚ => (q.map (fun _ => (1:ℚ)),q)) :=
    Binary.Automatic.Poly.program (by fun_prop)
  exact p.recode (fun x => List.ofFn x.p) (fun _ => rfl) (fun x => by
    simp only [List.map_const',List.length_ofFn,RoundingProgram.Input.encode,
      RoundingProgram.Input.raw,weightedInput,List.ofFn_const,Vector.toList_ofFn])

end MetricKMedian.SparseCardinalRounding.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)
local notation "erB" => ListOperation.er

noncomputable def startProgram : PolyProgram Input.encode State.encode Input.start := by
  let raw : PolyProgram ei (encodePair (encodePair ei Nat.bits) (ed et))
      (fun x : InputRaw => ((x,0),(((1:ℤ),[(1:ℤ)]),[x.2.map (fun _ => x.1.map (fun _ => false))]))) := by
    apply Binary.Automatic.Poly.program
    have hs : Binary.Automatic.Poly (fun x : InputRaw => x.2.map (fun _ => x.1.map (fun _ => false))) := by
      apply Binary.Automatic.Poly.list_map
      · apply Binary.Automatic.Poly.list_map <;> fun_prop
      · fun_prop
    fun_prop
  exact raw.recode Input.raw (fun _ => rfl) (fun x => by
    simp only [State.encode,Bundle.encode,Bundle.raw,Input.start,SparseIntegerLaw.dirac,
      List.map_const',Input.raw,List.length_ofFn,List.map_replicate,
      Vector.toList_replicate,List.ofFn_const,view,ListOperation.view,Finset.notMem_empty,decide_false]
    rfl)

noncomputable def countProgram : PolyProgram Input.encode Nat.bits Input.m :=
  ((snd (encodeList (fun _ : Unit => [])) (encodeList (ed erB))).comp (listLength (ed erB) ((1,[1]),[]))).recode
    Input.raw (fun _ => rfl) (fun x => by simp only [Function.comp_def,Input.raw,List.length_ofFn])

theorem input_bounds (x : Input) :
    x.n≤x.encode.length ∧ x.m≤x.encode.length ∧
    (∀ i, (x.columns i).length≤x.encode.length) ∧
    (∀ i, (x.columns i).law.denominator≤(2:ℤ)^x.encode.length) := by
  let L := x.encode.length
  have he : L=2*(encodeList (fun _ : Unit => []) x.raw.1).length+1+
      (encodeList (ed erB) x.raw.2).length := encodePair_length _ _ _
  have hn := EncodedList.length_le (fun _ : Unit => []) x.raw.1
  have hm := EncodedList.length_le (ed erB) x.raw.2
  simp only [Input.raw,List.length_ofFn,List.length_replicate] at hn hm he
  have hcol (i : Fin x.m) : (ed erB (columnRaw (x.columns i))).length≤L := by
    have h := EncodedList.member_length (ed erB) x.raw.2 (columnRaw (x.columns i))
      (List.mem_ofFn.mpr ⟨i,rfl⟩)
    simp only [Input.raw] at h
    omega
  have hc (i : Fin x.m) : (ed erB (columnRaw (x.columns i))).length=
      2*(2*(Signed.encode (x.columns i).law.denominator).length+1+
        (encodeList Signed.encode (List.ofFn (x.columns i).law.numerator)).length)+1+
      (encodeList erB ((x.columns i).states.toList.map ListOperation.setView)).length := by
    simp only [columnRaw,ed,el,IntegerLaw.ListPivot.el,encodePair_length]
  refine ⟨by change x.n≤L; omega,by change x.m≤L; omega,?_,?_⟩
  · intro i
    have h := EncodedList.length_le Signed.encode (List.ofFn (x.columns i).law.numerator)
    simp only [List.length_ofFn] at h
    have hh := hcol i
    rw [hc i] at hh
    change (x.columns i).length≤L
    omega
  · intro i
    have hh := hcol i
    rw [hc i] at hh
    have hl : (Signed.encode (x.columns i).law.denominator).length≤L := by omega
    exact (le_abs_self _).trans ((Signed.height_length _).trans (pow_le_pow_right₀ (by norm_num) hl))

theorem state_size (x : Input) (t : ℕ) (ht : t≤x.m) :
    (State.encode (x.state t)).length≤ sizePolynomial.eval x.encode.length := by
  let L := x.encode.length
  obtain ⟨hn,hm,hN,hD⟩ := input_bounds x
  have htL : t≤L := ht.trans hm
  have hc : (Context.encode ⟨x,t⟩).length≤3*L+2 := by
    have hbits : t.bits.length≤t+1 := NatBinary.length_le_height (Nat.lt_two_pow_self.le)
    change (encodePair Input.encode Nat.bits (x,t)).length≤_
    rw [encodePair_length]
    change 2*L+1+t.bits.length≤_
    omega
  have hsupport : (x.state t).law.length≤ supportBound L := by
    apply (run_length x.columns t).trans
    unfold supportBound
    gcongr
  have hheight : SparseGraph.stepHeight x.n x.m L L*t≤heightBound L := by
    unfold heightBound SparseGraph.stepHeight
    dsimp only
    gcongr
  have hden : (x.state t).law.law.denominator≤(2:ℤ)^(heightBound L) :=
    (denominator_height x.columns L L hN hD t).trans (pow_le_pow_right₀ (by norm_num) hheight)
  have hr (S : Finset (Fin x.n)) : (erB (ListOperation.setView S)).length≤3*L := by
    have h := EncodedList.length_bound encodeBool (ListOperation.setView S) 1 (fun _ _ => by rfl)
    simp only [ListOperation.setView,List.length_ofFn] at h
    exact h.trans (by omega)
  have hs (G : Graph x.n x.m) : (et (ListOperation.view G)).length≤graphSize L := by
    have h := EncodedList.length_bound erB (ListOperation.view G) (3*L) (by
      intro row hrow
      obtain ⟨i,rfl⟩ := List.mem_ofFn.mp hrow
      exact hr (G i))
    simp only [ListOperation.view,List.length_ofFn] at h
    apply h.trans
    unfold graphSize
    gcongr
  have hb := SparseIntegerLaw.encode_length_bound (fun G : Graph x.n x.m => et (ListOperation.view G))
    (run x.columns t) (supportBound L) (heightBound L) (graphSize L) hsupport hden (fun _ => hs _)
  have he : State.encode (x.state t)=encodePair Context.encode
      (SparseIntegerLaw.BinarySparse.encode (fun G : Graph x.n x.m => et (ListOperation.view G)))
        (⟨x,t⟩,run x.columns t) := by
    simp only [State.encode,Bundle.encode,Bundle.raw,Input.state,view,
      SparseIntegerLaw.BinarySparse.encode,SparseIntegerLaw.BinarySparse.raw,ed,encodePair,RoundingProgram.encodeList_map]
  rw [sizePolynomial_eval,he,encodePair_length]
  unfold sizeBound
  dsimp only at ⊢
  simp only [L] at hc hb ⊢
  omega

noncomputable def runStateProgram : PolyProgram Input.encode State.encode (fun x => x.state x.m) :=
  (stepProgram.repeatFrom startProgram countProgram X sizePolynomial
    (fun x => by simpa using (input_bounds x).2.1)
    (fun x t ht => by rw [state_iterate]; exact state_size x t ht)).congr _ (fun x => state_iterate x _)
end MetricKMedian.SparseGraph.Program
end

end OAI
end