The parity core of Louboutin's Conjecture 4.1, and a Möbius unit lemma

Let M ∈ M₂(ℤ) with M³ = ε·1 (ε = ±1), M ≠ ±1, and let F = X³ − aX²Y + bXY² − cY³ satisfy F ∘ M = ±F. Then c and a + b are odd, and X³ − aX² + bX − c has no root modulo 2. The proof: det M = 1 and tr M is odd (Cayley–Hamilton), so M mod 2 is one of the two elements of order 3 of GL₂(𝔽₂) and permutes ℙ¹(𝔽₂) cyclically; F(1, 0) = 1 forces F odd at (0, 1) and (1, 1) (a finite check by decide).

Not formalized here: that the Möbius matrix of σ lies in GL₂(ℤ) when ℤ[σα] = ℤ[α] (Bérczes–Evertse–Győry, Lemma 6.4), which is the input of cubic_parity, and Dedekind's criterion.

Main results

• Louboutin.CubicParity.cubic_parity, Louboutin.CubicParity.no_root_mod_two.
• Louboutin.CubicParity.mobius_unit: if β(rα + s) = pα + q then (rα + s)(p − rβ) = ps − qr, a unit if ps − qr = ±1.

References

• A. Bérczes, J.-H. Evertse and K. Győry, Multiply monogenic orders, Ann. Sc. Norm. Super. Pisa Cl. Sci. (5) 12 (2013), 467–497.
• 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).

def Louboutin.CubicParity.Fc {R : Type u_1} [CommRing R] (a b c X Y : R) : R

The binary cubic form F(X, Y) = X³ − aX²Y + bXY² − cY³ = Y³ Π(X/Y), Π = X³ − aX² + bX − c.

Equations

• Louboutin.CubicParity.Fc a b c X Y = X ^ 3 - a * X ^ 2 * Y + b * X * Y ^ 2 - c * Y ^ 3

theorem Louboutin.CubicParity.det_eq_one {M : Matrix (Fin 2) (Fin 2) ℤ} {ε : ℤ} (hε : ε = 1 ∨ ε = -1) (h : M ^ 3 = ε • 1) : M.det = 1

det M = 1 when M³ = ±1.

theorem Louboutin.CubicParity.trace_odd {M : Matrix (Fin 2) (Fin 2) ℤ} {ε : ℤ} (hε : ε = 1 ∨ ε = -1) (h : M ^ 3 = ε • 1) (h1 : M ≠ 1) (hm1 : M ≠ -1) : Odd (M 0 0 + M 1 1)

tr M is odd (indeed ±1) when M³ = ±1 and M ≠ ±1 (Cayley–Hamilton with det M = 1).

theorem Louboutin.CubicParity.parity_mod_two (m00 m01 m10 m11 a b c : ZMod 2) : m00 * m11 - m01 * m10 = 1 → m00 + m11 = 1 → Fc a b c m00 m10 = Fc a b c 1 0 → Fc a b c m01 m11 = Fc a b c 0 1 → Fc a b c (m00 + m01) (m10 + m11) = Fc a b c 1 1 → c ≠ 0 ∧ a + b ≠ 0

The mod-2 core: a matrix over 𝔽₂ with det 1 and trace 1 (an element of order 3 of GL₂(𝔽₂)), fixing the cubic form F at the three points (1,0), (0,1), (1,1) of ℙ¹(𝔽₂), forces F(0,1) = c ≠ 0 and F(1,1) ≠ 0, i.e. c = 1 and a + b = 1.

theorem Louboutin.CubicParity.odd_iff_zmod (n : ℤ) : Odd n ↔ ↑n ≠ 0

theorem Louboutin.CubicParity.cubic_parity {M : Matrix (Fin 2) (Fin 2) ℤ} {ε s : ℤ} (hε : ε = 1 ∨ ε = -1) (h : M ^ 3 = ε • 1) (h1 : M ≠ 1) (hm1 : M ≠ -1) (hs : s = 1 ∨ s = -1) {a b c : ℤ} (hF : ∀ (X Y : ℤ), Fc a b c (M 0 0 * X + M 0 1 * Y) (M 1 0 * X + M 1 1 * Y) = s * Fc a b c X Y) : Odd c ∧ Odd (a + b)

Cubic parity core of Prop. prop:c41 (Louboutin's Conjecture 4.1 without the BEG13 step): if M ∈ M₂(ℤ), M³ = ±1, M ≠ ±1 and F∘M = ±F for F = X³ − aX²Y + bXY² − cY³, then c and a + b are odd.

theorem Louboutin.CubicParity.no_root_mod_two {a b c : ℤ} (hc : Odd c) (hab : Odd (a + b)) (x : ZMod 2) : x ^ 3 - ↑a * x ^ 2 + ↑b * x - ↑c ≠ 0

Corollary of cubic_parity: Π = X³ − aX² + bX − c has no root modulo 2 (so, being cubic, it is irreducible modulo 2).

theorem Louboutin.CubicParity.mobius_mul {R : Type u_1} [CommRing R] {α β p q r s : R} (h : β * (r * α + s) = p * α + q) : (r * α + s) * (p - r * β) = p * s - q * r

Möbius unit lemma (Remark rem:mobius): in a commutative ring, if β(rα + s) = pα + q then (rα + s)(p − rβ) = ps − qr.

theorem Louboutin.CubicParity.mobius_unit {R : Type u_1} [CommRing R] {α β p q r s : R} (h : β * (r * α + s) = p * α + q) (hdet : p * s - q * r = 1 ∨ p * s - q * r = -1) : IsUnit (r * α + s)

If moreover ps − qr = ±1, then rα + s is a unit (so β = (pα + q)/(rα + s) ∈ ℤ[α] when p, q, r, s are integers and β(rα + s) = pα + q).

theorem Louboutin.CubicParity.mobius_eq {R : Type u_1} [CommRing R] {α β p q r s ε : R} (h : β * (r * α + s) = p * α + q) (hdet : p * s - q * r = ε) (hε : ε * ε = 1) : β = ε * ((p * α + q) * (p - r * β))

β itself: β = ±(pα + q)(p − rβ) when ps − qr = ±1 (the inverse of rα + s is ±(p − rβ)).