Square-root stochastic selection formulas

The executable squared-threshold comparisons implement the floor and RNITE formulas of §4.7.4 on the fractional part of the actual real square root. These equalities include exact roots and every supplied stochastic word. They make no probability or randomness-quality claim.

Reference: P3109 unapproved interim report 4.0.3, revision 34f5964, §§4.7.4, 4.10.8.

noncomputable def FloatLib.Floats.Formats.P3109.Arithmetic.sqrtFraction (numerator denominator : ℕ) : ℝ

Fractional part of the exact real square root, before selecting an integer candidate.

theorem FloatLib.Floats.Formats.P3109.Arithmetic.sqrtFraction_bounds (numerator denominator : ℕ) (hd : 0 < denominator) : 0 ≤ sqrtFraction numerator denominator ∧ sqrtFraction numerator denominator < 1

The square-root fractional part lies in [0, 1) for every positive denominator.

theorem FloatLib.Floats.Formats.P3109.Arithmetic.sqrtRoundAway_stochasticA (format : Format) (quantum : ℤ) (random : RandomBits) (numerator denominator : ℕ) (hd : 0 < denominator) : sqrtRoundAway format (RoundingMode.stochasticA random) quantum numerator denominator (sqrtFloor numerator denominator) = decide (2 ^ random.width ≤ ⌊sqrtFraction numerator denominator * 2 ^ random.width⌋₊ + random.toNat)

Executable stochastic A is the report's floor formula for the root's exact fractional part.

theorem FloatLib.Floats.Formats.P3109.Arithmetic.sqrtRoundAway_stochasticB (format : Format) (quantum : ℤ) (random : RandomBits) (numerator denominator : ℕ) (hd : 0 < denominator) : sqrtRoundAway format (RoundingMode.stochasticB random) quantum numerator denominator (sqrtFloor numerator denominator) = decide (2 ^ (random.width + 1) ≤ ⌊sqrtFraction numerator denominator * 2 ^ (random.width + 1)⌋₊ + (2 * random.toNat + 1))

Executable stochastic B is the report's doubled-word floor formula.

theorem FloatLib.Floats.Formats.P3109.Arithmetic.sqrtRoundAway_stochasticC (format : Format) (quantum : ℤ) (random : RandomBits) (numerator denominator : ℕ) (hd : 0 < denominator) : sqrtRoundAway format (RoundingMode.stochasticC random) quantum numerator denominator (sqrtFloor numerator denominator) = decide (2 ^ random.width ≤ RealRounding.nearestEven (sqrtFraction numerator denominator * 2 ^ random.width) + random.toNat)

Executable stochastic C is RNITE of the exact fraction, including even upper-boundary ties.