The common source clock covers legal factor and linear queries

theorem MIPRE.Introspection.AuxiliarySource.linear_query_size_le (R : ℕ) (hR : 1 ≤ R) (w : Player) (j : ℕ) (u y : Cost.BitStr) (hj : j.size ≤ R) (hu : List.length u ≤ R) (hy : List.length y ≤ R) : Cost.esize (CL.Sampler.Query.linear w j u y) + 1 ≤ 64 * R

theorem MIPRE.Introspection.AuxiliarySource.factor_query_size_le (R : ℕ) (hR : 1 ≤ R) (w : Player) (j : ℕ) (u : Cost.BitStr) (hj : j.size ≤ R) (hu : List.length u ≤ R) : Cost.esize (CL.Sampler.Query.factor w j u) + 1 ≤ 64 * R

theorem MIPRE.Introspection.AuxiliarySource.query_cost_le {lam n : ℕ} (hl : 1 ≤ lam) (hn : 1 ≤ n) (b : ℕ) (hb : b ≤ 64 * (2 ^ n) ^ lam) : (2 ^ n) ^ lam * b ^ lam ≤ ansBound 5 lam n

theorem MIPRE.Introspection.AuxiliarySource.bounded_query_result {ℓ lam n : ℕ} (V : Verifier ℓ) (hV : V.IsBounded lam) (hn : 1 ≤ n) (q : CL.Sampler.Query) (result : Cost.Data) (hq : Cost.esize q + 1 ≤ 64 * (2 ^ n) ^ lam) (hr : ∃ (t : ℕ), V.sampler.prog.Runs (Cost.encode (2 ^ n, q)) result t) : Cost.clockedResult V.sampler.prog (Cost.encode (2 ^ n, q)) (ansBound 5 lam n) = (Cost.encode true).cons result

theorem MIPRE.Introspection.AuxiliarySource.bounded_linear_result {ℓ lam n : ℕ} (V : Verifier ℓ) (hV : V.IsBounded lam) (hn : 1 ≤ n) (w : Player) (j : ℕ) (u y : Cost.BitStr) (hj : 1 ≤ j) (hjℓ : j ≤ ℓ) (hjR : j.size ≤ (2 ^ n) ^ lam) (hu : ∃ (x : Fin (V.sampler.dim (2 ^ n)) → CL.𝔽₂), u = CL.toBits ((CL.CLFun.truncate (j - 1) (V.sampler.cl (2 ^ n) w)).eval x)) (hy : List.length y = V.sampler.dim (2 ^ n)) : Cost.clockedResult V.sampler.prog (Cost.encode (2 ^ n, CL.Sampler.Query.linear w j u y)) (ansBound 5 lam n) = (Cost.encode true).cons (Cost.encode (CL.toBits (((V.sampler.cl (2 ^ n) w).mapOfPrefix (j - 1) (CL.ofBits (V.sampler.dim (2 ^ n)) u)) (CL.ofBits (V.sampler.dim (2 ^ n)) y))))

theorem MIPRE.Introspection.AuxiliarySource.bounded_factor_result {ℓ lam n : ℕ} (V : Verifier ℓ) (hV : V.IsBounded lam) (hn : 1 ≤ n) (w : Player) (j : ℕ) (u : Cost.BitStr) (hj : 1 ≤ j) (hjℓ : j ≤ ℓ) (hjR : j.size ≤ (2 ^ n) ^ lam) (hu : ∃ (x : Fin (V.sampler.dim (2 ^ n)) → CL.𝔽₂), u = CL.toBits ((CL.CLFun.truncate (j - 1) (V.sampler.cl (2 ^ n) w)).eval x)) : Cost.clockedResult V.sampler.prog (Cost.encode (2 ^ n, CL.Sampler.Query.factor w j u)) (ansBound 5 lam n) = (Cost.encode true).cons (Cost.encode (CL.indicatorBits ((V.sampler.cl (2 ^ n) w).factorOfPrefix (j - 1) (CL.ofBits (V.sampler.dim (2 ^ n)) u))))