Quaternary Iteration Control for Looped Transformers: A Four-Valued Iteration Contract with a Finite-Rank Termination Bound

Looped transformers apply a shared block repeatedly, decoupling effective depth from parameter count. Standard fixed-count, adaptive-computation, and fixed-point schedulers ultimately select whether another application occurs or control exits. Their internal halting quantities differ, but the scheduling action does not itself provide a typed distinction among checkable failure, absent evidence, a requested further pass, and unresolved dependency. We specify a four-valued iteration contract in which the evaluator returns NO with a canonically named failure mode, YES, MAYBE with a typed statement of what is missing (absent evidence or one further application of the block), or IFF with a named dependency. Every controller transition that continues after a non-YES verdict consumes one unit of exactly one finite resource: an exclusion set that grows monotonically, a bounded MAYBE-action budget, or a bounded dependency budget. We fix the contract's insertion point in a middle-cycle looped transformer, show that it restricts to prelude reinjection when the exclusion set is empty and to fixed-count control when the failure alphabet is empty, and quantify the exclusion representation: the default exact bitset adds |F|d projection parameters, while reserved-position and hashed alternatives have different compute and distinguishability costs. We prove that under stated assumptions the controller reaches a terminal disposition in at most rho_0+1 evaluations, where rho_0 is the initial controller rank, and that this bound is tight for fixed-count control. Termination is separated from evaluator soundness, which the theorem does not supply. Every evaluation emits a typed verdict and payload, and the controller records a transition receipt, yielding a finite, checkable trace of the iteration decisions without externalizing tokens. The note makes two claims, an interface and a theorem about it, and no empirical claim.