Learning.Checked.MomentCorrection

30def momentScaledRootWord =
31  (lambda unrestricted scaleNumerator : Nat .
32    (lambda unrestricted scaleDenominator : Nat .
33      (lambda unrestricted beta2Numerator : Nat .
34        (lambda unrestricted beta2Denominator : Nat .
35          (lambda unrestricted step : Nat .
36            (let unrestricted gap =
37              (momentPowerGap beta2Numerator beta2Denominator step) in
38            (let unrestricted denominator =
39              (momentNaturalPower beta2Denominator step) in
40            (let unrestricted root =
41              (float32ExactRootLow gap denominator) in
42              (float32ExactBetween
43                (naturalMultiply scaleNumerator root)
44                (naturalMultiply scaleDenominator
45                  (naturalMultiply denominator float32RootScale))
46                (naturalMultiply scaleNumerator (succ root))
47                (naturalMultiply scaleDenominator
48                  (naturalMultiply denominator float32RootScale)))))))))))