hex

4.8. Costs and limits🔗

Write M for the number of bits of the accumulated modulus. A push costs one extended Euclidean algorithm on numbers below the new modulus m, and additions, multiplications and reductions on numbers of M bits, each linear in M when m fits in a word. Accumulating k moduli of one word each therefore costs O(k²) word operations. A CrtVec push does the M-bit work once per coordinate and the extended Euclidean algorithm once. Building a CrtPlan checks every pair of moduli for coprimality, which is k² greatest common divisors of words.

Rational reconstruction runs the Euclidean algorithm on numbers of M bits until the remainder is at most P, which takes O(M²) word operations in the worst case. A failure may need the whole run, or may be detected when the first candidate fails the final checks. ratReconWide? also computes an integer square root, and the vector form usually runs one Euclidean algorithm for the whole vector and a multiplication and reduction for each later entry. The report reports/hex-modular-performance.md measures these costs. On Fibonacci inputs, which make the Euclidean algorithm as long as possible, a reconstruction modulo a number of 262144 bits took about 3 seconds, about 10 times as long as GMP's extended Euclidean algorithm called from Python, which is subquadratic; at 512 bits the ratio was 2.6. Accumulating residues was about three times as fast as the same Garner recurrence in FLINT called from Python.

These times were measured on one core of a shared machine (chungus2) on 2026-10-05, one run each, by the compiled benchmarks in bench/HexModular/Bench.lean. The moduli are prime powers of 23 to 48 bits, and the plan is built in advance:

computation

incremental

with a plan

one value, 1024 moduli

4.0 ms

3.0 ms

one value, 4096 moduli

45 ms

32 ms

4096 values, 16 moduli

34 ms

68 ms

A plan saves little for one value, and for many values with few moduli the incremental CrtVec was faster. The plan's advantage is that its inverses are computed once and reused for every later reconstruction with the same moduli.

The moduli are natural numbers of any size. Recovering an integer x needs moduli with product M > 2 |x|, and recovering a fraction with bounds P and Q needs M > 2 P Q. A finite supply may not reach the modulus a computation needs, so crtLoop takes fuel and a finite supply and returns none when either runs out; it is up to the caller to supply enough.