Off-chain differential (real-node binding): the Agda-extracted round-robin leader leaderRef (the §6 figure's leader(s)) checked against the REAL isLeader. This is the off-chain counterpart of the on-chain validator differentials: the extracted decision is pinned not just to a Haskell transcription of the figure but to the function the node actually runs, closing the figure↔Agda↔Haskell loop for leader selection.

Domain note: snapshot numbers in the protocol start at 1, but the property covers sn = 0 too. leaderRef works over Nat, whose truncated subtraction would make 0 - 1 zero where isLeader's Int arithmetic gives -1 mod n = n-1; the extracted checker adds m instead of subtracting 1 (the same residue for every sn >= 1, and n-1 at zero) precisely so the oracle cannot disagree with the node anywhere - including on an sn = 0 a peer could put in a ReqSn.