Polynomial identities for Louboutin's Conjecture 6.1 (biquadratic case)

Identities in an arbitrary commutative ring R, with x : Fin 4 → R standing for the conjugates x₁, …, x₄ and the Klein four-group acting by the labelling τ_i x_k = x_{i xor k}. Specialising R := ℤ[x₁, …, x₄] gives them as polynomial identities; specialising R := 𝓞_K gives them for the conjugates.

• The factorisation P(X) = ∏ (r_j X + ΔQ_j) with U = r₁r₂r₃, T = ΔQ₁ΔQ₂ΔQ₃, V, W, and Louboutin's formulas for T, U, V, W in the elementary symmetric functions a, b, c, d.
• The twelve certificates N_jk ∈ ∏_j (r_j, ΔQ_j) and Cramer's rule on all four conjugate rows; T, U, V, W as 4 × 4 determinants.
• The resolvent: Vand = (z₁ − z₂)(z₁ − z₃)(z₂ − z₃), D_j = a² − 4b + 4z_j, Δ even for integers, r_j ΔQ_j = a z_j − 2c. Here dQ j is ΔQ_j (the difference of the two quadratic factors).

Main results

• Louboutin.Conj61.factorisation, Louboutin.Conj61.T_eq, U_eq, V_eq, W_eq.
• Louboutin.Conj61.cramer1, cramer2, cramer3: ∑_k N_jk x_iᵏ = Vand · (x_i + x_{i xor j}).
• Louboutin.Conj61.Nc_scale: trilinearity of the certificates.
• Louboutin.Conj61.resolvent, Louboutin.Conj61.Vand_even, Louboutin.Conj61.cross_prod.
• Louboutin.Conj61.detT, detU, detV, detW: the determinant forms.

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).

V4 in the XOR labelling

def Louboutin.Conj61.xt : Fin 4 → Fin 4 → Fin 4

xt i k = i xor k: τ_i sends x_k to x_{i xor k}.

Equations

• Louboutin.Conj61.xt = ![![0, 1, 2, 3], ![1, 0, 3, 2], ![2, 3, 0, 1], ![3, 2, 1, 0]]

def Louboutin.Conj61.act {R : Type u_1} (x : Fin 4 → R) (i : Fin 4) : Fin 4 → R

conjugate family τ_i x : k ↦ x_{i xor k}.

Equations

• Louboutin.Conj61.act x i k = x (Louboutin.Conj61.xt i k)

S1: symmetric functions, Louboutin's T,U,V,W, and the factorisation

def Louboutin.Conj61.ea {R : Type u_1} [CommRing R] (x : Fin 4 → R) : R

Equations

• Louboutin.Conj61.ea x = x 0 + x 1 + x 2 + x 3

def Louboutin.Conj61.eb {R : Type u_1} [CommRing R] (x : Fin 4 → R) : R

Equations

• Louboutin.Conj61.eb x = x 0 * x 1 + x 0 * x 2 + x 0 * x 3 + x 1 * x 2 + x 1 * x 3 + x 2 * x 3

def Louboutin.Conj61.ec {R : Type u_1} [CommRing R] (x : Fin 4 → R) : R

Equations

• Louboutin.Conj61.ec x = x 0 * x 1 * x 2 + x 0 * x 1 * x 3 + x 0 * x 2 * x 3 + x 1 * x 2 * x 3

def Louboutin.Conj61.ed {R : Type u_1} [CommRing R] (x : Fin 4 → R) : R

Equations

• Louboutin.Conj61.ed x = x 0 * x 1 * x 2 * x 3

def Louboutin.Conj61.T {R : Type u_1} [CommRing R] (x : Fin 4 → R) : R

Louboutin's T, U, V, W as functions of a, b, c, d.

Equations

• Louboutin.Conj61.T x = Louboutin.Conj61.ea x ^ 2 * Louboutin.Conj61.ed x - Louboutin.Conj61.ec x ^ 2

def Louboutin.Conj61.U {R : Type u_1} [CommRing R] (x : Fin 4 → R) : R

Equations

