The discriminant and the invariant factors of ℤ[conj α] (biquadratic case)

In the model V4Data O of BiquadraticModel, A = ℤ[x₀, …, x₃] is the subring generated by the conjugates (Aring), ℤ[α] = ℤ + ℤα + ℤα² + ℤα³, indices are AddSubgroup.relIndex, and D(ω) = det[γ_i(ω_l)]. The triangular basis of A (Louboutin 2020, Prop. 10; Cohen 1993, Cor. 4.7.6) enters as the structure Louboutin.Triang for the image of A in ℚ⁴; it is used only for d₁, d₂, d₃ and the isomorphism. d₁ = 1 is proved, not assumed.

The route: [A : L] = 2 for L = ⟨1, η₁, η₂, η₃⟩ is shown by exhibiting A = L + ℤy through ring closure, where each product has an odd multiple in L + ℤy (a 2-adic computation) and a power-of-2 multiple in ⟨1, ϑ_j⟩, glued by Bézout; indices are computed by determinants (AddSubgroup.relIndex_eq_natAbs_det); d₂ is read from coordinates in the ϑ-basis, a global replacement of a local Nakayama argument.

Main results

• Louboutin.DiscV4.thm_disc: the discriminant theorem, with (n_j, t_j), h₀, m₀, g.
• Louboutin.DiscV4.Dat.prop_discA: g ∣ Δ, [A : ℤ[α]] = |Δ|/g, g² = Δ₁Δ₂Δ₃, and D(b)² = g² for every basis b of A (so disc A = g²).
• Louboutin.DiscV4.Dat.prop_smith: h₀ ∈ {1, 2}, h₀ ∣ m₀, d₁ = 1, d₂ = m₀/h₀, d₃ = I h₀/m₀, A/ℤ[α] ≅ ℤ/(m₀/h₀) × ℤ/(I h₀/m₀), and {1, α, α², ω} is a basis iff m₀ = h₀.

References

• S. R. Louboutin, On the order generated by the conjugates of an algebraic integer, in: Algebra, Logic and Number Theory, Banach Center Publ. 121 (2020), 107–124, doi:10.4064/bc121-10.
• S. R. Louboutin, When is the order generated by a cubic, quartic or quintic algebraic unit Galois invariant: three conjectures, Czechoslovak Math. J. 70 (2020), 905–919, doi:10.21136/CMJ.2020.0019-19.
• C. Marín, Orders generated by conjugates of Galois quartic integers, preprint (2026).

Part 1. Pure integer core

structure Louboutin.DiscV4.ZD : Type

Integer data extracted from the model (see Dat.toZD).

• a : ℤ
• n₁ : ℤ
• n₂ : ℤ
• n₃ : ℤ
• t₁ : ℤ
• t₂ : ℤ
• t₃ : ℤ
• e₁ : ℤ
• e₂ : ℤ
• e₃ : ℤ
• Δ₁ : ℤ
• Δ₂ : ℤ
• Δ₃ : ℤ
• Θ : ℤ
• δ : ℤ
• cop₁ : IsCoprime self.n₁ self.t₁
• cop₂ : IsCoprime self.n₂ self.t₂
• cop₃ : IsCoprime self.n₃ self.t₃
• I₁ : self.n₂ * self.n₃ * self.Θ = (self.a * self.n₁ - 4 * self.t₁) * self.Δ₁
• I₂ : self.n₁ * self.n₃ * self.Θ = (self.a * self.n₂ - 4 * self.t₂) * self.Δ₂
• I₃ : self.n₁ * self.n₂ * self.Θ = (self.a * self.n₃ - 4 * self.t₃) * self.Δ₃
• hΘ2 : self.Θ * self.Θ = self.Δ₁ * self.Δ₂ * self.Δ₃
• Θ0 : self.Θ ≠ 0
• nz₁ : ¬(self.n₂ = 0 ∧ self.n₃ = 0)
• nz₂ : ¬(self.n₁ = 0 ∧ self.n₃ = 0)
• nz₃ : ¬(self.n₁ = 0 ∧ self.n₂ = 0)
• sq₁ : 4 ∣ self.Δ₁ - self.e₁ ^ 2
• sq₂ : 4 ∣ self.Δ₂ - self.e₂ ^ 2
• sq₃ : 4 ∣ self.Δ₃ - self.e₃ ^ 2
• asq₁ : 4 ∣ self.a ^ 2 - self.n₁ ^ 2 * self.Δ₁
• F1 : 2 ∣ self.n₁ → 2 ∣ self.n₂ → 2 ∣ self.n₃ → 4 ∣ self.a - (self.n₁ * self.e₁ + self.n₂ * self.e₂ + self.n₃ * self.e₃)
• minors : self.Θ * ((self.n₁ * self.t₂ - self.n₂ * self.t₁) * (self.n₂ * self.t₃ - self.n₃ * self.t₂) * (self.n₃ * self.t₁ - self.n₁ * self.t₃)) = self.δ * (self.n₁ * self.n₂ * self.n₃)
• δ0 : self.δ ≠ 0

theorem Louboutin.DiscV4.ZD.Δ0₁ (Z : ZD) : Z.Δ₁ ≠ 0

theorem Louboutin.DiscV4.ZD.Δ0₂ (Z : ZD) : Z.Δ₂ ≠ 0

theorem Louboutin.DiscV4.ZD.Δ0₃ (Z : ZD) : Z.Δ₃ ≠ 0

theorem Louboutin.DiscV4.ZD.P₃ (Z : ZD) : Z.n₁ * Z.n₂ * Z.n₃ ^ 2 * Z.Δ₃ = (Z.a * Z.n₁ - 4 * Z.t₁) * (Z.a * Z.n₂ - 4 * Z.t₂)

pair identities P_l: n_j n_k n_l² Δ_l = c_j c_k.

theorem Louboutin.DiscV4.ZD.P₂ (Z : ZD) : Z.n₁ * Z.n₃ * Z.n₂ ^ 2 * Z.Δ₂ = (Z.a * Z.n₁ - 4 * Z.t₁) * (Z.a * Z.n₃ - 4 * Z.t₃)

theorem Louboutin.DiscV4.ZD.P₁ (Z : ZD) : Z.n₂ * Z.n₃ * Z.n₁ ^ 2 * Z.Δ₁ = (Z.a * Z.n₂ - 4 * Z.t₂) * (Z.a * Z.n₃ - 4 * Z.t₃)

theorem Louboutin.DiscV4.ZD.triple (Z : ZD) : (Z.n₁ * Z.n₂ * Z.n₃) ^ 2 * Z.Θ = (Z.a * Z.n₁ - 4 * Z.t₁) * (Z.a * Z.n₂ - 4 * Z.t₂) * (Z.a * Z.n₃ - 4 * Z.t₃)

triple identity: (n₁n₂n₃)² Θ = c₁c₂c₃.

Parity helpers

theorem Louboutin.DiscV4.not_dvd_t {p n t : ℤ} (hp : Prime p) (h : IsCoprime n t) (hn : p ∣ n) : ¬p ∣ t

theorem Louboutin.DiscV4.c_not_dvd {p : ℤ} (hp : Prime p) (hp2 : ¬p ∣ 2) {a n t : ℤ} (h : IsCoprime n t) (hn : p ∣ n) : ¬p ∣ a * n - 4 * t

theorem Louboutin.DiscV4.odd_of_cop_even {n t : ℤ} (h : IsCoprime n t) (hn : 2 ∣ n) : ¬Even t

theorem Louboutin.DiscV4.sq_mod4_odd {e : ℤ} (he : ¬Even e) : ¬4 ∣ e ^ 2

theorem Louboutin.DiscV4.even_iff_of_dvd4 {Δ e : ℤ} (h : 4 ∣ Δ - e ^ 2) : Even Δ ↔ Even e

theorem Louboutin.DiscV4.even_of_dvd4 {Δ e : ℤ} (h : 4 ∣ Δ - e ^ 2) (hΔ : 4 ∣ Δ) : Even e

theorem Louboutin.DiscV4.cop4_of_odd {u : ℤ} (hu : ¬Even u) : IsCoprime 4 u

def Louboutin.DiscV4.ev (x : ℤ) : Bool

parity as a Boolean (for decide).

Equations

• Louboutin.DiscV4.ev x = decide (Even x)

theorem Louboutin.DiscV4.ev_true {x : ℤ} : ev x = true ↔ Even x

theorem Louboutin.DiscV4.ev_false {x : ℤ} : ev x = false ↔ ¬Even x

theorem Louboutin.DiscV4.ev_iff {x y : ℤ} (h : Even x ↔ Even y) : ev x = ev y

theorem Louboutin.DiscV4.ev_mul (x y : ℤ) : ev (x * y) = (ev x || ev y)

theorem Louboutin.DiscV4.ev_add (x y : ℤ) : ev (x + y) = (ev x == ev y)

theorem Louboutin.DiscV4.ev_sub (x y : ℤ) : ev (x - y) = (ev x == ev y)

theorem Louboutin.DiscV4.ev_sq (x : ℤ) : ev (x ^ 2) = ev x

def Louboutin.DiscV4.ZD.d₁₂ (Z : ZD) : ℤ

the minors d_ij = n_i t_j − n_j t_i and the note's h₀, m₀.

Equations

• Z.d₁₂ = Z.n₁ * Z.t₂ - Z.n₂ * Z.t₁

def Louboutin.DiscV4.ZD.d₁₃ (Z : ZD) : ℤ

Equations

• Z.d₁₃ = Z.n₁ * Z.t₃ - Z.n₃ * Z.t₁

def Louboutin.DiscV4.ZD.d₂₃ (Z : ZD) : ℤ

Equations

• Z.d₂₃ = Z.n₂ * Z.t₃ - Z.n₃ * Z.t₂

def Louboutin.DiscV4.ZD.h0 (Z : ZD) : ℕ

Equations

• Z.h0 = (↑(Z.n₁.gcd Z.n₂)).gcd Z.n₃

def Louboutin.DiscV4.ZD.m0 (Z : ZD) : ℕ

Equations

• Z.m0 = (↑(Z.d₁₂.gcd Z.d₁₃)).gcd Z.d₂₃

theorem Louboutin.DiscV4.ZD.h0_dvd₁ (Z : ZD) : ↑Z.h0 ∣ Z.n₁

theorem Louboutin.DiscV4.ZD.h0_dvd₂ (Z : ZD) : ↑Z.h0 ∣ Z.n₂

theorem Louboutin.DiscV4.ZD.h0_dvd₃ (Z : ZD) : ↑Z.h0 ∣ Z.n₃

theorem Louboutin.DiscV4.ZD.m0_dvd₁₂ (Z : ZD) : ↑Z.m0 ∣ Z.d₁₂

theorem Louboutin.DiscV4.ZD.m0_dvd₁₃ (Z : ZD) : ↑Z.m0 ∣ Z.d₁₃

theorem Louboutin.DiscV4.ZD.m0_dvd₂₃ (Z : ZD) : ↑Z.m0 ∣ Z.d₂₃

theorem Louboutin.DiscV4.ZD.dvd_h0 (Z : ZD) {k : ℤ} (h1 : k ∣ Z.n₁) (h2 : k ∣ Z.n₂) (h3 : k ∣ Z.n₃) : k ∣ ↑Z.h0

theorem Louboutin.DiscV4.ZD.dvd_m0 (Z : ZD) {k : ℤ} (h1 : k ∣ Z.d₁₂) (h2 : k ∣ Z.d₁₃) (h3 : k ∣ Z.d₂₃) : k ∣ ↑Z.m0

theorem Louboutin.DiscV4.ZD.no_odd_prime (Z : ZD) {p : ℤ} (hp : Prime p) (hp2 : ¬p ∣ 2) : ¬(p ∣ Z.n₁ ∧ p ∣ Z.n₂ ∧ p ∣ Z.n₃)

No odd prime divides n₁, n₂, n₃ (proof of prop:smith, third item).

theorem Louboutin.DiscV4.ZD.a_even (Z : ZD) (h1 : 2 ∣ Z.n₁) : 2 ∣ Z.a

theorem Louboutin.DiscV4.ZD.parity_core (A M1 M2 M3 E1 E2 E3 : Bool) : (M1 || M2 || M3 || E3) = ((A || M1) == false || (A || M2) == false) → (M1 || M3 || M2 || E2) = ((A || M1) == false || (A || M3) == false) → (M2 || M3 || M1 || E1) = ((A || M2) == false || (A || M3) == false) → (A == (((M1 || E1) == (M2 || E2)) == (M3 || E3))) = true → (M1 = false → M2 = false → M3 = false → A = false → E1 = true ∧ E2 = true ∧ E3 = true) → A = false ∧ (M1 = false ∧ M2 = false ∧ M3 = true ∧ (E1 == E2) = false ∨ M1 = false ∧ M2 = true ∧ M3 = false ∧ (E1 == E3) = false ∨ M1 = true ∧ M2 = false ∧ M3 = false ∧ (E2 == E3) = false)

Boolean parity core of the all-even case (2⁷ cases; A = a₀, M_j = m_j, E_j = e_j even).

theorem Louboutin.DiscV4.ZD.even_case (Z : ZD) (h1 : 2 ∣ Z.n₁) (h2 : 2 ∣ Z.n₂) (h3 : 2 ∣ Z.n₃) : ∃ (a0 : ℤ) (m₁ : ℤ) (m₂ : ℤ) (m₃ : ℤ), Z.a = 2 * a0 ∧ Z.n₁ = 2 * m₁ ∧ Z.n₂ = 2 * m₂ ∧ Z.n₃ = 2 * m₃ ∧ ¬Even a0 ∧ (¬Even m₁ ∧ ¬Even m₂ ∧ Even m₃ ∧ ¬Even (Z.e₁ + Z.e₂) ∨ ¬Even m₁ ∧ Even m₂ ∧ ¬Even m₃ ∧ ¬Even (Z.e₁ + Z.e₃) ∨ Even m₁ ∧ ¬Even m₂ ∧ ¬Even m₃ ∧ ¬Even (Z.e₂ + Z.e₃))

The all-even case (Lemma lem:alleven, its first two steps, and the proof of prop:discA): a = 2a₀ with a₀ odd, n_j = 2m_j, exactly one m_j even, and e_i + e_j odd for the other two.

theorem Louboutin.DiscV4.ZD.not_four_dvd_all (Z : ZD) (h1 : 4 ∣ Z.n₁) (h2 : 4 ∣ Z.n₂) (h3 : 4 ∣ Z.n₃) : False

If 4 divides all n_j: contradiction (two of the m_j = n_j/2 are odd).

theorem Louboutin.DiscV4.ZD.h0_ne_zero (Z : ZD) : Z.h0 ≠ 0

theorem Louboutin.DiscV4.ZD.h0_one_or_two (Z : ZD) : Z.h0 = 1 ∨ Z.h0 = 2

