The circuit polynomial in the PCP clause coordinates #
noncomputable def
MIPRE.SAT.PcpParams.circuitArith
{F : Type u_1}
[Field F]
(P : PcpParams)
(C : Circuit)
(h : C.inputs + C.size = P.m')
:
MvPolynomial (Fin P.m') F
The exact finite circuit polynomial transported to the advertised PCP dimension.
Equations
- P.circuitArith C h = (MvPolynomial.rename (Fin.cast h)) C.finiteArith
Instances For
theorem
MIPRE.SAT.PcpParams.eval_circuitArith_bool
{F : Type u_1}
[Field F]
[CharP F 2]
(P : PcpParams)
(C : Circuit)
(hC : C.WellFormed)
(h : C.inputs + C.size = P.m')
(y : Fin P.m' → Bool)
:
(MvPolynomial.eval (LowDegree.pt y)) (P.circuitArith C h) = 0 ∨ (MvPolynomial.eval (LowDegree.pt y)) (P.circuitArith C h) = 1
theorem
MIPRE.SAT.PcpParams.eval_iff_exists_circuitArith
{F : Type u_1}
[Field F]
[CharP F 2]
(P : PcpParams)
(C : Circuit)
(hC : C.WellFormed)
(h : C.inputs + C.size = P.m')
(x : ℕ → Bool)
:
C.eval x = true ↔ ∃ (y : Fin P.m' → Bool),
(∀ (i : Fin C.inputs), y (Fin.cast h (Fin.castAdd C.size i)) = x ↑i) ∧ (MvPolynomial.eval (LowDegree.pt y)) (P.circuitArith C h) = 1
Every accepting input extends to a Boolean PCP point on which the circuit polynomial is one, and all its original input coordinates are retained.
theorem
MIPRE.SAT.PcpParams.pointClause_mem_of_circuitArith
{F : Type u_1}
[Field F]
[CharP F 2]
(P : PcpParams)
(C : Circuit)
(hC : C.WellFormed)
(hI : C.inputs = 5 * P.m + 5)
(h : C.inputs + C.size = P.m')
(y : Fin P.m' → Bool)
(hy : (MvPolynomial.eval (LowDegree.pt y)) (P.circuitArith C h) = 1)
:
On a satisfying Boolean point, the encoded clause belongs to the describer's actual five-block formula.
theorem
MIPRE.SAT.PcpParams.exists_point_of_clause_mem
{F : Type u_1}
[Field F]
[CharP F 2]
(P : PcpParams)
(C : Circuit)
(hC : C.WellFormed)
(hI : C.inputs = 5 * P.m + 5)
(h : C.inputs + C.size = P.m')
(c : Clause5 (Fin (2 ^ P.m)) (Fin (2 ^ P.m)) (Fin (2 ^ P.m)) (Fin (2 ^ P.m)) (Fin (2 ^ P.m)))
(hc : c ∈ C.formula5 P.m P.m)
:
∃ (y : Fin P.m' → Bool), P.pointClause y = c ∧ (MvPolynomial.eval (LowDegree.pt y)) (P.circuitArith C h) = 1
Every actual clause has a Boolean witness point whose blocks and signs decode back to precisely that clause.
theorem
MIPRE.SAT.PcpParams.exists_proof_of_formula5_sat
{F : Type u_1}
[Field F]
[CharP F 2]
(P : PcpParams)
(C : Circuit)
(hC : C.WellFormed)
(hI : C.inputs = 5 * P.m + 5)
(h : C.inputs + C.size = P.m')
(a : Fin 5 → Fin (2 ^ P.m) → Bool)
(ha : (C.formula5 P.m P.m).Sat (a 0) (a 1) (a 2) (a 3) (a 4))
:
∃ (pf : PcpProof P F),
(∀ (i : Fin 5), pf.g i = LowDegree.ldEnc fun (u : Fin P.m → Bool) => LowDegree.ofBool (a i (cubeIndex u))) ∧ ∀ (z : Fin P.m' → F), PcpAlgebra.TypedAccepts (P.circuitArith C h) z (pf.ev z)
A satisfying tuple for the describer's formula supplies an honest degree-seven PCP proof for the concrete circuit polynomial.
def
MIPRE.SAT.PcpParams.decodedAssignment
{F : Type u_1}
[Field F]
[DecidableEq F]
{P : PcpParams}
(pf : PcpProof P F)
(i : Fin 5)
(j : Fin (2 ^ P.m))
:
The Boolean assignment read from one low-degree answer polynomial.
Equations
- MIPRE.SAT.PcpParams.decodedAssignment pf i j = decide (MIPRE.LowDegree.coded (pf.g i) (MIPRE.SAT.indexCube j) = 1)
Instances For
theorem
MIPRE.SAT.PcpParams.formula5_sat_of_majority
{F : Type u_1}
[Field F]
[CharP F 2]
[Fintype F]
[DecidableEq F]
(P : PcpParams)
(C : Circuit)
(hC : C.WellFormed)
(hI : C.inputs = 5 * P.m + 5)
(h : C.inputs + C.size = P.m')
(pf : PcpProof P F)
(hq : 82 * P.m' ≤ Fintype.card F)
(S : Finset (Fin P.m' → F))
(hS : ∀ z ∈ S, PcpAlgebra.TypedAccepts (P.circuitArith C h) z (pf.ev z))
(hmajority : Fintype.card F ^ P.m' < 2 * S.card)
:
(C.formula5 P.m P.m).Sat (decodedAssignment pf 0) (decodedAssignment pf 1) (decodedAssignment pf 2)
(decodedAssignment pf 3) (decodedAssignment pf 4)
Majority acceptance supplies an actual satisfying five-tuple for the succinctly described clause set, including every Boolean clause witness.
theorem
MIPRE.SAT.PcpParams.completeness_of_describes
{F : Type u_1}
[Field F]
[CharP F 2]
(P : PcpParams)
(C : Circuit)
(hC : C.WellFormed)
(hI : C.inputs = 5 * P.m + 5)
(h : C.inputs + C.size = P.m')
(D : Decider)
(n T : ℕ)
(x y ap bp : Cost.BitStr)
(hD : C.DescribesDecider P.m P.m D n x y T)
(hap : List.length ap ≤ T)
(hbp : List.length bp ≤ T)
(hacc : D.AcceptsWithin n x y ap bp T)
:
∃ (pf : PcpProof P F),
pf.g 0 = LowDegree.ldEnc (answerVec F P.m ap) ∧ pf.g 1 = LowDegree.ldEnc (answerVec F P.m bp) ∧ ∀ (z : Fin P.m' → F), PcpAlgebra.TypedAccepts (P.circuitArith C h) z (pf.ev z)
Typed PCP completeness against the describer's actual accepting answer tapes.
theorem
MIPRE.SAT.PcpParams.soundness_of_describes
{F : Type u_1}
[Field F]
[CharP F 2]
[Fintype F]
[DecidableEq F]
(P : PcpParams)
(C : Circuit)
(hC : C.WellFormed)
(hI : C.inputs = 5 * P.m + 5)
(h : C.inputs + C.size = P.m')
(D : Decider)
(n T : ℕ)
(x y : Cost.BitStr)
(hD : C.DescribesDecider P.m P.m D n x y T)
(pf : PcpProof P F)
(hq : 82 * P.m' ≤ Fintype.card F)
(S : Finset (Fin P.m' → F))
(hS : ∀ z ∈ S, PcpAlgebra.TypedAccepts (P.circuitArith C h) z (pf.ev z))
(hmajority : Fintype.card F ^ P.m' < 2 * S.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) = answerVec F P.m ap ∧ LowDegree.coded (pf.g 1) = answerVec F P.m bp
Typed PCP soundness yields accepted prefixes and the entire decoded answer tapes, using the describer's exact tape relation.