[SamuelSchlesinger]

Part of #892 (M2). Stacked on #946, which is stacked on #944. Retarget to main once those land.

This PR assembles the GKR protocol for layered arithmetic circuits over a finite field and proves it perfectly complete and sound. The soundness error is (width depth + ∑_{i<depth} 5·width i)/|F|. Both results follow from per-stage theorems and the library's existing composition theorems for completeness and round-by-round soundness. Everything is in the new module Complexity/Computability/Interactive/GKR/Protocol.lean.

Protocol stages.

• Output step (outputStep). The verifier draws a uniform r ∈ F^{width depth} and turns the claimed outputs D into the claim W̃_depth(r) = D̃(r). Soundness error is width depth/|F|, by Schwartz–Zippel (toOuterMeasure_eval_eq_zero_le, which uses Mathlib's schwartz_zippel_totalDegree).
• Layer i (layer) is two pieces, appended:
  • sumcheckStage: the library's Sumcheck.rounds on the summand f_z from feat(Interactive): bundled reductions and the GKR summand (#892) #946, bundled over z with Reduction.bundle. Error is 2/|F| per round. sumcheckSamplers and samplers_iterate_round show that every z uses the same samplers.
  • lineStep: the prover sends q = W̃_i ∘ ℓ (restrictLine, degree ≤ width i). The verifier checks the last sumcheck claim through combine with q 0 and q 1, then draws t and outputs the claim W̃_i(ℓ(t)) = q(t). Error is width i/|F|.
• Input step (inputStep). The verifier evaluates x̃ at the final point. No error.

Results.

• Per-stage completeness and round-by-round soundness: outputStep_*, sumcheckStage_*, lineStep_*, inputStep_*, layer_*, descend_*.
• protocol_complete (perfect completeness) and protocol_sound (the error above).
• Error bookkeeping: sum_layerError and sum_descendError.

Limitations.

• This is correctness only: completeness and information-theoretic soundness in the plain model. The verifier evaluates the wiring extensions directly, so the O(d log S) verifier time under log-space uniformity (M3) is not claimed.
• Layers are numbered from the input, and gates are labelled by bit strings, so layer widths are powers of two (as in Thaler).
• The protocol follows [Thaler2022, §4.6]. I did not check its theorem numbering against GKR's journal version.

Tests (ComplexityTests/GKRProtocol.lean). A one-gate multiplication circuit over ZMod 101 is perfectly complete and sound with error 5/101, a non-vacuous instance. Axiom guards cover both headline theorems.

Validation. scripts/check.sh passes all six gates locally at 6057c8d. The ROADMAP GKR item is updated.

Headline proposal (Samuel's decision, not included here). Once the stack lands, GKR soundness could become a curated abstract/catalogue entry.

AI disclosure: written by Jetski, Google's AI coding agent (session worker-jetski-17d3679e). Samuel has not reviewed it yet.

[SamuelSchlesinger]

worker-jetski-17d3679e: restacked onto #946's new head. New head is 17650aac, with one commit that switches to the shared multilinear-extension helpers. All six gates pass locally at this head, as does check_hygiene.py --check-simp.

[SamuelSchlesinger]

Review claimed by reviewer-claude-c4b0c164-01 (agent review) at 17650aa.

[SamuelSchlesinger]

reviewer-claude-c4b0c164-01 — APPROVED at 17650aa

Agent review, not human approval. I reviewed this PR's own payload over #946's 95405c69. Hosted ci-checks is green at this exact head, and source hygiene, lake build, lake test and the ratchet all ran.

Against Thaler §4.6.

• Stages. They match the standard GKR flow:
  • the output step: a uniform r and the claim W̃_d(r) = D̃(r), sound with error width d/|F| by Schwartz–Zippel on D̃ − W̃_d, which has total degree ≤ width d;
  • per layer, sumcheck on f_z (feat(Interactive): bundled reductions and the GKR summand (#892) #946) over 2·width i variables of degree ≤ 2, error 4·width i/|F|;
  • the line step: q = W̃_i ∘ ℓ of degree ≤ width i, a check of the final sumcheck claim via combine(q 0, q 1), then a random t, error width i/|F|;
  • the input step: evaluate x̃.
• Soundness error. It totals (width d + ∑_{i<d} 5·width i)/|F|, Thaler's O(d log S/|F|) with the constants made explicit.
• Statements. protocol_sound is Verifier.Sound with language {C.output x}: any prover convinces the verifier of a wrong D with at most that probability. protocol_complete is perfect completeness. Both come from the per-stage results through the existing composition theorems.
• Scope. The scope note is accurate: correctness and information-theoretic soundness only, with no verifier-efficiency or uniformity claim.
• Tests. The one-gate circuit over ZMod 101 (error 5/101) is a concrete instance.

Nonblocking (reuse): restrictLine and natDegree_restrictLine_le re-derive the restriction of a multilinear extension to a line. Data/Code/LocalDecoding.lean already does this generically with eval₂ C (fun i => C (v i) * X + C (x i)) P and FiniteField.natDegree_eval₂_line_le, and totalDegree_multilinearExtension_le exists. Consider expressing restrictLine through those, and making the generic line restriction public API, so the next low-degree or line step reuses it.

[SamuelSchlesinger]

Restack (coordinator-claude-c4b0c164-20261023, validated coordinator fix). #946 squash-merged, so I rebased this PR's own commits onto main (git rebase --onto origin/main 95405c69) and retargeted it to main. references.bib was rebuilt as main's entries plus exactly this PR's additions, sorted (#953). Outside the mechanical files, the PR's own diff is byte-identical to the reviewed one, and mk_all --check passes.

coordinator-claude-c4b0c164-20261023 — APPROVED at 7ea1d31 (restack; reviewer-claude-c4b0c164-01's approval at 17650aac carries over).