prop:smith: h₀ ∈ {1, 2}.

theorem Louboutin.DiscV4.ZD.h0_dvd_m0 (Z : ZD) : Z.h0 ∣ Z.m0

prop:smith: h₀ ∣ m₀.

theorem Louboutin.DiscV4.ZD.unit_of_cop_zero {t : ℤ} (h : IsCoprime 0 t) : t = 1 ∨ t = -1

theorem Louboutin.DiscV4.ZD.m0_eq_h0_of_zero (Z : ZD) (h0N : Z.n₁ * Z.n₂ * Z.n₃ = 0) : Z.m0 = Z.h0

prop:smith, case U = 0: if some n_j = 0 then m₀ = h₀.

theorem Louboutin.DiscV4.ZD.m0_pos (Z : ZD) : 0 < Z.m0

prop:smith: m₀ > 0.

theorem Louboutin.DiscV4.ZD.h0_one_of_odd (Z : ZD) (h : ¬2 ∣ Z.n₁ ∨ ¬2 ∣ Z.n₂ ∨ ¬2 ∣ Z.n₃) : Z.h0 = 1

theorem Louboutin.DiscV4.ZD.h0_two_of_even (Z : ZD) (h1 : 2 ∣ Z.n₁) (h2 : 2 ∣ Z.n₂) (h3 : 2 ∣ Z.n₃) : Z.h0 = 2

theorem Louboutin.DiscV4.ZD.pair_contra {p n t n' t' : ℤ} (hp : Prime p) (hc : IsCoprime n t) (hn : p ∣ n) (hn' : ¬p ∣ n') (hd : p ∣ n * t' - n' * t) : False

p ∣ n, p ∤ n', p ∣ n t' − n' t with gcd(n, t) = 1: impossible.

theorem Louboutin.DiscV4.ZD.coprime_e_N (Z : ZD) : IsCoprime (↑(Z.m0 / Z.h0)) (Z.n₁ * Z.n₂ * Z.n₃)

gcd(m₀/h₀, n₁n₂n₃) = 1 (proof of prop:smith, the bullet items).

Part 2. The V4 model: the note's pairs (n_j, t_j) and the elements ϑ_j

def Louboutin.DiscV4.ntN (D E : ℤ) : ℤ

The note's n_j from (D_j, E_j): D/gcd(D, E) if D ≠ 0, else 0 (prop:smith).

Equations

• Louboutin.DiscV4.ntN D E = if D = 0 then 0 else D / ↑(D.gcd E)

def Louboutin.DiscV4.ntT (D E : ℤ) : ℤ

The note's t_j from (D_j, E_j): E/gcd(D, E) if D ≠ 0, else 1 (prop:smith).

Equations

• Louboutin.DiscV4.ntT D E = if D = 0 then 1 else E / ↑(D.gcd E)

theorem Louboutin.DiscV4.split_note {O : Type u_1} [CommRing O] [IsDomain O] [CharZero O] {r q : O} {D E : ℤ} (hD : r * r = ↑D) (hE : r * q = ↑E) : IsCoprime (ntN D E) (ntT D E) ∧ ∃ (ϑ : O), r = ↑(ntN D E) * ϑ ∧ q = ↑(ntT D E) * ϑ

With r² = D and rq = E (integers), the note's coprime pair (n, t) and some ϑ ∈ O satisfy r = nϑ, q = tϑ (proof of prop:smith, first paragraph; cf. split_pair in Conj61Model).

theorem Louboutin.DiscV4.theta_sign {O : Type u_1} [CommRing O] [IsDomain O] [CharZero O] (σ : O →+* O) {r q ϑ e : O} {n t u v : ℤ} (hb : u * n + v * t = 1) (hr : r = ↑n * ϑ) (hq : q = ↑t * ϑ) (hσr : σ r = e * r) (hσq : σ q = e * q) : σ ϑ = e * ϑ

A coprime splitting inherits the sign of the pair: τ r = e r, τ q = e q ⇒ τ ϑ = e ϑ.

structure Louboutin.DiscV4.Dat {O : Type u_1} [CommRing O] (M : Conj61.V4Data O) : Type u_1

The data of the note's proof of prop:discA / prop:smith in the model: the integers a, b, c, d, z_j, Δ = δ, the coprime pairs (n_j, t_j) with Bézout coefficients (u_j, v_j), the elements ϑ_j with r_j = n_j ϑ_j, q_j = t_j ϑ_j, Δ_j = ϑ_j², Θ = ϑ₁ϑ₂ϑ₃.

• a : ℤ
• b : ℤ
• c : ℤ
• d : ℤ
• ha : Conj61.ea M.x = ↑self.a
• hb : Conj61.eb M.x = ↑self.b
• hc : Conj61.ec M.x = ↑self.c
• hd : Conj61.ed M.x = ↑self.d
• z₁ : ℤ
• z₂ : ℤ
• z₃ : ℤ
• hz₁ : Conj61.z1 M.x = ↑self.z₁
• hz₂ : Conj61.z2 M.x = ↑self.z₂
• hz₃ : Conj61.z3 M.x = ↑self.z₃
• δ : ℤ
• hδ : Conj61.Vand M.x = ↑self.δ
• n₁ : ℤ
• n₂ : ℤ
• n₃ : ℤ
• t₁ : ℤ
• t₂ : ℤ
• t₃ : ℤ
• u₁ : ℤ
• u₂ : ℤ
• u₃ : ℤ
• v₁ : ℤ
• v₂ : ℤ
• v₃ : ℤ
• bez₁ : self.u₁ * self.n₁ + self.v₁ * self.t₁ = 1
• bez₂ : self.u₂ * self.n₂ + self.v₂ * self.t₂ = 1
• bez₃ : self.u₃ * self.n₃ + self.v₃ * self.t₃ = 1
• ϑ₁ : O
• ϑ₂ : O
• ϑ₃ : O
• hr₁ : Conj61.r1 M.x = ↑self.n₁ * self.ϑ₁
• hr₂ : Conj61.r2 M.x = ↑self.n₂ * self.ϑ₂
• hr₃ : Conj61.r3 M.x = ↑self.n₃ * self.ϑ₃
• hq₁ : Conj61.dQ1 M.x = ↑self.t₁ * self.ϑ₁
• hq₂ : Conj61.dQ2 M.x = ↑self.t₂ * self.ϑ₂
• hq₃ : Conj61.dQ3 M.x = ↑self.t₃ * self.ϑ₃
• Δ₁ : ℤ
• Δ₂ : ℤ
• Δ₃ : ℤ
• hΔ₁ : self.ϑ₁ * self.ϑ₁ = ↑self.Δ₁
• hΔ₂ : self.ϑ₂ * self.ϑ₂ = ↑self.Δ₂
• hΔ₃ : self.ϑ₃ * self.ϑ₃ = ↑self.Δ₃
• Θ : ℤ
• hΘ : self.ϑ₁ * self.ϑ₂ * self.ϑ₃ = ↑self.Θ

theorem Louboutin.DiscV4.Dat.exists_note {O : Type u_1} [CommRing O] [IsDomain O] [CharZero O] (M : Conj61.V4Data O) {a b c d z₁ z₂ z₃ δ : ℤ} (ha : Conj61.ea M.x = ↑a) (hb : Conj61.eb M.x = ↑b) (hc : Conj61.ec M.x = ↑c) (hd : Conj61.ed M.x = ↑d) (hz₁ : Conj61.z1 M.x = ↑z₁) (hz₂ : Conj61.z2 M.x = ↑z₂) (hz₃ : Conj61.z3 M.x = ↑z₃) (hδ : Conj61.Vand M.x = ↑δ) : ∃ (P : Dat M), P.a = a ∧ P.b = b ∧ P.c = c ∧ P.d = d ∧ P.z₁ = z₁ ∧ P.z₂ = z₂ ∧ P.z₃ = z₃ ∧ P.δ = δ ∧ P.n₁ = ntN (a ^ 2 - 4 * b + 4 * z₁) (a * z₁ - 2 * c) ∧ P.t₁ = ntT (a ^ 2 - 4 * b + 4 * z₁) (a * z₁ - 2 * c) ∧ P.n₂ = ntN (a ^ 2 - 4 * b + 4 * z₂) (a * z₂ - 2 * c) ∧ P.t₂ = ntT (a ^ 2 - 4 * b + 4 * z₂) (a * z₂ - 2 * c) ∧ P.n₃ = ntN (a ^ 2 - 4 * b + 4 * z₃) (a * z₃ - 2 * c) ∧ P.t₃ = ntT (a ^ 2 - 4 * b + 4 * z₃) (a * z₃ - 2 * c)

Existence of the data with the note's (n_j, t_j) = ntN/ntT (D_j, E_j), D_j = a² − 4b + 4z_j, E_j = a z_j − 2c.

Part 3. Identities in the model

def Louboutin.DiscV4.Dat.e₁ {O : Type u_1} [CommRing O] {M : Conj61.V4Data O} (P : Dat M) : ℤ

e_j = u_j a + v_j z_j (so that ϑ_j = 2η_j − e_j).

Equations

• P.e₁ = P.u₁ * P.a + P.v₁ * P.z₁

def Louboutin.DiscV4.Dat.e₂ {O : Type u_1} [CommRing O] {M : Conj61.V4Data O} (P : Dat M) : ℤ

Equations

• P.e₂ = P.u₂ * P.a + P.v₂ * P.z₂

def Louboutin.DiscV4.Dat.e₃ {O : Type u_1} [CommRing O] {M : Conj61.V4Data O} (P : Dat M) : ℤ

Equations

• P.e₃ = P.u₃ * P.a + P.v₃ * P.z₃

def Louboutin.DiscV4.Dat.η₁ {O : Type u_1} [CommRing O] {M : Conj61.V4Data O} (P : Dat M) : O

η_j = u_j S_j + v_j Q_j with S_j = α + τ_jα, Q_j = α·τ_jα: the generator of C_j = ℤ + ℤS_j + ℤQ_j (Lemma lem:Lambda), with ϑ_j = 2η_j − e_j.

Equations

• P.η₁ = ↑P.u₁ * (M.x 0 + M.x 1) + ↑P.v₁ * (M.x 0 * M.x 1)

def Louboutin.DiscV4.Dat.η₂ {O : Type u_1} [CommRing O] {M : Conj61.V4Data O} (P : Dat M) : O

Equations

• P.η₂ = ↑P.u₂ * (M.x 0 + M.x 2) + ↑P.v₂ * (M.x 0 * M.x 2)

def Louboutin.DiscV4.Dat.η₃ {O : Type u_1} [CommRing O] {M : Conj61.V4Data O} (P : Dat M) : O

Equations

• P.η₃ = ↑P.u₃ * (M.x 0 + M.x 3) + ↑P.v₃ * (M.x 0 * M.x 3)

theorem Louboutin.DiscV4.Dat.ϑ_eq₁ {O : Type u_1} [CommRing O] [IsDomain O] [CharZero O] {M : Conj61.V4Data O} (P : Dat M) : P.ϑ₁ = ↑P.u₁ * Conj61.r1 M.x + ↑P.v₁ * Conj61.dQ1 M.x

theorem Louboutin.DiscV4.Dat.ϑ_eq₂ {O : Type u_1} [CommRing O] [IsDomain O] [CharZero O] {M : Conj61.V4Data O} (P : Dat M) : P.ϑ₂ = ↑P.u₂ * Conj61.r2 M.x + ↑P.v₂ * Conj61.dQ2 M.x

theorem Louboutin.DiscV4.Dat.ϑ_eq₃ {O : Type u_1} [CommRing O] [IsDomain O] [CharZero O] {M : Conj61.V4Data O} (P : Dat M) : P.ϑ₃ = ↑P.u₃ * Conj61.r3 M.x + ↑P.v₃ * Conj61.dQ3 M.x

theorem Louboutin.DiscV4.Dat.two_η₁ {O : Type u_1} [CommRing O] [IsDomain O] [CharZero O] {M : Conj61.V4Data O} (P : Dat M) : 2 * P.η₁ - ↑P.e₁ = P.ϑ₁

theorem Louboutin.DiscV4.Dat.two_η₂ {O : Type u_1} [CommRing O] [IsDomain O] [CharZero O] {M : Conj61.V4Data O} (P : Dat M) : 2 * P.η₂ - ↑P.e₂ = P.ϑ₂

theorem Louboutin.DiscV4.Dat.two_η₃ {O : Type u_1} [CommRing O] [IsDomain O] [CharZero O] {M : Conj61.V4Data O} (P : Dat M) : 2 * P.η₃ - ↑P.e₃ = P.ϑ₃

theorem Louboutin.DiscV4.Dat.four_x0 {O : Type u_1} [CommRing O] [IsDomain O] [CharZero O] {M : Conj61.V4Data O} (P : Dat M) : 4 * M.x 0 = ↑P.a + ↑P.n₁ * P.ϑ₁ + ↑P.n₂ * P.ϑ₂ + ↑P.n₃ * P.ϑ₃

4α = a + n₁ϑ₁ + n₂ϑ₂ + n₃ϑ₃, and its conjugates.

theorem Louboutin.DiscV4.Dat.four_x1 {O : Type u_1} [CommRing O] [IsDomain O] [CharZero O] {M : Conj61.V4Data O} (P : Dat M) : 4 * M.x 1 = ↑P.a + ↑P.n₁ * P.ϑ₁ - ↑P.n₂ * P.ϑ₂ - ↑P.n₃ * P.ϑ₃

theorem Louboutin.DiscV4.Dat.four_x2 {O : Type u_1} [CommRing O] [IsDomain O] [CharZero O] {M : Conj61.V4Data O} (P : Dat M) : 4 * M.x 2 = ↑P.a - ↑P.n₁ * P.ϑ₁ + ↑P.n₂ * P.ϑ₂ - ↑P.n₃ * P.ϑ₃

theorem Louboutin.DiscV4.Dat.four_x3 {O : Type u_1} [CommRing O] [IsDomain O] [CharZero O] {M : Conj61.V4Data O} (P : Dat M) : 4 * M.x 3 = ↑P.a - ↑P.n₁ * P.ϑ₁ - ↑P.n₂ * P.ϑ₂ + ↑P.n₃ * P.ϑ₃

theorem Louboutin.DiscV4.Dat.prod₁ {O : Type u_1} [CommRing O] [IsDomain O] [CharZero O] {M : Conj61.V4Data O} (P : Dat M) : ↑P.n₂ * ↑P.n₃ * (P.ϑ₂ * P.ϑ₃) = (↑P.a * ↑P.n₁ - 4 * ↑P.t₁) * P.ϑ₁

r_k r_l = a r_j − 4q_j, i.e. n_k n_l ϑ_k ϑ_l = (a n_j − 4 t_j) ϑ_j (proof of lem:Lodd).

