Typed Inference Dynamics: Auditable State Transitions for Mathematical Reasoning

Hard mathematical problem solving evolves through persistent partial states: paths are pruned or reactivated, constraints are deposited, subgoals close, and frames change what the next solve can see. Final answers, linear rationales, and scalar process scores flatten this motion. We introduce typed inference dynamics (TID), a state-transition substrate in which a helper proposes typed operations over candidate paths, constraints, subgoals, frames, and determined values; a deterministic reducer accepts, rejects, and logs the operation trace; and the accepted state is rendered to a frozen solver or distilled into adapters. In the original loop, full MATH-500 Level 5 (n=134) within-loop cumulative coverage improves from 35/134 to 53/134 at 7B (+13.4 pp, 95% CI [+7.5,+19.4]) and from 36/134 to 59/134 at 14B-AWQ (+17.2 pp, [+11.2,+23.9]); on OlympiadBench, the 14B-AWQ carrier improves from 4/29 to 11/29, while AIME is null at the reported T2 endpoint. These cumulative endpoints are pass-by-budget coverage inside the original loop, not evidence that typing alone caused the lift; fresh fixed-horizon controls show that repeated attempts explain much of the discovery gain, detect no net any-turn advantage of full TID over a schema-lite state updater at n=134, and expose a discovery-versus-retention gap that terminal and frozen-selector endpoints only partly realize. In the fresh cost profile, D uses 488,512 total tokens, about 1.98x repeated sampling (B) and 1.05x schema-lite updating (C*), while a 5,000-example transition corpus lifts a 7B LoRA from 6/90 to 33/90 passes on a hard harness. The evidence supports typed inference dynamics as an auditable, trainable transition layer between informal rationales and formal proof objects, with retention and state-authority calibration as the next bottlenecks.