feat(Sparsification): select sharp first-success counting thresholds - #1293

Node.js 20 is deprecated. The following actions target Node.js 20 but are being forced to run on Node.js 24: actions/checkout@v4. For more information see: https://github.blog/changelog/2025-09-19-deprecation-of-node-20-on-github-actions-runners/

Not declared at the PR head: `CountingTreeBound`. Advisory only; see the job summary.

`Cslib.ReplacementCounting.Design.shiftedFactorEval` and `Cslib.AffineTaylor.affineInput` (Complexity/Foundations/Data/MvPolynomial/AffineTaylor.lean:105) share a 455-node subterm, 33% of the smaller body, built from `LinearMap`, `RingHom.id`, `Polynomial`, `Polynomial.semiring`, `Polynomial.module`. Advisory only; see the job summary.

`Cslib.ReplacementCounting.Design.shiftedFactorEval` and `Cslib.Circuits.Rational.Expansion.wronskianFamily` (Complexity/Computability/Circuit/Rational/Wronskian.lean:65) share a 455-node subterm, 56% of the smaller body, built from `LinearMap`, `RingHom.id`, `Polynomial`, `Polynomial.semiring`, `Polynomial.module`. Advisory only; see the job summary.