* Phase 1 + 3: eval-form prover and MSB/LSB convention layer

- Sumcheck/Src/EvalForm.lean: honestProverMessageEvalsAt eval-form round-poly
  primitive, layered on existing residualSum infrastructure
- Sumcheck/Properties/EvalForm.lean: consistency lemma proving
  eval (fun _ => c) (honestProverMessageAt …) = honestProverMessageEvalsAt …,
  plus pointwise Lagrange-interpolation corollary at the d+1 nodes
- Sumcheck/Src/Convention.lean: Convention | MSB | LSB inductive,
  reverseFin involution, honestProverMessageAtConv with MSB↔LSB equivalence
  via CMvPolynomial.rename reverseFin
- Adds eval_rename helper for CompPoly bridge

Pure addition: no edits to existing prover/verifier/Properties files.
lake build clean (warnings only).

* Tests: oracle test cases for eval-form sumcheck

Add Sumcheck/Tests/EvalFormTests.lean exercising
`honestProverMessageEvalsAt` (Phase 1 deliverable) on three concrete
polynomials over ZMod 17:

* n=1 multilinear  p(x)     = 1 + 2x
* n=2 multilinear  p(x,y)   = 1 + x + y + xy
* n=3 non-multilin p(x,y,z) = x^2 y + z

For each, pin the round-0 evaluations at c ∈ {0,1,2} via `native_decide`
(matching the existing test style — cf. ProtocolTests, VerifierTests),
plus the round-0 sumcheck consistency check (G_0(0)+G_0(1) = honest claim).

Example 2 also simulates one full round-0 → round-1 transcript with
challenge r_0 = 5: pin round-1's two evaluations, compute G_0(r_0) by
manual Lagrange interpolation through the two round-0 points, and assert
the verifier's between-rounds consistency Sigma_c G_1(c) = G_0(r_0).

These values are intended as a correctness oracle for `effsc` (the
external Rust eval-form prover). The file's docstring documents the
convention, how to consume the values as golden tests, and how to extend
with new polynomials.

* Phase 1 polish

- Clean lint warnings in `Sumcheck/Properties/EvalForm.lean`:
  * `point_snoc_eq_cons` now lives outside the `Field/Fintype/DecidableEq`
    `variable` block so the unused-section-vars lint stops firing.
  * Replace two `simpa [snoc_split_eq] using …` / `simpa [honest_split_eq]
    using …` with `have := <split-lemma>; omega` so the unnecessarySimpa
    lint stops firing.

- Land the deferred universal-`r` interpolation corollary
  `eval_honestProverMessageAt_eq_interpolate_eval`, replacing the
  Phase 1 fallback that only proved the equality at the `d+1`
  interpolation nodes.

  The proof routes the round polynomial through a univariate bridge:
    `toUnivariate : CMvPolynomial 1 𝔽 → Polynomial 𝔽`
  defined as `MvPolynomial.finOneEquiv 𝔽 ∘ CPoly.fromCMvPolynomial`,
  with two coherence lemmas:
    * `eval_toUnivariate` — Polynomial.eval r (toUnivariate q)
        = CMvPolynomial.eval (fun _ => r) q
      (proved via `MvPolynomial.eval_eq_eval_mv_eval'` plus
      `MvPolynomial.ringHom_ext` to identify `eval Fin.elim0` with
      `isEmptyAlgEquiv 𝔽 (Fin 0)` as ring homs).
    * `natDegree_toUnivariate_le` — natDegree of the bridge is bounded by
      `degreeOf 0 q`, via `MvPolynomial.natDegree_finSuccEquiv` and
      `Polynomial.natDegree_map_eq_of_injective`.
  The corollary follows from `Lagrange.eq_interpolate_of_eval_eq` after
  bounding the bridge's degree by the hypothesis `degreeOf 0 ≤ d`.

- The earlier at-the-nodes corollary `lagrange_interpolate_eq_eval_at_node`
  is retained as the operational form (the verifier only checks the
  `d+1` nodes).

- Update the file-level docstring to reflect the new bridge structure.

* Phase 4: IP-native eval-form instance

Add a parallel `PublicCoinProtocol` instance whose round prover messages
are evaluation tuples `Fin (d+1) → 𝔽` rather than symbolic
`CMvPolynomial 1 𝔽`. The verifier reconstructs each round's polynomial
via Mathlib's `Lagrange.interpolate` only when evaluating at its
challenge; the per-round sum-on-domain check uses the same interpolant
without symbolic-polynomial allocation.

