Documentation

MIPRE.TM.CookLevin.ClassicalPcp

The effective classical PCP for deciders #

The complete inhabitant uses Shoup's existing irreducible-polynomial contract. Field elements have the polynomial-basis coefficient representation; the later effective self-dual normal basis remains a separate algorithmic construction.

source
noncomputable def MIPRE.TM.CookLevin.Pad.parameterField (n T Q σ : ℕ) :
SAT.BinField (pcpParams n T Q σ).k
Equations
Instances For
    source
    instance MIPRE.TM.CookLevin.Pad.parameterField_charP (n T Q σ : ℕ) :
    CharP (parameterField n T Q σ).carrier 2
    source
    theorem MIPRE.TM.CookLevin.Pad.verifyPcp_rawView_iff (D : Cost.Prog) (n T Q σ : ℕ) (x y : Cost.BitStr) (hV : SAT.Valid D n T Q σ x y) (pf : SAT.PcpProof (pcpParams n T Q σ) (parameterField n T Q σ).carrier) (z : Fin (pcpParams n T Q σ).m' → (parameterField n T Q σ).carrier) :
    verifyPcp.toFun (SAT.pcpInput D n T Q σ x y (SAT.PcpProof.rawView (parameterField n T Q σ) pf z).1 (SAT.PcpProof.rawView (parameterField n T Q σ) pf z).2) = true ↔ SAT.PcpAlgebra.TypedAccepts (clausePolynomial D n T Q σ x y hV) z (pf.ev z)

    On every low-degree proof view, raw acceptance is exactly the typed algebraic test.

    source
    theorem MIPRE.TM.CookLevin.Pad.classicalPcp_completeness (D : Decider) (n T Q σ : ℕ) (x y : Cost.BitStr) (hV : SAT.Valid D.prog n T Q σ x y) (ap bp : Cost.BitStr) (hap : List.length ap ≤ T) (hbp : List.length bp ≤ T) (hacc : D.AcceptsWithin n x y ap bp T) :
    ∃ (pf : SAT.PcpProof (pcpParams n T Q σ) (parameterField n T Q σ).carrier), pf.g 0 = LowDegree.ldEnc (SAT.answerVec (parameterField n T Q σ).carrier (pcpParams n T Q σ).m ap) ∧ pf.g 1 = LowDegree.ldEnc (SAT.answerVec (parameterField n T Q σ).carrier (pcpParams n T Q σ).m bp) ∧ ∀ (z : Fin (pcpParams n T Q σ).m' → (parameterField n T Q σ).carrier), verifyPcp.toFun (SAT.pcpInput D.prog n T Q σ x y (SAT.PcpProof.rawView (parameterField n T Q σ) pf z).1 (SAT.PcpProof.rawView (parameterField n T Q σ) pf z).2) = true

    Every accepted pair of answer prefixes admits the required raw PCP proof.

    source
    theorem MIPRE.TM.CookLevin.Pad.classicalPcp_soundness (D : Decider) (n T Q σ : ℕ) (x y : Cost.BitStr) (hV : SAT.Valid D.prog n T Q σ x y) (pf : SAT.PcpProof (pcpParams n T Q σ) (parameterField n T Q σ).carrier) (hmajority : (pcpParams n T Q σ).q ^ (pcpParams n T Q σ).m' < 2 * {z : Fin (pcpParams n T Q σ).m' → (parameterField n T Q σ).carrier | verifyPcp.toFun (SAT.pcpInput D.prog n T Q σ x y (SAT.PcpProof.rawView (parameterField n T Q σ) pf z).1 (SAT.PcpProof.rawView (parameterField n T Q σ) pf z).2) = true}.card) :
    ∃ (ap : Cost.BitStr) (bp : Cost.BitStr), List.length ap ≤ T ∧ List.length bp ≤ T ∧ D.AcceptsWithin n x y ap bp T ∧ LowDegree.coded (pf.g 0) = SAT.answerVec (parameterField n T Q σ).carrier (pcpParams n T Q σ).m ap ∧ LowDegree.coded (pf.g 1) = SAT.answerVec (parameterField n T Q σ).carrier (pcpParams n T Q σ).m bp

    Majority acceptance of any low-degree raw PCP proof decodes to accepted answer prefixes and identifies both entire padded answer tapes.

    source
    noncomputable def MIPRE.TM.CookLevin.Pad.classicalPcpDecider :
    SAT.PcpDecider

    The bespoke effective classical PCP theorem, with no additional proof assumptions.

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