Bennett half Integer ne nat
ProvedD1Bound5.bennett_halfInteger_ne_natdiophantine-tuplesnumber-theory
Every half-integer parameter in the Bennett node-removal induction differs from every natural number. This is the exact parity obstruction, transported through the characteristic-zero cast.
Preamble
import Lean.Elab.Tactic.Omega import Mathlib.RingTheory.Binomial import Mathlib.Tactic.LinearCombination
Formal statement
section
open Polynomial
namespace D1Bound5
variable {F : Type*} [Field F] [CharZero F]
theorem _root_.D1Bound5.bennett_halfInteger_ne_nat (k v j : ℕ) :
(k : F) + (1 / 2 : F) - (v : F) * (k : F) ≠ (j : F) := by sorry
end D1Bound5
end
Source
D1Bound5/BennettChooseNonzero.lean, lines 28-38, SHA-256 242284e834a07d1f10f92c6ff0dc397a65048f9ca805d58c05766b00a9bc4ab5. Project: https://github.com/tomislav-math/d1-bound5-lean