theorem Louboutin.DiscV4.Dat.prod₂ {O : Type u_1} [CommRing O] [IsDomain O] [CharZero O] {M : Conj61.V4Data O} (P : Dat M) : ↑P.n₁ * ↑P.n₃ * (P.ϑ₁ * P.ϑ₃) = (↑P.a * ↑P.n₂ - 4 * ↑P.t₂) * P.ϑ₂

theorem Louboutin.DiscV4.Dat.prod₃ {O : Type u_1} [CommRing O] [IsDomain O] [CharZero O] {M : Conj61.V4Data O} (P : Dat M) : ↑P.n₁ * ↑P.n₂ * (P.ϑ₁ * P.ϑ₂) = (↑P.a * ↑P.n₃ - 4 * ↑P.t₃) * P.ϑ₃

theorem Louboutin.DiscV4.Dat.ϑ₁_ne {O : Type u_1} [CommRing O] [IsDomain O] [CharZero O] {M : Conj61.V4Data O} (P : Dat M) : P.ϑ₁ ≠ 0

ϑ_j ≠ 0: (α − x_k)(α − x_l) = α r_j − q_j = (α n_j − t_j) ϑ_j.

theorem Louboutin.DiscV4.Dat.ϑ₂_ne {O : Type u_1} [CommRing O] [IsDomain O] [CharZero O] {M : Conj61.V4Data O} (P : Dat M) : P.ϑ₂ ≠ 0

theorem Louboutin.DiscV4.Dat.ϑ₃_ne {O : Type u_1} [CommRing O] [IsDomain O] [CharZero O] {M : Conj61.V4Data O} (P : Dat M) : P.ϑ₃ ≠ 0

theorem Louboutin.DiscV4.Dat.Θ_ne {O : Type u_1} [CommRing O] [IsDomain O] [CharZero O] {M : Conj61.V4Data O} (P : Dat M) : P.Θ ≠ 0

theorem Louboutin.DiscV4.Dat.I₁ {O : Type u_1} [CommRing O] [IsDomain O] [CharZero O] {M : Conj61.V4Data O} (P : Dat M) : P.n₂ * P.n₃ * P.Θ = (P.a * P.n₁ - 4 * P.t₁) * P.Δ₁

integer identities I_j: n_k n_l Θ = (a n_j − 4t_j) Δ_j.

theorem Louboutin.DiscV4.Dat.I₂ {O : Type u_1} [CommRing O] [IsDomain O] [CharZero O] {M : Conj61.V4Data O} (P : Dat M) : P.n₁ * P.n₃ * P.Θ = (P.a * P.n₂ - 4 * P.t₂) * P.Δ₂

theorem Louboutin.DiscV4.Dat.I₃ {O : Type u_1} [CommRing O] [IsDomain O] [CharZero O] {M : Conj61.V4Data O} (P : Dat M) : P.n₁ * P.n₂ * P.Θ = (P.a * P.n₃ - 4 * P.t₃) * P.Δ₃

theorem Louboutin.DiscV4.Dat.hΘ2 {O : Type u_1} [CommRing O] [IsDomain O] [CharZero O] {M : Conj61.V4Data O} (P : Dat M) : P.Θ * P.Θ = P.Δ₁ * P.Δ₂ * P.Δ₃

theorem Louboutin.DiscV4.Dat.nz₁ {O : Type u_1} [CommRing O] [IsDomain O] [CharZero O] {M : Conj61.V4Data O} (P : Dat M) : ¬(P.n₂ = 0 ∧ P.n₃ = 0)

At most one n_j vanishes (proof of prop:smith, Preliminaries).

theorem Louboutin.DiscV4.Dat.nz₂ {O : Type u_1} [CommRing O] [IsDomain O] [CharZero O] {M : Conj61.V4Data O} (P : Dat M) : ¬(P.n₁ = 0 ∧ P.n₃ = 0)

theorem Louboutin.DiscV4.Dat.nz₃ {O : Type u_1} [CommRing O] [IsDomain O] [CharZero O] {M : Conj61.V4Data O} (P : Dat M) : ¬(P.n₁ = 0 ∧ P.n₂ = 0)

theorem Louboutin.DiscV4.Dat.sq₁ {O : Type u_1} [CommRing O] [IsDomain O] [CharZero O] {M : Conj61.V4Data O} (P : Dat M) : 4 ∣ P.Δ₁ - P.e₁ ^ 2

Δ_j ≡ e_j² (mod 4): Δ_j − e_j² = 4(η_j² − e_j η_j).

theorem Louboutin.DiscV4.Dat.sq₂ {O : Type u_1} [CommRing O] [IsDomain O] [CharZero O] {M : Conj61.V4Data O} (P : Dat M) : 4 ∣ P.Δ₂ - P.e₂ ^ 2

theorem Louboutin.DiscV4.Dat.sq₃ {O : Type u_1} [CommRing O] [IsDomain O] [CharZero O] {M : Conj61.V4Data O} (P : Dat M) : 4 ∣ P.Δ₃ - P.e₃ ^ 2

theorem Louboutin.DiscV4.Dat.asq₁ {O : Type u_1} [CommRing O] [IsDomain O] [CharZero O] {M : Conj61.V4Data O} (P : Dat M) : 4 ∣ P.a ^ 2 - P.n₁ ^ 2 * P.Δ₁

a² − n₁²Δ₁ = 4(b − z₁) (from r₁² = a² − 4b + 4z₁).

theorem Louboutin.DiscV4.Dat.F1 {O : Type u_1} [CommRing O] [IsDomain O] [CharZero O] {M : Conj61.V4Data O} (P : Dat M) : 2 ∣ P.n₁ → 2 ∣ P.n₂ → 2 ∣ P.n₃ → 4 ∣ P.a - (P.n₁ * P.e₁ + P.n₂ * P.e₂ + P.n₃ * P.e₃)

2α − Σ n_j η_j is an integer s with a − Σ n_j e_j = 2s; if all n_j are even, 4 ∣ a − Σ n_j e_j.

theorem Louboutin.DiscV4.Dat.minors {O : Type u_1} [CommRing O] [IsDomain O] [CharZero O] {M : Conj61.V4Data O} (P : Dat M) : P.Θ * ((P.n₁ * P.t₂ - P.n₂ * P.t₁) * (P.n₂ * P.t₃ - P.n₃ * P.t₂) * (P.n₃ * P.t₁ - P.n₁ * P.t₃)) = P.δ * (P.n₁ * P.n₂ * P.n₃)

Θ·d₁₂d₂₃d₃₁ = Δ·n₁n₂n₃ (from cross_prod; proof of cor:weak).

def Louboutin.DiscV4.Dat.toZD {O : Type u_1} [CommRing O] [IsDomain O] [CharZero O] {M : Conj61.V4Data O} (P : Dat M) : ZD

The integer data of the model.

Equations

• One or more equations did not get rendered due to their size.

Part 4. Lattices in O: the determinant D (the note's detG), indices, Cramer

noncomputable def Louboutin.DiscV4.D {O : Type u_1} [CommRing O] (M : Conj61.V4Data O) (w : Fin 4 → O) : O

D(ω) = det[γ_i(ω_l)], the note's detG (γ₀ = id, γ_j = τ_j).

Equations

• Louboutin.DiscV4.D M w = (Matrix.of fun (i l : Fin 4) => (M.ρ i) (w l)).det

theorem Louboutin.DiscV4.D_comb {O : Type u_1} [CommRing O] [IsDomain O] [CharZero O] (M : Conj61.V4Data O) (v w : Fin 4 → O) (C : Matrix (Fin 4) (Fin 4) ℤ) (h : ∀ (l : Fin 4), w l = ∑ k : Fin 4, ↑(C l k) * v k) : D M w = D M v * ↑C.det

Lemma lem:sub (general form): if ω'_l = Σ_k C_lk ω_k with C integral, D(ω') = D(ω) det C.

theorem Louboutin.DiscV4.linIndep_of_D {O : Type u_1} [CommRing O] [IsDomain O] [CharZero O] (M : Conj61.V4Data O) {v : Fin 4 → O} (hv : D M v ≠ 0) : LinearIndependent ℤ v

D(ω) ≠ 0 ⇒ ω₁, …, ω₄ are ℤ-independent.

@[reducible, inline]

abbrev Louboutin.DiscV4.Lat {O : Type u_1} [CommRing O] (v : Fin 4 → O) : AddSubgroup O

The lattice spanned by a family.

Equations

• Louboutin.DiscV4.Lat v = (Submodule.span ℤ (Set.range v)).toAddSubgroup

theorem Louboutin.DiscV4.relIndex_D {O : Type u_1} [CommRing O] [IsDomain O] [CharZero O] (M : Conj61.V4Data O) {v w : Fin 4 → O} (hv : D M v ≠ 0) (hw : D M w ≠ 0) (hwv : ∀ (l : Fin 4), w l ∈ Submodule.span ℤ (Set.range v)) : ∃ (C : Matrix (Fin 4) (Fin 4) ℤ), D M w = D M v * ↑C.det ∧ (Lat w).relIndex (Lat v) = C.det.natAbs

Index of lattices by determinants (AddSubgroup.relIndex_eq_natAbs_det): [⟨v⟩ : ⟨w⟩] = |det C| where w = C v, and D(w) = D(v) det C.

Part 5. The order A = ℤ[x₁, …, x₄], Cramer's rule, and the closure arguments

def Louboutin.DiscV4.Aring {O : Type u_1} [CommRing O] (M : Conj61.V4Data O) : Subring O

A = ℤ[conj(α)] = ℤ[x₁, x₂, x₃, x₄], the subring generated by the conjugates.

Equations

• Louboutin.DiscV4.Aring M = Subring.closure (Set.range M.x)

theorem Louboutin.DiscV4.x_mem_A {O : Type u_1} [CommRing O] [IsDomain O] [CharZero O] (M : Conj61.V4Data O) (k : Fin 4) : M.x k ∈ Aring M

theorem Louboutin.DiscV4.ρ_x {O : Type u_1} [CommRing O] [IsDomain O] [CharZero O] (M : Conj61.V4Data O) (a k : Fin 4) : (M.ρ a) (M.x k) = M.x (Conj61.xt a k)

theorem Louboutin.DiscV4.xt_assoc (a i k : Fin 4) : Conj61.xt a (Conj61.xt i k) = Conj61.xt (Conj61.xt a i) k

def Louboutin.DiscV4.compSub {O : Type u_1} [CommRing O] (M : Conj61.V4Data O) : Subring O

The elements on which the γ's compose as the group V₄ (γ_a γ_i = γ_{a xor i}).

Equations

• One or more equations did not get rendered due to their size.

theorem Louboutin.DiscV4.comp_of_mem {O : Type u_1} [CommRing O] [IsDomain O] [CharZero O] (M : Conj61.V4Data O) {y : O} (hy : y ∈ Aring M) (a i : Fin 4) : (M.ρ a) ((M.ρ i) y) = (M.ρ (Conj61.xt a i)) y

def Louboutin.DiscV4.xtPerm (a : Fin 4) : Equiv.Perm (Fin 4)

the permutation k ↦ a xor k.

Equations

• Louboutin.DiscV4.xtPerm a = { toFun := Louboutin.Conj61.xt a, invFun := Louboutin.Conj61.xt a, left_inv := ⋯, right_inv := ⋯ }

theorem Louboutin.DiscV4.sign_xtPerm (a : Fin 4) : Equiv.Perm.sign (xtPerm a) = 1

theorem Louboutin.DiscV4.cramer_mem {O : Type u_1} [CommRing O] [IsDomain O] [CharZero O] (M : Conj61.V4Data O) {y : O} (hy : y ∈ Aring M) : Conj61.Vand M.x * y ∈ M.Zα

Cramer's rule with integer numerators (Lemma lem:cramer, first part, for every y ∈ A): Δ·y ∈ ℤ[α].

theorem Louboutin.DiscV4.A_le_of_stable {O : Type u_1} [CommRing O] [IsDomain O] [CharZero O] (M : Conj61.V4Data O) (N : Submodule ℤ O) (h1 : 1 ∈ N) (hmul : ∀ (m : Fin 4), ∀ w ∈ N, M.x m * w ∈ N) (y : O) : y ∈ Aring M → y ∈ N

If 1 ∈ N and N is stable under multiplication by every conjugate, then A ⊆ N.

theorem Louboutin.DiscV4.stable_of_gens {O : Type u_1} [CommRing O] [IsDomain O] [CharZero O] (M : Conj61.V4Data O) (G : Set O) (m : Fin 4) (h : ∀ g ∈ G, M.x m * g ∈ Submodule.span ℤ G) (w : O) : w ∈ Submodule.span ℤ G → M.x m * w ∈ Submodule.span ℤ G

Stability can be checked on generators.

theorem Louboutin.DiscV4.bezout_mem {O : Type u_1} [CommRing O] [IsDomain O] [CharZero O] (N : Submodule ℤ O) {z : O} {s : ℤ} (hs : ¬Even s) (k : ℕ) (h1 : ↑s * z ∈ N) (h2 : 2 ^ k * z ∈ N) : z ∈ N

Local-global by Bézout: s·z ∈ N with s odd and 2ᵏ·z ∈ N give z ∈ N.

Part 6. The lattices M = ⟨1, ϑ_j⟩ ⊆ L = ⟨1, η_j⟩ ⊆ A, and ℤ[α]

theorem Louboutin.DiscV4.Dat.ϑ₁_mem {O : Type u_1} [CommRing O] [IsDomain O] [CharZero O] {M : Conj61.V4Data O} (P : Dat M) : P.ϑ₁ ∈ Aring M

theorem Louboutin.DiscV4.Dat.ϑ₂_mem {O : Type u_1} [CommRing O] [IsDomain O] [CharZero O] {M : Conj61.V4Data O} (P : Dat M) : P.ϑ₂ ∈ Aring M

theorem Louboutin.DiscV4.Dat.ϑ₃_mem {O : Type u_1} [CommRing O] [IsDomain O] [CharZero O] {M : Conj61.V4Data O} (P : Dat M) : P.ϑ₃ ∈ Aring M

theorem Louboutin.DiscV4.Dat.η₁_mem {O : Type u_1} [CommRing O] [IsDomain O] [CharZero O] {M : Conj61.V4Data O} (P : Dat M) : P.η₁ ∈ Aring M

theorem Louboutin.DiscV4.Dat.η₂_mem {O : Type u_1} [CommRing O] [IsDomain O] [CharZero O] {M : Conj61.V4Data O} (P : Dat M) : P.η₂ ∈ Aring M

theorem Louboutin.DiscV4.Dat.η₃_mem {O : Type u_1} [CommRing O] [IsDomain O] [CharZero O] {M : Conj61.V4Data O} (P : Dat M) : P.η₃ ∈ Aring M

