Some fixes before finalization

[erdkocak]

No description provided.

[github-actions]

Build Timing Report

• Commit: 877ad35
• Message: Merge f1b1f53 into 6f4a280
• Ref: fixes
• Comparison baseline: 6f4a280 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	274.67	258.19	-16.48	ok
Warm rebuild	1.67	1.86	+0.19	ok
Test path	21.81	20.84	-0.97	ok

Incremental Rebuild Signal

• Warm rebuild saved 256.33s vs clean (138.81x 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
83.00	86.00	-3.00	CompPoly/Fields/Binary/BF128Ghash/XPowTwoPowModCertificate.lean
62.00	64.00	-2.00	CompPoly/Fields/Binary/Tower/Abstract/Basis.lean
49.00	50.00	-1.00	CompPoly/Bivariate/ToPoly.lean
35.00	43.00	-8.00	CompPoly/Fields/Binary/BF128Ghash/Impl.lean
27.00	28.00	-1.00	CompPoly/Univariate/Raw/Proofs.lean
21.00	19.00	+2.00	CompPoly/Fields/Binary/AdditiveNTT/NovelPolynomialBasis.lean
21.00	24.00	-3.00	CompPoly/Fields/Binary/Tower/Support/Preliminaries.lean
21.00	22.00	-1.00	CompPoly/Univariate/Lagrange.lean
19.00	21.00	-2.00	CompPoly/Multivariate/Unlawful.lean
18.00	18.00	+0.00	CompPoly/Fields/Binary/AdditiveNTT/Intermediate.lean
18.00	19.00	-1.00	CompPoly/Univariate/NTT/Forward.lean
17.00	19.00	-2.00	CompPoly/Univariate/Quotient/Core.lean
16.00	15.00	+1.00	CompPoly/Univariate/Basic.lean
15.00	13.00	+2.00	CompPoly/Multilinear/Basic.lean
14.00	16.00	-2.00	CompPoly/Fields/Binary/AdditiveNTT/Domain.lean
14.00	11.00	+3.00	CompPoly/Fields/Binary/Tower/Abstract/Core.lean
13.00	12.00	+1.00	CompPoly/Fields/Binary/AdditiveNTT/Correctness.lean
12.00	15.00	-3.00	CompPoly/Multivariate/MvPolyEquiv/Instances.lean
11.00	8.20	+2.80	CompPoly/Fields/Binary/Tower/TensorAlgebra.lean
11.00	12.00	-1.00	CompPoly/Fields/KoalaBear.lean

[doran2728]

Good improvements in proofing structure, merging.