Points on the conics a² + δ b² = 1

Over a field K the conic a² + δ b² = 1 always has the points (±1, 0). This file shows that over an infinite field in which 2 ≠ 0 it also has a point with both coordinates nonzero, for every δ. The rational parametrisation t ↦ ((1 - δ t²) / (1 + δ t²), 2t / (1 + δ t²)) gives such a point for every t with t ≠ 0 and δ t² ≠ ±1, and these exclusions are the roots of a nonzero polynomial, so an infinite field has admissible t.

Neither hypothesis can be dropped: in characteristic two a² + b² δ = (a + b √δ)², so over 𝔽₂(δ) the only solutions have b = 0, and over 𝔽₃ the circle a² + b² = 1 has no point with both coordinates nonzero.

The statement is what makes a binary form ⟨1, δ⟩ represent 1 with both coordinates nonzero; it supplies the even unitary units a + b • ω outside the Lipschitz group in TauCeti/LinearAlgebra/CliffordAlgebra/Spin/LowRank/Six.lean.

Main results

• TauCeti.exists_sq_add_sq_mul_eq_one: the conic a² + b² δ = 1 has a point with both coordinates nonzero over every infinite field in which 2 ≠ 0.

theorem TauCeti.exists_sq_add_sq_mul_eq_one {K : Type u_1} [Field K] [Infinite K] [NeZero 2] (δ : K) : ∃ (a : K) (b : K), a ≠ 0 ∧ b ≠ 0 ∧ a ^ 2 + b ^ 2 * δ = 1

The conic a² + b² δ = 1 has a point with both coordinates nonzero over every infinite field in which 2 ≠ 0.