theorem Louboutin.DiscV4.Dat.sgnϑ {O : Type u_1} [CommRing O] [IsDomain O] [CharZero O] {M : Conj61.V4Data O} (P : Dat M) : M.τ₁ P.ϑ₁ = P.ϑ₁ ∧ M.τ₁ P.ϑ₂ = -P.ϑ₂ ∧ M.τ₁ P.ϑ₃ = -P.ϑ₃ ∧ M.τ₂ P.ϑ₁ = -P.ϑ₁ ∧ M.τ₂ P.ϑ₂ = P.ϑ₂ ∧ M.τ₂ P.ϑ₃ = -P.ϑ₃ ∧ M.τ₃ P.ϑ₁ = -P.ϑ₁ ∧ M.τ₃ P.ϑ₂ = -P.ϑ₂ ∧ M.τ₃ P.ϑ₃ = P.ϑ₃

the action of V₄ on the ϑ_j (each is an eigenvector of a nontrivial character).

def Louboutin.DiscV4.Dat.vϑ {O : Type u_1} [CommRing O] {M : Conj61.V4Data O} (P : Dat M) : Fin 4 → O

the families 1, ϑ_j; 1, η_j; Δ, Δϑ_j; and 1, α, α², α³.

Equations

• P.vϑ = ![1, P.ϑ₁, P.ϑ₂, P.ϑ₃]

def Louboutin.DiscV4.Dat.vη {O : Type u_1} [CommRing O] {M : Conj61.V4Data O} (P : Dat M) : Fin 4 → O

Equations

• P.vη = ![1, P.η₁, P.η₂, P.η₃]

def Louboutin.DiscV4.Dat.vX {O : Type u_1} [CommRing O] {M : Conj61.V4Data O} (P : Dat M) : Fin 4 → O

Equations

• P.vX = ![↑P.δ, ↑P.δ * P.ϑ₁, ↑P.δ * P.ϑ₂, ↑P.δ * P.ϑ₃]

def Louboutin.DiscV4.Dat.vpow {O : Type u_1} [CommRing O] (M : Conj61.V4Data O) : Fin 4 → O

Equations

• Louboutin.DiscV4.Dat.vpow M k = M.x 0 ^ ↑k

theorem Louboutin.DiscV4.Dat.D_vϑ {O : Type u_1} [CommRing O] [IsDomain O] [CharZero O] {M : Conj61.V4Data O} (P : Dat M) : D M P.vϑ = -16 * ↑P.Θ

D(1, ϑ₁, ϑ₂, ϑ₃) = −16Θ (the ϑ_j are eigenvectors of the three nontrivial characters).

theorem Louboutin.DiscV4.Dat.D_vpow {O : Type u_1} [CommRing O] [IsDomain O] [CharZero O] {M : Conj61.V4Data O} : D M (vpow M) = Conj61.Vand M.x

theorem Louboutin.DiscV4.Dat.det_C8 (e₁ e₂ e₃ : ℤ) : !![1, 0, 0, 0; -e₁, 2, 0, 0; -e₂, 0, 2, 0; -e₃, 0, 0, 2].det = 8

theorem Louboutin.DiscV4.Dat.det_Cδ (δ : ℤ) : !![δ, 0, 0, 0; 0, δ, 0, 0; 0, 0, δ, 0; 0, 0, 0, δ].det = δ ^ 4

theorem Louboutin.DiscV4.Dat.D_vη {O : Type u_1} [CommRing O] [IsDomain O] [CharZero O] {M : Conj61.V4Data O} (P : Dat M) : D M P.vη = -2 * ↑P.Θ

theorem Louboutin.DiscV4.Dat.D_vX {O : Type u_1} [CommRing O] [IsDomain O] [CharZero O] {M : Conj61.V4Data O} (P : Dat M) : D M P.vX = ↑P.δ ^ 4 * (-16 * ↑P.Θ)

Part 7. M[1/2] is a ring containing A; the indices of M, L, X, ℤ[α]

theorem Louboutin.DiscV4.Dat.four_ϑ₁ {O : Type u_1} [CommRing O] [IsDomain O] [CharZero O] {M : Conj61.V4Data O} (P : Dat M) : 4 * P.ϑ₁ = (4 * ↑P.u₁ + ↑P.a * ↑P.v₁) * ↑P.n₁ * P.ϑ₁ - ↑P.v₁ * ↑P.n₂ * ↑P.n₃ * (P.ϑ₂ * P.ϑ₃)

4ϑ_j = (4u_j + a v_j) n_j ϑ_j − v_j n_k n_l ϑ_k ϑ_l (from 4q_j = a r_j − r_k r_l).

theorem Louboutin.DiscV4.Dat.four_ϑ₂ {O : Type u_1} [CommRing O] [IsDomain O] [CharZero O] {M : Conj61.V4Data O} (P : Dat M) : 4 * P.ϑ₂ = (4 * ↑P.u₂ + ↑P.a * ↑P.v₂) * ↑P.n₂ * P.ϑ₂ - ↑P.v₂ * ↑P.n₁ * ↑P.n₃ * (P.ϑ₁ * P.ϑ₃)

theorem Louboutin.DiscV4.Dat.four_ϑ₃ {O : Type u_1} [CommRing O] [IsDomain O] [CharZero O] {M : Conj61.V4Data O} (P : Dat M) : 4 * P.ϑ₃ = (4 * ↑P.u₃ + ↑P.a * ↑P.v₃) * ↑P.n₃ * P.ϑ₃ - ↑P.v₃ * ↑P.n₁ * ↑P.n₂ * (P.ϑ₁ * P.ϑ₂)

theorem Louboutin.DiscV4.Dat.sixteen₁₂ {O : Type u_1} [CommRing O] [IsDomain O] [CharZero O] {M : Conj61.V4Data O} (P : Dat M) : ∃ (K : ℤ), 16 * (P.ϑ₁ * P.ϑ₂) = ↑K * P.ϑ₃

16 ϑ_i ϑ_j ∈ ℤ ϑ_k (so M[1/2] is a ring; cf. the proof of lem:Lodd).

theorem Louboutin.DiscV4.Dat.sixteen₁₃ {O : Type u_1} [CommRing O] [IsDomain O] [CharZero O] {M : Conj61.V4Data O} (P : Dat M) : ∃ (K : ℤ), 16 * (P.ϑ₁ * P.ϑ₃) = ↑K * P.ϑ₂

theorem Louboutin.DiscV4.Dat.sixteen₂₃ {O : Type u_1} [CommRing O] [IsDomain O] [CharZero O] {M : Conj61.V4Data O} (P : Dat M) : ∃ (K : ℤ), 16 * (P.ϑ₂ * P.ϑ₃) = ↑K * P.ϑ₁

@[reducible, inline]

abbrev Louboutin.DiscV4.Dat.Mℓ {O : Type u_1} [CommRing O] {M : Conj61.V4Data O} (P : Dat M) : Submodule ℤ O

M = ℤ + ℤϑ₁ + ℤϑ₂ + ℤϑ₃ (as a ℤ-submodule of O).

Equations

• P.Mℓ = Submodule.span ℤ (Set.range P.vϑ)

@[reducible, inline]

abbrev Louboutin.DiscV4.Dat.Lℓ {O : Type u_1} [CommRing O] {M : Conj61.V4Data O} (P : Dat M) : Submodule ℤ O

L = ℤ + ℤη₁ + ℤη₂ + ℤη₃.

Equations

• P.Lℓ = Submodule.span ℤ (Set.range P.vη)

theorem Louboutin.DiscV4.Dat.mem_Mℓ {O : Type u_1} [CommRing O] [IsDomain O] [CharZero O] {M : Conj61.V4Data O} (P : Dat M) (k : Fin 4) : P.vϑ k ∈ P.Mℓ

theorem Louboutin.DiscV4.Dat.mem_Lℓ {O : Type u_1} [CommRing O] [IsDomain O] [CharZero O] {M : Conj61.V4Data O} (P : Dat M) (k : Fin 4) : P.vη k ∈ P.Lℓ

theorem Louboutin.DiscV4.Dat.smul_mem' {O : Type u_1} [CommRing O] [IsDomain O] [CharZero O] (N : Submodule ℤ O) (n : ℤ) {y : O} (hy : y ∈ N) : ↑n * y ∈ N

theorem Louboutin.DiscV4.Dat.one_Mℓ {O : Type u_1} [CommRing O] [IsDomain O] [CharZero O] {M : Conj61.V4Data O} (P : Dat M) : 1 ∈ P.Mℓ

theorem Louboutin.DiscV4.Dat.ϑ₁_Mℓ {O : Type u_1} [CommRing O] [IsDomain O] [CharZero O] {M : Conj61.V4Data O} (P : Dat M) : P.ϑ₁ ∈ P.Mℓ

theorem Louboutin.DiscV4.Dat.ϑ₂_Mℓ {O : Type u_1} [CommRing O] [IsDomain O] [CharZero O] {M : Conj61.V4Data O} (P : Dat M) : P.ϑ₂ ∈ P.Mℓ

theorem Louboutin.DiscV4.Dat.ϑ₃_Mℓ {O : Type u_1} [CommRing O] [IsDomain O] [CharZero O] {M : Conj61.V4Data O} (P : Dat M) : P.ϑ₃ ∈ P.Mℓ

theorem Louboutin.DiscV4.Dat.one_Lℓ {O : Type u_1} [CommRing O] [IsDomain O] [CharZero O] {M : Conj61.V4Data O} (P : Dat M) : 1 ∈ P.Lℓ

theorem Louboutin.DiscV4.Dat.η₁_Lℓ {O : Type u_1} [CommRing O] [IsDomain O] [CharZero O] {M : Conj61.V4Data O} (P : Dat M) : P.η₁ ∈ P.Lℓ

theorem Louboutin.DiscV4.Dat.η₂_Lℓ {O : Type u_1} [CommRing O] [IsDomain O] [CharZero O] {M : Conj61.V4Data O} (P : Dat M) : P.η₂ ∈ P.Lℓ

theorem Louboutin.DiscV4.Dat.η₃_Lℓ {O : Type u_1} [CommRing O] [IsDomain O] [CharZero O] {M : Conj61.V4Data O} (P : Dat M) : P.η₃ ∈ P.Lℓ

theorem Louboutin.DiscV4.Dat.gen16 {O : Type u_1} [CommRing O] [IsDomain O] [CharZero O] {M : Conj61.V4Data O} (P : Dat M) (a b : Fin 4) : 16 * (P.vϑ a * P.vϑ b) ∈ P.Mℓ

theorem Louboutin.DiscV4.Dat.Mℓ16 {O : Type u_1} [CommRing O] [IsDomain O] [CharZero O] {M : Conj61.V4Data O} (P : Dat M) {p q : O} (hp : p ∈ P.Mℓ) (hq : q ∈ P.Mℓ) : 16 * (p * q) ∈ P.Mℓ

16·M·M ⊆ M.

theorem Louboutin.DiscV4.Dat.four_x_Mℓ {O : Type u_1} [CommRing O] [IsDomain O] [CharZero O] {M : Conj61.V4Data O} (P : Dat M) (m : Fin 4) : 4 * M.x m ∈ P.Mℓ

4x_m ∈ M for every conjugate.

theorem Louboutin.DiscV4.Dat.half_loc {O : Type u_1} [CommRing O] [IsDomain O] [CharZero O] {M : Conj61.V4Data O} (P : Dat M) {y : O} (hy : y ∈ Aring M) : ∃ (K : ℕ), 2 ^ K * y ∈ P.Mℓ

A ⊆ M[1/2]: every y ∈ A has 2ᴷ y ∈ M (proof of lem:Lodd, globally).

The indices

theorem Louboutin.DiscV4.Dat.Mℓ_le_Lℓ {O : Type u_1} [CommRing O] [IsDomain O] [CharZero O] {M : Conj61.V4Data O} (P : Dat M) : P.Mℓ ≤ P.Lℓ

theorem Louboutin.DiscV4.Dat.span_le_A {O : Type u_1} [CommRing O] [IsDomain O] [CharZero O] {M : Conj61.V4Data O} {v : Fin 4 → O} (hv : ∀ (k : Fin 4), v k ∈ Aring M) {y : O} (hy : y ∈ Submodule.span ℤ (Set.range v)) : y ∈ Aring M

a span of elements of A lies in A.

theorem Louboutin.DiscV4.Dat.vη_mem_A {O : Type u_1} [CommRing O] [IsDomain O] [CharZero O] {M : Conj61.V4Data O} (P : Dat M) (k : Fin 4) : P.vη k ∈ Aring M

theorem Louboutin.DiscV4.Dat.D_vϑ_ne {O : Type u_1} [CommRing O] [IsDomain O] [CharZero O] {M : Conj61.V4Data O} (P : Dat M) : D M P.vϑ ≠ 0

theorem Louboutin.DiscV4.Dat.D_vη_ne {O : Type u_1} [CommRing O] [IsDomain O] [CharZero O] {M : Conj61.V4Data O} (P : Dat M) : D M P.vη ≠ 0

theorem Louboutin.DiscV4.Dat.δ_ne {O : Type u_1} [CommRing O] [IsDomain O] [CharZero O] {M : Conj61.V4Data O} (P : Dat M) : P.δ ≠ 0

theorem Louboutin.DiscV4.Dat.D_vX_ne {O : Type u_1} [CommRing O] [IsDomain O] [CharZero O] {M : Conj61.V4Data O} (P : Dat M) : D M P.vX ≠ 0

theorem Louboutin.DiscV4.Dat.D_vpow_ne {O : Type u_1} [CommRing O] [IsDomain O] [CharZero O] {M : Conj61.V4Data O} : D M (vpow M) ≠ 0

theorem Louboutin.DiscV4.Dat.relIndex_Mℓ_Lℓ {O : Type u_1} [CommRing O] [IsDomain O] [CharZero O] {M : Conj61.V4Data O} (P : Dat M) : (Lat P.vϑ).relIndex (Lat P.vη) = 8

[L : M] = 8 (proof of prop:discA).

theorem Louboutin.DiscV4.Dat.vX_mem {O : Type u_1} [CommRing O] [IsDomain O] [CharZero O] {M : Conj61.V4Data O} (P : Dat M) (l : Fin 4) : P.vX l ∈ P.Mℓ

theorem Louboutin.DiscV4.Dat.relIndex_X_Mℓ {O : Type u_1} [CommRing O] [IsDomain O] [CharZero O] {M : Conj61.V4Data O} (P : Dat M) : (Lat P.vX).relIndex (Lat P.vϑ) = P.δ.natAbs ^ 4

[M : X] = |Δ|⁴ for X = ΔM.

theorem Louboutin.DiscV4.Dat.vX_mem_Zα {O : Type u_1} [CommRing O] [IsDomain O] [CharZero O] {M : Conj61.V4Data O} (P : Dat M) (l : Fin 4) : P.vX l ∈ Submodule.span ℤ (Set.range (vpow M))

