chore(SplitFold): docstring and attribute hygiene follow-up to #670

[alexanderlhicks]

Follow-up to #670, which was merged as-is because none of these were blocking. Docstring and
attribute hygiene only — no statement, definition or proof term changes semantics.

Docstrings

• splitNth_eval_comp_pow referenced splitNth_def, which Clean-up 🧼 of the SplitFold.lean #670 renamed to eq_sum_splitNth.
• The module docstring and that same docstring both advertised Polynomial.foldNth, which does
  not exist anywhere in the repo (git grep -E '(def|abbrev) foldNth' → 0 hits). The file's fold
  operation is FoldingPolynomial.polyFold; pointed at it, and at
  polyFold_eq_sum_of_splitNth for the connection to splitNth.
• eq_sum_splitNth and splitNth_degree_le used /- … -/ rather than /-- … -/, so the file's
  key identity had no docstring at all. Promoted both (pre-existing, not from Clean-up 🧼 of the SplitFold.lean #670).
• Noted in splitNth that the n = 0 branch is unreachable because Fin 0 is uninhabited.

Attributes and names

• Dropped @[simp] from splitNth_degree_le and passed it explicitly to the one aesop
  call that needs it. It is an inequality, so as a global simp lemma it can only rewrite the goal
  to True — but it was also load-bearing invisibly: folding_polynomial_eq_sum_splitNth
  relied on the attribute without naming it, and removing the attribute alone gives
  unsolved goals at that proof. Making the dependency explicit keeps the proof honest and lets
  the global attribute go.
• splitNthNoncomputable_of_nz → private lemma splitNthNoncomputable_of_neZero. It is a
  @[simp] lemma about the private definition splitNthNoncomputable, so it was putting a simp
  lemma with an inaccessible LHS constant into the global simp set; its sibling
  splitNthNoncomputable_coeff was already private. Also spelled out nz → neZero.
• splitNthNoncomputable_eq_splitNth → splitNth_eq_splitNthNoncomputable: the name was the
  wrong way round relative to the statement, which is
  splitNth f n = splitNthNoncomputable f n.

Deprecation sweep

• Polynomial.eval_finset_sum → Polynomial.eval_finsetSum (4 call sites in
  Fri/RoundConsistency.lean), which was emitting deprecation warnings on every build.

Validation

./scripts/validate.sh green. The two remaining warnings in Fri/RoundConsistency.lean
(overlapping instance parameters at L28, empty-line-in-command at L76) are pre-existing on main
and untouched here.

One further change was tried and reverted: discharging splitNth's unreachable n = 0 branch
with absurd i.2 (by omega) instead of returning f. It is tidier in principle, but it breaks
splitNth_coeff's aesop proof, and rewriting a working proof for a cosmetic gain is not worth
it. Left the junk value with a comment explaining why it is unreachable.

[github-actions]

🤖 PR Summary

https://github.com/ark-lang/ark-lib/pull/674

---

Statistics

Metric	Count
📝 Files Changed	2
✅ Lines Added	16
❌ Lines Removed	17

---

Lean Declarations

✏️ Removed: 2 declaration(s)

ArkLib/Data/Polynomial/SplitFold.lean (2)

• lemma splitNthNoncomputable_of_nz {f : 𝔽[X]} {n : ℕ} [inst : NeZero n] {i : Fin n} :
• private lemma splitNthNoncomputable_eq_splitNth {n : ℕ} {f : 𝔽[X]} :

✏️ Added: 2 declaration(s)

ArkLib/Data/Polynomial/SplitFold.lean (2)

• private lemma splitNthNoncomputable_of_neZero {f : 𝔽[X]} {n : ℕ} [inst : NeZero n] {i : Fin n} :
• private lemma splitNth_eq_splitNthNoncomputable {n : ℕ} {f : 𝔽[X]} :

---

sorry Tracking

• No sorrys were added, removed, or affected.

---

📋 **Additional Analysis**

No findings.

---

📄 **Per-File Summaries**

• ArkLib/Data/Polynomial/SplitFold.lean: The module docstring and the docstrings of eq_sum_splitNth and splitNth_degree_le were updated to improve clarity and reflect the renaming of foldNth to polyFold. The lemma splitNthNoncomputable_of_nz was renamed to splitNthNoncomputable_of_neZero, made private, and had its @[simp] attribute removed; the lemma splitNthNoncomputable_eq_splitNth was renamed to splitNth_eq_splitNthNoncomputable. The @[simp] attribute was also removed from splitNth_degree_le. The proofs of eq_sum_splitNth and folding_polynomial_eq_sum_splitNth were updated to use the renamed lemmas, with the latter also gaining splitNth_degree_le as a simp hint in its aesop block.
• ArkLib/ProofSystem/Fri/RoundConsistency.lean: Renamed the lemma eval_finset_sum to eval_finsetSum in three uses within the proof of generalised_round_consistency_completeness. No definitions, signatures, or logical content changed; the diff is a mechanical rename of a helper lemma reference.

---

Last updated: 2026-08-05 14:17 UTC.

[github-actions]

Build Timing Report

• Commit: c5a05f1
• Message: chore(SplitFold): docstring and attribute hygiene follow-up to Clean-up 🧼 of the SplitFold.lean #670
• Ref: alh/splitfold-cleanup
• Comparison baseline: 646fb08 from current base of main.
• Measured on ubuntu-latest with /usr/bin/time -p.
• Commands: clean build rm -rf .lake/build && lake build; warm rebuild lake build; validation wrapper ./scripts/validate.sh.

Measurement	Baseline (s)	Current (s)	Delta (s)	Status
Clean build	782.95	578.17	-204.78	ok
Warm rebuild	2.31	3.17	+0.86	ok
Validation wrapper	2.47	2.31	-0.16	ok

Incremental Rebuild Signal

• Warm rebuild saved 575.00s vs clean (182.39x faster).

This compares a clean project build against an incremental rebuild in the same CI job; it is a lightweight variability signal, not a full cross-run benchmark.

Slowest Current Clean-Build Files

Showing 20 slowest current targets, with comparison against the selected baseline when available.

Current (s)	Baseline (s)	Delta (s)	Path
49.00	73.00	-24.00	ArkLib/ProofSystem/Stir/Combine.lean
45.00	68.00	-23.00	ArkLib/Data/CodingTheory/GuruswamiSudan/Basic.lean
44.00	56.00	-12.00	ArkLib/Data/CodingTheory/ProximityGap/BCIKS20/AffineLines/BWMatrix.lean
44.00	54.00	-10.00	ArkLib/Data/CodingTheory/ProximityGap/BCIKS20/AffineSpaces.lean
44.00	64.00	-20.00	ArkLib/Data/CodingTheory/ProximityGap/DG25/MainResults.lean
42.00	59.00	-17.00	ArkLib/Data/CodingTheory/JohnsonBound/Lemmas.lean
38.00	43.00	-5.00	ArkLib/Data/CodingTheory/ProximityGap/AHIV22.lean
31.00	43.00	-12.00	ArkLib/Data/CodingTheory/BerlekampWelch/Condition.lean
31.00	41.00	-10.00	ArkLib/Data/CodingTheory/ProximityGap/Folding.lean
28.00	39.00	-11.00	ArkLib/OracleReduction/LiftContext/Reduction.lean
26.00	33.00	-7.00	ArkLib/Commitments/Functional/KZG/FunctionBinding/EvaluationBindingConflict.lean
26.00	35.00	-9.00	ArkLib/ProofSystem/Binius/BinaryBasefold/Prelude.lean
24.00	33.00	-9.00	ArkLib/OracleReduction/Security/RoundByRound.lean
24.00	36.00	-12.00	ArkLib/Commitments/Functional/KZG/Binding.lean
24.00	30.00	-6.00	ArkLib/Data/CodingTheory/DivergenceOfSets.lean
23.00	30.00	-7.00	ArkLib/Data/CodingTheory/JohnsonBound/Basic.lean
19.00	16.00	+3.00	ArkLib/Data/CodingTheory/ProximityGap/AffineGenerator.lean
19.00	20.00	-1.00	ArkLib/Data/CodingTheory/PolishchukSpielman/Existence.lean
19.00	22.00	-3.00	ArkLib/Data/Polynomial/Indicator.lean
19.00	27.00	-8.00	ArkLib/Data/Polynomial/FoldingPolynomial.lean