• Louboutin.Conj61.U x = Louboutin.Conj61.ea x ^ 3 - 4 * Louboutin.Conj61.ea x * Louboutin.Conj61.eb x + 8 * Louboutin.Conj61.ec x

def Louboutin.Conj61.V {R : Type u_1} [CommRing R] (x : Fin 4 → R) : R

Equations

• Louboutin.Conj61.V x = Louboutin.Conj61.ea x ^ 2 * Louboutin.Conj61.eb x + 2 * Louboutin.Conj61.ea x * Louboutin.Conj61.ec x - 4 * Louboutin.Conj61.eb x ^ 2 + 16 * Louboutin.Conj61.ed x

def Louboutin.Conj61.W {R : Type u_1} [CommRing R] (x : Fin 4 → R) : R

Equations

• Louboutin.Conj61.W x = Louboutin.Conj61.ea x ^ 2 * Louboutin.Conj61.ec x + 8 * Louboutin.Conj61.ea x * Louboutin.Conj61.ed x - 4 * Louboutin.Conj61.eb x * Louboutin.Conj61.ec x

def Louboutin.Conj61.r1 {R : Type u_1} [CommRing R] (x : Fin 4 → R) : R

r_j = x₁ + x_{j+1} − x_k − x_l.

Equations

• Louboutin.Conj61.r1 x = x 0 + x 1 - x 2 - x 3

def Louboutin.Conj61.r2 {R : Type u_1} [CommRing R] (x : Fin 4 → R) : R

Equations

• Louboutin.Conj61.r2 x = x 0 + x 2 - x 1 - x 3

def Louboutin.Conj61.r3 {R : Type u_1} [CommRing R] (x : Fin 4 → R) : R

Equations

• Louboutin.Conj61.r3 x = x 0 + x 3 - x 1 - x 2

def Louboutin.Conj61.dQ1 {R : Type u_1} [CommRing R] (x : Fin 4 → R) : R

ΔQ_j = x₁x_{j+1} − x_k x_l.

Equations

• Louboutin.Conj61.dQ1 x = x 0 * x 1 - x 2 * x 3

def Louboutin.Conj61.dQ2 {R : Type u_1} [CommRing R] (x : Fin 4 → R) : R

Equations

• Louboutin.Conj61.dQ2 x = x 0 * x 2 - x 1 * x 3

def Louboutin.Conj61.dQ3 {R : Type u_1} [CommRing R] (x : Fin 4 → R) : R

Equations

• Louboutin.Conj61.dQ3 x = x 0 * x 3 - x 1 * x 2

def Louboutin.Conj61.z1 {R : Type u_1} [CommRing R] (x : Fin 4 → R) : R

z_j = x₁x_{j+1} + x_k x_l (roots of the resolvent cubic).

Equations

• Louboutin.Conj61.z1 x = x 0 * x 1 + x 2 * x 3

def Louboutin.Conj61.z2 {R : Type u_1} [CommRing R] (x : Fin 4 → R) : R

Equations

• Louboutin.Conj61.z2 x = x 0 * x 2 + x 1 * x 3

def Louboutin.Conj61.z3 {R : Type u_1} [CommRing R] (x : Fin 4 → R) : R

Equations

• Louboutin.Conj61.z3 x = x 0 * x 3 + x 1 * x 2

theorem Louboutin.Conj61.U_eq {R : Type u_1} [CommRing R] (x : Fin 4 → R) : U x = r1 x * r2 x * r3 x

theorem Louboutin.Conj61.T_eq {R : Type u_1} [CommRing R] (x : Fin 4 → R) : T x = dQ1 x * dQ2 x * dQ3 x

theorem Louboutin.Conj61.V_eq {R : Type u_1} [CommRing R] (x : Fin 4 → R) : V x = r1 x * r2 x * dQ3 x + r1 x * dQ2 x * r3 x + dQ1 x * r2 x * r3 x

theorem Louboutin.Conj61.W_eq {R : Type u_1} [CommRing R] (x : Fin 4 → R) : W x = r1 x * dQ2 x * dQ3 x + dQ1 x * r2 x * dQ3 x + dQ1 x * dQ2 x * r3 x

