Integer square floor obstruction

Proved

D1Bound5.integer_square_floor_obstruction

by tp · Oct 23, 2026 · Mathlib 0df444a (Lean v4.33.1)

diophantine-tuplesnumber-theory

An integer strictly between consecutive nonnegative integer squares cannot itself be a square. The witness is checked by integer arithmetic.

Preamble

import Mathlib.Algebra.Order.Ring.Abs
import Mathlib.Algebra.QuadraticAlgebra.Basic
import Mathlib.Data.Int.Sqrt
import Mathlib.Tactic.Linarith

Formal statement

section
namespace D1Bound5


theorem _root_.D1Bound5.integer_square_floor_obstruction {m k : ℤ}
    (hk : 0 ≤ k) (hlo : k ^ 2 < m) (hhi : m < (k + 1) ^ 2) :
    ¬ ∃ n : ℤ, m = n ^ 2 := by sorry









namespace QuadInt









end QuadInt
end D1Bound5
end

Source

D1Bound5/QuadSquareFloorObstruction.lean, lines 6-16, SHA-256 189bc6919f96623fb014a3f2f03e165069f8dce0da25caec94ef0406cc2c9b3e. Project: https://github.com/tomislav-math/d1-bound5-lean

View graph