theorem Louboutin.DiscV4.Dat.relIndex_X_Z {O : Type u_1} [CommRing O] [IsDomain O] [CharZero O] {M : Conj61.V4Data O} (P : Dat M) : (Lat P.vX).relIndex (Lat (vpow M)) = 16 * P.δ.natAbs ^ 3 * P.Θ.natAbs

[ℤ[α] : X] = 16 |Δ|³ |Θ|.

theorem Louboutin.DiscV4.Dat.zsmul_mem_iff {O : Type u_1} [CommRing O] [IsDomain O] [CharZero O] (L : Submodule ℤ O) {y : O} (h2y : 2 * y ∈ L) (hny : y ∉ L) (k : ℤ) : k • y ∈ L ↔ Even k

k·y ∈ L ⟺ k even, when 2y ∈ L and y ∉ L.

theorem Louboutin.DiscV4.Dat.relIndex_two {O : Type u_1} [CommRing O] [IsDomain O] [CharZero O] {M : Conj61.V4Data O} (L : Submodule ℤ O) {y : O} (hyA : y ∈ Aring M) (h2y : 2 * y ∈ L) (hny : y ∉ L) (hAN : ∀ z ∈ Aring M, ∃ l ∈ L, ∃ (k : ℤ), z = l + k • y) : L.toAddSubgroup.relIndex (Aring M).toAddSubgroup = 2

[A : L] = 2 when A = L + ℤy with 2y ∈ L, y ∉ L.

theorem Louboutin.DiscV4.Dat.index_of_two {O : Type u_1} [CommRing O] [IsDomain O] [CharZero O] {M : Conj61.V4Data O} (P : Dat M) (h2 : P.Lℓ.toAddSubgroup.relIndex (Aring M).toAddSubgroup = 2) : (Lat (vpow M)).relIndex (Aring M).toAddSubgroup * P.Θ.natAbs = P.δ.natAbs

prop:discA, the index: from [A : L] = 2, [A : ℤ[α]] · |Θ| = |Δ|.

Part 8. [A : L] = 2 (proof of prop:discA)

theorem Louboutin.DiscV4.half_int {O : Type u_1} [CommRing O] [IsDomain O] [CharZero O] (M : Conj61.V4Data O) {k : ℤ} {w : O} (h : ↑k = 2 * w) : ∃ (m : ℤ), w = ↑m

An element w ∈ O with 2w ∈ ℤ is an integer (O ∩ ℚ = ℤ in the model).

@[reducible, inline]

abbrev Louboutin.DiscV4.Dat.Nℓ {O : Type u_1} [CommRing O] {M : Conj61.V4Data O} (P : Dat M) (y : O) : Submodule ℤ O

N = L + ℤy.

Equations

• P.Nℓ y = Submodule.span ℤ (Set.range P.vη ∪ {y})

theorem Louboutin.DiscV4.Dat.Nℓ_eq {O : Type u_1} [CommRing O] [IsDomain O] [CharZero O] {M : Conj61.V4Data O} (P : Dat M) (y : O) : P.Nℓ y = P.Lℓ ⊔ ℤ ∙ y

theorem Louboutin.DiscV4.Dat.Lℓ_le_N {O : Type u_1} [CommRing O] [IsDomain O] [CharZero O] {M : Conj61.V4Data O} (P : Dat M) (y : O) : P.Lℓ ≤ P.Nℓ y

theorem Louboutin.DiscV4.Dat.y_mem_N {O : Type u_1} [CommRing O] [IsDomain O] [CharZero O] {M : Conj61.V4Data O} (P : Dat M) (y : O) : y ∈ P.Nℓ y

theorem Louboutin.DiscV4.Dat.decomp {O : Type u_1} [CommRing O] [IsDomain O] [CharZero O] {M : Conj61.V4Data O} (P : Dat M) {y z : O} (hz : z ∈ P.Nℓ y) : ∃ l ∈ P.Lℓ, ∃ (k : ℤ), z = l + k • y

theorem Louboutin.DiscV4.Dat.A_le_N {O : Type u_1} [CommRing O] [IsDomain O] [CharZero O] {M : Conj61.V4Data O} (P : Dat M) {y : O} (hyA : y ∈ Aring M) {s : ℤ} (hs : ¬Even s) (hodd : ∀ (m : Fin 4), ∀ g ∈ Set.range P.vη ∪ {y}, ↑s * (M.x m * g) ∈ P.Nℓ y) (z : O) : z ∈ Aring M → z ∈ P.Nℓ y

The closure scheme: if every product x_m·g (g a generator of N = L + ℤy) has an odd multiple in N, then A ⊆ N (the 2-power multiple is supplied by half_loc; Bézout glues).

theorem Louboutin.DiscV4.Dat.coeff_η {O : Type u_1} [CommRing O] [IsDomain O] [CharZero O] {M : Conj61.V4Data O} (P : Dat M) {c d : Fin 4 → ℤ} (h : ∑ k : Fin 4, c k • P.vη k = ∑ k : Fin 4, d k • P.vη k) : c = d

Coefficients in the ℤ-basis 1, η₁, η₂, η₃ of L are unique.

theorem Louboutin.DiscV4.Dat.mem_Lℓ_iff {O : Type u_1} [CommRing O] [IsDomain O] [CharZero O] {M : Conj61.V4Data O} (P : Dat M) {z : O} : z ∈ P.Lℓ ↔ ∃ (c : Fin 4 → ℤ), ∑ k : Fin 4, c k • P.vη k = z

theorem Louboutin.DiscV4.Dat.sum_vη {O : Type u_1} [CommRing O] [IsDomain O] [CharZero O] {M : Conj61.V4Data O} (P : Dat M) (c : Fin 4 → ℤ) : ∑ k : Fin 4, c k • P.vη k = ↑(c 0) + ↑(c 1) * P.η₁ + ↑(c 2) * P.η₂ + ↑(c 3) * P.η₃

theorem Louboutin.DiscV4.Dat.two_x0 {O : Type u_1} [CommRing O] [IsDomain O] [CharZero O] {M : Conj61.V4Data O} (P : Dat M) : ∃ (s : ℤ), 2 * M.x 0 = ↑s + ↑P.n₁ * P.η₁ + ↑P.n₂ * P.η₂ + ↑P.n₃ * P.η₃

2α = Σ n_j η_j + s with s ∈ ℤ (proof of prop:discA).

theorem Louboutin.DiscV4.Dat.S₁_eq {O : Type u_1} [CommRing O] [IsDomain O] [CharZero O] {M : Conj61.V4Data O} (P : Dat M) : ∃ (s : ℤ), M.x 0 + M.x 1 = ↑P.n₁ * P.η₁ + ↑s

S_j = n_j η_j + s_j, Q_j = t_j η_j + s'_j (lem:Lambda: C_j = ℤ + ℤη_j).

theorem Louboutin.DiscV4.Dat.S₂_eq {O : Type u_1} [CommRing O] [IsDomain O] [CharZero O] {M : Conj61.V4Data O} (P : Dat M) : ∃ (s : ℤ), M.x 0 + M.x 2 = ↑P.n₂ * P.η₂ + ↑s

theorem Louboutin.DiscV4.Dat.S₃_eq {O : Type u_1} [CommRing O] [IsDomain O] [CharZero O] {M : Conj61.V4Data O} (P : Dat M) : ∃ (s : ℤ), M.x 0 + M.x 3 = ↑P.n₃ * P.η₃ + ↑s

theorem Louboutin.DiscV4.Dat.Q₁_eq {O : Type u_1} [CommRing O] [IsDomain O] [CharZero O] {M : Conj61.V4Data O} (P : Dat M) : ∃ (s : ℤ), M.x 0 * M.x 1 = ↑P.t₁ * P.η₁ + ↑s

theorem Louboutin.DiscV4.Dat.Q₂_eq {O : Type u_1} [CommRing O] [IsDomain O] [CharZero O] {M : Conj61.V4Data O} (P : Dat M) : ∃ (s : ℤ), M.x 0 * M.x 2 = ↑P.t₂ * P.η₂ + ↑s

theorem Louboutin.DiscV4.Dat.Q₃_eq {O : Type u_1} [CommRing O] [IsDomain O] [CharZero O] {M : Conj61.V4Data O} (P : Dat M) : ∃ (s : ℤ), M.x 0 * M.x 3 = ↑P.t₃ * P.η₃ + ↑s

theorem Louboutin.DiscV4.Dat.nQ₁ {O : Type u_1} [CommRing O] [IsDomain O] [CharZero O] {M : Conj61.V4Data O} (P : Dat M) : ∃ (l : ℤ), ↑P.n₁ * (M.x 0 * M.x 1) = ↑P.t₁ * (M.x 0 + M.x 1) + ↑l

n_j Q_j = t_j S_j + ℓ_j with ℓ_j ∈ ℤ (n_j ϑ_j and t_j ϑ_j give r_j t_j = q_j n_j).

theorem Louboutin.DiscV4.Dat.nQ₂ {O : Type u_1} [CommRing O] [IsDomain O] [CharZero O] {M : Conj61.V4Data O} (P : Dat M) : ∃ (l : ℤ), ↑P.n₂ * (M.x 0 * M.x 2) = ↑P.t₂ * (M.x 0 + M.x 2) + ↑l

theorem Louboutin.DiscV4.Dat.nQ₃ {O : Type u_1} [CommRing O] [IsDomain O] [CharZero O] {M : Conj61.V4Data O} (P : Dat M) : ∃ (l : ℤ), ↑P.n₃ * (M.x 0 * M.x 3) = ↑P.t₃ * (M.x 0 + M.x 3) + ↑l

Case I: some n_i odd, A = L + ℤα

theorem Louboutin.DiscV4.Dat.int_N {O : Type u_1} [CommRing O] [IsDomain O] [CharZero O] {M : Conj61.V4Data O} (P : Dat M) (y : O) (k : ℤ) : ↑k ∈ P.Nℓ y

theorem Louboutin.DiscV4.Dat.η₁_N {O : Type u_1} [CommRing O] [IsDomain O] [CharZero O] {M : Conj61.V4Data O} (P : Dat M) (y : O) : P.η₁ ∈ P.Nℓ y

theorem Louboutin.DiscV4.Dat.η₂_N {O : Type u_1} [CommRing O] [IsDomain O] [CharZero O] {M : Conj61.V4Data O} (P : Dat M) (y : O) : P.η₂ ∈ P.Nℓ y

theorem Louboutin.DiscV4.Dat.η₃_N {O : Type u_1} [CommRing O] [IsDomain O] [CharZero O] {M : Conj61.V4Data O} (P : Dat M) (y : O) : P.η₃ ∈ P.Nℓ y

theorem Louboutin.DiscV4.Dat.I_x {O : Type u_1} [CommRing O] [IsDomain O] [CharZero O] {M : Conj61.V4Data O} (P : Dat M) (m : Fin 4) : M.x m ∈ P.Nℓ (M.x 0)

In N = L + ℤα: all x_m and all products x_a x_b (squares included) lie in N.

theorem Louboutin.DiscV4.Dat.I_pairs {O : Type u_1} [CommRing O] [IsDomain O] [CharZero O] {M : Conj61.V4Data O} (P : Dat M) : M.x 0 * M.x 1 ∈ P.Nℓ (M.x 0) ∧ M.x 0 * M.x 2 ∈ P.Nℓ (M.x 0) ∧ M.x 0 * M.x 3 ∈ P.Nℓ (M.x 0) ∧ M.x 2 * M.x 3 ∈ P.Nℓ (M.x 0) ∧ M.x 1 * M.x 3 ∈ P.Nℓ (M.x 0) ∧ M.x 1 * M.x 2 ∈ P.Nℓ (M.x 0)

theorem Louboutin.DiscV4.Dat.I_deg2 {O : Type u_1} [CommRing O] [IsDomain O] [CharZero O] {M : Conj61.V4Data O} (P : Dat M) (a b : Fin 4) : M.x a * M.x b ∈ P.Nℓ (M.x 0)

theorem Louboutin.DiscV4.Dat.I_odd_of_triples {O : Type u_1} [CommRing O] [IsDomain O] [CharZero O] {M : Conj61.V4Data O} (P : Dat M) {s : ℤ} (T012 : ↑s * (M.x 0 * M.x 1 * M.x 2) ∈ P.Nℓ (M.x 0)) (T013 : ↑s * (M.x 0 * M.x 1 * M.x 3) ∈ P.Nℓ (M.x 0)) (T023 : ↑s * (M.x 0 * M.x 2 * M.x 3) ∈ P.Nℓ (M.x 0)) (T123 : ↑s * (M.x 1 * M.x 2 * M.x 3) ∈ P.Nℓ (M.x 0)) (m : Fin 4) (g : O) : g ∈ Set.range P.vη ∪ {M.x 0} → ↑s * (M.x m * g) ∈ P.Nℓ (M.x 0)

From the four triple products to all products x_m·g, g ∈ {1, η_j, α} (Case I).

theorem Louboutin.DiscV4.Dat.I_xQ {O : Type u_1} [CommRing O] [IsDomain O] [CharZero O] {M : Conj61.V4Data O} (P : Dat M) {n t l : ℤ} {i : Fin 4} (h : ↑n * (M.x 0 * M.x i) = ↑t * (M.x 0 + M.x i) + ↑l) (m : Fin 4) : ↑n * (M.x m * (M.x 0 * M.x i)) ∈ P.Nℓ (M.x 0) ∧ ∀ (z : ℤ), ↑n * (M.x m * (↑z - M.x 0 * M.x i)) ∈ P.Nℓ (M.x 0)

n Q = t S + ℓ gives n·x_m·Q ∈ N and n·x_m·(z − Q) ∈ N.

theorem Louboutin.DiscV4.Dat.caseI_A_le {O : Type u_1} [CommRing O] [IsDomain O] [CharZero O] {M : Conj61.V4Data O} (P : Dat M) (hodd : ¬Even P.n₁ ∨ ¬Even P.n₂ ∨ ¬Even P.n₃) (z : O) : z ∈ Aring M → z ∈ P.Nℓ (M.x 0)

Case I of prop:discA: if some n_i is odd, A ⊆ L + ℤα.

theorem Louboutin.DiscV4.Dat.caseI {O : Type u_1} [CommRing O] [IsDomain O] [CharZero O] {M : Conj61.V4Data O} (P : Dat M) (hodd : ¬Even P.n₁ ∨ ¬Even P.n₂ ∨ ¬Even P.n₃) : M.x 0 ∈ Aring M ∧ 2 * M.x 0 ∈ P.Lℓ ∧ M.x 0 ∉ P.Lℓ ∧ ∀ z ∈ Aring M, z ∈ P.Nℓ (M.x 0)

Case I of prop:discA: if some n_i is odd, A = L + ℤα with 2α ∈ L, α ∉ L.

Case II: all n_j even, A = L + ℤ η_i η_j

