The raw polynomial-time classical PCP verifier

The verifier rejects invalid specifications and malformed field views, constructs the exact circuit within the supplied view budget, evaluates its polynomial, and checks both algebraic identities on coefficient vectors. Its correspondence to typed low-degree proofs is established separately.

noncomputable def MIPRE.TM.CookLevin.Pad.verifierParams : Cost.PolyTimeFun SAT.PcpInput ParamInput

Equations

• MIPRE.TM.CookLevin.Pad.verifierParams = MIPRE.Cost.PolyTimeFun.snd.comp (MIPRE.Cost.PolyTimeFun.fst.comp MIPRE.Cost.PolyTimeFun.fst)

noncomputable def MIPRE.TM.CookLevin.Pad.pointProg : Cost.PolyTimeFun SAT.PcpInput (List Cost.BitStr)

Equations

• MIPRE.TM.CookLevin.Pad.pointProg = MIPRE.Cost.PolyTimeFun.fst.comp MIPRE.Cost.PolyTimeFun.snd

noncomputable def MIPRE.TM.CookLevin.Pad.claimsProg : Cost.PolyTimeFun SAT.PcpInput (List Cost.BitStr)

Equations

• MIPRE.TM.CookLevin.Pad.claimsProg = MIPRE.Cost.PolyTimeFun.snd.comp MIPRE.Cost.PolyTimeFun.snd

noncomputable def MIPRE.TM.CookLevin.Pad.verifierModulus : Cost.PolyTimeFun SAT.PcpInput Cost.BitStr

Construct the binary field modulus once from its unary degree.

Equations

• MIPRE.TM.CookLevin.Pad.verifierModulus = MIPRE.LowDegree.BinaryPolynomial.shoupLowerCoeffs.comp (MIPRE.TM.CookLevin.Pad.fieldDegreeU.comp MIPRE.TM.CookLevin.Pad.verifierParams)

theorem MIPRE.TM.CookLevin.Pad.verifierModulus_apply (D : Cost.Prog) (n T Q σ : ℕ) (x y : Cost.BitStr) (z ev : List Cost.BitStr) : verifierModulus.toFun (SAT.pcpInput D n T Q σ x y z ev) = LowDegree.BinaryPolynomial.shoupLowerCoeffs.toFun (Cost.unary (pcpParams n T Q σ).k)

noncomputable def MIPRE.TM.CookLevin.Pad.verifierCircuitValue : Cost.PolyTimeFun SAT.PcpInput Cost.BitStr

Evaluate the concrete circuit polynomial at the supplied field point.

Equations

• One or more equations did not get rendered due to their size.

theorem MIPRE.TM.CookLevin.Pad.verifierCircuitValue_apply (D : Cost.Prog) (n T Q σ : ℕ) (x y : Cost.BitStr) (z ev : List Cost.BitStr) : verifierCircuitValue.toFun (SAT.pcpInput D n T Q σ x y z ev) = SAT.Circuit.circuitBits (verifierModulus.toFun (SAT.pcpInput D n T Q σ x y z ev)) (List.take (5 * (pcpParams n T Q σ).m + 5) z) (List.drop (5 * (pcpParams n T Q σ).m + 5) z) (pcpCircuitProg.toFun (SAT.pcpInput D n T Q σ x y z ev)).gates

noncomputable def MIPRE.TM.CookLevin.Pad.verifierLiterals : Cost.PolyTimeFun SAT.PcpInput (List (Cost.BitStr × Cost.BitStr))

Pair the five claimed answer evaluations with the five sign coordinates.

Equations

• One or more equations did not get rendered due to their size.

theorem MIPRE.TM.CookLevin.Pad.verifierLiterals_apply (D : Cost.Prog) (n T Q σ : ℕ) (x y : Cost.BitStr) (z ev : List Cost.BitStr) : verifierLiterals.toFun (SAT.pcpInput D n T Q σ x y z ev) = (List.take 5 ev).zip (List.take 5 (List.drop (5 * (pcpParams n T Q σ).m) z))

