The PCP of the answer reduction: its blocks, its checks, and Schwartz–Zippel #
Paper II's degree-d PCP for the combined succinct 6-decoupled SAT and 5-decoupled linear system
(Definitions defn:blocks_of_vars_circuit and defn:PCP_of_V_n_satisfied, II:8939–9013; the checks
of Observation obs:satisfiability_vs_PCP). Its variables are the wires of the circuit C that
describes the output indicator through three windows (lem:ar-window-describer): the window
A (a parity wire, then the ℓ bits of a cell of the first readable answer), the window B
(likewise for the second), the window C (a parity wire, then the 2ℓ + 3◇ + 6 bits of an index
of the table O), the three witness indices, the six signs, and the gates. The index of O is
itself the paper's S₀: the bits of the two linear answers' cells, of the three copies, and the six
signs of the decoupled system (the layout of MIPRE.Tailored.AnsRed.indTable).
PcpDims: the four sizesℓ, ◇, r, sand the positions of the blocks.Pcp: the eleven assignments —gA, gBonℓvariables,gOon2ℓ + 3◇ + 6, threegWonr, readable;gLa, gLbonℓand threegLon◇, linear — and the helpersαandβ.- The thirteen checks at a point (
Pcp.Passes): the formula check (FormulaCheck), the system check (SystemCheck), and eleven assignment checks (AssignCheck); as identities, each at every point of its own space (Pcp.Identities). - The checks as the vanishing of thirteen polynomials (
chkPolys,passes_iff), of degree at mostchkDeg dT d = dT + 6(d + 1)in each variable for a PCP of degreedand a circuit polynomial of degreedT(degreeOf_chkPolys_le). - The first step of the soundness of prop:completeness_and_soundness_of_PCP_for_V_n: passing on
a set of density more than
m · chkDeg / qmakes the check polynomials zero, by Schwartz–Zippel (chkPolys_eq_zero), so the checks hold identically (identities_of_dense). The second step, from the identities to the formula and the system, isMIPRE/Tailored/AnsRed/PcpSound.lean.
Two departures from the paper's text. The windows of the describer hold tape encodings
(0 ↦ 00, 1 ↦ 01), so the literal of a window at (π, u) is π · g(u) for the polynomial g
of the raw table: the tape encoding is affine in the table, and the paper's raw-table assignments
are kept. And a literal of the repository's clauses is true when its variable equals its sign
(Lit.pos), so its factor is g - sign where the paper writes g + ε + 1 with ε the
negated sign (fact:polynomial_condition_for_satisfiability). The certificates X_i (1 - X_i) are
the paper's zero_X, X (X + 1) in characteristic 2.
The blocks #
The proof #
A PCP (Definition defn:PCP_of_V_n_satisfied): the eleven assignments and the helpers. The
readable part is gA, gB, gO, gW, αR, βA, βB, βO, βW; the linear part is gLa, gLb, gL, αL, βLa, βLb, βL.
- gA : MvPolynomial (Fin L.ℓ) F
- gB : MvPolynomial (Fin L.ℓ) F
- gO : MvPolynomial (Fin L.oW) F
- gW : Fin 3 → MvPolynomial (Fin L.r) F
- gLa : MvPolynomial (Fin L.ℓ) F
- gLb : MvPolynomial (Fin L.ℓ) F
- gL : Fin 3 → MvPolynomial (Fin L.dm) F
- αR : Fin L.m → MvPolynomial (Fin L.m) F
- αL : Fin L.oW → MvPolynomial (Fin L.oW) F
- βA : Fin L.ℓ → MvPolynomial (Fin L.ℓ) F
- βB : Fin L.ℓ → MvPolynomial (Fin L.ℓ) F
- βO : Fin L.oW → MvPolynomial (Fin L.oW) F
- βLa : Fin L.ℓ → MvPolynomial (Fin L.ℓ) F
- βLb : Fin L.ℓ → MvPolynomial (Fin L.ℓ) F
Instances For
The checks #
An assignment check (eq:PCP_condition_1, eq:PCP_condition_2): g (1 - g) is the
certificate sum at the point x of its block.
Equations
- MIPRE.Tailored.AnsRed.AssignCheck g β x = ((MvPolynomial.eval x) g * (1 - (MvPolynomial.eval x) g) = ∑ i : Fin k, x i * (1 - x i) * (MvPolynomial.eval x) (β i))
Instances For
The formula check (eq:Tseitin_satisfiable_induced) at the point p, against the Tseitin
polynomial T of the circuit: T times the six literal factors — the window literals the parity
times the table polynomial — is the certificate sum.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The system check (eq:induced_system_is_satisfied) at the point x of the index space of
O: O times the equation ε_A g_{La} + ε_B g_{Lb} + Σ ε_i g_{L,i} - ε₀ is the certificate
sum.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The thirteen checks at a point (Definition defn:PCP_of_V_n_satisfied, Observation
obs:satisfiability_vs_PCP): the formula check, the system check at the point's index of O, and
the eleven assignment checks at the point's blocks.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The thirteen checks as identities: each holds at every point of its own space — what the honest PCP satisfies (the completeness of prop:completeness_and_soundness_of_PCP_for_V_n) and what a PCP passing often enough must satisfy (its soundness).
Equations
- One or more equations did not get rendered due to their size.
Instances For
A PCP satisfying the identities passes the checks at every point.
The checks as polynomials #
The polynomial of an assignment check, on the variables of the PCP through the embedding v
of its block.
Equations
- MIPRE.Tailored.AnsRed.chkAssign v g β = (MvPolynomial.rename v) (g * (1 - g) - ∑ i : Fin k, MvPolynomial.X i * (1 - MvPolynomial.X i) * β i)
Instances For
The polynomial of the system check, on the index space of O.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The polynomial of the formula check.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The thirteen polynomials of the checks, on the variables of the PCP.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The checks pass at a point exactly when the thirteen polynomials vanish there.
Degrees #
A certificate sum Σ_i X_i (1 - X_i) c_i has degree at most d + 2 in each variable.
The degree bound of the thirteen check polynomials, for a PCP of degree d and a circuit
polynomial of degree dT: each of the six literal factors counted separately.
Equations
- MIPRE.Tailored.AnsRed.chkDeg dT d = dT + 6 * (d + 1)
Instances For
A factor X_π · g ∘ v - X_ε or g ∘ v - X_ε of the formula check has degree at most d + 1
in each variable.
The thirteen check polynomials have degree at most chkDeg dT d in each variable, for a
PCP of degree d and a circuit polynomial of degree dT.
Soundness by Schwartz–Zippel #
The check polynomials of a PCP passing often are zero
(prop:completeness_and_soundness_of_PCP_for_V_n, soundness, by Schwartz–Zippel): a PCP of degree
d passing the thirteen checks at every point of a set of density more than m · chkDeg / q
has all thirteen check polynomials zero.
The checks hold identically when their polynomials vanish.
The soundness of the PCP, first step (prop:completeness_and_soundness_of_PCP_for_V_n): a PCP
of degree d passing the thirteen checks on a set of points of density more than m · chkDeg / q
satisfies them identically.