Interface 2: the prescribed order trial

For a unit $a$ modulo $m$, define

The frozen order-trial claim is

with output either no candidate or $1\le d<B$ satisfying $r\mid d$. The trial receives $m,a$, not $r$ or a factorization.

The source uses an interpolated phase construction, actual unnormalized ancillary success probabilities, and exact correction branches SourceOrder,SourceDyadic. The audit must check:

1. the actual fixed-gate implementation, not an ideal Fourier transform substituted afterwards;

2. the uniqueness and efficient recovery of candidate labels;

3. the exact mass identity (eq:order-law), including $r=1$;

4. polynomial evaluation of correction totals without summing an exponential number of residues;

5. no use of an unknown order in the implementation.

None of these is discharged merely by quoting Shor's algorithm.

Two elementary consequences can nevertheless be proved directly.