theorem Louboutin.Conj61.factorisation {R : Type u_1} [CommRing R] (x : Fin 4 → R) (X : R) : U x * X ^ 3 + V x * X ^ 2 + W x * X + T x = (r1 x * X + dQ1 x) * (r2 x * X + dQ2 x) * (r3 x * X + dQ3 x)

Key factorisation (Prop. 2.1(3)), with X any element of R (take R := O[X] and x := C ∘ x for the polynomial statement, see Conj61Model).

theorem Louboutin.Conj61.T_shift {R : Type u_1} [CommRing R] (x : Fin 4 → R) (X : R) : (T fun (i : Fin 4) => x i + X) = U x * X ^ 3 + V x * X ^ 2 + W x * X + T x

Prop. 2.1(1): P(X) = T(α + X) (Louboutin's a'²d' − c'² of the shifted conjugates).

theorem Louboutin.Conj61.dQ_shift {R : Type u_1} [CommRing R] (x : Fin 4 → R) (X : R) : (dQ1 fun (i : Fin 4) => x i + X) = r1 x * X + dQ1 x ∧ (dQ2 fun (i : Fin 4) => x i + X) = r2 x * X + dQ2 x ∧ (dQ3 fun (i : Fin 4) => x i + X) = r3 x * X + dQ3 x

ΔQ_j(x + X) = r_j X + ΔQ_j (the linear factors).

S3: Vandermonde, resolvent, parity

def Louboutin.Conj61.Vand {R : Type u_1} [CommRing R] (x : Fin 4 → R) : R

Vand = ∏_{i<j} (x_j − x_i) = D(1, α, α², α³).

Equations

• Louboutin.Conj61.Vand x = (x 1 - x 0) * (x 2 - x 0) * (x 3 - x 0) * (x 2 - x 1) * (x 3 - x 1) * (x 3 - x 2)

theorem Louboutin.Conj61.z_diff {R : Type u_1} [CommRing R] (x : Fin 4 → R) : z1 x - z2 x = (x 0 - x 3) * (x 1 - x 2) ∧ z1 x - z3 x = (x 0 - x 2) * (x 1 - x 3) ∧ z2 x - z3 x = (x 0 - x 1) * (x 2 - x 3)

theorem Louboutin.Conj61.Vand_eq_z {R : Type u_1} [CommRing R] (x : Fin 4 → R) : Vand x = (z1 x - z2 x) * (z1 x - z3 x) * (z2 x - z3 x)

Lemma 1.2: Vand = +(z₁ − z₂)(z₁ − z₃)(z₂ − z₃).

theorem Louboutin.Conj61.resolvent {R : Type u_1} [CommRing R] (x : Fin 4 → R) : z1 x + z2 x + z3 x = eb x ∧ z1 x * z2 x + z1 x * z3 x + z2 x * z3 x = ea x * ec x - 4 * ed x ∧ z1 x * z2 x * z3 x = ea x ^ 2 * ed x + ec x ^ 2 - 4 * eb x * ed x

Resolvent: e₁(z) = b, e₂(z) = ac − 4d, e₃(z) = a²d + c² − 4bd.

theorem Louboutin.Conj61.rsq {R : Type u_1} [CommRing R] (x : Fin 4 → R) : r1 x ^ 2 = ea x ^ 2 - 4 * eb x + 4 * z1 x ∧ r2 x ^ 2 = ea x ^ 2 - 4 * eb x + 4 * z2 x ∧ r3 x ^ 2 = ea x ^ 2 - 4 * eb x + 4 * z3 x

D_j := r_j² = a² − 4b + 4z_j.

theorem Louboutin.Conj61.rq_eq {R : Type u_1} [CommRing R] (x : Fin 4 → R) : r1 x * dQ1 x = ea x * z1 x - 2 * ec x ∧ r2 x * dQ2 x = ea x * z2 x - 2 * ec x ∧ r3 x * dQ3 x = ea x * z3 x - 2 * ec x

r_j ΔQ_j = a z_j − 2c (note, after prop:discA: D_j = r_j², a z_j − 2c = r_j q_j).

