Effective parameters for the classical PCP

The odd extension degree makes the field admissible. Its size is large enough for the classical majority argument, and both power-of-two dimensions divide the field size. It is also eventually larger than every fixed power of 8 (Q + 1) m' (pcpParams_field_eventually_large): the degree carries the square of s = size Q + size m' + 3, and 8 (Q + 1) m' < 2^s, so (8 (Q + 1) m')^e < 2^{s e} ≤ q once s ≥ e. Answer reduction's low-degree test needs a field polynomially larger than m' with an exponent this module need not know; the degree stays polylogarithmic (fieldDegree_le).

noncomputable def MIPRE.TM.CookLevin.Pad.fieldBase (n T Q σ : ℕ) : ℕ

The base of the field degree: 8 (Q + 1) m' < 2^{fieldBase}.

Equations

• MIPRE.TM.CookLevin.Pad.fieldBase n T Q σ = Q.size + (MIPRE.TM.CookLevin.Pad.outerDim n T Q σ).size + 3

noncomputable def MIPRE.TM.CookLevin.Pad.fieldDegree (n T Q σ : ℕ) : ℕ

An odd degree giving at least 82 field elements per outer coordinate, and eventually more than any fixed power of 8 (Q + 1) m'.

Equations

• MIPRE.TM.CookLevin.Pad.fieldDegree n T Q σ = 2 * (MIPRE.TM.CookLevin.Pad.fieldBase n T Q σ ^ 2 + (MIPRE.TM.CookLevin.Pad.outerDim n T Q σ).size) + 7

noncomputable def MIPRE.TM.CookLevin.Pad.pcpParams (n T Q σ : ℕ) : SAT.PcpParams

The complete classical PCP parameters.

Equations

• MIPRE.TM.CookLevin.Pad.pcpParams n T Q σ = { k := MIPRE.TM.CookLevin.Pad.fieldDegree n T Q σ, m := MIPRE.TM.CookLevin.Pad.innerDim T σ, s := MIPRE.TM.CookLevin.Pad.gateCount n T Q σ }

theorem MIPRE.TM.CookLevin.Pad.pcpParams_outer (n T Q σ : ℕ) : (pcpParams n T Q σ).m' = outerDim n T Q σ

theorem MIPRE.TM.CookLevin.Pad.pcpParams_odd (n T Q σ : ℕ) : Odd (pcpParams n T Q σ).k

theorem MIPRE.TM.CookLevin.Pad.pcpParams_field_large (n T Q σ : ℕ) : 82 * (pcpParams n T Q σ).m' ≤ (pcpParams n T Q σ).q

theorem MIPRE.TM.CookLevin.Pad.power_dvd_of_le {j k : ℕ} (h : 2 ^ j ≤ 2 ^ k) : 2 ^ j ∣ 2 ^ k

theorem MIPRE.TM.CookLevin.Pad.pcpParams_outer_dvd (n T Q σ : ℕ) : (pcpParams n T Q σ).m' ∣ (pcpParams n T Q σ).q

theorem MIPRE.TM.CookLevin.Pad.pcpParams_inner_dvd (n T Q σ : ℕ) : (pcpParams n T Q σ).m ∣ (pcpParams n T Q σ).q

theorem MIPRE.TM.CookLevin.Pad.pcpParams_field_eventually_large (e n T Q σ : ℕ) : 2 ^ e ≤ Q → (8 * ((Q + 1) * (pcpParams n T Q σ).m')) ^ e ≤ (pcpParams n T Q σ).q

The field is eventually large: for every exponent e, once Q ≥ 2^e the field has at least (8 (Q + 1) m')^e elements.

theorem MIPRE.TM.CookLevin.Pad.fieldDegree_le (n T Q σ : ℕ) : fieldDegree n T Q σ ≤ 2 * ((Q + outerDim n T Q σ + 3) ^ 2 + outerDim n T Q σ) + 7

The field degree is polylogarithmic in Q m': at most 2 ((Q + m' + 3)^2 + m') + 7.

noncomputable def MIPRE.TM.CookLevin.Pad.fieldBaseU : Cost.PolyTimeFun ParamInput Cost.Unary

The field degree's base, in unary.

Equations

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

@[simp]

theorem MIPRE.TM.CookLevin.Pad.length_fieldBaseU (p : ParamInput) : List.length (fieldBaseU.toFun p) = fieldBase p.1 p.2.1 p.2.2.1 p.2.2.2

noncomputable def MIPRE.TM.CookLevin.Pad.fieldDegreeU : Cost.PolyTimeFun ParamInput Cost.Unary

The field degree in unary, for the existing Shoup modulus program.

Equations

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

theorem MIPRE.TM.CookLevin.Pad.fieldDegreeU_length (p : ParamInput) : List.length (fieldDegreeU.toFun p) = (pcpParams p.1 p.2.1 p.2.2.1 p.2.2.2).k

noncomputable def MIPRE.TM.CookLevin.Pad.fieldDegreeProg : Cost.PolyTimeFun ParamInput ℕ

Compute the extension degree from binary parameters without expanding the field.

Equations

• MIPRE.TM.CookLevin.Pad.fieldDegreeProg = MIPRE.Cost.PolyTimeFun.unaryToBin.comp MIPRE.TM.CookLevin.Pad.fieldDegreeU

theorem MIPRE.TM.CookLevin.Pad.fieldDegreeProg_apply (p : ParamInput) : fieldDegreeProg.toFun p = fieldDegree p.1 p.2.1 p.2.2.1 p.2.2.2

noncomputable def MIPRE.TM.CookLevin.Pad.pcpParamsProg : Cost.PolyTimeFun ParamInput (ℕ × ℕ × ℕ)

The actual program for the three fields of PcpDecider.paramsProg.

Equations

• MIPRE.TM.CookLevin.Pad.pcpParamsProg = MIPRE.TM.CookLevin.Pad.fieldDegreeProg.pair MIPRE.TM.CookLevin.Pad.paddingParams

theorem MIPRE.TM.CookLevin.Pad.pcpParamsProg_apply (n T Q σ : ℕ) : pcpParamsProg.toFun (n, T, Q, σ) = ((pcpParams n T Q σ).k, (pcpParams n T Q σ).m, (pcpParams n T Q σ).s)