noncomputable def MIPRE.TM.CookLevin.Pad.verifierCertificates : Cost.PolyTimeFun SAT.PcpInput (List (Cost.BitStr × Cost.BitStr))

Pair the certificate evaluations after the main certificate with each coordinate.

Equations

• One or more equations did not get rendered due to their size.

theorem MIPRE.TM.CookLevin.Pad.verifierCertificates_apply (D : Cost.Prog) (n T Q σ : ℕ) (x y : Cost.BitStr) (z ev : List Cost.BitStr) : verifierCertificates.toFun (SAT.pcpInput D n T Q σ x y z ev) = (List.drop 6 ev).zip z

noncomputable def MIPRE.TM.CookLevin.Pad.verifierTests : Cost.PolyTimeFun SAT.PcpInput Bool

Both field identities, including the single circuit-polynomial evaluation.

Equations

• One or more equations did not get rendered due to their size.

theorem MIPRE.TM.CookLevin.Pad.verifierTests_apply (D : Cost.Prog) (n T Q σ : ℕ) (x y : Cost.BitStr) (z ev : List Cost.BitStr) : verifierTests.toFun (SAT.pcpInput D n T Q σ x y z ev) = SAT.PcpFieldTests.checksProg.toFun (verifierModulus.toFun (SAT.pcpInput D n T Q σ x y z ev), verifierCircuitValue.toFun (SAT.pcpInput D n T Q σ x y z ev), ev.getD 5 [], (List.take 5 ev).zip (List.take 5 (List.drop (5 * (pcpParams n T Q σ).m) z)), (List.drop 6 ev).zip z)

noncomputable def MIPRE.TM.CookLevin.Pad.verifierFormat : Cost.PolyTimeFun SAT.PcpInput Bool

The constructed parameter family's exact raw view check.

Equations

• One or more equations did not get rendered due to their size.

theorem MIPRE.TM.CookLevin.Pad.verifierFormat_true_iff (D : Cost.Prog) (n T Q σ : ℕ) (x y : Cost.BitStr) (z ev : List Cost.BitStr) : verifierFormat.toFun (SAT.pcpInput D n T Q σ x y z ev) = true ↔ SAT.ViewFormat (pcpParams n T Q σ) z ev

noncomputable def MIPRE.TM.CookLevin.Pad.verifyPcp : Cost.PolyTimeFun SAT.PcpInput Bool

The actual globally polynomial-time verifier, with both mandatory rejection checks.

Equations

• One or more equations did not get rendered due to their size.

theorem MIPRE.TM.CookLevin.Pad.verifyPcp_true_iff (D : Cost.Prog) (n T Q σ : ℕ) (x y : Cost.BitStr) (z ev : List Cost.BitStr) : verifyPcp.toFun (SAT.pcpInput D n T Q σ x y z ev) = true ↔ SAT.Valid D n T Q σ x y ∧ SAT.ViewFormat (pcpParams n T Q σ) z ev ∧ verifierTests.toFun (SAT.pcpInput D n T Q σ x y z ev) = true

theorem MIPRE.TM.CookLevin.Pad.verifyPcp_reject_invalid (D : Cost.Prog) (n T Q σ : ℕ) (x y : Cost.BitStr) (z ev : List Cost.BitStr) (h : ¬SAT.Valid D n T Q σ x y ∨ ¬SAT.ViewFormat (pcpParams n T Q σ) z ev) : verifyPcp.toFun (SAT.pcpInput D n T Q σ x y z ev) = false

Invalid specifications and malformed views are rejected unconditionally.

theorem MIPRE.TM.CookLevin.Pad.verifyPcp_time_le : ∃ (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, verifyPcp.code.Runs (Cost.encode (SAT.pcpInput D n T Q σ x y z ev)) (Cost.encode (verifyPcp.toFun (SAT.pcpInput D n T Q σ x y z ev))) t

The raw verifier has exactly the source-parameter time bound in the PCP contract.