Cleanup master plan: full fork assessment — slop removal, prize-research isolation, and the road to an upstream PR

[lalalune]

Full audit of lalalune/ArkLib (fork/main e66366b36+) vs upstream Verified-zkEVM/ArkLib (merge-base d61905b25, 2026-07-07; upstream only 5 trivial commits ahead). Fork is 14,415 commits / ~12,170 tracked files / +2.94M lines over upstream. This is the complete plan for what to delete, move, finish, consolidate, and eventually PR upstream. The upstream PR is Phase 4 — not yet.

Provenance: five parallel deep audits + a dedicated cruft sweep, 2026-07-09. Counts are measured (git diff --name-only d61905b25..fork/main aggregations, git ls-tree -r -l fork/main, tip-tree greps).

---

0. TL;DR

• 91% of the delta is the δ prize campaign*: 4,259 files under ProximityGap/ (upstream: 23), 2,341 of them Frontier/ rungs, plus 30 MB scripts/probes and a 1,173-file kb.
• Verdict on naming: ProximityGap/ is legitimately named — keep the name, evict the campaign. Upstream defines the directory as proximity-gaps literature formalization (BCIKS20/DG25/AHIV22) + protocol-facing abstractions (Basic, Folding, MCAGenerator, ProximityGenerators) consumed by BatchedFri/Stir/Whir. That is what it should contain — nothing else.
• The campaign is a research program, not library content. Canonical home: top-level Research/ProximityPrize/ Lean lib target on branch research/proximity-prize; end-state a separate repo (lalalune/rs-proximity-gaps already exists) via lake require once churn stabilizes. Invariant: Research imports ArkLib, never the reverse — this single rule makes the upstream PR fall out for free.
• The "core API blocker" dissolves on inspection: Lattice2, GSFactorExtract, CapacityBounds have zero real protocol consumers (their importers are campaign files); Hab25ConjectureGlue's only ProofSystem consumers are Whir/MCAConjecture* files that are themselves campaign work squatting in ProofSystem/. Only Errors.lean (17 external importers) has genuine library character.
• Honesty flag: the tree is sorry-free, but carries 9 named axiom declarations and 151 *Residual open-hypothesis declarations across 82 files. "Done" was partly achieved by converting holes into named axioms/hypotheses — that is the real remaining proof debt and must never be silently discharged.
• The upstream-worthy core: Binius/BinaryBasefold/FRIBinius/RingSwitching Binius closeout: remove residual hypotheses and restore focused build validation #313 closeout (sorry-free, needs consolidation), ~8 general ToMathlib lemma files (of 354!), ~10 modified shared-Data files incl. a genuine Fin.castSum correctness bug-fix.

---

1. DELETE — pure cruft, zero knowledge loss (git history retains all)

1a. Scratch & experiment mass

Target	Size/count
scripts/probes/**	4,724 files, ~30 MB (3,893 .py; incl. .err/.out/empty files); zero CI references
scripts/{rust-pg,wf,cuda-pg,conjectures,deltastar-grind}	~89 files, ~710 KB; CI-unwired
Root-level scratch	205 files: _iNNN.json, _357_*.md/.patch, _ll_*.lean, _tmp_*.lean, _my_equiv_backup.lean, _ent2.txt(empty), _i357_* mega-notes (0.5 MB each)
Root duplicate insight-logs	DISPROOF_LOG.md (1.1 MB), _disproof_log.md (0.7 MB), _dl_main.md (0.5 MB), _dossier_local.md — all stale copies of the canonical PG ledger
Root project-log strays	AUDIT_LEDGER.md, journal.md, PAPERS_NEEDED.md, hd_peak.py, audit.sh
audit/ dir	3 files, stale 2026-06-10 snapshot

1b. Cruft sweep finds (new)

• 10 committed arXiv/paper PDFs — docs/references/proximity-gap-paley-spectrum/*.pdf, ~6.4 MB of copyrighted papers. Replace with citation entries in kb/sources (which already exists for exactly this).
• Committed GitHub-issue archaeology: docs/kb/audits/issue357-comments-archive{,-final}.json (~2.2 MB), _357_comments_all.jsonl (0.6 MB), _issue232_*, _issue304_*.
• macOS AppleDouble file: ._deepband_extremal.md.
• Mojibake Windows-path filename: C：UsersAdministratorarklib_a03_comments.json (0.7 MB).
• Stray artifacts in the Lean tree: ToMathlib/SpartanBricks.lean.bak, OracleReduction/FiatShamir/StateRestorationTransport.lean.patch, Binius/.../Steps/FinalSumcheckExtractorDraft.wip, Binius/BinaryBasefold/docs/reversal-cluster-diagnosis-2026-06-24.md, ProximityGap/_444_issue_comment_draft.md, Frontier/Template.lean (scaffold template).
• ~20 empty files (probe _out/_err.txt and root _ent* leftovers).
• scripts/cuda-pg/results-growthlaw-*/rho4.out and similar result dumps.

