A 127K-Parameter Cell in a Fixed Horner Program: Exactness, Compression, and a Verified Scaffold for Cross-Prime Modular Multiplication

Monolithic learners stall on $(a,b)\bmod p$ across primes, and the sharper question is cross-prime: one model, primes it never saw. We report a compact neuro-symbolic construction in which a fixed, hand-coded bit-serial Horner program supplies the schedule and a single learned cell supplies the arithmetic. The cell, a two-layer bidirectional GRU conditioned on the modulus, learns the per-step transition $s' = (2s + d,x)\bmod p$ and is re-run to reduce $a\bmod p$, reduce $b\bmod p$, and multiply the residues, with the per-step state width sized to each prime's bit-length at inference. A 470,849-parameter cell scores exact-match $1.00$ on all ten scored tiers of the SAIR Modular Arithmetic Challenge's official scorer, reproduced across three operand seeds inside the time budget; randomizing its weights drops every tier to $0/64$. A matched-budget width study shrinks the cell to 126,603 parameters (hidden width 61) while keeping every gate: a 249K and a 127K arm pass, a 63K arm fails the endpoint rollout, and the 127K cell then transfers through width bridges at 256, 512, and 1,024 bits with 256/256 exact confirmations on the retained tiers, before a 2,048-bit repair run fails its retention gate. A Lean 4 development machine-checks the integer double-and-add algorithm the program imitates and a conditional exact-prefix theorem for any transition cell; the bridge from a checkpoint to that premise is stated as open. We report where exactness stops: Fermat-number operands, a pure-multiplication diagnostic, and three fixed-Hamming cases at 2,048 bits.