14.7. Performance🔗

The cost of rcf is the cost of elaborating the tactic: running the compiled search, building the certificate as a literal, and having the kernel replay it. The table gives the median added time of a fresh module containing one by rcf theorem over the same module without it, so it includes elaboration and kernel replay but not the fixed cost of loading Mathlib.

The compiled decision procedure on its own, Hex.RCF.decide with no proof, takes 32 ms, 85 ms, 184 ms, 333 ms and 541 ms on one-atom sentences whose polynomial has 16, 20, 24, 28 and 32 real roots, consistent with the declared quartic model in the root count. Measured on chungus2; the artefacts and their provenance are recorded in reports/hex-rcf-performance.md in the hex-dev repository, and the three tactic budgets they sit under are 2 s, 12 s and 30 s.