theorem Louboutin.Conj61.cross_eq {R : Type u_1} [CommRing R] (x : Fin 4 → R) : r1 x * dQ2 x - r2 x * dQ1 x = -(r3 x * (z1 x - z2 x)) ∧ r2 x * dQ3 x - r3 x * dQ2 x = -(r1 x * (z2 x - z3 x)) ∧ r3 x * dQ1 x - r1 x * dQ3 x = -(r2 x * (z3 x - z1 x))

Proof of Cor. cor:weak (Program S10): r_i q_j − r_j q_i = −r_k (z_i − z_j), {i, j, k} = {1, 2, 3} in the cyclic order (12), (23), (31).

theorem Louboutin.Conj61.cross_prod {R : Type u_1} [CommRing R] (x : Fin 4 → R) : (r1 x * dQ2 x - r2 x * dQ1 x) * (r2 x * dQ3 x - r3 x * dQ2 x) * (r3 x * dQ1 x - r1 x * dQ3 x) = Vand x * (r1 x * r2 x * r3 x)

Proof of Cor. cor:weak: ∏cyc (r_i q_j − r_j q_i) = +Vand · r₁r₂r₃, the product over the cyclic pairs (12), (23), (31), with Vand = ∏{i<j} (x_j − x_i) (sign +, exactly).

theorem Louboutin.Conj61.even_prod_diff (a b c : ℤ) : Even ((a - b) * (a - c) * (b - c))

Parity half of Lemma 1.2: for integers z₁, z₂, z₃, (z₁−z₂)(z₁−z₃)(z₂−z₃) is even.

theorem Louboutin.Conj61.Vand_even {R : Type u_1} [CommRing R] (x : Fin 4 → R) {k1 k2 k3 : ℤ} (h1 : z1 x = ↑k1) (h2 : z2 x = ↑k2) (h3 : z3 x = ↑k3) : ∃ (δ : ℤ), Vand x = ↑δ ∧ Even δ

Lemma 1.2 for integer-valued z_j: if the z_j are (images of) integers, Vand is an even integer.

S2: the twelve certificates and Cramer

NcJK (paper j = J ∈ 1..3, power k = K ∈ 0..3) is the Cramer numerator of the coordinate of S_j = α + τ_jα on αᵏ, written as a function of the generators (R_j, Q_j) of the product ideal ∏j (r_j, ΔQ_j): each summand is λ·h₁h₂h₃ with h_j ∈ {R_j, Q_j} (the certificates were found by computer algebra and are checked here by ring); NJK is it at R_j = r_j, Q_j = ΔQ_j. cramerJ proves Σ_k N_jk x_iᵏ = Vand·(x_i + x{i xor j}) for all four rows i, i.e. N_jk = Vand·(coordinate) whenever Vand is cancellable. Nc_scale is the trilinearity used in S4.

The twelve certificates as functions of the generators: NcJK x R₁ R₂ R₃ Q₁ Q₂ Q₃ is trilinear in the pairs (R_j, Q_j): every summand is λ·h₁h₂h₃ with h_j ∈ {R_j, Q_j} and λ ∈ ℤ[x] of degree ≤ 2. J = the index j of the paper, K = power k.

def Louboutin.Conj61.Nc10 {R : Type u_1} [CommRing R] (x : Fin 4 → R) (R₁ R₂ R₃ Q₁ Q₂ Q₃ : R) : R

Equations

• Louboutin.Conj61.Nc10 x R₁ R₂ R₃ Q₁ Q₂ Q₃ = (x 0 * x 2 - x 0 * x 3 - x 1 * x 2 + x 1 * x 3) * R₁ * Q₂ * Q₃ - x 0 * x 2 * Q₁ * R₂ * Q₃ + x 0 * x 3 * Q₁ * Q₂ * R₃ + (x 2 - x 3) * Q₁ * Q₂ * Q₃

def Louboutin.Conj61.Nc11 {R : Type u_1} [CommRing R] (x : Fin 4 → R) (R₁ R₂ R₃ Q₁ Q₂ Q₃ : R) : R

Equations

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

def Louboutin.Conj61.Nc12 {R : Type u_1} [CommRing R] (x : Fin 4 → R) (R₁ R₂ R₃ Q₁ Q₂ Q₃ : R) : R

