The source runtime bound for formatted PCP views

An ambient polynomial-time program is polynomial in encoded input size. This module bounds that size in the paper's parameter log n + log T + Q + sigma, including all field coordinates in the view.

theorem MIPRE.TM.CookLevin.Pad.esize_bitBlocks_le (l : List Cost.BitStr) (k : ℕ) (h : ∀ b ∈ l, List.length b = k) : Cost.esize l ≤ (4 * k + 2) * l.length + 1

theorem MIPRE.TM.CookLevin.Pad.esize_view_le (P : SAT.PcpParams) (z ev : List Cost.BitStr) (h : SAT.ViewFormat P z ev) : Cost.esize (z, ev) ≤ (4 * P.k + 2) * (2 * P.m' + 6) + 3

theorem MIPRE.TM.CookLevin.Pad.pcpInput_size_polynomial : ∃ (B : Polynomial ℕ), ∀ (D : Cost.Prog) (n T Q σ : ℕ) (x y : Cost.BitStr) (z ev : List Cost.BitStr), SAT.Valid D n T Q σ x y → SAT.ViewFormat (pcpParams n T Q σ) z ev → Cost.esize (SAT.pcpInput D n T Q σ x y z ev) ≤ Polynomial.eval (Desc.LOf n T Q σ) B

The complete encoded verifier input is polynomially bounded in precisely the source's four runtime parameters.

theorem MIPRE.TM.CookLevin.Pad.pcpProgram_time_le (verify : Cost.PolyTimeFun SAT.PcpInput Bool) : ∃ (R : Polynomial ℕ), ∀ (D : Cost.Prog) (n T Q σ : ℕ) (x y : Cost.BitStr) (z ev : List Cost.BitStr), SAT.Valid D n T Q σ x y → SAT.ViewFormat (pcpParams n T Q σ) z ev → ∃ t ≤ Polynomial.eval (n.size + T.size + Q + σ) R, verify.code.Runs (Cost.encode (SAT.pcpInput D n T Q σ x y z ev)) (Cost.encode (verify.toFun (SAT.pcpInput D n T Q σ x y z ev))) t

Any ambient polynomial-time PCP program has the prescribed source runtime bound on valid formatted views, for the constructed parameter family.