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 the retired ℚ-Newton upper sqrt (accuracy ~10⁻¹⁰, output denominators arbitrary), 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. The lower square root sqrtℚLow13 (in Checker/ApproxSqrt.lean) has the same fixed-point shape at scale 10⁻¹³.

sqrtApprox16 packages it as an Approx together with the fixed-point lower square root sqrtℚLow13 from Checker/ApproxSqrt.lean. Since upper square roots only ever appear in check-hardening positions, any upper bound is sound here, and a tighter one 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

The Approx bundle used by all checkers: sqrtℚLow below, sqrtℚUp16 above, and rational upper bounds for √2 and √5.

Equations

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

Sanity checks