1c. Repo bloat & branches

• docs/kb/_generated/declarations.json = 32.9 MB (largest blob in the repo), dedup-report.md = 1.8 MB — both regenerated by kb-generated.yml on every push. Gitignore the two big ones; keep the small citations/references JSONs if CI needs them.
• 10 stale automation/kb-generated-<sha> remote branches + review codex/r382-half-radius-mds-line, integrate/goal-2026-07-09 if merged.
• Superseded kb renderings: DOSSIER-v2 (75 KB), deltastar-444-phd-thesis*.md (111 KB + 35 KB), DELTASTAR_444_ESSAY_{I..IV}, PAPER_UnifiedDefect, FINAL_PAPER duplicates — dossier v3 subsumes all.
• "Nubs" check: NubsCarson's 209 commits were all Prove δ* — complete research dossier for the RS proximity-gap prize (successor to #407) #444/The sub-Johnson supply wall: the remaining statement of the deep-band MCA programme (successor to #371) #389 prize research confined to _scratch_proofs/, which is already untracked on HEAD — nothing of his ships; no dedicated action needed.

Est. Phase-1 shrink: ~75 MB and ~5,300 files, no proof surface touched.

---

2. RESTORE ProximityGap/ + CREATE Research/ProximityPrize/

2a. ProximityGap/ on main returns to canonical shape

1. Upstream's 23-file skeleton (our modified Basic, BCIKS20/Curves diff-reviewed against upstream's).
2. Our genuine extensions of the same papers, in upstream's paper-keyed subdirectory convention: the real parts of our 145-file BCIKS20/ subtree (ListDecoding, ErrorBound, WeightedAgreement — the latter gated on §3.1), real DG25/ additions.
3. Errors.lean (ε-accounting API) beside Basic.
   No new names for library content — upstream's names ARE the names (no ProximityGap/Core/).

2b. Everything else → Research/ProximityPrize/ (branch research/proximity-prize)