Equations

• Louboutin.Conj61.Nc12 x R₁ R₂ R₃ Q₁ Q₂ Q₃ = -(x 0 + x 1 + x 2 + x 3) * R₁ * R₂ * Q₃ + (x 0 + x 1 + x 2 + x 3) * R₁ * Q₂ * R₃ + Q₁ * R₂ * Q₃ - Q₁ * Q₂ * R₃

def Louboutin.Conj61.Nc13 {R : Type u_1} [CommRing R] (x : Fin 4 → R) (R₁ R₂ R₃ Q₁ Q₂ Q₃ : R) : R

Equations

• Louboutin.Conj61.Nc13 x R₁ R₂ R₃ Q₁ Q₂ Q₃ = R₁ * R₂ * Q₃ - R₁ * Q₂ * R₃

def Louboutin.Conj61.Nc20 {R : Type u_1} [CommRing R] (x : Fin 4 → R) (R₁ R₂ R₃ Q₁ Q₂ Q₃ : R) : R

Equations

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

def Louboutin.Conj61.Nc21 {R : Type u_1} [CommRing R] (x : Fin 4 → R) (R₁ R₂ R₃ Q₁ Q₂ Q₃ : R) : R

Equations

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

def Louboutin.Conj61.Nc22 {R : Type u_1} [CommRing R] (x : Fin 4 → R) (R₁ R₂ R₃ Q₁ Q₂ Q₃ : R) : R

Equations

• Louboutin.Conj61.Nc22 x R₁ R₂ R₃ Q₁ Q₂ Q₃ = (x 0 + x 1 + x 2 + x 3) * R₁ * R₂ * Q₃ - R₁ * Q₂ * Q₃ - (x 0 + x 1 + x 2 + x 3) * Q₁ * R₂ * R₃ + Q₁ * Q₂ * R₃

def Louboutin.Conj61.Nc23 {R : Type u_1} [CommRing R] (x : Fin 4 → R) (R₁ R₂ R₃ Q₁ Q₂ Q₃ : R) : R

Equations

• Louboutin.Conj61.Nc23 x R₁ R₂ R₃ Q₁ Q₂ Q₃ = -R₁ * R₂ * Q₃ + Q₁ * R₂ * R₃

def Louboutin.Conj61.Nc30 {R : Type u_1} [CommRing R] (x : Fin 4 → R) (R₁ R₂ R₃ Q₁ Q₂ Q₃ : R) : R

Equations

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

def Louboutin.Conj61.Nc31 {R : Type u_1} [CommRing R] (x : Fin 4 → R) (R₁ R₂ R₃ Q₁ Q₂ Q₃ : R) : R

Equations

• Louboutin.Conj61.Nc31 x R₁ R₂ R₃ Q₁ Q₂ Q₃ = (x 0 * x 1 + x 0 * x 2 + x 1 * x 3) * R₁ * Q₂ * R₃ + (-x 0 * x 1 - x 0 * x 2 - x 2 * x 3) * Q₁ * R₂ * R₃ + (-x 1 + x 2) * Q₁ * Q₂ * R₃

def Louboutin.Conj61.Nc32 {R : Type u_1} [CommRing R] (x : Fin 4 → R) (R₁ R₂ R₃ Q₁ Q₂ Q₃ : R) : R

Equations

• Louboutin.Conj61.Nc32 x R₁ R₂ R₃ Q₁ Q₂ Q₃ = -(x 0 + x 1 + x 2 + x 3) * R₁ * Q₂ * R₃ + R₁ * Q₂ * Q₃ + (x 0 + x 1 + x 2 + x 3) * Q₁ * R₂ * R₃ - Q₁ * R₂ * Q₃

def Louboutin.Conj61.Nc33 {R : Type u_1} [CommRing R] (x : Fin 4 → R) (R₁ R₂ R₃ Q₁ Q₂ Q₃ : R) : R

Equations

• Louboutin.Conj61.Nc33 x R₁ R₂ R₃ Q₁ Q₂ Q₃ = R₁ * Q₂ * R₃ - Q₁ * R₂ * R₃

