Draft: GS using the goal mode of Codex

[clarus]

In this PR we supposedly get:

• A Lean version of the GS algorithm from Lambdaclass in Rust
• Benchmarks saying it returns the same results as in Rust
• Benchmarks saying the speed is three times slower than Rust with optimized 🐨 fields
• A formal proof (it remains to understand of why). Apparently the Lambdaclass algorithm uses a heuristic to find roots, which is not always true.

See formal-land/lambdaworks#1 for the bench on the Rust side.

[github-actions]

Build Timing Report

• Commit: 13f9e58
• Message: Merge 715e461 into 57c7229
• Ref: guillaume-claret@gs-goal
• Comparison baseline: 57c7229 from merge-base on master.
• Measured on ubuntu-latest with /usr/bin/time -p.
• Commands: clean build rm -rf .lake/build && lake build; warm rebuild lake build; test path lake test.

Measurement	Baseline (s)	Current (s)	Delta (s)	Status
Clean build	289.18	299.42	+10.24	ok
Warm rebuild	1.30	1.29	-0.01	ok
Test path	21.13	26.13	+5.00	ok

Incremental Rebuild Signal

• Warm rebuild saved 298.13s vs clean (232.11x 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
53.00	60.00	-7.00	CompPoly/Fields/Binary/Tower/Abstract/Basis.lean
46.00	46.00	+0.00	CompPoly/Fields/Binary/BF128Ghash/XPowTwoPowModCertificate.lean
46.00	48.00	-2.00	CompPoly/Univariate/DivisionCorrectness.lean
38.00	40.00	-2.00	CompPoly/Fields/Binary/BF128Ghash/Impl.lean
30.00	31.00	-1.00	CompPoly/Bivariate/ToPoly.lean
27.00	27.00	+0.00	CompPoly/Univariate/Raw/Proofs.lean
22.00	17.00	+5.00	CompPoly/Fields/KoalaBear/Fast.lean
20.00	20.00	+0.00	CompPoly/Univariate/NTTFast/Correctness/Radix4DIT.lean
18.00	22.00	-4.00	CompPoly/Fields/Binary/Tower/Support/Preliminaries.lean
17.00	21.00	-4.00	CompPoly/Fields/Binary/AdditiveNTT/NovelPolynomialBasis.lean
16.00	17.00	-1.00	CompPoly/Fields/Binary/AdditiveNTT/Intermediate.lean
15.00	15.00	+0.00	CompPoly/Univariate/NTT/Forward.lean
14.00	14.00	+0.00	CompPoly/Univariate/NTTFast/Correctness/Radix4DIF.lean
13.00	13.00	+0.00	CompPoly/Univariate/Lagrange.lean
12.00	12.00	+0.00	CompPoly/Univariate/Basic.lean
12.00	13.00	-1.00	CompPoly/Univariate/NTTFast/Correctness/DIF.lean
11.00	14.00	-3.00	CompPoly/Fields/Binary/AdditiveNTT/Domain.lean
11.00	12.00	-1.00	CompPoly/Univariate/Quotient/Core.lean
11.00	12.00	-1.00	CompPoly/Fields/Binary/BF128Ghash/XPowTwoPowGcdCertificate.lean
10.00	12.00	-2.00	CompPoly/Multilinear/Basic.lean