• Own lake lib target; PROXIMITY_PRIZE_WORKBENCH.lean is its root module (it already aggregates the machine-checked spine).
• Moves: all 2,341 Frontier/ rungs (incl. the 0.6 MB CampaignProvenIndex.lean import index), 149 _probe/_wf/_scratch files, the 39-file QRWeil* adapter family, 105 _R1xx rungs, one-off numeric instances (F17×9, Fermat257×4, 65537×2, F41×2), 16 ALL-CAPS narrative .lean files, ~1,700 top-level research files, Lattice2, GSFactorExtract, CapacityBounds, Hab25ConjectureGlue.
• Campaign tendrils outside PG move too: ProofSystem/Whir/{Hab25WindowMCA, MCAConjectureEllaryReduction, MCAConjecturePairReduction}; the ~300 paper/prize-named ToMathlib/ files (BCIKS20*, BKR06*, Beta*, Bridge2*, CS25*, CZ25*, AGL2x, Gauss/Paley/Wick/Saddle/Keystone); campaign bridges in GuruswamiSudan/ (real GS machinery stays); prize-support Data/Polynomial infra (RationalFunctionsCore +3027 etc.) travels with its consumers.
• Knowledge corpus lives beside the code: Research/ProximityPrize/{DISPROOF_LOG.md (2.78 MB, 482 refutation certificates — the irreplaceable anti-repeat ledger), DOSSIER.md (v3 content, unversioned filename — git is the version), kb/papers/, kb/sources/, AGENTS.md}. Zero .md under ArkLib/** (currently 45–48). The nested duplicate kb (ProximityGap/docs/kb/, ~26 files) folds in or dies.
• The 862 datestamped kb session notes + 16 round-notes + mega-notes (297 KB deltastar-100-attacks/README, 447 KB refute-round-25-lessons) drop — conclusions are distilled into LOG+dossier; history retains them.
• Strict gates (laundering, zero-hole census, axiom audit) run over BOTH lib targets — the research branch keeps the honesty contract.
• website/{deltastar-paper,truthmining} + their Cloudflare workflows accompany the research branch (they deploy; keep only if wanted).
• Rule: Research → ArkLib imports only, never reverse.

---

3. FINISH / CLOSE OUT (real work)

1. 9 named axioms: BCIKS20 weighted_correlated_agreement_* ×4 + large_agreement_set_on_curve_implies_correlated_agreement['] ×2 (= the paper's weighted Theorem 1.2 — real formalization project), Steps/Fold.lean foldKnowledgeStateFunction_toFun_full + foldOracleVerifier_rbrKnowledgeSoundness, CyclotomicRing/Subfield/Field.lean no_selfReciprocal_factor. Prove, or register as documented external assumptions with issue refs.
2. 151 *Residual declarations / 82 files: triage — honest campaign-conditionals (move with Research), Binius grant-out-of-scope (documented in docs/wiki/Binius_Closeout_Audit.md, fine), plain unfinished (finish).
3. DuplexSponge *Paper cluster (15 files, OracleReduction/FiatShamir/DuplexSponge/Security/): structurally incomplete; finish before OracleReduction upstreaming.
4. Binius WIP hotspot: BinaryBasefold/Relations.lean (20 TODO-family markers), Basic.lean (8), Steps/Fold.lean (7) — resolve or convert to documented boundaries.
5. Prove δ* — complete research dossier (v3) for the RS proximity-gap prize (successor to #464) #466 stays open — it IS the research; the honesty contract forbids closing it without the wall.

---

4. CONSOLIDATE / REFACTOR

• One-lemma-per-file explosion: Binius Soundness/ (30+ micro-files), OracleReduction/Composition/Sequential/Append* (~40 micro-files) — merge into upstream-conventional file counts.
• ToMathlib split: keep ~8 general candidates (BalogSzemerediGowers, SumProduct, AppendHelpers, AveragingExistence, BivariateDegreeToolkit, BivariateGradedDvd, CoeffExtract, CyclotomicPatternInjectivity); everything paper-named moves (§2b). Delete ToMathlib/README.md if stale.
• ArkLibScratch.Issue62 namespace in ProofSystem/BCS/ErrorAccounting.lean — rename; scratch namespaces can't ship.
• Adopt upstream's CommitmentScheme/ retirement: fork still tracks the legacy dir (4 files) upstream deleted — migrate remains into Commitments/Functional/, delete.
• Comment slop pass over the kept surface: change-narration, session-log comments, campaign archaeology in docstrings — headers describe the math, not the hunt.
• AGL24* (119 files), GMMDS (50), GuruswamiSudan (44), ListDecoding (45) under CodingTheory: same research-drift flavor — triage each family lib-vs-Research with the §2b rule.

---

5. UPSTREAM PR CARVE-OUT (Phase 4 — later)

1. Rebase over origin/main (5 commits: Rq lemma move refactor: move constRq and Rq degree/coef lemmas into Rq.lean Verified-zkEVM/ArkLib#621 + CI tweaks — trivial).
2. Dependency re-pointing (the hard blocker): lalalune/VCV-io → Verified-zkEVM/VCV-io v4.30.0; lalalune/CompPoly → Verified-zkEVM/CompPoly v4.30.0; fork-only PolyFun dep upstreamed-or-dropped; doc-gen4 v4.29.0 → v4.30.0; regen manifest. (Note: this pinning is also why the auto-update workflow can never succeed — see Updates available but manual intervention required #468 diagnosis.)
3. Exclude fork-only workflows: deltastar-cloudflare, truthmining-cloudflare, sorry-tracker.
4. PR contents: consolidated Binius/RingSwitching closeout; the 8 general ToMathlib picks; reviewed shared-Data improvements (Fin/Basic castSum bug-fix + induction_three/four, Fin/Sigma, Fin/Tuple/Lemmas cleanup, Matrix/Vandermonde, MvPolynomial/Multilinear, CodingTheory/Basic/{Distance,LinearCode}, Data/Probability/Instances, Polynomial/SplitFold after review); BCIKS20/DG25 paper-extension files from §2a. The PR then reads as "extend BCIKS20/DG25 formalizations + Binius closeout + shared fixes" — reviewable.

---

6. EXECUTION ORDER

• Phase 1 — mechanical (no proof risk): all of §1; ~75 MB / ~5,300 files gone; gitignore _generated/{declarations.json,dedup-report.md}; prune branches; kb dedup.
• Phase 2 — structural: restore ProximityGap/ canonical shape; create Research/ProximityPrize lib + research/proximity-prize branch; move the campaign + tendrils; CI green on both.
• Phase 3 — quality: §4 consolidations, §3 axiom/Residual triage, comment pass.
• Phase 4 — upstream: §5. Not yet.

[lalalune]

Naming & factoring verdict: ProximityGap/ is legitimately named — restore it to what the name means; the campaign moves to a top-level Research/ library

What the name canonically means (measured, not guessed): upstream Verified-zkEVM/ArkLib defines ArkLib/Data/CodingTheory/ProximityGap/ as 23 files — the formalizations of the proximity-gaps literature (BCIKS20/ affine-lines/spaces/curves/list-decoding/weighted-agreement, DG25/, AHIV22) plus the protocol-facing abstractions (Basic, Folding, MCAGenerator, ProximityGenerators) that BatchedFri/Security, Stir/Combine, and Whir/ProximityGen import. That is exactly the right name for exactly that content. The fork has 4,259 files under the same path — a 185× inflation of a library directory by a research program.

So: keep the name, evict the campaign. Target shape for ProximityGap/ on main:

1. Upstream's 23-file skeleton (ours diff-reviewed against it — Basic and BCIKS20/Curves exist upstream and we modified them).
2. Our genuine extensions of the same papers, kept in upstream's paper-keyed-subdirectory convention: the parts of our 145-file BCIKS20/ subtree that extend the paper formalization (ListDecoding, ErrorBound, WeightedAgreement — the latter gated on proving its 6 axioms), similarly any real DG25/ additions.
3. Errors.lean (the ε-accounting API, 17 external importers — fits beside Basic; it's the one fork-only module with genuine library character).

The "Core API" carve-out shrinks to almost nothing on inspection. Of the fork-only modules protocol code appears to consume: Lattice2, GSFactorExtract, CapacityBounds have zero ProofSystem/OracleReduction importers (their importers are campaign files); Hab25ConjectureGlue's only ProofSystem consumers are Whir/{Hab25WindowMCA, MCAConjectureEllaryReduction, MCAConjecturePairReduction} — which are themselves δ*-campaign files squatting in ProofSystem/Whir/, not WHIR-the-protocol. Campaign tendrils outside ProximityGap/ move with the campaign: those Whir MCA-conjecture files, the ~300 paper/prize-named ToMathlib/ files, campaign bridges in GuruswamiSudan/ (real GS machinery stays in CodingTheory/GuruswamiSudan/).

Where the campaign canonically goes: a top-level Research/ProximityPrize/ Lean library — its own lakefile lib target and module root, on the research/proximity-prize branch. Rules that make it self-contained and honest:

• Dependency direction: Research → ArkLib only, never the reverse. (This is the invariant that upstream-PR-ability falls out of for free: main's library never mentions Research.)
• PROXIMITY_PRIZE_WORKBENCH.lean becomes the research lib's root module (it already is the de-facto aggregation of the machine-checked spine).
• The knowledge corpus lives beside it: Research/ProximityPrize/{DISPROOF_LOG.md, DOSSIER.md (v3, unversioned filename — git is the version), kb/papers, kb/sources, AGENTS.md}. No .md in ArkLib/** at all.
• The strict gates (laundering, zero-hole census, axiom audit) keep running over BOTH targets — the research lib keeps the honesty contract.
• End-state once churn stabilizes: promote Research/ProximityPrize to the separate repo that already exists for this (lalalune/rs-proximity-gaps), depending on ArkLib via lake require. Not now — same-repo branch keeps the swarm's CI loop simple.

Net effect on the phase plan: Phase 2 becomes "restore ProximityGap/ to canonical shape (23-file skeleton + paper extensions + Errors) and create Research/ProximityPrize with everything else", rather than inventing a new ProximityGap/Core/ name — no new names for library content, upstream's names ARE the names. The upstream PR (Phase 4) then naturally reads as: "extend BCIKS20/DG25 formalizations + Binius closeout + Fin/shared-Data fixes", which is a PR upstream can actually review.

[lalalune]

🚧 Execution has started (2026-07-09). Safety rails in place, in order:

1. ✅ Working tree synced with fork/main (through fcfaa2d47, incl. the zk-payments submodule pointer another lane just added — left untouched).
2. ✅ Immutable snapshot: tag archive/pre-refactor-2026-07-09.
3. ✅ Long-lived research branch created from the pre-refactor tip: research/proximity-prize (the full corpus, buildable as-is).
4. ✅ Warnings for concurrent agents: root REFACTOR_NOTICE.md + banners in the ProximityGap AGENTS.md/CLAUDE.md (pushed to main first so swarm agents see them immediately), + comment on Prove δ* — complete research dossier (v3) for the RS proximity-gap prize (successor to #464) #466.

Now executing: Phase 1 (mechanical cruft deletion) → Phase 2 (import-graph-driven campaign eviction with adversarial review of every gray-zone file; ProximityGap/ restored to upstream-canonical shape) → full build + gate verification → push. Upstream origin/main merge (5 trivial commits) is deliberately deferred to Phase 4 prep — mid-refactor is the wrong moment. A quality/cleanup pass (consolidation, axiom/Residual triage, comment de-slop) follows as a separate pass per the plan.

Note for later: an intermittent Binius/BinaryBasefold/Steps/Relay build failure was observed against a mid-churn tip — will be re-verified against the refactored tree.

[lalalune]

✅ Phases 1 + 2 EXECUTED — main is refactored (tip 615025baf)

The numbers: 12,174 tracked files → 1,790. ProximityGap/ 4,259 → 157 (upstream: 23). Root module 5,365 imports → 1,551. ToMathlib → 272. docs/kb → 96 (upstream baseline + papers/sources digests + Binius audit records).

How the eviction was decided (no guesswork): import-graph classifier over 5,707 Lean files → 4,032 evictable leaves + 163 gray-zone files pulled into the keep-closure → 38-agent adjudication with adversarial verification of every gray file and every proposed importer-eviction → guarded fixpoint (campaign zones cascade-evict, protocol/library zones pin dependencies back). Zero residual import violations; full build verified.

Landed on main:

• Phase 1 (cfd8da127): 5,044 cruft files (~45 MB) — probes, root scratch, PDFs, archives, stale artifacts.
• Phase 2 (827af16df): 4,229 campaign Lean files + 46 narrative .md + 1,091 kb/wiki notes evicted; websites + Cloudflare workflows moved to the research branch; barrels stripped; root regenerated; ProximityGap AGENTS/CLAUDE rewritten as canonical library guides; one eviction-exposed fix (ProximityGapP zero_le).
• Gates: forbidden-token clean, sorry census 0, kb pipeline regenerated.

On research/proximity-prize (tip 97e43abd5): the full corpus (snapshot parity with tag archive/pre-refactor-2026-07-09), website deploys re-triggered from that branch, and RESEARCH_BRANCH.md stating the contract (campaign lands there; never merge into main; sync main→research only).

73 pinned-back files (campaign-conditional but load-bearing for WHIR/STIR soundness and kept BCIKS20 work — the honest coupling the audit predicted): the Hab25* arithmetic chain + MCAJohnsonBound/Hab25WhirBridge/MCAConjecturePairReduction in Whir, Lattice2/*, CapacityBounds, LDThreshold*, LineDecoding*, the BCIKS20 P2*/AlphaWeight*/FaaDiBruno pieces, and the ToMathlib Hensel/beta supply chain (BetaRecGenuineBridge, CurveHensel*, LocalHenselSeries, GenuineMonicCapstone, …). These are frozen for the consolidation pass: do not grow them; the pass either discharges the WHIR dependency or moves the chain wholesale.