The Cramer numerators N_jk: the certificates at the actual generators r_j, ΔQ_j.

def Louboutin.Conj61.N10 {R : Type u_1} [CommRing R] (x : Fin 4 → R) : R

Equations

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

def Louboutin.Conj61.N11 {R : Type u_1} [CommRing R] (x : Fin 4 → R) : R

Equations

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

def Louboutin.Conj61.N12 {R : Type u_1} [CommRing R] (x : Fin 4 → R) : R

Equations

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

def Louboutin.Conj61.N13 {R : Type u_1} [CommRing R] (x : Fin 4 → R) : R

Equations

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

def Louboutin.Conj61.N20 {R : Type u_1} [CommRing R] (x : Fin 4 → R) : R

Equations

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

def Louboutin.Conj61.N21 {R : Type u_1} [CommRing R] (x : Fin 4 → R) : R

Equations

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

def Louboutin.Conj61.N22 {R : Type u_1} [CommRing R] (x : Fin 4 → R) : R

Equations

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

def Louboutin.Conj61.N23 {R : Type u_1} [CommRing R] (x : Fin 4 → R) : R

Equations

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

def Louboutin.Conj61.N30 {R : Type u_1} [CommRing R] (x : Fin 4 → R) : R

Equations

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

def Louboutin.Conj61.N31 {R : Type u_1} [CommRing R] (x : Fin 4 → R) : R

Equations

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

def Louboutin.Conj61.N32 {R : Type u_1} [CommRing R] (x : Fin 4 → R) : R

Equations

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

def Louboutin.Conj61.N33 {R : Type u_1} [CommRing R] (x : Fin 4 → R) : R

Equations

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

theorem Louboutin.Conj61.Nc_scale {R : Type u_1} [CommRing R] (x : Fin 4 → R) (n₁ n₂ n₃ t₁ t₂ t₃ θ₁ θ₂ θ₃ : R) : Nc10 x (n₁ * θ₁) (n₂ * θ₂) (n₃ * θ₃) (t₁ * θ₁) (t₂ * θ₂) (t₃ * θ₃) = θ₁ * θ₂ * θ₃ * Nc10 x n₁ n₂ n₃ t₁ t₂ t₃ ∧ Nc11 x (n₁ * θ₁) (n₂ * θ₂) (n₃ * θ₃) (t₁ * θ₁) (t₂ * θ₂) (t₃ * θ₃) = θ₁ * θ₂ * θ₃ * Nc11 x n₁ n₂ n₃ t₁ t₂ t₃ ∧ Nc12 x (n₁ * θ₁) (n₂ * θ₂) (n₃ * θ₃) (t₁ * θ₁) (t₂ * θ₂) (t₃ * θ₃) = θ₁ * θ₂ * θ₃ * Nc12 x n₁ n₂ n₃ t₁ t₂ t₃ ∧ Nc13 x (n₁ * θ₁) (n₂ * θ₂) (n₃ * θ₃) (t₁ * θ₁) (t₂ * θ₂) (t₃ * θ₃) = θ₁ * θ₂ * θ₃ * Nc13 x n₁ n₂ n₃ t₁ t₂ t₃ ∧ Nc20 x (n₁ * θ₁) (n₂ * θ₂) (n₃ * θ₃) (t₁ * θ₁) (t₂ * θ₂) (t₃ * θ₃) = θ₁ * θ₂ * θ₃ * Nc20 x n₁ n₂ n₃ t₁ t₂ t₃ ∧ Nc21 x (n₁ * θ₁) (n₂ * θ₂) (n₃ * θ₃) (t₁ * θ₁) (t₂ * θ₂) (t₃ * θ₃) = θ₁ * θ₂ * θ₃ * Nc21 x n₁ n₂ n₃ t₁ t₂ t₃ ∧ Nc22 x (n₁ * θ₁) (n₂ * θ₂) (n₃ * θ₃) (t₁ * θ₁) (t₂ * θ₂) (t₃ * θ₃) = θ₁ * θ₂ * θ₃ * Nc22 x n₁ n₂ n₃ t₁ t₂ t₃ ∧ Nc23 x (n₁ * θ₁) (n₂ * θ₂) (n₃ * θ₃) (t₁ * θ₁) (t₂ * θ₂) (t₃ * θ₃) = θ₁ * θ₂ * θ₃ * Nc23 x n₁ n₂ n₃ t₁ t₂ t₃ ∧ Nc30 x (n₁ * θ₁) (n₂ * θ₂) (n₃ * θ₃) (t₁ * θ₁) (t₂ * θ₂) (t₃ * θ₃) = θ₁ * θ₂ * θ₃ * Nc30 x n₁ n₂ n₃ t₁ t₂ t₃ ∧ Nc31 x (n₁ * θ₁) (n₂ * θ₂) (n₃ * θ₃) (t₁ * θ₁) (t₂ * θ₂) (t₃ * θ₃) = θ₁ * θ₂ * θ₃ * Nc31 x n₁ n₂ n₃ t₁ t₂ t₃ ∧ Nc32 x (n₁ * θ₁) (n₂ * θ₂) (n₃ * θ₃) (t₁ * θ₁) (t₂ * θ₂) (t₃ * θ₃) = θ₁ * θ₂ * θ₃ * Nc32 x n₁ n₂ n₃ t₁ t₂ t₃ ∧ Nc33 x (n₁ * θ₁) (n₂ * θ₂) (n₃ * θ₃) (t₁ * θ₁) (t₂ * θ₂) (t₃ * θ₃) = θ₁ * θ₂ * θ₃ * Nc33 x n₁ n₂ n₃ t₁ t₂ t₃

