noncomputable def NPCompleteness.BoolFormula.arithEval {R : Type u_1} [CommRing R] (σ : ℕ → R) : BoolFormula → R

Arithmetization of a Boolean formula: lifts a Boolean formula φ to a polynomial expression over a commutative ring R using the standard encoding true ↦ 1, false ↦ 0, ¬x ↦ 1 - x, x ∧ y ↦ x * y, x ∨ y ↦ x + y - x*y. This is the foundation of the sum-check protocol used to show #SAT ∈ IP.

noncomputable def NPCompleteness.BoolFormula.partialCount (φ : BoolFormula) (m i : ℕ) (presets : Fin i → Bool) : ℕ

Partial count: number of satisfying assignments of φ over m variables, where the first i variables are fixed by presets and the remaining m - i are quantified. Used to express intermediate sums in the sum-check protocol.

noncomputable def NPCompleteness.BoolFormula.countSatFin (φ : BoolFormula) (m : ℕ) : ℕ

Count of satisfying assignments of φ indexed by the first m Boolean variables. Equivalent to #SAT for the formula φ when m bounds its variable indices.

structure SharpSATInIP.SharpSATEncoding (Γ : Type) : Type

An encoding of #SAT instances ⟨φ, k⟩ (a Boolean formula together with a count) as strings over the tape alphabet Γ. The roundtripping laws decode_encode and encode_decode make the encoding a bijection onto its image.

• encode : NPCompleteness.BoolFormula × ℕ → List Γ
• decode : List Γ → Option (NPCompleteness.BoolFormula × ℕ)
• decode_encode (p : NPCompleteness.BoolFormula × ℕ) : self.decode (self.encode p) = some p
• encode_decode (w : List Γ) (p : NPCompleteness.BoolFormula × ℕ) : self.decode w = some p → self.encode p = w

def SharpSATInIP.SharpSAT_enc {Γ : Type} (enc : SharpSATEncoding Γ) : Set (List Γ)

The language #SAT realised over the alphabet Γ via enc: {w | enc(w) = ⟨φ, k⟩ and k = #sat(φ)}, i.e. encodings of ⟨φ, k⟩ where φ has exactly k satisfying assignments.

structure SharpSATInIP.SumCheckEncoding (Γ : Type) extends SharpSATInIP.SharpSATEncoding Γ : Type

A SumCheckEncoding extends a SharpSATEncoding with the auxiliary data needed to run the sum-check protocol:

• a finite field ZMod q (with q ≠ 0),
• a fixed number of random bits per field element (bitsPerField) with a conversion coinsToField,
• encode/decode functions for both a single field element and a triple of field elements (used by the verifier to send a challenge and by the prover to send the three values v₀, v₁, v_r per round).

• encode : NPCompleteness.BoolFormula × ℕ → List Γ
• decode : List Γ → Option (NPCompleteness.BoolFormula × ℕ)
• decode_encode (p : NPCompleteness.BoolFormula × ℕ) : self.decode (self.encode p) = some p
• encode_decode (w : List Γ) (p : NPCompleteness.BoolFormula × ℕ) : self.decode w = some p → self.encode p = w
• q : ℕ
• hq_ne : NeZero self.q
• bitsPerField : ℕ
• hbits_pos : 0 < self.bitsPerField
• coinsToField : (Fin self.bitsPerField → Bool) → ZMod self.q
• encodeTriple : ZMod self.q → ZMod self.q → ZMod self.q → List Γ
• decodeTriple : List Γ → Option (ZMod self.q × ZMod self.q × ZMod self.q)
• decode_encodeTriple (a b c : ZMod self.q) : self.decodeTriple (self.encodeTriple a b c) = some (a, b, c)
• encodeField : ZMod self.q → List Γ
• decodeField : List Γ → Option (ZMod self.q)
• decode_encodeField (x : ZMod self.q) : self.decodeField (self.encodeField x) = some x

noncomputable def SharpSATInIP.arithPartialSum {q : ℕ} [NeZero q] (φ : NPCompleteness.BoolFormula) (m : ℕ) (challenges : ℕ → ZMod q) (i : ℕ) (z : ZMod q) : ZMod q

The univariate polynomial that the honest prover sends in round i of the sum-check protocol, evaluated at point z: with the first i variables fixed to the previously chosen field challenges, variable x_i set to z, sum over all Boolean assignments of the remaining m - i - 1 variables of arithEval φ.

noncomputable def SharpSATInIP.sumCheckVerifier {Γ : Type} (enc : SumCheckEncoding Γ) : InteractiveProofs.Verifier Unit Γ

The verifier in the sum-check protocol for #SAT. In each of the m rounds it extracts random field-element challenges from its coin tape and sends them to the prover. After all rounds it checks (i) that each prover-message triple (v₀, v₁, v_r) satisfies v₀ + v₁ = previously claimed value, and (ii) that the final claim equals arithEval φ at the chosen random point.