Known-red on main, NOT from this refactor: the 5-file KState cluster (BinaryBasefold/Steps/{Commit,Relay}, QueryPhase, FiatShamir/HVZKTransferReduction, CWSS/Composition) — a concurrent lane's in-flight substrate refactor, broken before the refactor (verified: identical failures at the pre-refactor tag; no evicted file declares the missing instances). That lane owns the fix.

Remaining (the cleanup pass, next): §3 axiom/Residual triage, §4 consolidations (micro-file merges, ArkLibScratch namespace, CommitmentScheme retirement adoption, comment de-slop), pinned-back discharge, then Phase 4 upstream prep (dependency re-pointing).

[lalalune]

🚧 Finalization pass in flight (fix-all-red + upstream-shape everything + dependency-fork prep)

Red on main — root-caused and being repaired (we own it now): the 5-file breakage traced to 681128736 ("Land dirty worktree"), which half-landed a substrate refactor: it broke Steps/Commit, Steps/Relay, QueryPhase, HVZKTransferReduction, CWSS/Composition AND regressed two proven Steps/Fold theorems into axioms — while also (the good half) clearing 22 sorries in Implications/SeqCompose. The repair keeps the good half, restores the pre-681 proofs, ports the sum_cube_snoc Domain block the structured sumcheck needs, fixes CWSS/Composition (OracleVerifier.append gained an AppendCoherent instance requirement post-Verified-zkEVM#530), and forward-fixes Fold's fold-order drift sites. Commit 3ce91fceb has the first half; a dedicated repair loop is finishing the Fold cone now.

Complete triage results now in hand (all audits done):

• ToMathlib (271 files): 8 upstream-canonical (restore), 16 protocol-support, 20 general mathlib-candidates + 2 rescues, 11 borderline, 114 campaign evict-now, 102 campaign-pinned (move with the chain).
• Data/CodingTheory (285 fork files): 38 pinned via the Whir chain, 247 with zero kept consumers — of which we're keeping the three library-grade clusters (GMMDS/Lovett 50, HigherOrderMDS 10, classical-bounds ~40: GV/Plotkin/Singleton/entropy) as genuine coding-theory content; the rest (AGL24 ×40, Quarantine, Connections, RandomLinearCode…) evicts. Includes one malformed git-tracked blob (shell-fragment filename) to remove.
• Whir/STIR MCA discharge plan: upstream's own pattern is conjecture-as-named-hypothesis (hasMutualCorrAgreement, mca_johnson_bound_CONJECTURE, IsMCAGenerator). Recipe: REVERT 6 in-place-mutated upstream files (Whir/MutualCorrAgreement, Stir/Combine, BCIKS20/{Curves, AffineLines/Main, ListDecoding/Agreement}, AHIV22 — re-axiomatizing upstream's sorries with paper refs so the census stays strict), RESHAPE ProtocolSoundness + CheckingVerifier (drop campaign imports/re-exports), MOVE the ~12 fork-only Whir MCA files. Verified by import-graph simulation: the pinned-back set then dissolves to zero campaign dependencies.
• Axioms: 7 on main, 6 = BCIKS20 literature statements (upstream carries the same as theorem := sorry) → keeping the axiom form with per-axiom paper-theorem refs + issue links; 1 (no_selfReciprocal_factor) documented + provable (Upstream-inherited sorry holes: prove or retire the 49 baselined census entries #470-tracked). The 2 Fold axioms disappear with the proof restoration.
• Conformance: lakefile re-point plan confirmed (VCVio+CompPoly → Verified-zkEVM v4.30.0, drop the direct PolyFun require — upstream resolves it transitively; doc-gen4 bump; header-linter options; toolchain rc2 → v4.30.0); ArkLib/Interaction/ is fork-only and self-declared unused → evicts; README/AGENTS carry a δ* section to strip; blueprint/src/proof_systems/fri.tex to resolve; micro-file consolidation targets mapped (Composition/Sequential 72→2-ish, BinaryBasefold 68→7-ish).

Dependency-fork prep running in parallel (separate clones):

• lalalune/VCV-io → branch arklib-prep off upstream/main: the obsolete rc2-compat commit is dropped (verified superseded upstream); 15 pure ToVCVio infrastructure files migrating (dep-range EagerTable, identical-until-bad for failing games, dependent uniform comap, LazyPerm bricks, …); 2 files stay in ArkLib (genuine protocol glue); 2 redundant with upstream.
• lalalune/CompPoly → branch arklib-prep: merge upstream/master into the 78-commit fork line; the ArkLib-facing payload (Univariate/Additional, Lagrange.interpolation_of_constants) verified present — ArkLib/ToCompPoly is a stale duplicate and will be deleted with importers redirected.
• lalalune/mathlib4 (fork created) → topic branches for the ~22 general lemma files (additive combinatorics incl. Balog–Szemerédi–Gowers + sum-product, Finset Chebyshev/Markov, polynomial lemmas incl. Hasse-deriv eval, Desnanot–Jacobi, Gauss-sum norms, Schwartz–Zippel existence), mathlib-styled, deduped against mathlib mainline.

Next after the Fold cone is green: the mega-batch (evictions + reverts + reshapes + barrel regen + fixpoint re-run + doc de-campaign), then lakefile/toolchain alignment with a full rebuild, then consolidation.

[lalalune]

Progress: dependency forks + research branch

✅ CompPoly prep complete — branch [arklib-prep on lalalune/CompPoly]: merged upstream/master into the 78-commit fork line (53 conflicts resolved with an anti-Frankenstein pass — upstream's final v4.31-proofed versions win wherever the fork added no unique declarations), took upstream's v4.31.0 toolchain (migration was tractable, ~10 files of proof drift), kept the fork's genuine additions (Koetter interpolation backend, Shoup root search, Univariate/Additional + Division, binary-field clMul, Lagrange interpolation_of_constants), dropped superseded duplicates. Now 81 ahead / 0 behind upstream, full build green (2542 jobs incl. tests + bench), zero sorries/new axioms, and the complete ArkLib-facing API verified axiom-clean (incl. monomial_eq_zero, ported from the stale ArkLib staging copy). This is the PR payload toward Verified-zkEVM/CompPoly.

✅ PolyFun — fork carried zero custom commits; fast-forwarded lalalune/PolyFun main to upstream. ArkLib main will drop its direct [[require]] (upstream resolves PolyFun transitively via CompPoly) in the lakefile re-point.

✅ research/proximity-prize synced with main's fixes — and a footgun documented: a plain main → research merge silently deletes the whole campaign corpus (git takes main's deletions for unmodified files). The sync was redone corpus-preserving (10,380 paths restored; 12,192 tracked files; root regenerated at 5,709 imports) and the procedure is now written into RESEARCH_BRANCH.md. Note: swarm lanes are already landing on the research branch (PR #501) — the routing notices worked.

🔄 In flight: Binius-cone forward repair (QueryPhase/Fold/Domain iterating, restores the two Fold proofs 681 regressed to axioms), VCV-io arklib-prep branch (15 pure ToVCVio infrastructure files), mathlib4 topic branches (~22 general lemma files, deduped + mathlib-styled). The main-tree mega-batch (evictions + Whir reshape + reverts + fixpoint) executes as soon as the Binius repair lands.