def HexArith.Nat.floorSqrt (n : Nat) : Nat

The floor of the square root of n.

Equations

• HexArith.Nat.floorSqrt n = if n = 0 then 0 else HexArith.Nat.sqrtAux✝ n (2 * n.log2 + 1) (HexArith.Nat.sqrtInit✝ n)

def HexArith.Nat.ceilSqrt (n : Nat) : Nat

The least natural number whose square is at least n.

Equations

• HexArith.Nat.ceilSqrt n = if HexArith.Nat.floorSqrt n * HexArith.Nat.floorSqrt n = n then HexArith.Nat.floorSqrt n else HexArith.Nat.floorSqrt n + 1

@[simp]

theorem HexArith.Nat.floorSqrt_zero : floorSqrt 0 = 0

Base case of floorSqrt: the n = 0 guard fires before the Newton iteration, so floorSqrt 0 normalizes to 0.

theorem HexArith.Nat.floorSqrt_sq_le (n : Nat) : floorSqrt n * floorSqrt n ≤ n

The square of floorSqrt n is at most n: it is a lower square root.

theorem HexArith.Nat.lt_floorSqrt_succ (n : Nat) : n < (floorSqrt n + 1) ^ 2

The successor of the floor square root has square strictly above n.

theorem HexArith.Nat.floorSqrt_eq (n : Nat) : floorSqrt n = n.sqrt

The Newton implementation agrees with Lean's natural square root.

@[simp]

theorem HexArith.Nat.ceilSqrt_zero : ceilSqrt 0 = 0

Base case of ceilSqrt: since floorSqrt 0 = 0 is a perfect square, ceilSqrt returns its floor branch, normalizing ceilSqrt 0 to 0.

theorem HexArith.Nat.le_ceilSqrt_sq (n : Nat) : n ≤ ceilSqrt n ^ 2

The square of HexArith.Nat.ceilSqrt applied to n is at least n. This is the executable upper-square bound used by the Mignotte coefficient norm chain: in the perfect-square branch of the ceiling square root, equality holds; in the non-perfect-square branch, the bound follows from the Newton iterator invariant.

theorem HexArith.Nat.ceilSqrt_le {n b : Nat} (h : n ≤ b ^ 2) : ceilSqrt n ≤ b

A natural square upper bound also bounds the ceiling square root.