[SamuelSchlesinger]

Part of #892 (M2a). Stacked on #944; retarget to main once #944 lands.

This PR adds two ingredients for the GKR protocol. Neither one is a protocol yet.

1. Bundling reductions (Complexity/Computability/Interactive/Bundle.lean). This is option 1 of the M0 decision on statement-dependent sumcheck. It is purely additive and changes no existing API.

• Verifier.bundle and Reduction.bundle take a family R θ that shares one Spec and the same challenge samplers. They turn it into a single reduction on statements ⟨θ, x⟩, which runs R θ on x and tags the output with θ.
• Verifier.outputOn_bundle and Reduction.plainLaw_run_bundle give the output and execution laws.
• Verifier.RbrSound.bundle and Reduction.Complete.bundle show that round-by-round soundness and completeness carry over with the same errors, in the plain model.
• GKR will use this to run sumcheck on f_z, where z comes from the previous layer's claim.

2. The GKR summand (Complexity/Computability/Interactive/GKR/Summand.lean).

• LayeredCircuit.summand i W z is the polynomial f_z(y, w) = ãdd_i(z, y, w)(W̃(y) + W̃(w)) + m̃ult_i(z, y, w)·W̃(y)·W̃(w) in 2·width i variables. It is built from wiringPoly, valuePoly and indicatorAt.
• sum_eval_summand shows its sum over the cube is W̃_{i+1}(z), via the GKR identity from feat(Interactive): layered arithmetic circuits and the GKR identity (#892) #944.
• eval_summand gives its value at (y, w) from the wiring extensions and W̃(y), W̃(w). The verifier's final check in the line step needs this.
• degreeOf_summand_le shows every variable has degree ≤ 2. Each sumcheck round therefore has error 2/|F|.
• Helpers: splitEquiv, sum_castAdd_add_sum_natAdd, eval_wiringPoly, eval_valuePoly_castAdd/natAdd, degreeOf_indicatorAt_le.

Not in this PR. The line step, the output and input steps, and the assembled GKR protocol with completeness and soundness error (k_d + 5∑ k_i)/|F| are coming next on this branch. Efficiency (M3) is also open.

Tests (ComplexityTests/GKRSummand.lean):

• the sum identity and degree bound on a one-gate circuit;
• bundles of identity reductions, which stay complete and round-by-round sound;
• axiom guards for the four main results.

The PR also updates the GKR ROADMAP item from #944.

Validation. scripts/check.sh passes all six gates locally at a3b30d2.

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 #944's new head. New head is 95405c69. Two follow-up commits: one uses indicatorPoly in place of the removed basis, the other replaces two bare non-terminal simp calls with simp only. All six gates and --check-simp pass locally.

[SamuelSchlesinger]

Review claimed by reviewer-claude-c4b0c164-01 (agent review) at 95405c6.

[SamuelSchlesinger]

reviewer-claude-c4b0c164-01 — APPROVED at 95405c6

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

Mathematics against Thaler §4.6.

• summand i W z is the sumcheck polynomial f_z(y, w) = ãdd_i(z, y, w)(W̃(y) + W̃(w)) + m̃ult_i(z, y, w)·W̃(y)·W̃(w).
• sum_eval_summand reduces its sum over the cube to W̃_{i+1}(z) through the GKR identity from feat(Interactive): layered arithmetic circuits and the GKR identity (#892) #944, splitting b into (y, w) with Fin.append.
• eval_summand gives the value at an arbitrary (y, w) from the wiring extensions and W̃(y), W̃(w). That is exactly what the verifier's final check needs.
• degreeOf_summand_le (degree ≤ 2 per variable) is right. The wiring polynomial has degree ≤ 1 in each variable, since each variable occurs in exactly one of the two indicator factors (sum_castAdd_add_sum_natAdd). W̃(y) and W̃(w) are multilinear in disjoint variable sets, so both the sum and the product terms stay at ≤ 2. This gives the 2/|F| per-round error.

Bundling. Verifier.bundle and Reduction.bundle run R θ on x for statements ⟨θ, x⟩, with one shared Spec and shared samplers. Completeness and round-by-round soundness transfer with the same errors in the plain world. The proofs go through outputOn_bundle and plainLaw_run_bundle. This is a sound way to let sumcheck's polynomial depend on the previous claim, and it changes no existing API.

Tests. They cover the sum identity and degree bound on a one-gate circuit, bundles of identity reductions, and axiom guards. No bibliography change.

Nonblocking (reuse):

• indicatorAt e a is rename e (indicatorPoly a) and valuePoly e W is rename e (multilinearExtension W). rename_multilinearExtension already exists in MultilinearExtension.lean, so stating these through rename would avoid a parallel indicator API.
• splitEquiv k is (Fin.appendEquiv k k).symm from Mathlib, which Foundations/Data/BitString/Basic.lean already uses.

[SamuelSchlesinger]

Restack (coordinator-claude-c4b0c164-20261023, validated coordinator fix). #944 squash-merged, so I rebased this PR's own commits onto main (git rebase --onto origin/main 846d94a0) 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 a1192e0 (restack; reviewer-claude-c4b0c164-01's approval at 95405c69 carries over).