theorem Louboutin.DiscV4.caseII_odd {R : Type u_1} [CommRing R] (N : Submodule ℤ R) {ηi ηj ηk : R} {ei ej ek Ci Cj Ck mi mj c K : ℤ} (hi : ηi * ηi = ↑ei * ηi + ↑Ci) (hj : ηj * ηj = ↑ej * ηj + ↑Cj) (hk : ηk * ηk = ↑ek * ηk + ↑Ck) (hE : ↑c * ηk = 2 * ↑mi * ↑mj * (ηi * ηj) - ↑mi * ↑mj * ↑ej * ηi - ↑mi * ↑mj * ↑ei * ηj + ↑K) (n1 : 1 ∈ N) (ni : ηi ∈ N) (nj : ηj ∈ N) (nk : ηk ∈ N) (nij : ηi * ηj ∈ N) (a : R) : a ∈ {1, ηi, ηj, ηk} → ∀ g ∈ {1, ηi, ηj, ηk, ηi * ηj}, ↑c * (a * g) ∈ N

Products in L·N for the configuration (i, j, k) with c η_k = 2m_im_j η_iη_j − … (an odd multiple of every product lands in N = L + ℤ η_iη_j). Abstract over a commutative ring.

theorem Louboutin.DiscV4.caseII_notin {R : Type u_1} [CommRing R] {ηi ηj ηk : R} {ei ej mi mj c K : ℤ} (hli : LinearIndependent ℤ ![1, ηi, ηj, ηk]) (hE : ↑c * ηk = 2 * ↑mi * ↑mj * (ηi * ηj) - ↑mi * ↑mj * ↑ej * ηi - ↑mi * ↑mj * ↑ei * ηj + ↑K) (hc : ¬Even c) : ηi * ηj ∉ Submodule.span ℤ (Set.range ![1, ηi, ηj, ηk])

η_iη_j ∉ ℤ + ℤη_i + ℤη_j + ℤη_k when c is odd (comparing η_k-coordinates).

theorem Louboutin.DiscV4.div_int {O : Type u_1} [CommRing O] [IsDomain O] [CharZero O] (M : Conj61.V4Data O) {g k : ℤ} (hg : g ≠ 0) {w : O} (h : ↑k = ↑g * w) : ∃ (m : ℤ), w = ↑m

An element w ∈ O with g·w ∈ ℤ (g ≠ 0) is an integer.

theorem Louboutin.DiscV4.eta_sq {O : Type u_1} [CommRing O] [IsDomain O] [CharZero O] (M : Conj61.V4Data O) {η ϑ : O} {e Δ : ℤ} (hη : 2 * η - ↑e = ϑ) (hΔ : ϑ * ϑ = ↑Δ) : ∃ (C : ℤ), η * η = ↑e * η + ↑C

η² = eη + C with C = (Δ − e²)/4 ∈ ℤ, when ϑ = 2η − e and ϑ² = Δ (C_j = ℤ[η_j] is a ring).

theorem Louboutin.DiscV4.range_four {R : Type u_1} (a b c d : R) : Set.range ![a, b, c, d] = {a, b, c, d}

theorem Louboutin.DiscV4.eta_rel {O : Type u_1} [CommRing O] [IsDomain O] [CharZero O] (M : Conj61.V4Data O) {ηi ηj ηk ϑi ϑj ϑk : O} {ei ej ek mi mj c : ℤ} (hi : 2 * ηi - ↑ei = ϑi) (hj : 2 * ηj - ↑ej = ϑj) (hk : 2 * ηk - ↑ek = ϑk) (h : ↑mi * ↑mj * (ϑi * ϑj) = ↑c * ϑk) : ∃ (K : ℤ), ↑c * ηk = 2 * ↑mi * ↑mj * (ηi * ηj) - ↑mi * ↑mj * ↑ej * ηi - ↑mi * ↑mj * ↑ei * ηj + ↑K

From m_i m_j ϑ_i ϑ_j = c ϑ_k and ϑ = 2η − e: c η_k = 2m_im_j η_iη_j − m_im_j e_j η_i − m_im_j e_i η_j + K with K ∈ ℤ (proof of prop:discA, all-even case).

theorem Louboutin.DiscV4.Dat.x_in_L {O : Type u_1} [CommRing O] [IsDomain O] [CharZero O] {M : Conj61.V4Data O} (P : Dat M) (h1 : 2 ∣ P.n₁) (h2 : 2 ∣ P.n₂) (h3 : 2 ∣ P.n₃) (m : Fin 4) : M.x m ∈ P.Lℓ

If all n_j are even, every conjugate lies in L (α = s + Σ m_j η_j).

theorem Louboutin.DiscV4.Dat.caseII_gen {O : Type u_1} [CommRing O] [IsDomain O] [CharZero O] {M : Conj61.V4Data O} (P : Dat M) {ηi ηj ηk : O} {ei ej ek mi mj c K : ℤ} (hset : Set.range P.vη = {1, ηi, ηj, ηk}) (hli : LinearIndependent ℤ ![1, ηi, ηj, ηk]) (hiA : ηi ∈ Aring M) (hjA : ηj ∈ Aring M) (hi : ∃ (C : ℤ), ηi * ηi = ↑ei * ηi + ↑C) (hj : ∃ (C : ℤ), ηj * ηj = ↑ej * ηj + ↑C) (hk : ∃ (C : ℤ), ηk * ηk = ↑ek * ηk + ↑C) (hE : ↑c * ηk = 2 * ↑mi * ↑mj * (ηi * ηj) - ↑mi * ↑mj * ↑ej * ηi - ↑mi * ↑mj * ↑ei * ηj + ↑K) (hc : ¬Even c) (hm : ¬Even (mi * mj)) (hx : ∀ (m : Fin 4), M.x m ∈ P.Lℓ) : ηi * ηj ∈ Aring M ∧ 2 * (ηi * ηj) ∈ P.Lℓ ∧ ηi * ηj ∉ P.Lℓ ∧ ∀ z ∈ Aring M, z ∈ P.Nℓ (ηi * ηj)

Case II of prop:discA for one configuration (i, j, k): A = L + ℤ η_iη_j, 2η_iη_j ∈ L, η_iη_j ∉ L.

theorem Louboutin.DiscV4.Dat.caseII {O : Type u_1} [CommRing O] [IsDomain O] [CharZero O] {M : Conj61.V4Data O} (P : Dat M) (h1 : 2 ∣ P.n₁) (h2 : 2 ∣ P.n₂) (h3 : 2 ∣ P.n₃) : ∃ y ∈ Aring M, 2 * y ∈ P.Lℓ ∧ y ∉ P.Lℓ ∧ ∀ z ∈ Aring M, z ∈ P.Nℓ y

Case II of prop:discA: all n_j even ⇒ A = L + ℤ η_iη_j for the pair with m_i, m_j odd.

theorem Louboutin.DiscV4.Dat.exists_y {O : Type u_1} [CommRing O] [IsDomain O] [CharZero O] {M : Conj61.V4Data O} (P : Dat M) : ∃ y ∈ Aring M, 2 * y ∈ P.Lℓ ∧ y ∉ P.Lℓ ∧ ∀ z ∈ Aring M, z ∈ P.Nℓ y

A = L + ℤy with 2y ∈ L, y ∉ L, in all cases (y = α or y = η_iη_j; proof of prop:discA).

theorem Louboutin.DiscV4.Dat.relIndex_L_A {O : Type u_1} [CommRing O] [IsDomain O] [CharZero O] {M : Conj61.V4Data O} (P : Dat M) : P.Lℓ.toAddSubgroup.relIndex (Aring M).toAddSubgroup = 2

[A : L] = 2 in all cases (proof of prop:discA).

theorem Louboutin.DiscV4.Dat.index_mul_Θ {O : Type u_1} [CommRing O] [IsDomain O] [CharZero O] {M : Conj61.V4Data O} (P : Dat M) : (Lat (vpow M)).relIndex (Aring M).toAddSubgroup * P.Θ.natAbs = P.δ.natAbs

prop:discA, the index: [A : ℤ[α]] · |Θ| = |Δ_α|.

theorem Louboutin.DiscV4.Dat.gcd_eq {O : Type u_1} [CommRing O] [IsDomain O] [CharZero O] {M : Conj61.V4Data O} (P : Dat M) {t u v w : ℤ} (ht : Conj61.T M.x = ↑t) (hu : Conj61.U M.x = ↑u) (hv : Conj61.V M.x = ↑v) (hw : Conj61.W M.x = ↑w) : (↑(t.gcd u)).gcd ↑(v.gcd w) = P.Θ.natAbs

gcd(T, U, V, W) = |Θ| for the note's (n_j, t_j) (Lemma lem:split, cf. gcd_TUVW).

Part 9. Integer core of prop:smith (the invariant factors)

theorem Louboutin.DiscV4.cop_of_common {a b : ℤ} (h : ∀ (g : ℤ), g ∣ a → g ∣ b → IsUnit g) : IsCoprime a b

theorem Louboutin.DiscV4.odd_cop_two {d : ℤ} (hd : ¬Even d) : IsCoprime d 2

theorem Louboutin.DiscV4.d1_caseI {d c c₁ c₂ c₃ n₁ n₂ n₃ : ℤ} (h1 : (1 - d * c) * n₁ = 2 * d * c₁) (h2 : (1 - d * c) * n₂ = 2 * d * c₂) (h3 : (1 - d * c) * n₃ = 2 * d * c₃) : d ∣ n₁ ∧ d ∣ n₂ ∧ d ∣ n₃

d₁ = 1, Case I: (1 − dc) n_l = 2 d c_l for all l ⇒ d ∣ n_l for all l.

theorem Louboutin.DiscV4.odd_part {d x y : ℤ} (h : ¬Even (d * (2 * x + y))) : ¬Even y

theorem Louboutin.DiscV4.odd_right {c e : ℤ} (h : ¬Even (c * e)) : ¬Even e

theorem Louboutin.DiscV4.odd_left {c e : ℤ} (h : ¬Even (c * e)) : ¬Even c

theorem Louboutin.DiscV4.d1_caseII {d c ci cj ei ej mi mj : ℤ} (hi : d * (2 * ci + c * ej) = 2 * mi) (hj : d * (2 * cj + c * ei) = 2 * mj) (he : ¬Even (ei + ej)) (hm : IsCoprime mi mj) (hmi : ¬Even mi) (hmj : ¬Even mj) : IsUnit d

d₁ = 1, Case II: d(2c_i + c e_j) = 2m_i, d(2c_j + c e_i) = 2m_j with e_i + e_j odd, m_i, m_j odd and gcd(m_i, m_j) = 1 force d to be a unit.

theorem Louboutin.DiscV4.d2_caseI {d c P c₁ c₂ c₃ n₁ n₂ n₃ t₁ t₂ t₃ : ℤ} (h1 : P * n₁ - 2 * t₁ = 2 * d * c₁ + d * c * n₁) (h2 : P * n₂ - 2 * t₂ = 2 * d * c₂ + d * c * n₂) (h3 : P * n₃ - 2 * t₃ = 2 * d * c₃ + d * c * n₃) (hodd : ¬Even n₁ ∨ ¬Even n₂ ∨ ¬Even n₃) : d ∣ n₁ * t₂ - n₂ * t₁ ∧ d ∣ n₁ * t₃ - n₃ * t₁ ∧ d ∣ n₂ * t₃ - n₃ * t₂

d₂ ∣ m₀, Case I: (P − dc) n_l − 2t_l = 2d c_l for all l, with some n_i odd.

theorem Louboutin.DiscV4.d2_caseII {d c P ci cj ck c' ei ej mi mj mk ti tj tk : ℤ} (hk : d * (2 * (mi * mj) * ck + c * c') = 2 * (mi * mj) * (P * mk - tk)) (hi : d * (2 * ci + c * ej) = 2 * (P * mi - ti)) (hj : d * (2 * cj + c * ei) = 2 * (P * mj - tj)) (hmi : ¬Even mi) (hmj : ¬Even mj) (hmk : Even mk) (hti : ¬Even ti) (htj : ¬Even tj) (htk : ¬Even tk) (he : ¬Even (ei + ej)) (copi : ∀ (g : ℤ), g ∣ mi → g ∣ ti → IsUnit g) (copj : ∀ (g : ℤ), g ∣ mj → g ∣ tj → IsUnit g) : d ∣ mi * tj - mj * ti ∧ d ∣ mi * tk - mk * ti ∧ d ∣ mj * tk - mk * tj

d₂ ∣ m₀/2, Case II (configuration (i, j, k): m_i, m_j odd, m_k even).

Part 10. Coordinates: A ↪ ℚ⁴ in the basis 1, α, α², α³ (bridge to T1Completo)

noncomputable def Louboutin.DiscV4.Dat.bZ {O : Type u_1} [CommRing O] [IsDomain O] [CharZero O] (M : Conj61.V4Data O) : Module.Basis (Fin 4) ℤ ↥(Submodule.span ℤ (Set.range (vpow M)))

the ℤ-basis 1, α, α², α³ of ℤ[α].

Equations

• Louboutin.DiscV4.Dat.bZ M = Module.Basis.span ⋯

theorem Louboutin.DiscV4.Dat.pow_indep {O : Type u_1} [CommRing O] [IsDomain O] [CharZero O] {M : Conj61.V4Data O} {g : Fin 4 → ℤ} (h : ∑ k : Fin 4, ↑(g k) * M.x 0 ^ ↑k = 0) : g = 0

theorem Louboutin.DiscV4.Dat.δy_mem {O : Type u_1} [CommRing O] [IsDomain O] [CharZero O] {M : Conj61.V4Data O} (P : Dat M) {y : O} (hy : y ∈ Aring M) : ↑P.δ * y ∈ Submodule.span ℤ (Set.range (vpow M))

noncomputable def Louboutin.DiscV4.Dat.rc {O : Type u_1} [CommRing O] [IsDomain O] [CharZero O] {M : Conj61.V4Data O} (P : Dat M) (y : ↥(Aring M).toAddSubgroup) : Fin 4 → ℤ

integer coordinates of Δ·y.

Equations

• P.rc y k = ((Louboutin.DiscV4.Dat.bZ M).repr ⟨↑P.δ * ↑y, ⋯⟩) k

theorem Louboutin.DiscV4.Dat.rc_sum {O : Type u_1} [CommRing O] [IsDomain O] [CharZero O] {M : Conj61.V4Data O} (P : Dat M) (y : ↥(Aring M).toAddSubgroup) : ∑ k : Fin 4, ↑(P.rc y k) * M.x 0 ^ ↑k = ↑P.δ * ↑y

theorem Louboutin.DiscV4.Dat.rc_add {O : Type u_1} [CommRing O] [IsDomain O] [CharZero O] {M : Conj61.V4Data O} (P : Dat M) (y z : ↥(Aring M).toAddSubgroup) : P.rc (y + z) = P.rc y + P.rc z

noncomputable def Louboutin.DiscV4.Dat.φ {O : Type u_1} [CommRing O] [IsDomain O] [CharZero O] {M : Conj61.V4Data O} (P : Dat M) : ↥(Aring M).toAddSubgroup →+ Fin 4 → ℚ

