Trace zero parameter not three mod four

Proved

D1Bound5.trace_zero_parameter_not_three_mod_four

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

diophantine-tuplesnumber-theory

If nu is 3 modulo 4 then (1+omega)/2 is an extra integral element. Thus a trace-zero model with that parameter cannot be the full integer ring.

Preamble

import Mathlib.Algebra.Polynomial.Monic
import Mathlib.Algebra.QuadraticAlgebra.Basic
import Mathlib.Algebra.Squarefree.Basic
import Mathlib.Data.Int.GCD
import Mathlib.LinearAlgebra.Dimension.Free
import Mathlib.NumberTheory.NumberField.Norm
import Mathlib.Tactic.Linarith
import Mathlib.Tactic.LinearCombination
import Definitions.Def_D1Bound5_Coordinates_Definitions

Formal statement

section
open scoped NumberField
open Module Polynomial

namespace D1Bound5

variable {K : Type*} [Field K]



variable [NumberField K]








theorem _root_.D1Bound5.trace_zero_parameter_not_three_mod_four {nu : ℤ}
    (e : QuadInt 0 nu ≃+* 𝓞 K) : nu % 4 ≠ 3 := by sorry

end D1Bound5
end

Source

D1Bound5/MaximalCoordinates.lean, lines 101-134, SHA-256 db32306018b4cc9c601d0bd15648a6675ec234d51750d3dd04f9988129483527. Project: https://github.com/tomislav-math/d1-bound5-lean

View graph