CRT-Theta Lifts and Toric Resolvents for Cyclotomic Mock-Theta Values: Exact Foundations for a Hecke-Projected Arithmetic Detector

For a prime p ≥ 7, the finite cyclotomic value Tp governs the odd-order radial limit of Ramanujan's third-order mock theta function f(q). This paper rewrites Tp as a centred CRT-weighted unary-theta packet, proves an explicit chamber rule for the attached winding number, and derives from it the exact power-basis coefficients, histograms, constant term and trace. The quadratic Galois resolvent factors exactly through an integer invariant Mp, for which the paper gives the first unconditional bound by identifying the underlying character sum as a Kloosterman sum, and proves that the dominant Dirichlet character is of size √p. A level-39 theta packet, its Shimura lift, local gate and good-prime Hecke system are constructed exactly, and an analytic detector is defined by simultaneous all-cusp truncation rather than by formal rearrangement of a divergent mock series. The paper is explicit about what it does not prove: two research gates remain open, and every unresolved problem is stated together with the single mathematical input it is missing. Machine-checked. Fifty-nine of the paper's numbered statements are formalized in Lean 4 against Mathlib and are reproduced verbatim beside the printed statement. The axiom audit admits only propext, Classical.choice and Quot.sound; there is no sorry, no admit, no project-defined axiom, no unsafe, and no native_decide. A generated index maps every formalized LaTeX label to the Lean declarations that discharge it, and a drift checker fails if the paper and the development disagree. Reproducible. Every finite computation quoted is regenerated by one of seven distributed scripts, each of which validates itself against a kernel-checked result before reporting anything new. All arithmetic is exact except one shortlisting step, which is certified in 40-digit arithmetic against an explicit error bound. A SHA-256 manifest covers every distributed file. Licensing. The manuscript is CC BY 4.0. The Lean development and the scripts are Apache-2.0, matching Mathlib; see COPYING.md in the archive.