Trilinearity of the certificates (the product-ideal structure ∏_j (r_j, ΔQ_j)): if R_j = n_j θ_j and Q_j = t_j θ_j then each certificate equals θ₁θ₂θ₃ times the certificate at (n_j, t_j).

Cramer, all 12 pairs × 4 conjugate rows: Σ_k N_jk x_iᵏ = Vand · (x_i + x_{i xor j}). Row i = 0 is Σ_k N_jk αᵏ = Vand·S_j of c1 §5 (S_j = α + τ_jα); rows 1..3 are its conjugates, so N_jk / Vand are the coordinates of S_j in the basis 1, α, α², α³.

theorem Louboutin.Conj61.cramer1 {R : Type u_1} [CommRing R] (x : Fin 4 → R) : N10 x + N11 x * x 0 + N12 x * x 0 ^ 2 + N13 x * x 0 ^ 3 = Vand x * (x 0 + x 1) ∧ N10 x + N11 x * x 1 + N12 x * x 1 ^ 2 + N13 x * x 1 ^ 3 = Vand x * (x 1 + x 0) ∧ N10 x + N11 x * x 2 + N12 x * x 2 ^ 2 + N13 x * x 2 ^ 3 = Vand x * (x 2 + x 3) ∧ N10 x + N11 x * x 3 + N12 x * x 3 ^ 2 + N13 x * x 3 ^ 3 = Vand x * (x 3 + x 2)

theorem Louboutin.Conj61.cramer2 {R : Type u_1} [CommRing R] (x : Fin 4 → R) : N20 x + N21 x * x 0 + N22 x * x 0 ^ 2 + N23 x * x 0 ^ 3 = Vand x * (x 0 + x 2) ∧ N20 x + N21 x * x 1 + N22 x * x 1 ^ 2 + N23 x * x 1 ^ 3 = Vand x * (x 1 + x 3) ∧ N20 x + N21 x * x 2 + N22 x * x 2 ^ 2 + N23 x * x 2 ^ 3 = Vand x * (x 2 + x 0) ∧ N20 x + N21 x * x 3 + N22 x * x 3 ^ 2 + N23 x * x 3 ^ 3 = Vand x * (x 3 + x 1)