noncomputable def SharpSATInIP.sumCheckHonestProver {Γ : Type} (enc : SumCheckEncoding Γ) : InteractiveProofs.Prover Γ

The honest prover for the sum-check protocol on #SAT. In round i it sends the triple (v₀, v₁, v_r) where v_b = Σ_{x_{i+1},…,x_{m-1}} arithEval φ with x_0,…,x_{i-1} set to past challenges and x_i = b (or b = r, the current verifier challenge).

theorem SharpSATInIP.acceptProb_ge_of_all_accept {Q Γ : Type} [DecidableEq Γ] (V : InteractiveProofs.Verifier Q Γ) (P : InteractiveProofs.Prover Γ) (w : List Γ) (n numRounds : ℕ) (h : ∀ (coins : Fin n → Bool), InteractiveProofs.runProtocol V P w n coins numRounds = true) : V.acceptProb P w n numRounds ≥ 2 / 3

If the verifier accepts on every coin sequence then the acceptance probability is 1 ≥ 2/3. Used as the completeness side of the IP membership argument.

theorem SharpSATInIP.acceptProb_le_of_all_reject {Q Γ : Type} [DecidableEq Γ] (V : InteractiveProofs.Verifier Q Γ) (P : InteractiveProofs.Prover Γ) (w : List Γ) (n numRounds : ℕ) (h : ∀ (coins : Fin n → Bool), InteractiveProofs.runProtocol V P w n coins numRounds = false) : V.acceptProb P w n numRounds ≤ 1 / 3

If the verifier rejects on every coin sequence then the acceptance probability is 0 ≤ 1/3. Used to handle the degenerate (decode-failure) branch of the sum-check soundness argument.

theorem SharpSATInIP.sumCheck_completeness {Γ : Type} [DecidableEq Γ] (enc : SumCheckEncoding Γ) (w : List Γ) (φ : NPCompleteness.BoolFormula) (k : ℕ) (hdec : enc.decode w = some (φ, k)) (hk : k = φ.sharpSat) (coins : Fin (w.length * enc.bitsPerField) → Bool) : InteractiveProofs.runProtocol (sumCheckVerifier enc) (sumCheckHonestProver enc) w (w.length * enc.bitsPerField) coins w.length = true

Completeness of the sum-check protocol: if w encodes ⟨φ, k⟩ with k = #sat(φ), then for every coin tape the verifier accepts when run against the honest prover. This is the easy direction of #SAT ∈ IP.

theorem SharpSATInIP.schwartz_zippel_numAccepting_bound {Γ : Type} [DecidableEq Γ] (enc : SumCheckEncoding Γ) (w : List Γ) (φ : NPCompleteness.BoolFormula) (k : ℕ) (hdec : enc.decode w = some (φ, k)) (hk : k ≠ φ.sharpSat) (P' : InteractiveProofs.Prover Γ) : (sumCheckVerifier enc).numAccepting P' w (w.length * enc.bitsPerField) w.length * 3 ≤ 2 ^ (w.length * enc.bitsPerField)

Soundness bound via Schwartz–Zippel: if w encodes ⟨φ, k⟩ with k ≠ #sat(φ), then for any (possibly dishonest) prover P', the number of coin sequences on which the sum-check verifier accepts is at most 2^(n)/3 where n is the length of the coin tape. This is the quantitative form of the soundness guarantee Pr[V accepts] ≤ 1/3.

theorem SharpSATInIP.sumCheck_soundness {Γ : Type} [DecidableEq Γ] (enc : SumCheckEncoding Γ) (w : List Γ) (hw : ∀ (φ : NPCompleteness.BoolFormula) (k : ℕ), enc.decode w = some (φ, k) → k ≠ φ.sharpSat) (P' : InteractiveProofs.Prover Γ) : (sumCheckVerifier enc).acceptProb P' w (w.length * enc.bitsPerField) w.length ≤ 1 / 3

Soundness of the sum-check protocol: if w is not in #SAT (either it fails to decode or it decodes to ⟨φ, k⟩ with k ≠ #sat(φ)), then no prover can make the verifier accept with probability greater than 1/3.

theorem SharpSATInIP.sharpSAT_in_IP {Γ : Type} [DecidableEq Γ] (enc : SumCheckEncoding Γ) : InteractiveProofs.InIP (SharpSAT_enc enc.toSharpSATEncoding)

The main theorem of this file: #SAT ∈ IP. Given any SumCheckEncoding of ⟨φ, k⟩ instances, the sum-check protocol (verifier + honest prover) is an interactive proof system for the language SharpSAT_enc with polynomially many rounds and coins, completeness ≥ 2/3 and soundness ≤ 1/3.