φ(y) = (coordinates of y in 1, α, α², α³) ∈ ℚ⁴.

Equations

• P.φ = { toFun := fun (y : ↥(Louboutin.DiscV4.Aring M).toAddSubgroup) (k : Fin 4) => ↑(P.rc y k) / ↑P.δ, map_zero' := ⋯, map_add' := ⋯ }

theorem Louboutin.DiscV4.Dat.φ_apply {O : Type u_1} [CommRing O] [IsDomain O] [CharZero O] {M : Conj61.V4Data O} (P : Dat M) (y : ↥(Aring M).toAddSubgroup) (k : Fin 4) : P.φ y k = ↑(P.rc y k) / ↑P.δ

theorem Louboutin.DiscV4.Dat.φ_eq_iff {O : Type u_1} [CommRing O] [IsDomain O] [CharZero O] {M : Conj61.V4Data O} (P : Dat M) (y : ↥(Aring M).toAddSubgroup) {d : ℤ} (hd : d ≠ 0) (c : Fin 4 → ℤ) : ↑d * ↑y = ∑ k : Fin 4, ↑(c k) * M.x 0 ^ ↑k ↔ P.φ y = fun (k : Fin 4) => ↑(c k) / ↑d

d·y = Σ c_k αᵏ ⟺ φ(y) = c/d (d ≠ 0).

theorem Louboutin.DiscV4.Dat.φ_injective {O : Type u_1} [CommRing O] [IsDomain O] [CharZero O] {M : Conj61.V4Data O} (P : Dat M) : Function.Injective ⇑P.φ

noncomputable def Louboutin.DiscV4.Dat.MQ {O : Type u_1} [CommRing O] [IsDomain O] [CharZero O] {M : Conj61.V4Data O} (P : Dat M) : AddSubgroup (Fin 4 → ℚ)

the image of A in ℚ⁴.

Equations

• P.MQ = P.φ.range

theorem Louboutin.DiscV4.Dat.mem_Zα_iff {O : Type u_1} [CommRing O] [IsDomain O] [CharZero O] {M : Conj61.V4Data O} (P : Dat M) (y : ↥(Aring M).toAddSubgroup) : ↑y ∈ Lat (vpow M) ↔ P.φ y ∈ Z4

theorem Louboutin.DiscV4.Dat.index_MQ {O : Type u_1} [CommRing O] [IsDomain O] [CharZero O] {M : Conj61.V4Data O} (P : Dat M) : (Z4.addSubgroupOf P.MQ).index = (Lat (vpow M)).relIndex (Aring M).toAddSubgroup

[φ(A) : ℤ⁴ ∩ φ(A)] = [A : ℤ[α]].

Part 11. Coordinates on the ϑ-basis (comparison of coefficients)

theorem Louboutin.DiscV4.coeff4 {R : Type u_1} [CommRing R] {v₁ v₂ v₃ : R} (hli : LinearIndependent ℤ ![1, v₁, v₂, v₃]) {A0 A1 A2 A3 : ℤ} (h : ↑A0 + ↑A1 * v₁ + ↑A2 * v₂ + ↑A3 * v₃ = 0) : A0 = 0 ∧ A1 = 0 ∧ A2 = 0 ∧ A3 = 0

theorem Louboutin.DiscV4.coeffI_d1 {R : Type u_1} [CommRing R] {ϑ₁ ϑ₂ ϑ₃ η₁ η₂ η₃ x0 w : R} {a n₁ n₂ n₃ e₁ e₂ e₃ : ℤ} (hli : LinearIndependent ℤ ![1, ϑ₁, ϑ₂, ϑ₃]) (h1 : 2 * η₁ - ↑e₁ = ϑ₁) (h2 : 2 * η₂ - ↑e₂ = ϑ₂) (h3 : 2 * η₃ - ↑e₃ = ϑ₃) (hx : 4 * x0 = ↑a + ↑n₁ * ϑ₁ + ↑n₂ * ϑ₂ + ↑n₃ * ϑ₃) {c0 c1 c2 c3 κ d p : ℤ} (hw : w = ↑c0 + ↑c1 * η₁ + ↑c2 * η₂ + ↑c3 * η₃ + ↑κ * x0) (hd : ↑d * w = ↑p + x0) : (1 - d * κ) * n₁ = 2 * d * c1 ∧ (1 - d * κ) * n₂ = 2 * d * c2 ∧ (1 - d * κ) * n₃ = 2 * d * c3

Case I, d₁: d·w = p + α with w = c₀ + Σ c_l η_l + κα gives (1 − dκ) n_l = 2d c_l.

theorem Louboutin.DiscV4.coeffI_d2 {R : Type u_1} [CommRing R] {ϑ₁ ϑ₂ ϑ₃ η₁ η₂ η₃ x0 w : R} {a n₁ n₂ n₃ t₁ t₂ t₃ e₁ e₂ e₃ Δ₁ Δ₂ Δ₃ : ℤ} (hli : LinearIndependent ℤ ![1, ϑ₁, ϑ₂, ϑ₃]) (h1 : 2 * η₁ - ↑e₁ = ϑ₁) (h2 : 2 * η₂ - ↑e₂ = ϑ₂) (h3 : 2 * η₃ - ↑e₃ = ϑ₃) (hx : 4 * x0 = ↑a + ↑n₁ * ϑ₁ + ↑n₂ * ϑ₂ + ↑n₃ * ϑ₃) (hΔ₁ : ϑ₁ * ϑ₁ = ↑Δ₁) (hΔ₂ : ϑ₂ * ϑ₂ = ↑Δ₂) (hΔ₃ : ϑ₃ * ϑ₃ = ↑Δ₃) (p₁ : ↑n₂ * ↑n₃ * (ϑ₂ * ϑ₃) = (↑a * ↑n₁ - 4 * ↑t₁) * ϑ₁) (p₂ : ↑n₁ * ↑n₃ * (ϑ₁ * ϑ₃) = (↑a * ↑n₂ - 4 * ↑t₂) * ϑ₂) (p₃ : ↑n₁ * ↑n₂ * (ϑ₁ * ϑ₂) = (↑a * ↑n₃ - 4 * ↑t₃) * ϑ₃) {c0 c1 c2 c3 κ d p q : ℤ} (hw : w = ↑c0 + ↑c1 * η₁ + ↑c2 * η₂ + ↑c3 * η₃ + ↑κ * x0) (hd : ↑d * w = ↑q + ↑p * x0 + x0 ^ 2) : (a + p) * n₁ - 2 * t₁ = 2 * d * c1 + d * κ * n₁ ∧ (a + p) * n₂ - 2 * t₂ = 2 * d * c2 + d * κ * n₂ ∧ (a + p) * n₃ - 2 * t₃ = 2 * d * c3 + d * κ * n₃

Case I, d₂: d·w = q + pα + α² gives (a + p) n_l − 2t_l = 2d c_l + dκ n_l.

theorem Louboutin.DiscV4.coeffII_d1 {R : Type u_1} [CommRing R] {ϑi ϑj ϑk ηi ηj ηk x0 w : R} {a ni nj nk ei ej ek mi mj c' : ℤ} (hli : LinearIndependent ℤ ![1, ϑi, ϑj, ϑk]) (hi : 2 * ηi - ↑ei = ϑi) (hj : 2 * ηj - ↑ej = ϑj) (hk : 2 * ηk - ↑ek = ϑk) (hx : 4 * x0 = ↑a + ↑ni * ϑi + ↑nj * ϑj + ↑nk * ϑk) (hrel : ↑mi * ↑mj * (ϑi * ϑj) = ↑c' * ϑk) (hm : mi * mj ≠ 0) {c0 ci cj ck κ d p : ℤ} (hw : w = ↑c0 + ↑ci * ηi + ↑cj * ηj + ↑ck * ηk + ↑κ * (ηi * ηj)) (hd : ↑d * w = ↑p + x0) : d * (2 * ci + κ * ej) = ni ∧ d * (2 * cj + κ * ei) = nj

Case II, d₁ (configuration (i, j, k)): d·w = p + α with w = c₀ + Σ c_l η_l + κ η_iη_j.

theorem Louboutin.DiscV4.coeffII_d2 {R : Type u_1} [CommRing R] {ϑi ϑj ϑk ηi ηj ηk x0 w : R} {a ni nj nk ti tj tk ei ej ek Δi Δj Δk mi mj c' : ℤ} (hli : LinearIndependent ℤ ![1, ϑi, ϑj, ϑk]) (hi : 2 * ηi - ↑ei = ϑi) (hj : 2 * ηj - ↑ej = ϑj) (hk : 2 * ηk - ↑ek = ϑk) (hx : 4 * x0 = ↑a + ↑ni * ϑi + ↑nj * ϑj + ↑nk * ϑk) (hΔi : ϑi * ϑi = ↑Δi) (hΔj : ϑj * ϑj = ↑Δj) (hΔk : ϑk * ϑk = ↑Δk) (pij : ↑ni * ↑nj * (ϑi * ϑj) = (↑a * ↑nk - 4 * ↑tk) * ϑk) (pik : ↑ni * ↑nk * (ϑi * ϑk) = (↑a * ↑nj - 4 * ↑tj) * ϑj) (pjk : ↑nj * ↑nk * (ϑj * ϑk) = (↑a * ↑ni - 4 * ↑ti) * ϑi) (hrel : ↑mi * ↑mj * (ϑi * ϑj) = ↑c' * ϑk) (hm : mi * mj ≠ 0) {c0 ci cj ck κ d p q : ℤ} (hw : w = ↑c0 + ↑ci * ηi + ↑cj * ηj + ↑ck * ηk + ↑κ * (ηi * ηj)) (hd : ↑d * w = ↑q + ↑p * x0 + x0 ^ 2) : 2 * (mi * mj) * d * ck + d * κ * c' = mi * mj * ((p + a) * nk - 2 * tk) ∧ d * (2 * ci + κ * ej) = (p + a) * ni - 2 * ti ∧ d * (2 * cj + κ * ei) = (p + a) * nj - 2 * tj

Case II, d₂ (configuration (i, j, k)): d·w = q + pα + α².

Part 12. prop:smith in the model: d₁ = 1 and d₂ = m₀/h₀ for the triangular basis

theorem Louboutin.DiscV4.Dat.omega1_eq (d : ℕ) (p : ℤ) : omega1 d p = fun (k : Fin (Nat.succ 3)) => ↑(![p, 1, 0, 0] k) / ↑↑d

theorem Louboutin.DiscV4.Dat.omega2_eq (d : ℕ) (p0 p1 : ℤ) : omega2 d p0 p1 = fun (k : Fin (Nat.succ 3)) => ↑(![p0, p1, 1, 0] k) / ↑↑d

theorem Louboutin.DiscV4.Dat.tri_y1 {O : Type u_1} [CommRing O] [IsDomain O] [CharZero O] {M : Conj61.V4Data O} (P : Dat M) (B : Triang P.MQ) : ∃ y ∈ Aring M, ↑B.d₁ * y = ↑B.p₁₀ + M.x 0

The elements of A behind ω₁ and ω₂: d₁y₁ = p₁₀ + α and d₂y₂ = p₂₀ + p₂₁α + α².

theorem Louboutin.DiscV4.Dat.tri_y2 {O : Type u_1} [CommRing O] [IsDomain O] [CharZero O] {M : Conj61.V4Data O} (P : Dat M) (B : Triang P.MQ) : ∃ y ∈ Aring M, ↑B.d₂ * y = ↑B.p₂₀ + ↑B.p₂₁ * M.x 0 + M.x 0 ^ 2

theorem Louboutin.DiscV4.Dat.N_form {O : Type u_1} [CommRing O] [IsDomain O] [CharZero O] {M : Conj61.V4Data O} (P : Dat M) {y z : O} (hz : z ∈ P.Nℓ y) : ∃ (c0 : ℤ) (c1 : ℤ) (c2 : ℤ) (c3 : ℤ) (κ : ℤ), z = ↑c0 + ↑c1 * P.η₁ + ↑c2 * P.η₂ + ↑c3 * P.η₃ + ↑κ * y

elements of L + ℤy in coordinates.

theorem Louboutin.DiscV4.Dat.tierC_I {O : Type u_1} [CommRing O] [IsDomain O] [CharZero O] {M : Conj61.V4Data O} (P : Dat M) (hodd : ¬Even P.n₁ ∨ ¬Even P.n₂ ∨ ¬Even P.n₃) (B : Triang P.MQ) : B.d₁ = 1 ∧ ↑B.d₂ ∣ P.toZD.d₁₂ ∧ ↑B.d₂ ∣ P.toZD.d₁₃ ∧ ↑B.d₂ ∣ P.toZD.d₂₃

Case I of prop:smith: d₁ = 1 and d₂ divides d₁₂, d₁₃, d₂₃.

theorem Louboutin.DiscV4.Dat.key_Y {O : Type u_1} [CommRing O] [IsDomain O] [CharZero O] {M : Conj61.V4Data O} (P : Dat M) : ∃ (K0 : ℤ) (K1 : ℤ), 2 * ↑(P.n₁ * P.n₂ * P.n₃) * M.x 0 ^ 2 = ↑K0 + ↑K1 * M.x 0 + 2 * ↑(P.n₂ * P.toZD.d₁₃) * M.x 1 + 2 * ↑(P.n₁ * P.toZD.d₂₃) * M.x 2

The element of A behind the lower bound: 2N α² = K₀ + K₁α + 2n₂d₁₃ x₁ + 2n₁d₂₃ x₂.

theorem Louboutin.DiscV4.cop_m {m m' t t' n n' a0 X : ℤ} (hn : n = 2 * m) (hn' : n' = 2 * m') (c : IsCoprime n t) (c' : IsCoprime n' t') (hQ : m * m' * X = (a0 * m - t) * (a0 * m' - t')) : IsCoprime m m'

gcd(m_i, m_j) = 1 from m_i m_j X = (a₀m_i − t_i)(a₀m_j − t_j) (pair identity P_k).

