Learning.Checked.MomentCorrection

For positive update t, the two correction factors used by a decoupled moment update are lr * sqrt(1 - beta2^t) / (1 - beta1^t) and eps * sqrt(1 - beta2^t). Keep the square root interval exact until both bounds round to the same F32 word; a host or GPU must never substitute a host-language floating-point approximation for these launch scalars.

11def momentNaturalPower =
12  (lambda unrestricted base : Nat .
13    (lambda unrestricted exponent : Nat .
14      (nat-eliminate
15        (lambda unrestricted current : Nat . Nat)
16        1
17        (lambda unrestricted predecessor : Nat .
18          (lambda unrestricted result : Nat .
19            (naturalMultiply base result)))
20        exponent)))