Layer 2b: Canonical Form for ideals of QuadraticOrder — scaffolding

This file is the first PR of the Lemma 3.2.4 (canonical form) sequence. It introduces the central definitions and proves the structural identity that the canonical ideal coincides with the plain ℤ-span of its two generators.

For d : ℤ, a natural-number "prime power exponent" pair (k, m) with m/2 ≤ k ≤ m, and an integer A, the canonical ideal

canonicalIdeal d p k m A = ⟨p^k, p^(m-k) · (τ - A)⟩

is the generic 𝔭-primary ideal of QuadraticOrder d predicted by Lemma 3.2.4. The integer pair (k, A) is admissible if p^(2k-m) divides A² - dA + (d²-d)/4 — equivalently, if poly d evaluated at A is divisible by p^(2k-m).

Main results

• canonicalIdeal / CanonicalAdmissible — the two definitions.
• canonicalZSpan — the ℤ-submodule spanned by the two generators.
• canonicalIdeal_eq_zSpan — under k ≤ m ≤ 2·k and admissibility, the underlying additive subgroup of canonicalIdeal coincides with canonicalZSpan. The proof goes via τ-stability of canonicalZSpan.

The arithmetic content (index = p^m, existence and uniqueness of canonical forms) is developed in subsequent PRs on top of this scaffolding.

Definitions

noncomputable def QuadraticOrder.canonicalIdeal (d : ℤ) (p k m : ℕ) (A : ℤ) : Ideal (QuadraticOrder d)

The canonical ideal ⟨p^k, p^(m-k) · (τ - A)⟩ of QuadraticOrder d. The intended parameter range is m/2 ≤ k ≤ m with A taken modulo p^(2k-m).

Equations

• QuadraticOrder.canonicalIdeal d p k m A = Ideal.span {↑p ^ k, ↑p ^ (m - k) * (QuadraticOrder.tau - ↑A)}

def QuadraticOrder.CanonicalAdmissible (d : ℤ) (p k m : ℕ) (A : ℤ) : Prop

A canonical-form parameter (k, A) is admissible at index p^m if p^(2k-m) divides A² - dA + (d²-d)/4 — equivalently, the integer (poly d).eval A is divisible by p^(2k-m).

The ℕ-subtraction 2 * k - m is 0 whenever 2 * k < m, in which case the predicate is vacuous; this is used only in tandem with the m ≤ 2 * k constraint.

Equations

• QuadraticOrder.CanonicalAdmissible d p k m A = (↑p ^ (2 * k - m) ∣ A ^ 2 - d * A + (d ^ 2 - d) / 4)

The "Z-span" of the two canonical generators

We work with canonicalZSpan := Submodule.span ℤ {p^k, p^(m-k)·(τ-A)} as an intermediate stepping stone: under the canonical hypotheses we prove it coincides with canonicalIdeal as an additive subgroup, and it admits the obvious ℤ-basis used in the determinant computation.

noncomputable def QuadraticOrder.canonicalZSpan (d : ℤ) (p k m : ℕ) (A : ℤ) : Submodule ℤ (QuadraticOrder d)

The ℤ-span of the two canonical generators {p^k · 1, p^(m-k) · (τ - A)} inside QuadraticOrder d.

Equations

• QuadraticOrder.canonicalZSpan d p k m A = Submodule.span ℤ {↑p ^ k, ↑p ^ (m - k) * (QuadraticOrder.tau - ↑A)}

τ-stability of the generators

These two identities are the arithmetic core: they exhibit τ · g as an integer linear combination of the two generators, for each generator g. The first needs only m ≤ 2·k; the second also needs admissibility.

R-stability of the Z-span

Canonical ideal = canonical Z-span (under admissibility)

theorem QuadraticOrder.canonicalIdeal_eq_zSpan {d : ℤ} {p k m : ℕ} {A : ℤ} (hk_hi : k ≤ m) (hk_lo : m ≤ 2 * k) (hA : CanonicalAdmissible d p k m A) : Submodule.restrictScalars ℤ (canonicalIdeal d p k m A) = canonicalZSpan d p k m A

Under k ≤ m ≤ 2·k and admissibility, the underlying additive subgroup of canonicalIdeal coincides with the Z-span of its two generators.