theorem Louboutin.DiscV4.Dat.tierC_II_gen {O : Type u_1} [CommRing O] [IsDomain O] [CharZero O] {M : Conj61.V4Data O} (P : Dat M) {ηi ηj ηk ϑi ϑj ϑk : O} {ei ej ek ni nj nk ti tj tk Δi Δj Δk mi mj mk c' : ℤ} (hset : Set.range P.vη = {1, ηi, ηj, ηk}) (hliη : LinearIndependent ℤ ![1, ηi, ηj, ηk]) (hli : LinearIndependent ℤ ![1, ϑi, ϑj, ϑk]) (hiA : ηi ∈ Aring M) (hjA : ηj ∈ Aring M) (hi : 2 * ηi - ↑ei = ϑi) (hj : 2 * ηj - ↑ej = ϑj) (hk : 2 * ηk - ↑ek = ϑk) (hx : 4 * M.x 0 = ↑P.a + ↑ni * ϑi + ↑nj * ϑj + ↑nk * ϑk) (hΔi : ϑi * ϑi = ↑Δi) (hΔj : ϑj * ϑj = ↑Δj) (hΔk : ϑk * ϑk = ↑Δk) (pij : ↑ni * ↑nj * (ϑi * ϑj) = (↑P.a * ↑nk - 4 * ↑tk) * ϑk) (pik : ↑ni * ↑nk * (ϑi * ϑk) = (↑P.a * ↑nj - 4 * ↑tj) * ϑj) (pjk : ↑nj * ↑nk * (ϑj * ϑk) = (↑P.a * ↑ni - 4 * ↑ti) * ϑi) (hrel : ↑mi * ↑mj * (ϑi * ϑj) = ↑c' * ϑk) (hni : ni = 2 * mi) (hnj : nj = 2 * mj) (hnk : nk = 2 * mk) (hmi : ¬Even mi) (hmj : ¬Even mj) (hmk : Even mk) (hti : ¬Even ti) (htj : ¬Even tj) (htk : ¬Even tk) (hc' : ¬Even c') (he : ¬Even (ei + ej)) (hcop : IsCoprime mi mj) (copi : IsCoprime ni ti) (copj : IsCoprime nj tj) (hxL : ∀ (m : Fin 4), M.x m ∈ P.Lℓ) (B : Triang P.MQ) : B.d₁ = 1 ∧ ↑B.d₂ ∣ mi * tj - mj * ti ∧ ↑B.d₂ ∣ mi * tk - mk * ti ∧ ↑B.d₂ ∣ mj * tk - mk * tj

Case II of prop:smith for one configuration (i, j, k): d₁ = 1 and d₂ divides the three reduced minors m_i t_j − m_j t_i, … (= d_ij/2).

theorem Louboutin.DiscV4.Dat.tierC_II {O : Type u_1} [CommRing O] [IsDomain O] [CharZero O] {M : Conj61.V4Data O} (P : Dat M) (h1 : 2 ∣ P.n₁) (h2 : 2 ∣ P.n₂) (h3 : 2 ∣ P.n₃) (B : Triang P.MQ) : B.d₁ = 1 ∧ 2 * ↑B.d₂ ∣ P.toZD.d₁₂ ∧ 2 * ↑B.d₂ ∣ P.toZD.d₁₃ ∧ 2 * ↑B.d₂ ∣ P.toZD.d₂₃

Case II of prop:smith (all n_j even): d₁ = 1 and 2d₂ divides d₁₂, d₁₃, d₂₃.

theorem Louboutin.DiscV4.Dat.e_pos {O : Type u_1} [CommRing O] [IsDomain O] [CharZero O] {M : Conj61.V4Data O} (P : Dat M) : 0 < P.toZD.m0 / P.toZD.h0

theorem Louboutin.DiscV4.Dat.e_dvd_d2 {O : Type u_1} [CommRing O] [IsDomain O] [CharZero O] {M : Conj61.V4Data O} (P : Dat M) (B : Triang P.MQ) : ↑(P.toZD.m0 / P.toZD.h0) ∣ ↑B.d₂

prop:smith, lower bound: m₀/h₀ ∣ d₂ (via the element (2Nα² − K₀ − K₁α)/(2e) ∈ A ∩ V₂).

theorem Louboutin.DiscV4.Dat.d1_d2 {O : Type u_1} [CommRing O] [IsDomain O] [CharZero O] {M : Conj61.V4Data O} (P : Dat M) (B : Triang P.MQ) : B.d₁ = 1 ∧ B.d₂ = P.toZD.m0 / P.toZD.h0

prop:smith (core): for the triangular basis of A (prop:triang, cited), d₁ = 1 and d₂ = m₀/h₀.

Part 13. Statements: prop:discA, prop:smith, thm:disc

noncomputable def Louboutin.DiscV4.Dat.φequiv {O : Type u_1} [CommRing O] [IsDomain O] [CharZero O] {M : Conj61.V4Data O} (P : Dat M) : ↥(Aring M).toAddSubgroup ≃+ ↥P.MQ

A ≃ φ(A) (additive), carrying ℤ[α] onto ℤ⁴.

Equations

• P.φequiv = AddEquiv.ofBijective P.φ.rangeRestrict ⋯

theorem Louboutin.DiscV4.Dat.quot_equiv {O : Type u_1} [CommRing O] [IsDomain O] [CharZero O] {M : Conj61.V4Data O} (P : Dat M) : Nonempty (↥(Aring M).toAddSubgroup ⧸ (Lat (vpow M)).addSubgroupOf (Aring M).toAddSubgroup ≃+ ↥P.MQ ⧸ Z4.addSubgroupOf P.MQ)

theorem Louboutin.DiscV4.Dat.prop_discA {O : Type u_1} [CommRing O] [IsDomain O] [CharZero O] {M : Conj61.V4Data O} (P : Dat M) {t u v w : ℤ} (ht : Conj61.T M.x = ↑t) (hu : Conj61.U M.x = ↑u) (hv : Conj61.V M.x = ↑v) (hw : Conj61.W M.x = ↑w) : (↑(t.gcd u)).gcd ↑(v.gcd w) ∣ P.δ.natAbs ∧ (Lat (vpow M)).relIndex (Aring M).toAddSubgroup = P.δ.natAbs / (↑(t.gcd u)).gcd ↑(v.gcd w) ∧ ↑((↑(t.gcd u)).gcd ↑(v.gcd w)) ^ 2 = P.Δ₁ * P.Δ₂ * P.Δ₃ ∧ ∀ (b : Fin 4 → O), Lat b = (Aring M).toAddSubgroup → D M b ^ 2 = ↑((↑(t.gcd u)).gcd ↑(v.gcd w)) ^ 2

prop:discA (in the model): with g = gcd(T, U, V, W), g ∣ Δ_α, [A : ℤ[α]] = |Δ_α|/g, g² = Δ₁Δ₂Δ₃, and D(b)² = g² for every family b spanning A (disc A = D(b)², b a ℤ-basis of A).

theorem Louboutin.DiscV4.Dat.prop_smith {O : Type u_1} [CommRing O] [IsDomain O] [CharZero O] {M : Conj61.V4Data O} (P : Dat M) (B : Triang P.MQ) : (P.toZD.h0 = 1 ∨ P.toZD.h0 = 2) ∧ P.toZD.h0 ∣ P.toZD.m0 ∧ B.d₁ = 1 ∧ B.d₂ = P.toZD.m0 / P.toZD.h0 ∧ B.d₃ = (Lat (vpow M)).relIndex (Aring M).toAddSubgroup * P.toZD.h0 / P.toZD.m0 ∧ Nonempty (↥(Aring M).toAddSubgroup ⧸ (Lat (vpow M)).addSubgroupOf (Aring M).toAddSubgroup ≃+ ZMod (P.toZD.m0 / P.toZD.h0) × ZMod ((Lat (vpow M)).relIndex (Aring M).toAddSubgroup * P.toZD.h0 / P.toZD.m0)) ∧ ((∃ (ω : Fin 4 → ℚ), BasisWith P.MQ ω) ↔ P.toZD.m0 = P.toZD.h0)

prop:smith (in the model), for the triangular basis B of A given by prop:triang (cited): h₀ ∈ {1, 2}, h₀ ∣ m₀, d₁ = 1, d₂ = m₀/h₀, d₃ = I h₀/m₀ with I = [A : ℤ[α]], A/ℤ[α] ≅ ℤ/(m₀/h₀) × ℤ/(I h₀/m₀), and A has a ℤ-basis {1, α, α², ω} iff m₀ = h₀.

theorem Louboutin.DiscV4.Dat.basis_of_rel {O : Type u_1} [CommRing O] [IsDomain O] [CharZero O] {M : Conj61.V4Data O} (P : Dat M) {y g₁ g₂ g₃ : O} {l0 q l2 l3 : ℤ} (hset : Set.range P.vη = {1, g₁, g₂, g₃}) (hyA : y ∈ Aring M) (hA : ∀ z ∈ Aring M, z ∈ P.Nℓ y) (hrel : 2 * y = ↑l0 + (2 * ↑q + 1) * g₁ + ↑l2 * g₂ + ↑l3 * g₃) : Lat ![1, y - ↑q * g₁, g₂, g₃] = (Aring M).toAddSubgroup

From A = L + ℤy with 2y = λ₀ + (2q+1)g₁ + λ₂g₂ + λ₃g₃ ({g₁, g₂, g₃} = {η₁, η₂, η₃}): the four elements 1, y − q g₁, g₂, g₃ span A.

theorem Louboutin.DiscV4.Dat.exists_basis {O : Type u_1} [CommRing O] [IsDomain O] [CharZero O] {M : Conj61.V4Data O} (P : Dat M) : ∃ (b : Fin 4 → O), Lat b = (Aring M).toAddSubgroup

A has a family of four elements spanning it (hence, by prop_discA, a ℤ-basis with D(b)² = g² ≠ 0): the statement disc A = g² is not vacuous.

Part 14. Theorem B (thm:disc) in the V4 model

def Louboutin.DiscV4.noteN (a b c z : ℤ) : ℤ

the note's n_j = D_j/gcd(D_j, E_j) (or 0), D_j = a² − 4b + 4z_j, E_j = a z_j − 2c.

Equations

• Louboutin.DiscV4.noteN a b c z = Louboutin.DiscV4.ntN (a ^ 2 - 4 * b + 4 * z) (a * z - 2 * c)

def Louboutin.DiscV4.noteT (a b c z : ℤ) : ℤ

the note's t_j = E_j/gcd(D_j, E_j) (or 1).

Equations

• Louboutin.DiscV4.noteT a b c z = Louboutin.DiscV4.ntT (a ^ 2 - 4 * b + 4 * z) (a * z - 2 * c)

def Louboutin.DiscV4.h0N (a b c z₁ z₂ z₃ : ℤ) : ℕ

the note's h₀ = gcd(n₁, n₂, n₃).

Equations

• Louboutin.DiscV4.h0N a b c z₁ z₂ z₃ = (↑((Louboutin.DiscV4.noteN a b c z₁).gcd (Louboutin.DiscV4.noteN a b c z₂))).gcd (Louboutin.DiscV4.noteN a b c z₃)

def Louboutin.DiscV4.m0N (a b c z₁ z₂ z₃ : ℤ) : ℕ

the note's m₀ = gcd(d₁₂, d₁₃, d₂₃), d_ij = n_i t_j − n_j t_i.

Equations

• One or more equations did not get rendered due to their size.

theorem Louboutin.DiscV4.thm_disc {O : Type u_1} [CommRing O] [IsDomain O] [CharZero O] (M : Conj61.V4Data O) {a b c d z₁ z₂ z₃ t u v w δ : ℤ} (ha : Conj61.ea M.x = ↑a) (hb : Conj61.eb M.x = ↑b) (hc : Conj61.ec M.x = ↑c) (hd : Conj61.ed M.x = ↑d) (hz₁ : Conj61.z1 M.x = ↑z₁) (hz₂ : Conj61.z2 M.x = ↑z₂) (hz₃ : Conj61.z3 M.x = ↑z₃) (hδ : Conj61.Vand M.x = ↑δ) (ht : Conj61.T M.x = ↑t) (hu : Conj61.U M.x = ↑u) (hv : Conj61.V M.x = ↑v) (hw : Conj61.W M.x = ↑w) : (h0N a b c z₁ z₂ z₃ = 1 ∨ h0N a b c z₁ z₂ z₃ = 2) ∧ h0N a b c z₁ z₂ z₃ ∣ m0N a b c z₁ z₂ z₃ ∧ (↑(t.gcd u)).gcd ↑(v.gcd w) ∣ δ.natAbs ∧ (Lat (Dat.vpow M)).relIndex (Aring M).toAddSubgroup = δ.natAbs / (↑(t.gcd u)).gcd ↑(v.gcd w) ∧ (∀ (β : Fin 4 → O), Lat β = (Aring M).toAddSubgroup → D M β ^ 2 = ↑((↑(t.gcd u)).gcd ↑(v.gcd w)) ^ 2) ∧ (∃ (β : Fin 4 → O), Lat β = (Aring M).toAddSubgroup) ∧ ∃ (P : Dat M), P.n₁ = noteN a b c z₁ ∧ P.t₁ = noteT a b c z₁ ∧ P.n₂ = noteN a b c z₂ ∧ P.t₂ = noteT a b c z₂ ∧ P.n₃ = noteN a b c z₃ ∧ P.t₃ = noteT a b c z₃ ∧ ∀ (B : Triang P.MQ), B.d₁ = 1 ∧ B.d₂ = m0N a b c z₁ z₂ z₃ / h0N a b c z₁ z₂ z₃ ∧ B.d₃ = δ.natAbs / (↑(t.gcd u)).gcd ↑(v.gcd w) * h0N a b c z₁ z₂ z₃ / m0N a b c z₁ z₂ z₃ ∧ Nonempty (↥(Aring M).toAddSubgroup ⧸ (Lat (Dat.vpow M)).addSubgroupOf (Aring M).toAddSubgroup ≃+ ZMod (m0N a b c z₁ z₂ z₃ / h0N a b c z₁ z₂ z₃) × ZMod (δ.natAbs / (↑(t.gcd u)).gcd ↑(v.gcd w) * h0N a b c z₁ z₂ z₃ / m0N a b c z₁ z₂ z₃)) ∧ ((∃ (ω : Fin 4 → ℚ), BasisWith P.MQ ω) ↔ m0N a b c z₁ z₂ z₃ = h0N a b c z₁ z₂ z₃)

Theorem B (thm:disc) in the abstract V4 model. Let a, b, c, d be the coefficients of Π_α, z₁, z₂, z₃ the roots of the resolvent, Δ = Δ_α, T, U, V, W as in the note, g = gcd(T, U, V, W), and (n_j, t_j), h₀, m₀ as in the note (noteN, noteT, h0N, m0N). Then, for A = ℤ[x₁, …, x₄] and ℤ[α] = ℤ + ℤα + ℤα² + ℤα³ (Lat (Dat.vpow M)): h₀ ∈ {1, 2}, h₀ ∣ m₀, g ∣ Δ, [A : ℤ[α]] = |Δ|/g, disc A = g² (D(b)² = g² for every family b spanning A, and such b exist); and for the triangular basis of A (prop:triang, cited, Triang, in the coordinates φ : A ↪ ℚ⁴ of Dat.MQ): d₁ = 1, d₂ = m₀/h₀, d₃ = (|Δ|/g)h₀/m₀, A/ℤ[α] ≅ ℤ/(m₀/h₀) × ℤ/((|Δ|/g)h₀/m₀), and A has a ℤ-basis {1, α, α², ω} iff m₀ = h₀.