The quadratic order O_d — definition and power basis

Thesis. §1.2 (Notation) and §3.2, the order O = O_d = ℤ[(d + √d)/2] ≅ ℤ[x]/(x² − dx + (d² − d)/4).

This file defines the core object and its most basic structure:

• poly d — the defining polynomial X² − dX + (d² − d)/4
• QuadraticOrder d — the order, as AdjoinRoot (poly d)
• tau — the root τ = (d + √d)/2
• tau_minimal_poly — τ satisfies its defining polynomial
• basis — the rank-2 ℤ-power basis {1, τ}, with the basis_repr_* coordinate-extraction helpers
• dvd_four_of_valid_disc — 4 ∣ d² − d under d ≡ 0, 1 (mod 4) (shared by the discriminant computations downstream)

The norm form lives in Norm.lean; the discriminant identity (τ − tauConj)² = d in Discriminant.lean.

Divergence from thesis. The thesis works over an honest discriminant d (so d ≡ 0, 1 (mod 4)). Here QuadraticOrder d is defined for every d : ℤ via Euclidean division in the constant term; the congruence hypothesis is introduced only where it is actually needed (see Discriminant.lean). For d ≢ 0, 1 (mod 4) the object is still a well-defined quadratic ℤ-algebra but no longer matches the order of discriminant d.

noncomputable def poly (d : ℤ) : Polynomial ℤ

The defining polynomial of QuadraticOrder d.

Equations

• poly d = Polynomial.X ^ 2 - Polynomial.C d * Polynomial.X + Polynomial.C ((d ^ 2 - d) / 4)

@[reducible, inline]

abbrev QuadraticOrder (d : ℤ) : Type

QuadraticOrder d is the quadratic ℤ-algebra ℤ[x] / (x^2 - d * x + (d^2 - d) / 4), where the constant term is formed using Euclidean division in ℤ.

For integers d with d ≡ 0, 1 (mod 4), this ring coincides with the (imaginary) quadratic order of discriminant d in the quadratic field ℚ(√d). When d does not satisfy these congruence conditions, this definition should simply be understood as this explicit quadratic quotient ring over ℤ.

Equations

• QuadraticOrder d = AdjoinRoot (poly d)

Defining polynomial

We define poly before the variable command so the auto-binder does not add a second implicit d to its signature.

theorem QuadraticOrder.poly_monic (d : ℤ) : (poly d).Monic

The defining polynomial is monic of degree 2.

theorem QuadraticOrder.poly_natDegree (d : ℤ) : (poly d).natDegree = 2

The natural degree of the defining polynomial is 2.

theorem QuadraticOrder.poly_degree (d : ℤ) : (poly d).degree = 2

The degree of the defining polynomial is 2.

noncomputable def QuadraticOrder.tau {d : ℤ} : QuadraticOrder d

The element τ corresponding to (d + √d)/2 in the order.

Equations

• QuadraticOrder.tau = AdjoinRoot.root (poly d)

Layer 1: Basic algebraic properties

theorem QuadraticOrder.tau_minimal_poly {d : ℤ} : tau ^ 2 - d • tau + ((d ^ 2 - d) / 4) • 1 = 0

τ is a root of the defining polynomial X² - dX + (d²-d)/4.

Proof sketch: aeval τ (poly d) = mk (poly d) (poly d) = 0 by AdjoinRoot.aeval_eq and AdjoinRoot.mk_self.

@[simp]

theorem QuadraticOrder.poly_aeval_tau {d : ℤ} : (Polynomial.aeval tau) (poly d) = 0

τ is a root of the defining polynomial poly d in QuadraticOrder d.

noncomputable def QuadraticOrder.basis {d : ℤ} : PowerBasis ℤ (QuadraticOrder d)

QuadraticOrder d has a ℤ-module power basis {1, τ} of rank 2.

Equations

• QuadraticOrder.basis = AdjoinRoot.powerBasis' ⋯

instance QuadraticOrder.instFreeInt {d : ℤ} : Module.Free ℤ (QuadraticOrder d)

QuadraticOrder d is a free ℤ-module (of rank 2).

instance QuadraticOrder.instFiniteInt {d : ℤ} : Module.Finite ℤ (QuadraticOrder d)

QuadraticOrder d is a finite ℤ-module.

theorem QuadraticOrder.dvd_four_of_valid_disc {d : ℤ} (hd : d % 4 = 0 ∨ d % 4 = 1) : 4 ∣ d ^ 2 - d

For an honest discriminant (d ≡ 0 ∨ 1 (mod 4)), 4 ∣ d² − d. This is the shared arithmetic fact underlying the discriminant computations in Discriminant.lean and Prime/PolyMod.lean.

Basis helpers

These extract (basis.basis.repr α) i — the τ-component (or 1-component) of a ring element — via the modByMonic representation underlying AdjoinRoot's powerBasis'.

@[simp]

theorem QuadraticOrder.basis_dim {d : ℤ} : basis.dim = 2

The dimension of the power basis equals the degree of the defining polynomial, namely 2.

theorem QuadraticOrder.basis_repr_apply {d : ℤ} (α : QuadraticOrder d) (i : Fin basis.dim) : (basis.basis.repr α) i = ((AdjoinRoot.modByMonicHom ⋯) α).coeff ↑i

The basis-representation coefficient at index i is the i-th coefficient of the unique polynomial of degree < 2 representing α (its modByMonic remainder).

theorem QuadraticOrder.basis_repr_tau_one {d : ℤ} : (basis.basis.repr tau) ⟨1, ⋯⟩ = 1

The τ-coefficient (index 1) of τ itself is 1.