theorem Louboutin.Conj61.cramer3 {R : Type u_1} [CommRing R] (x : Fin 4 → R) : N30 x + N31 x * x 0 + N32 x * x 0 ^ 2 + N33 x * x 0 ^ 3 = Vand x * (x 0 + x 3) ∧ N30 x + N31 x * x 1 + N32 x * x 1 ^ 2 + N33 x * x 1 ^ 3 = Vand x * (x 1 + x 2) ∧ N30 x + N31 x * x 2 + N32 x * x 2 ^ 2 + N33 x * x 2 ^ 3 = Vand x * (x 2 + x 1) ∧ N30 x + N31 x * x 3 + N32 x * x 3 ^ 2 + N33 x * x 3 ^ 3 = Vand x * (x 3 + x 0)

S1 (cont.): T, U, V, W as determinants D(ω) = det[σ_i(ω_l)] (Prop. 2.1 (2),(4),(5), (6.3))

det4e is the cofactor expansion of a 4×4 determinant along row 0 (entries row-major); Conj61Model.det4 identifies it with Matrix.det. Row i is ω with x_k ↦ x_{i xor k}.

def Louboutin.Conj61.det4e {R : Type u_1} [CommRing R] (a00 a01 a02 a03 a10 a11 a12 a13 a20 a21 a22 a23 a30 a31 a32 a33 : R) : R

Explicit 4×4 determinant, entries aIL (row I, column L).

Equations

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

theorem Louboutin.Conj61.detT {R : Type u_1} [CommRing R] (x : Fin 4 → R) : det4e 1 (x 0) (x 0 * x 1) (x 0 * x 1 * x 2) 1 (x 1) (x 1 * x 0) (x 1 * x 0 * x 3) 1 (x 2) (x 2 * x 3) (x 2 * x 3 * x 0) 1 (x 3) (x 3 * x 2) (x 3 * x 2 * x 1) = -T x

(6.2): D(1, α, α·τ₁α, α·τ₁α·τ₂α) = −T.

theorem Louboutin.Conj61.detU {R : Type u_1} [CommRing R] (x : Fin 4 → R) : det4e 1 (x 0) (x 1) (x 2) 1 (x 1) (x 0) (x 3) 1 (x 2) (x 3) (x 0) 1 (x 3) (x 2) (x 1) = -U x

(6.3): D(1, α, τ₁α, τ₂α) = −U.

theorem Louboutin.Conj61.detV {R : Type u_1} [CommRing R] (x : Fin 4 → R) : det4e 1 (x 0) (x 1) (x 0 * x 1 + x 0 * x 2 + x 1 * x 2) 1 (x 1) (x 0) (x 1 * x 0 + x 1 * x 3 + x 0 * x 3) 1 (x 2) (x 3) (x 2 * x 3 + x 2 * x 0 + x 3 * x 0) 1 (x 3) (x 2) (x 3 * x 2 + x 3 * x 1 + x 2 * x 1) + det4e 1 (x 0) (x 0 * x 1) (x 1 + x 2) 1 (x 1) (x 1 * x 0) (x 0 + x 3) 1 (x 2) (x 2 * x 3) (x 3 + x 0) 1 (x 3) (x 3 * x 2) (x 2 + x 1) = -V x

Prop. 2.1(4): V = −[D(1, α, τ₁α, α·τ₁α + α·τ₂α + τ₁α·τ₂α) + D(1, α, α·τ₁α, τ₁α + τ₂α)].

theorem Louboutin.Conj61.detW {R : Type u_1} [CommRing R] (x : Fin 4 → R) : det4e 1 (x 0) (x 1) (x 0 * x 1 * x 2) 1 (x 1) (x 0) (x 1 * x 0 * x 3) 1 (x 2) (x 3) (x 2 * x 3 * x 0) 1 (x 3) (x 2) (x 3 * x 2 * x 1) + det4e 1 (x 0) (x 0 * x 1) (x 0 * x 2 + x 1 * x 2) 1 (x 1) (x 1 * x 0) (x 1 * x 3 + x 0 * x 3) 1 (x 2) (x 2 * x 3) (x 2 * x 0 + x 3 * x 0) 1 (x 3) (x 3 * x 2) (x 3 * x 1 + x 2 * x 1) = -W x

Prop. 2.1(5): W = −[D(1, α, τ₁α, α·τ₁α·τ₂α) + D(1, α, α·τ₁α, α·τ₂α + τ₁α·τ₂α)].