The lemmas are the facts about iterates and orbits that the LCG,
Park and Miller's generator, and xorshift64
share. loop_eq_iterate states that LeanExe.loop with an unused index computes an iterate, so
advance n x is step^[n.toNat] x. minimalPeriod_eq_of_isPeriodicPt_iff gives the minimal
period of a point as the N whose multiples are its periods. existsUnique_iterate states that an
orbit that stays in a finite set with as many elements as the period reaches each element at
exactly one count below the period, and natCard_uint64 counts the words.
minimalPeriod_eq_of_primes gives a point the minimal period N when it returns after N steps
and after no N / q steps for any prime q that divides N, and the period of xorshift64 uses
it. shift_and_one_ne_zero reads the programs' test of bit k of a word as Nat.testBit, and
card_topBits states that exactly 2^(64 - j) words have the top j bits v.