Fixed-point upper square root

sqrtℚUp16 is an upper rational square root whose output always has denominator dividing 10¹⁶: for x > 0,

sqrtℚUp16 x = (Nat.sqrt ⌈x · 10³²⌉ + 1) / 10¹⁶ ≥ √x.

Compared to sqrtℚUp (accuracy ~10⁻¹⁰, output denominators arbitrary — e.g. sqrtℚUp 2 = 50000000000/35355339059), this is both more accurate (error < 2·10⁻¹⁶ relative to the input scale) and fixed-point, which is what lets the checkers' hot loops run on integer numerators with statically known scales: every upper-sqrt output is an integer multiple of 10⁻¹⁶, and for inputs that are themselves multiples of 10⁻³² the ceiling is exact.

sqrtApprox16 packages it as an Approx (same lower_sqrt and √2/√5 constants as sqrtApprox). Since upper square roots only ever appear in check-hardening positions, swapping sqrtApprox → sqrtApprox16 in a checker keeps it sound (any upper bound works) and — being tighter — only makes it easier for certificate rows to pass.

def RationalApprox.sqrtℚUp16 (x : ℚ) : ℚ

Fixed-point upper square root: √x ≤ sqrtℚUp16 x, with output an integer multiple of 10⁻¹⁶ (and 0 for x ≤ 0).

Equations

• RationalApprox.sqrtℚUp16 x = if x ≤ 0 then 0 else (↑⌈x * 10 ^ 32⌉.toNat.sqrt + 1) / 10 ^ 16

theorem RationalApprox.sqrtℚUp16_nonneg (x : ℚ) : 0 ≤ sqrtℚUp16 x

theorem RationalApprox.sqrt_le_sqrtℚUp16 (x : ℚ) (hx : 0 ≤ x) : √↑x ≤ ↑(sqrtℚUp16 x)

The upper-bound property: √x ≤ sqrtℚUp16 x for 0 ≤ x.

theorem RationalApprox.UpperSqrt.le_mul_self (s : UpperSqrt) {x : ℚ} (hx : 0 ≤ x) : x ≤ s.f x * s.f x

Rational lower bound on the square of any upper sqrt: x ≤ s.f x · s.f x for 0 ≤ x.

theorem RationalApprox.le_mul_self_sqrtℚUp16 {x : ℚ} (hx : 0 ≤ x) : x ≤ sqrtℚUp16 x * sqrtℚUp16 x

Rational lower bound on the square of sqrtℚUp16.

theorem RationalApprox.sqrtℚUp16_le_add_of_le_mul_self {x Y : ℚ} (hY : 0 ≤ Y) (h : x ≤ Y * Y) : sqrtℚUp16 x ≤ Y + 2 / 10 ^ 16

Tight computable upper bound on sqrtℚUp16: if x ≤ Y·Y with 0 ≤ Y, then sqrtℚUp16 x ≤ Y + 2·10⁻¹⁶. This replaces the crude √⁺x ≤ 2·Y bound used with sqrtℚUp — the cheap-test constants shrink accordingly.

def RationalApprox.upperSqrt16 : UpperSqrt

sqrtℚUp16 as an UpperSqrt.

Equations

• RationalApprox.upperSqrt16 = { f := RationalApprox.sqrtℚUp16, bound := ⋯ }

def RationalApprox.sqrtApprox16 : Approx

sqrtApprox with the fixed-point upper square root.

Equations

• One or more equations did not get rendered due to their size.

Sanity checks