TALLY: Learned Approximately, Proved Exactly

Neural models can learn the correct computation and still fail to execute it reliably. TALLY studies this separation on finite group state tracking. An eight dimensional, input conditioned orthogonal transport makes latent group structure recoverable and raises gated DeltaProduct's pooled median accuracy at $16\times$ training length from 0.014 to 0.989 across twenty matched runs. Its operators encode the task's finite structure, but satisfy the group relations only approximately, so continuous execution eventually drifts. Given frozen operators and the recovered finite orbit, a conditional moment recursion predicts mean squared state deviation with 3.1% mean relative discrepancy across 120 combinations of checkpoint and length. On one frozen model, halving or doubling the operator defect moves the first sampled horizon below 90% transport accuracy from 8,192 to 32,768 or 2,048, while an exact realisation has no observed errors through 32,768. This controlled intervention supports a causal role for approximation error in the transport's failure. TALLY then recovers the latent finite action from checkpoints and unlabelled words, compiles it into discrete execution, and checks every transition and output against the task. The compiled scan makes no errors across 83,886,080 evaluated positions at length 1,048,576. Separate finite checks prove 53 extracted executors and readouts correct on every input at every length. The guarantee covers the frozen discrete executor and readout, not the unchanged neural decoder. Learned approximately, compiled and proved exactly.