feat(circuit/frontier): native tapered recovery computes recoverFromValues mod 2^p (Lemma D.5) - #1925

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: `p_t`. Advisory only; see the job summary.

`Cslib.GaloisRingArith.reduce` and `Cslib.GaloisRingArith.pval` (Complexity/Computability/PolyTime/GaloisRingInterpolation.lean:76) share a 323-node subterm, 32% of the smaller body, built from `Polynomial.map`, `ZMod`, `ZMod.commRing`, `Int.castRingHom`, `Cslib.GaloisRingArith.monicOf`. Advisory only; see the job summary.

`Cslib.GaloisRingArith.reduce` and `Cslib.GaloisRingArith.Ring` (Complexity/Computability/PolyTime/GaloisRingArithmetic.lean:118) share a 323-node subterm, 80% of the smaller body, built from `Polynomial.map`, `ZMod`, `ZMod.commRing`, `Int.castRingHom`, `Cslib.GaloisRingArith.monicOf`. Advisory only; see the job summary.

`Cslib.GaloisRingArith.reduce` and `Cslib.GaloisRingArith.val` (Complexity/Computability/PolyTime/GaloisRingArithmetic.lean:123) share a 323-node subterm, 32% of the smaller body, built from `Polynomial.map`, `ZMod`, `ZMod.commRing`, `Int.castRingHom`, `Cslib.GaloisRingArith.monicOf`. Advisory only; see the job summary.