Includes the statement bundle, transcript, protocol instance, honest
prover (consuming Phase 1's `honestProverMessageEvalsAt`), the eval-form
verifier checks, and the operational bridge lemmas
(`interpolateRound_eval_at_node`, `interpolateRound_eval_on_domain`,
`sumOnDomain_honest_eq_symbolic`). The full bidirectional
`verifierAccepts_iff` reduction depends on a univariate ↔ multivariate-1
polynomial bridge (Phase 1's "type-conversion swamp") and is left to a
follow-up phase per the plan's scope-adjustment fallback.

* Phase 2: multilinear eval-table prover

Add the evaluation-table prover from the Rust `multilinear_sumcheck.rs`
algorithm, mirroring `compute_sumcheck_polynomial` and `fold` natively
in MSB convention.

Src/MultilinearProver.lean:
* `EvalTable n 𝔽 := CompPoly.CMlPolynomialEval 𝔽 n` — length-`2^n` vector
  state, indexed by Boolean assignments.
* `boolPoint_msb` — turn `Fin (2^n)` into a Boolean point under MSB
  (variable 0 most-significant), composed with `Sumcheck.reverseFin`.
* `toEvalTable` — materialise a `CMvPolynomial n 𝔽` as its MSB
  evaluation table over the Boolean hypercube.
* `computeS0S1_msb` — `(s0, s1)` round message: sums over the low/high
  halves of the table.
* `fold_msb_succ` / `fold_msb` — pointwise fold
  `t'[k] = t[k] + (t[k+2^m] - t[k]) * w`.
* `multilinearProverEvalForm` — round-by-round prover by structural
  recursion on `n`; emits a length-`n` list of `(s0, s1)` pairs.

Properties/MultilinearProver.lean (table-internal correctness):
* `getElem_toEvalTable`, `computeS0S1_msb_succ_def`,
  `getElem_fold_msb_succ` — clean unfoldings.
* `compute_correctness_table` (theorem (a), narrowed) — round-0 message
  on a materialised polynomial equals the explicit pair of low/high
  half sums of `eval`. The bridge to `honestProverMessageEvalsAt`
  domain-`[0,1]` form is documented as deferred since it requires
  MSB↔LSB rewrites at the spec layer.
* `fold_msb_succ_lerp_form` (theorem (b), narrowed) — pointwise
  algebraic invariant `lo + (hi - lo) * w` of the fold under
  `toEvalTable`. The full
  `toEvalTable (substRound0 w p) = fold_msb_succ w (toEvalTable p)`
  awaits a `substRound0` definition + `MLE_substitute_x0` (not in
  CompPoly yet).
* `multilinearProverEvalForm_length_and_head` (theorem (c), narrowed)
  + companion `_length` — the prover emits exactly `n` rounds and the
  head is `computeS0S1_msb` of the input table. Full transcript
  equivalence inducting through `fold_msb_succ` is deferred to once
  (b) is symbolically available.

No `sorry`. Each correctness theorem is narrowed to a fully closed
statement, with the deferred symbolic-spec bridges documented in the
file header for the next phase.

* Phase 2 follow-up: eval-form MSB/LSB convention bridge

Adds honestProverMessageEvalsAtConv mirroring the symbolic
honestProverMessageAtConv pattern, plus the four standard equivalence
lemmas. Lets the multilinear evaluation-table prover (natively MSB)
bridge to the symbolic spec without ad-hoc renaming at call sites.

Pure additive; no edits to existing prover/verifier code.
lake build clean.

* Phase 5(a): native two-oracle inner-product

Adds a native eval-form inner-product sumcheck whose prover never
materialises `f * g`. The hypercube walker `residualSumPair` multiplies
`f.eval pt * g.eval pt` *inside* the sum (the genuine sum-of-products,
not `(Σ f) · (Σ g)`).

New file `Sumcheck/IP/InnerProductNative.lean`:

* `residualSumPair` — two-oracle hypercube walker.
* `nativeHonestMessageEvalsAt` — eval-form per-round message at a
  single field point `c`, mirroring `honestProverMessageEvalsAt` but
  for the inner-product sum.
* `InnerProduct.NativeStatement` — bundle of `domain`, `claim`,
  `f`, `g`, three-node `evalPoints`, injectivity, `domain ⊆ evalPoints`,
  and per-variable multilinearity bounds for `f` and `g`.
* `NativeStatement.{toInnerProduct, Valid}` — forgetful map to the
  thin-wrapper statement and validity inherited from it.
* `residualSumPair_eq_residualSumWithOpenVars_mul` — sum-level
  equivalence: per-summand `(f * g).eval = f.eval * g.eval` then
  `sum_over_domain_recursive_congr`.
* `nativeHonestMessageEvalsAt_eq_thinWrapper` — the round-message
  equivalence to `honestProverMessageEvalsAt domain (f * g) …`.
* `nativeHonestMessageEvalsAt_tuple_eq_thinWrapper` — tuple-level
  corollary at the three eval nodes.
* `NativeStatement.toEvalFormStatement` — bridge into the Phase 4
  `SumcheckStatementEvalForm 𝔽 n 2`; `degree_le` is discharged via
  `SharpSAT.degreeOf_mul_le_c` plus the multilinearity bounds.

Purely additive: no existing files modified except `Sumcheck.lean` to
re-export the new module. No `sorry`. `lake build` clean.

* Phase 4 extension: full lift theorems

Closes the eval-form perfect-completeness lift on top of the Phase 4
floor: `sumcheck_hasPerfectCompleteness_evalForm` plus the supporting
honest-direction `verifierAccepts` reduction (`honest_evalForm_accepts_at`),
the Lagrange round-trip `interpolate_evaluate_round_trip`, and
`evaluate_interpolate_round_trip_honest` (eval-equivalence form for
honest round polynomials, leveraging Phase 1 polish's universal-r
interpolation theorem).

Soundness lift narrowed: ships the adversary-transport definitions
`liftEvalToSymbolic`, `liftEvalProverToSymbolic`, and the
eval-equivalence bridges `toUnivariate_liftEvalToSymbolic`,
`eval_liftEvalToSymbolic`. The full
`sumcheck_hasSoundnessError_evalForm` is deferred (documented gap):
the symbolic verifier's per-round `degreeOf 0 ≤ indDegreeK p i` check
is strictly stronger than the Lagrange interpolant's `≤ d` guarantee
when `indDegreeK p i < d`.

* Tests: MSB vs LSB convention oracle examples

Adds Example4 to EvalFormTests demonstrating the convention parameter is
non-vacuous. Uses an asymmetric multilinear p(x_0,x_1) = 1+2x_0+3x_1+5x_0x_1
where LSB and MSB round-0 messages differ:
  G_0^LSB(c) = 5 + 9c   (binds x_0 first)
  G_0^MSB(c) = 4 + 11c  (binds x_1 first)

Both satisfy the round-0 sumcheck identity G_0(0)+G_0(1) = honestClaim,
since the total sum over the hypercube is permutation-invariant.

Pure additive; build clean.

* Phase 5(a) Task 5: native two-oracle completeness lift

Adds nativeInnerProduct_perfectCompleteness via Phase 4 ext's
sumcheck_hasPerfectCompleteness_evalForm. The IP-framework Prover is
statement-keyed by SumcheckStatementEvalForm (which carries a single
polynomial), so the native two-oracle algorithm is an *implementation*
of the same mathematical object: sumcheckHonestProverEvalForm on
S.toEvalFormStatement matches nativeHonestMessageEvalsAt on (S.f, S.g)
pointwise, without ever materialising f * g.

Includes:
- toEvalFormStatement_claim_isCorrect: native validity ⇒ eval-form correct
- sumcheckHonestProverEvalForm_respond_native: pointwise equivalence
- nativeInnerProduct_perfectCompleteness: completeness via Phase 4 ext

Soundness still deferred (chained from Phase 4 ext deferral).

* Phase 5(a): native soundness lift via Phase 4 conditional soundness

Adds nativeInnerProduct_soundness conditional on UniformDegreePoly 2 (f*g).
Lifts the bound 2*n/|F| from sumcheck_hasSoundnessError_evalForm_uniform
through the toEvalFormStatement bridge.

The uniform hypothesis is restrictive (requires (f*g).degreeOf i = 2
for every i, equivalent to both f and g having non-trivial dependence
on every variable), but it's the cleanest way to transport soundness
through the IP-framework eval-form instance. Looser bounds for
non-uniform (f, g) are not lifted here.

* Phase 5(b) Task 1: RoundPolyEvaluator structure

Add a value-level structure mirroring effsc's RoundPolyEvaluator trait:
a polynomial-with-degree-bound bundle. Concrete instances follow.

The shape is intentionally minimal: an evaluator IS a polynomial together
with a per-variable individual-degree bound. The 'callback contribution'
of the Rust trait is virtualPolynomial.eval point, and the library's
hypercube iteration is honestProverMessageEvalsAt.

* Phase 5(b) Task 2: multilinearEvaluator instance

A 'd = 1' RoundPolyEvaluator built directly from a polynomial and a
per-variable multilinearity hypothesis. The shape is trivial — the
degree bound flows through unchanged — but it is the canonical
'multilinear evaluator' callers reach for in Phase 2 contexts.

simp lemma exposed for downstream rewriting.

* Phase 5(b) Task 3: innerProductEvaluator instance

A 'd = 2' RoundPolyEvaluator built from two multilinears f, g and
their per-variable bounds. The virtual polynomial is the symbolic
product f * g; the degree bound chains SharpSAT.degreeOf_mul_le_c with
Nat.add_le_add to land at <= 1 + 1.

This packages, as a generic evaluator, the same content that Phase 5(a)
already exposes via InnerProduct.NativeStatement.toEvalFormStatement —
useful when the caller wants a uniform RoundPolyEvaluator interface
across degrees rather than a bespoke statement bundle.

* Phase 5(b) Task 4: RoundPolyEvaluator -> SumcheckStatementEvalForm bridge

Plumb a RoundPolyEvaluator into a SumcheckStatementEvalForm by accepting
domain, claim, and evaluation-node data alongside the evaluator. The
degree bound transfers through E.virtualPolynomial_degree_le directly.

Mirrors the structural composition of effsc's CoefficientProver over a
RoundPolyEvaluator: the user supplies the per-pair contribution (i.e.
the virtual polynomial) once, and the library hands back the bundle the
IP framework consumes. Per-field simp lemmas exposed for downstream
rewriting.

* Phase 2 bridge: Task 1 — sumOverDomainRecursive_bool_eq_finSum

Define LSB/MSB Boolean point indexings boolFromFin_lsb / boolFromFin_msb
on Fin (2^n). Prove the LSB form matches boolPoint_msb after the
bit-reversal involution (definitionally for the MSB form), and
sumOverDomainRecursive [0,1] (·+·) 0 F = ∑ k : Fin (2^n), F (boolFromFin_lsb k)
by induction on n via a Fin 2 × Fin (2^n) ≃ Fin (2^(n+1)) packing.

* Phase 2 bridge: Task 2 — bit-reversal bijection finSum_lsb_eq_msb

Define bitReverseEquiv : Fin (2^n) ≃ Fin (2^n) by induction on n via
the lsbEquiv ∘ msbEquiv composition. Prove its computational content:
bit j of bitReverseEquiv n k equals bit n-1-j of k. This gives
boolFromFin_lsb (bitReverseEquiv n k) = boolFromFin_msb k pointwise,
and finSum_lsb_eq_msb follows from Equiv.sum_comp.

* Tests: multilinear eval-table prover oracle examples

* Phase 2 bridge: Task 3+4 — compute_correctness final bridge

Add compute_correctness_at_zero / compute_correctness_at_one / compute_correctness:
the eval-table prover's (s0, s1) round-0 message exactly matches
honestProverMessageEvalsAt [0,1] p ⟨0, _⟩ Fin.elim0 0 / 1.

Helpers:
- residual_point_round_zero: addCasesFun-form point at round 0 = Fin.cons c x.
- honestProverMessageEvalsAt_zero_unfold: spec → sumOverDomainRecursive over n.
- Fin_cons_zero / one _boolFromFin_msb_eq: boolPoint_msb on the low / high
  half of Fin (2^(n+1)) factors as Fin.cons 0/1 (boolFromFin_msb k).

Bridge chain: compute_correctness_table → split per half →
sumOverDomainRecursive_bool_eq_finSum (Task 1) → finSum_lsb_eq_msb (Task 2)
→ Fin_cons_*_boolFromFin_msb_eq → honestProverMessageEvalsAt_zero_unfold.

* Phase 2 bridge: suppress unused-section-var warnings via omit

* Phase 2 substRound0 primitive (definitions, eval lemmas deferred)

Adds substRound0 w p := bind₁ (Fin.cases (C w) X) p as a thin wrapper around
CompPoly's bind₁ machinery. Substitutes the round-0 variable of p with constant w.

Includes substRound0_C and substRound0_add (homomorphism shape). Eval lemmas
deferred — eval_substRound0 (unconditional) needs a CMvPolynomial-level
analogue of MvPolynomial.aeval_bind₁ (best upstreamed to CompPoly), and
eval_substRound0_multilinear needs the multilinear coefficient decomposition.

Documented as upstream-PR candidates: a more general substAt (i : Fin n) (w)
substitution plus the two eval lemmas would be the right primitive to land in
CompPoly. With those, Phase 2 multi-round induction (fold_correctness +
multi_round_correctness) becomes a few lines.

* chkpt

* chkpt: Sumcheck/IP/EvalForm.lean WIP

Sumcheck-only slice of the original d6f7e62 chkpt on
z-tech/vc-and-sumcheck-refactor (the VC/ Merkle tree from that commit
is left on the parent branch).

* Sumcheck/Tests: v4.29.1 fallout for eval-form oracle tests

Same playbook as the linear-codes branch bump: Mathlib.Algebra.Field.ZMod
no longer transitively re-exported from Mathlib.Data.ZMod.Basic, and the
default 200k heartbeats time out on the `#eval`-driven instance synthesis
under v4.29.1.

* Rename Sumcheck → SumcheckProtocol

Directory `Sumcheck/` → `SumcheckProtocol/`, root file
`Sumcheck.lean` → `SumcheckProtocol.lean`, library
`«Sumcheck»` → `«SumcheckProtocol»`. All 72 .lean files in
the tree updated (imports, namespaces, qualified refs).
README.md, CHANGELOG.md, and SumcheckProtocol/README.md
updated to match. Build green at 2635 jobs.

* P0 council fallout: pin CompPoly, drop FS stub, dead-code cleanup

- Pin CompPoly to rev 01609714 (was `master`); council flagged the
  unpinned dep as a CI risk
- Delete InteractiveProtocol/{Src,Properties}/FiatShamir.lean: the
  Properties file was a `sorry` placeholder returning `True`, and the
  Src structure had no external consumers. NIZK is now out of scope;
  any future ROM-FS work resurrects from git history
- Remove dead `have h : (by exact True) := by trivial` debug stub in
  Properties/Lemmas/Accepts.lean:25-30 (the `h` was never used)

* P0 council fallout: docs + CI + Nodup invariant

- Extend CI sorry/axiom audit to SumcheckProtocol/ + InteractiveProtocol/
  (was: LinearCodes/ + Upstream/ only; PM-flagged as embarrassing gap)
- Add SumcheckProtocol/doc/stability.md (Stable / Recently-landed /
  Partial / Noncomputable / Out-of-scope tiers) — mirror LinearCodes pattern
- Add AGENTS.md (AI-PR policy, heartbeat budget, branch hygiene)
- Correct README "Fully computable" claim — symbolic protocol is
  computable, eval-form layer is noncomputable pending barycentric fix
- Add `domain_nodup : domain.Nodup` field to SumcheckProtocolStatement,
  SumcheckProtocolStatementEvalForm, InnerProductStatement, NativeStatement;
  thread through constructors. Without it the claim inflates on repeated
  domain values and the soundness theorem silently assumes uniform F-sampling

* P0-9: delete noncomputable eval-form layer

Per the council punch list and the user's directive: the eval-form IP
wrapper existed for efficiency vs. the symbolic protocol, but its
`nextClaimEvalForm` / `sumOnDomainEvalForm` / `verifierCheckEvalForm`
defs route through `Lagrange.interpolate` from Mathlib, which is
`noncomputable` (depends on `Polynomial.commRing`). A noncomputable
"efficient" path is self-defeating — correctness is already provided
by the symbolic protocol.

Deleted:
- SumcheckProtocol/Src/EvalFormVerifier.lean
- SumcheckProtocol/IP/EvalForm.lean (1277 lines)
- SumcheckProtocol/IP/CoefficientProver.lean
- SumcheckProtocol/IP/InnerProductNative.lean
- SumcheckProtocol/Properties/EvalForm.lean

The eval-form *prover* (Src/EvalForm.lean::honestProverMessageEvalsAt)
is computable and remains, as does the VSBW multilinear prover in
Src/MultilinearProver.lean. If a future implementer wants to restore
a verifier on the eval tuples, they should define a scalar-level
barycentric evaluator (see doc/stability.md for sketch).

Drops the SumcheckProtocol README claim "eval-form is partial" — the
README is now honest. 2630 jobs build green.

* VSBW correctness: round-by-round soundness + fold_correctness + recurse

Three concrete additions on the council punch list:

1. soundness_per_round (Properties/Theorems/Soundness.lean):
   Public theorem exporting the per-round Schwartz-Zippel bound. The
   underlying lemma (prob_single_round_accepts_and_disagree_le) was
   proven internally; this lifts it to the public API with a clean
   GKR-friendly signature. Crypto council finding 1a.

2. fold_correctness (Properties/MultilinearProverBridge.lean):
   For multilinear p, toEvalTable (substRound0 w p) = fold_msb_succ w
   (toEvalTable p). The table↔substitution bridge. Conditional on
   EvalSubstRound0MultilinearHyp (the upstream CompPoly piece —
   pointwise eval property of substRound0 at multilinear variable 0).

3. multilinearProverEvalForm_recurse:
   Operational equation expressing the prover's recursive shape — the
   head is computeS0S1_msb of the table, the tail recurses on the
   eval-table of the substituted polynomial. Combined with (1)/(2)
   and a symbolic-side recursion lemma (HonestProverSubstRound0Hyp,
   not yet added), this inducts to full multi_round_correctness.

The conditional hypotheses (EvalSubstRound0Hyp,
EvalSubstRound0MultilinearHyp) live as Prop-valued defs in
Src/SubstRound0.lean. When upstream CompPoly lands eval_substAt,
each callsite supplies the proof and the hypotheses vanish.

Build green at 2439 jobs.

* docs: VSBW degree-d generalization design notes

Three options analysed for extending the eval-table prover to general
individual degree d > 1:

- Option A (keep EvalTable, generalize fold): doesn't work — the
  Boolean-hypercube representation can't carry the information needed
  for d ≥ 2.
- Option B (CoefficientProver, symbolic walk): general-purpose, ~2-3
  weeks. Resurrects the deleted scaffold with a computable verifier.
- Option C (ProductEvalTable for product polynomials): optimized for
  inner-product / GKR. Keeps VSBW's O(2^n) advantage. ~1-2 months.

Both Tracks 1 and 2 block on the same upstream CompPoly piece as
fold_correctness (eval_substAt + multilinear extension property),
plus a computable scalar-level barycentric evaluator.

Updated SumcheckProtocol/doc/stability.md to point to the new doc.

* Prove eval_substRound0 unconditionally

The pointwise-evaluation property of substRound0 is now a theorem in
SumcheckProtocol/Src/SubstRound0.lean, no longer parked on upstream
CompPoly:

  (substRound0 w p).eval b = p.eval (Fin.cons w b)

Proof goes through a general eval_bind₁_aux helper:

  (bind₁ f p).eval b = p.eval (fun i => (f i).eval b)

which is the universal property of bind₁: composition with eval factors
as eval of the substituted-then-evaluated map. Proven by packaging both
sides as RingHom CMvPolynomial n 𝔽 →+* 𝔽, transporting through
CPoly.polyRingEquiv to the MvPolynomial side, applying
MvPolynomial.ringHom_ext (agreement on C and X), and applying at p.

This unblocks the symbolic-side fold_correctness chain. Next steps:
prove the multilinear extension property (linear blend at variable 0),
drop the hypotheses from fold_correctness and multilinearProverEvalForm_recurse,
then close multi_round_correctness.

EvalSubstRound0Hyp and EvalSubstRound0MultilinearHyp Prop-valued defs
retained for downstream callers that still take them by hypothesis
(removable in a follow-up).

* Prove eval_substRound0_multilinear + drop hypotheses from fold_correctness chain

eval_substRound0_multilinear is now a theorem in SumcheckProtocol/Src/SubstRound0.lean:

  degreeOf 0 p ≤ 1 → (substRound0 w p).eval b
    = (1-w) * p.eval (Fin.cons 0 b) + w * p.eval (Fin.cons 1 b)

Proof route:
1. eval_substRound0 (already proven) converts LHS to p.eval (Fin.cons w b)
2. Bridge to MvPolynomial side via CPoly.eval_equiv
3. Mathlib's MvPolynomial.eval_polynomial_eval_finSuccEquiv expresses each
   evaluation as Polynomial.eval (C v) (finSuccEquiv R n f) lifted through
   (eval b)
4. Polynomial.eval_affine_of_natDegree_le_one (new local lemma) gives the
   linear blend formula for any Polynomial with natDegree ≤ 1
5. natDegree_finSuccEquiv plus degreeOf_equiv supplies the degree bound

With both eval lemmas now proven, fold_correctness and
multilinearProverEvalForm_recurse no longer take any hypotheses beyond
multilinearity at variable 0.

Build green at 2440 jobs.

* Land multi_round_correctness (modulo two named bridge hypotheses)

Adds the full inductive proof that the VSBW eval-table prover's i-th
output matches the symbolic spec's round-i message:

  (multilinearProverEvalForm challenges (toEvalTable p))[i.val]
    = (honestProverMessageEvalsAt [0,1] p i ch_prefix 0,
       honestProverMessageEvalsAt [0,1] p i ch_prefix 1)

The induction combines:
1. multilinearProverEvalForm_recurse (operational shape, landed unconditional)
2. compute_correctness (round-0 bridge, landed unconditional)
3. The IH applied to substRound0-substituted polynomial

Two named hypotheses remain to be dispatched separately, both pure
mathematical lemmas with no further upstream dependencies:

- HonestProverSubstRound0Bridge: symbolic-side recursion under substRound0.
  Provable from CPoly.eval_substRound0 (now proven) + careful Fin index
  manipulation through residualSumWithOpenVars.
- SubstRound0PreservesMultilinear: degreeOf (substRound0 w p) ≤
  degreeOf p (after the variable shift). Dispatchable via Mathlib's
  MvPolynomial.degreeOf_coeff_finSuccEquiv.

When both land, multi_round_correctness drops its hypotheses and becomes
unconditional. The full chain VSBW prover ↔ symbolic spec is then formal.

Build green at 2440 jobs.

* multi_round_correctness: bridge file actually elaborated, all 5 theorems live

The previous commits had `fold_correctness`, `multilinearProverEvalForm_recurse`,
and `multi_round_correctness` committed to MultilinearProverBridge.lean, but
the umbrella `SumcheckProtocol.lean` didn't import that file, so the proofs
were never elaborated. Build-green reports were technically true but
misleading — the bridge file was silently skipped.

This commit:

1. Adds `import SumcheckProtocol.Properties.MultilinearProverBridge` to the
   umbrella so the bridge is part of CI.

2. Fixes v4.29.1 fallout in helper lemmas (Codex-assisted):
   - `residual_point_round_zero` (line ~487): replaced brittle `rw [h0]`
     with an explicit `change` to the `Fin.castAdd` shape. The `rw` was
     failing because v4.29.1's stricter elaboration won't unify
     implicit-proof arguments on `Fin.cast`.
   - Line ~520: replaced the second `rw [h0]` with a `calc` using
     `congrArg` over `Fin.addCases`.
   - `honestProverMessageEvalsAt_zero_unfold` (line ~575): replaced
     downstream rewrite with a pointwise `calc`.
   - `multi_round_correctness` (line ~890): reworked to split `Fin`
     before dependent list rewriting, use branch-local `simp only`,
     explicit tail bounds, `let` bindings, and `Fin.cases` for the
     `Fin.cons` prefix equality.

3. Adjusts `eval_substRound0_multilinear` (Src/SubstRound0.lean) to drop
   the redundant `CPoly.` prefix inside its `namespace CPoly` declaration
   (the resolved name was previously `CPoly.CPoly.eval_substRound0_multilinear`
   which broke `rw` callers in the bridge).

End state: `lake build SumcheckProtocol` builds 2441 jobs clean. CI
sorry/axiom audit clean. The VSBW eval-table prover's correctness is now
formally bridged to the symbolic spec, modulo two named hypotheses
(HonestProverSubstRound0Bridge, SubstRound0PreservesMultilinear) which
are concrete next steps with no further upstream dependencies.

Co-Authored-By: Codex

* VSBW formally bridged: multi_round_correctness now unconditional

Codex landed both remaining bridge lemmas as concrete theorems:

- `honestProver_substRound0_bridge : HonestProverSubstRound0Bridge 𝔽`
  Symbolic-side recursion under substRound0. Proven by unfolding
  honestProverMessageEvalsAt to residualSumWithOpenVars and applying
  sum_over_domain_recursive_congr + CPoly.eval_substRound0 + careful
  Fin-cases analysis on the eval point.

- `substRound0_preserves_multilinear : SubstRound0PreservesMultilinear 𝔽`
  Degree preservation under substRound0. Proven by bridging to
  MvPolynomial through CPoly.polyRingEquiv, showing
  fromCMv (substRound0 w q) = Polynomial.eval (C w) (finSuccEquiv (fromCMv q))
  via ring-hom-extensionality, and using
  MvPolynomial.degreeOf_coeff_finSuccEquiv to bound the eval's degreeOf.

`multi_round_correctness` now drops both hypotheses — its only premise is
the actual multilinearity `hp_ml : ∀ i, p.degreeOf i ≤ 1`. The VSBW
eval-table prover is now formally certified to produce the same
transcript as the symbolic spec on multilinear polynomials.

Build green at 2441 jobs. Zero sorry, zero axiom in the umbrella.

Co-Authored-By: Codex

* SumcheckProtocol: collapse Convention layer to MSB-only

Drop the `Convention` LSB/MSB inductive and the `*Conv*` parameterized
wrappers in `Src/Convention.lean`; replace with direct MSB-only wrappers
`honestProverMessageAtMSB` / `honestProverMessageEvalsAtMSB`. LSB has no
non-streaming use case so the parameterization was just plumbing.

Killed the brittle `:= rfl` proof of `boolFromFin_msb_eq_boolPoint_msb`
in `Properties/MultilinearProverBridge.lean`: replaced with an explicit
`BitVec.toNat_ofFin` + `reverseFin_val` rewrite that no longer relies on
`BitVec.getLsb` / `BitVec.ofFin` unfolding by def-equal through three
layers of upstream definitions.

`EvalFormTests.lean` Example 4 updated to pin MSB-wrapper outputs
against raw LSB-spec outputs (the wrapper is non-vacuous on asymmetric
multilinears — kept as a regression guard).

Build green at 2441 jobs; `EvalFormTests` `#eval` outputs unchanged.

* chkpt

* Bump lean toolchain to v4.30.0-rc2 + repin CompPoly

Coordinated bump to match the base CompPoly is now built on (CompPoly
master rebased onto v4.30.0-rc2). Three pin moves in lockstep:

- lean-toolchain: v4.29.1 -> v4.30.0-rc2
- lakefile: mathlib v4.29.1 -> v4.30.0-rc2
- lakefile: CompPoly Verified-zkEVM@01609714 -> z-tech fork@e0fd375d
  (z-tech/cmvpoly-univariate-evalext-and-lawfulbeq); the comment notes
  this is temporary until the branch merges to Verified-zkEVM master,
  at which point we switch the URL back to upstream.

The CompPoly branch adds two helpers we'll consume in a follow-up:
- CPoly.lawfulBEqOfDecidableEq (collapses the LawfulBEq letI kludges in
  HonestRoundProofs.lean:407-422 and SoundnessLemmas.lean:759-761)
- CPoly.CMvPolynomial.eval_ext_univariate (degree-bounded univariate
  eval-extensionality, for the agreement_set_card_le contrapositive).

Zero Mathlib v4.30 API fallout across SumcheckProtocol, LinearCodes,
InteractiveProtocol, Upstream. Only noise: two push_neg deprecation
warnings in LinearCodes/MCA/RS/{ArrayBridge,MCABound}.lean (push_neg ->
push Not); non-fatal, deferred to a separate cleanup.

Builds green at 2476 jobs (SumcheckProtocol) and 2329 jobs (LinearCodes
default targets). Smoke-tested lawfulBEqOfDecidableEq as a drop-in at
the HonestRoundProofs kludge site before reverting; helper works.

* SumcheckProtocol: consume CompPoly helpers, drop three local kludges

Two LawfulBEq letI hand-builds and one open-coded Schwartz-Zippel chain
replaced by upstream-helper calls now that CompPoly @ e0fd375 ships
CPoly.lawfulBEqOfDecidableEq and CPoly.CMvPolynomial.eval_ext_univariate.

- HonestRoundProofs.lean (honestTranscript_roundPoly_eq_honestRoundPoly):
  17-line LawfulBEq record build collapses to
  `letI : LawfulBEq F := CPoly.lawfulBEqOfDecidableEq`. New import:
  CompPoly.Data.Classes.LawfulBEq.

- SoundnessLemmas.lean (accepts_on_challenges_dishonest_implies_bad):
  3-line `letI : LawfulBEq F := by classical exact inferInstance` becomes
  the same one-liner. Same new import.

- SoundnessLemmas.lean (agreement_set_card_le): 56-line ratio-shuffling
  proof (via prob_agreement_le_degree_over_field_size +
  countAssignmentsCausingAgreement bookkeeping + Q-cast munging) becomes
  a 10-line by_contra + CMvPolynomial.eval_ext_univariate application.
  The unused-after-this-change probabilistic chain stays in place since
  it's exported and may have other callers; only the local proof here is
  rewritten.

`push Not` replaces `push_neg` at the new use site to avoid introducing
fresh occurrences of the deprecated tactic.

Total diff: -65 / +15 across the two files. Build green at 2476 jobs.

* SumcheckProtocol: add residualSum_full_eq_eval bridge (Step 1/4 of partial-run)

Adds three lemmas in Hypercube.lean that together let downstream code
treat the existing `residualSum` as the partial-run residual primitive,
collapsing to the existing `p.eval challenges` final check at k = n:

- `residualSumWithOpenVars_zero_eq_eval`: the openVars = 0 base case,
  using a Fin.castAdd rewrite + `Fin.addCases_left` to bridge through
  the addCasesFun glue.
- `residualSumWithOpenVars_collapse_eq_eval`: openVars-generalised
  wrapper taking the `openVars = 0` evidence as a hypothesis (so subst
  works on the openVars binder).
- `residualSum_full_eq_eval`: the public-facing bridge for k = numVars,
  one-line corollary via `Nat.sub_self`.

No protocol changes yet — this is just the bridge needed for Step 2's
verifier rewrite (where `claims (Fin.last k.val) = residualSum domain
challenges p _` is the final check, recovering the current
`p.eval challenges` behavior when k = n).

Build green at 2476 jobs.

* SumcheckProtocol: k-parameterize verifier + protocol (Step 2/4 of partial-run)

Adds `k : Fin (n+1)` stop-parameter to `isVerifierAccepts` and
`sumcheckProtocol`. `k.val` is the number of rounds the protocol runs;
`k = ⟨n, _⟩` recovers the existing full-run behavior (final claim collapses
to `p.eval challenges` via `residualSum_full_eq_eval`).

Soundness and completeness theorems are *not yet* k-parameterized — that's
Step 3 of the epic. To keep this step's diff scoped, the downstream
properties/lemmas tree continues to operate on the full-run case via three
backward-compat aliases in `IP/Statement.lean`:

  abbrev sumcheckProtocolFull := sumcheckProtocol ⟨n, _⟩
  abbrev proverTranscriptFull := proverTranscript ⟨n, _⟩
  abbrev sumcheckHonestProverFull := sumcheckHonestProver ⟨n, _⟩

These are `abbrev`s so they're def-transparent for typeclass resolution
and proof bridging. Step 3 will remove them by properly k-parameterizing
the soundness/completeness theorems.

Touched 17 files:
- `Src/Verifier.lean`: `isVerifierAccepts` gains k param; final check now
  goes through `residualSum` instead of `eval`.
- `IP/Statement.lean`: protocol/honestProver/proverTranscript all gain k
  param; three `Full` abbrevs added at the bottom.
- `Properties/Events/Accepts.lean`: `AcceptsEvent` calls the new verifier
  with `⟨n, _⟩` internally; surface signature unchanged.
- `Properties/Lemmas/Accepts.lean`: simp set picks up
  `residualSum_full_eq_eval` to bridge the final-check shape.
- `Properties/Theorems/Completeness.lean`: same simp bridging in the
  full-eval case.
- `Properties/Lemmas/SoundnessLemmas.lean` (n=0 base case): explicit
  k = ⟨0, _⟩ argument + residualSum_full_eq_eval in the simp set.
- Eleven more files: mechanical rename
  `sumcheckProtocol`/`proverTranscript`/`sumcheckHonestProver` →
  their `Full`-suffixed variant.
- `Tests/TranscriptTests.lean`: pass `⟨2, by decide⟩` for the smoke test.

Build green at 2476 jobs across SumcheckProtocol; downstream LinearCodes
and InteractiveProtocol unchanged. All `#eval` outputs in tests preserved.

* SumcheckProtocol: delete orphaned agreement/counting probability chain

The Schwartz-Zippel-via-probability chain became dead code after the
`agreement_set_card_le` refactor in 7f4d8bf (which switched to
`CPoly.CMvPolynomial.eval_ext_univariate` from the bumped CompPoly).
Removing the orphaned modules + their unused imports.

Deleted (5 files, all callers gone):
- Properties/Events/Agreement.lean (AgreementEvent, AgreementAtEvent,
  agreementEvent_decidable, AgreementEvent_eval_equiv)
- Properties/Probability/Agreement.lean (probAgreementAtRandomChallenge)
- Properties/Probability/CountingAgreement.lean
  (countAssignmentsCausingAgreement)
- Properties/Probability/CountingPolynomials.lean (countAllAssignmentsN)
- Properties/Probability/Universe.lean (allAssignmentsN — was a thin
  alias for InteractiveProtocol's allChallenges)

Trimmed Properties/Lemmas/Agreement.lean from 47 lines to 9: removed
`prob_agreement_le_degree_over_field_size` and
`difference_poly_eq_zero_iff` (both only used by the dead chain). Kept
`differencePoly` since SoundnessLemmas still uses it for the
`eval_ext_univariate` invocation.

Updated 5 importing files:
- Properties/Probability.lean and Properties/Events.lean: drop dead imports.
- Properties/Probability/Challenges.lean: import
  InteractiveProtocol.Properties.Probability directly (was getting
  allChallenges transitively via the deleted Universe.lean).
- Properties/Lemmas/Accepts.lean: drop dead Events.Agreement import.
- Tests/ProtocolTests.lean: drop dead CountingPolynomials import.

Two import backfills where deleted modules were transitively pulling
in Mathlib.Algebra.Field.ZMod:
- Tests/InteractiveProtocolTests.lean
- IP/SharpSAT/IP.lean

Build green at 2016 jobs (was 2476 before deletion — 460 fewer build
units now that the dead chain is gone). Zero behavioural change.

* SumcheckProtocol: k-parameterize events + cascade (Phase 3a-3c)

Adds `k : Fin (n+1)` parameter to all event definitions in
`Properties/Events/`, threads it through `Properties/Lemmas/*` and
`Properties/Theorems/{Soundness,Completeness}`, and IP/Test consumers.

Events (Properties/Events/):
- BadRound.lean: `BadRound`, `LastBadRound`,
  `RoundDisagreeButAgreeAtChallenge` gain `k` param. Adds
  `honestRoundPolyAtK k domain p (ch : Fin k.val → 𝔽) (i : Fin k.val)`
  alongside the original `honestRoundPoly` (which keeps `Fin n` shape
  so existing proofs stay intact). Bridge lemma
  `honestRoundPolyAtK_full` is `rfl` — `honestRoundPolyAtK ⟨n, _⟩ = honestRoundPoly`
  for the full-run case.
- BadTranscript.lean: `BadTranscriptEvent` gains `k`.
- Accepts.lean: `AcceptsEvent`, `AcceptsOnChallenges`,
  `AcceptsAndBadTranscriptOnChallenges` gain `k`.

Lemmas (Properties/Lemmas/):
- BadTranscript, BadTranscriptAnalysis, Accepts, SoundnessLemmas: pass
  `⟨n, Nat.lt_succ_self n⟩` to every event call site (mechanical).
- SoundnessLemmas adds an `hh_eqK` bridge inside `agreement_set_card_le`'s
  caller — converts the existing `hh_eq : honestRoundPoly ... = h` to
  `honestRoundPolyAtK ⟨n'+1, _⟩ ... = h` via the rfl bridge lemma.

Theorems + Probability:
- Probability/Soundness.lean, Theorems/{Soundness,Completeness}: pass
  `⟨n, _⟩` explicitly to all event references.

IP + Tests:
- IP/InteractiveProtocol.lean and Tests/InteractiveProtocolTests.lean:
  pass `⟨n, _⟩` to AcceptsEvent / AcceptsOnChallenges calls.

Build green at 2016 jobs across SumcheckProtocol; partial-run protocol
remains operationally usable with full-run completeness/soundness still
proven. Subsequent commits will drop the `sumcheckProtocolFull` /
`proverTranscriptFull` / `sumcheckHonestProverFull` aliases now that the
events accept explicit k.

* SumcheckProtocol: drop Full aliases, pass k explicitly (Phase 3d)

Removes the three backward-compat abbrevs from IP/Statement.lean
introduced in commit e76eb2a:
- `sumcheckProtocolFull`
- `proverTranscriptFull`
- `sumcheckHonestProverFull`

Every downstream call site now passes `⟨n, Nat.lt_succ_self n⟩`
(or `⟨k, Nat.lt_succ_self k⟩` in size-indexed contexts, or
`⟨n' + 1, Nat.lt_succ_self _⟩` inside `cases n with | succ n'`)
explicitly to the underlying `sumcheckProtocol` / `proverTranscript` /
`sumcheckHonestProver` functions.

The council's "single sumcheckProtocol parameterised by k" API shape is
now in place: there is one protocol, one prover, one transcript builder,
all taking k. Full-run is just `k = ⟨n, _⟩`.

Touched 11 files:
- IP/Statement.lean: deleted the three abbrevs.
- IP/{InteractiveProtocol, InnerProduct, SharpSAT/IP}: explicit k.
- Properties/{Probability/Soundness, Theorems/Soundness}: explicit k.
- Properties/Lemmas/{BadTranscript, BadTranscriptAnalysis, SoundnessLemmas}: explicit k.
- Tests/{SharpSATTests, InteractiveProtocolTests}: explicit k
  (`⟨2, by decide⟩` for the n=2 smoke tests).

Build green at 2016 jobs. End-to-end completeness/soundness still proven
for the full-run case; partial-run case (k < n) operationally usable via
the same protocol/honest-prover API.

* SumcheckProtocol: partial-run smoke test (Phase 3e)

Adds `Tests/PartialRunTests.lean` exercising `sumcheckProtocol` at
non-trivial `k` on a concrete polynomial:

  p(x₀, x₁, x₂) = x₀·x₁·x₂ + 1 over ZMod 7
  domain = {0, 1}, honestClaim = 9 ≡ 2 mod 7

Smoke checks (all `native_decide`):
- honestClaim returns 2 mod 7 as expected.
- k = 1: honest prover transcript with challenge [3] accepts; residual
  check at the end of round 0 equals `residualSum domain [3] p _`.
- k = 2: honest transcript with challenges [3, 5] accepts; residual is
  `residualSum domain [3, 5] p _`.
- k = 3 (full run): honest transcript with [3, 5, 6] accepts; residual
  collapses to `p.eval [3, 5, 6]` via `residualSum_full_eq_eval`.

Confirms the partial-run protocol works end-to-end for all three k
values on the same polynomial - the unified k-parameterized API is
correct operationally.

Wired into the umbrella Tests.lean. Build green at 2017 jobs.

* SumcheckProtocol: add 4 k-parameterized helpers (Phase 3 cont.)

Adds the foundation helpers needed for k-parameterized soundness theorems:

- `acceptsEvent_rounds_ok_k`: rounds-OK part of AcceptsEvent for a
  partial-run transcript of length `k.val`. Threads `indDegreeK p ⟨i.val, _⟩`
  via the Fin lift.
- `acceptsEvent_round_facts_k`: per-round facts (verifier check + claims
  consistency) for round `i : Fin k.val`.
- `acceptsEvent_domain_sum_eq_claim_k`: domain-sum identity from
  an accepted partial-run transcript.
- `adversary_poly_degree_le_max_ind_degree_k`: round-`i` poly degree bound
  from a partial-run acceptance (`i : Fin k.val`).

All four are direct k-generalizations of the existing helpers, with `n`
replaced by `k.val` and the Fin index lifted via
`⟨i.val, lt_of_lt_of_le i.isLt (Nat.le_of_lt_succ k.isLt)⟩`.

Build green at 2017 jobs; existing helpers unchanged so no downstream
churn. These are foundation for `prob_single_round_accepts_and_disagree_le_k`
and the eventual k-parameterized headline theorems.

* chkpt

* SumcheckProtocol: k-parameterize soundness_per_round

* SumcheckProtocol: add 3 more k-helpers (acceptsEvent_final_ok_k,
acceptsEvent_domain_sum_eq_claim_of_honest_k, badTranscript_implies_lastBadRound_k)

- `acceptsEvent_final_ok_k` (Accepts.lean): partial-run version, asserts
  `t.claims (Fin.last k.val) = residualSum domain challenges p _` (note:
  residualSum, not eval — that's the partial-run final-check shape).
- `acceptsEvent_domain_sum_eq_claim_of_honest_k` (Accepts.lean): partial-run
  version of the domain-sum identity when the round-i polynomial is honest.
- `badTranscript_implies_lastBadRound_k` (BadTranscript.lean): direct k-version,
  uses honestRoundPolyAtK instead of honestRoundPoly.

Foundation for the not-yet-proven `accepts_and_bad_implies_exists_round_disagree_but_agree_k`
(blocked on two new helpers needed: a partial-run version of
`honest_last_round` that bridges to residualSum, and `honest_step_round_k`
that uses honestRoundPolyAtK throughout).

Build green at 2017 jobs.

* SumcheckProtocol: add honestRoundPolyAtK_eq_honestRoundPoly_of_extend bridge

Bridge lemma showing that `honestRoundPolyAtK k r i` equals
`honestRoundPoly r' iN` for any `Fin n → 𝔽` extension `r'` of the partial
challenges `r` that agrees on the first `i.val` positions. Lets the
partial-run analysis reuse existing full-run honest-round-poly machinery
(e.g. `honest_step_round`, `honest_last_round`) by padding `r` to `Fin n`.

Build green at 2017 jobs.

* Repin CompPoly to current z-tech branch tip (84e478d)

The previous pin e0fd375 was a stale rev — the z-tech fork branch
`cmvpoly-univariate-evalext-and-lawfulbeq` was rebased, leaving e0fd375
reachable only from a local branch on my machine, not on the GitHub
remote. Cloners (including aleph's CI) couldn't fetch it.

84e478d is the current remote tip and contains the same helpers
(`lawfulBEqOfDecidableEq`, `eval_ext_univariate`) we rely on.

`lake build` (bare) succeeds at 2470 jobs. Switch the pin back to
Verified-zkEVM/CompPoly when the branch lands upstream.

* Proof for soundness (#24)

Automated commit at 20260531_121101

Co-authored-by: aleph-prover[bot] <247409690+aleph-prover[bot]@users.noreply.github.com>

* chkpt

* Proof for soundness_k (#25)

Automated commit at 20260531_132404

Co-authored-by: aleph-prover[bot] <247409690+aleph-prover[bot]@users.noreply.github.com>

* chkpt

* Proof for soundness_dishonest_k (#26)

Automated commit at 20260531_135229

Co-authored-by: aleph-prover[bot] <247409690+aleph-prover[bot]@users.noreply.github.com>

* Proof for perfect_completeness_k (#27)

Automated commit at 20260531_141658

Co-authored-by: aleph-prover[bot] <247409690+aleph-prover[bot]@users.noreply.github.com>

* SumcheckProtocol: collapse soundness, soundness_dishonest into _k aliases

Now that `soundness_k` and `soundness_dishonest_k` are proven for general
`k : Fin (n+1)`, the hardcoded-n versions reduce to one-line specialisations
at `k = ⟨n, Nat.lt_succ_self n⟩`. Removes ~63 lines of duplicated proof
chains (union bound + accepts-bad reduction); existing downstream consumers
in `IP/InteractiveProtocol.lean` keep working unchanged via the alias.

`perfect_completeness` is left in place — its signature is slightly stronger
than `perfect_completeness_k` (no `domain_nodup` hypothesis required), so
it's not strictly redundant.

Build green at 2022 jobs.

* SumcheckProtocol: k-parameterize IP framework theorems

Adds `sumcheck_hasSoundnessError_k k` and `sumcheck_hasPerfectCompleteness_k k`
in `IP/InteractiveProtocol.lean` — partial-run-aware framework instances
that wrap `soundness_dishonest_k` and `perfect_completeness_k`. Old
hardcoded-n versions `sumcheck_hasSoundnessError` and
`sumcheck_hasPerfectCompleteness` collapse to one-line specialisations
at `k = ⟨n, Nat.lt_succ_self n⟩`.

Downstream user-facing theorems (`innerProduct_*`, `sharpSAT_*`) in
`IP/InnerProduct.lean` and `IP/SharpSAT/IP.lean` remain at full-run via
the alias; partial-run analogues would be one-liners off the new
`_k` framework theorems if a use case appears.

Build green at 2022 jobs.

---------

Co-authored-by: aleph-prover[bot] <247409690+aleph-prover[bot]@users.noreply.github.com>