Many computations admit several valid execution orders because independent subgoals or disjoint state updates can commute.
Reinforcement learning with verifiable rewards usually treats each successful trace as a separate token sequence, so serialization choices can be mistaken for logical dependencies.
We introduce Verifier-Certified Rule Transport (VCRT)
Verifier-Certified Rule Transport (VCRT), which replays adjacent operation pairs with native verifiers.
Pairs whose two orders are accepted and reach the same canonical state provide commutation certificates; rejected or state-changing reversals provide anti-diamonds.
VCRT uses anti-diamonds to preserve genuine prerequisites and assigns policy credit to the total probability mass of each certified orbit.
It also constrains post-swap consistency, source retention, and policy drift.
Evaluation
We evaluate leave-one-environment-out transfer across ProofWriter, CLRS, and Lean through a shared anonymized relation-graph interface.
All training and checkpoint decisions are frozen before held-out evaluation, which uses one greedy trajectory per item without search or verifier feedback.
VCRT obtains a 77.60% macro pass rate versus 64.53% for the strongest matched baseline, a paired gain of 13.06 points (95% bootstrap CI [12.58, 13.54]).
Lean accounts for most of this gain at 33.49 points, while ProofWriter and CLRS improve by 2.85 points on average.
Results
Mechanism tests consistently favor anti-diamond supervision, whereas No-Orbit is statistically indistinguishable from full VCRT.
The evidence does not establish a general benefit from exact orbit aggregation.