Keyboard shortcuts

Press ← or → to navigate between chapters

Press ? to show this help

Press Esc to hide this help

A square-discriminant obstruction for the Pascalian polynomial of degree 49

Abstract

The square discriminant of the degree twenty-four binomial truncation refutes the odd-index Galois-group conjecture at n = 49.

Definition 1.1 (The Pascalian polynomial).

Formalization. D5/S3/Factorization/Galois/LevensPascalian.P (✓ std3).

Citation. Owen Levens (2025). Polynomials Arising from Sorted Binomial Coefficients. DOI: 10.48550/arXiv.2511.03082. URL: https://arxiv.org/abs/2511.03082v1.

Commentary.

Section 1, printed page 1: “let ⟨n k⟩ = C(n, ⌊(n−k)/2⌋) for 0 ≤ k ≤ n, call the ⟨n k⟩ triangle the Pascalian numbers, and let the nth Pascalian polynomial be P_n(z) = Σ_{k=0}^{n} ⟨n k⟩ z^{n−k}.” The coefficient binomial is Nat.choose, cast into ℚ and then embedded by Polynomial.C. The index k ranges from zero through n; subtraction and Nat.div are operations on ℕ, so Nat.div (n − k) 2 is the floor in this range.

Definition 1.2 (Sign change on the signed letters).

Formalization. D5/S3/Factorization/Galois/LevensPascalian.signFlip (✓ std3).

Source. Repository-derived.

Commentary.

The two Boolean values represent the two signs. Equiv.prodCongr fixes the Fin m coordinate and swaps false with true.

Definition 1.3 (The group of signed permutations).

Formalization. D5/S3/Factorization/Galois/LevensPascalian.hyperoctahedral (✓ std3).

Source. Repository-derived.

Commentary.

The mth hyperoctahedral group is represented as the subgroup of permutations of Fin m × Bool commuting with signFlip m. This centralizer has order 2^m m!.

Definition 1.4 (Levens Conjecture 6.4, odd-index clause).

Formalization. D5/S3/Factorization/Galois/LevensPascalian.claim (✓ std3).

Citation. Owen Levens (2025). Polynomials Arising from Sorted Binomial Coefficients. DOI: 10.48550/arXiv.2511.03082. URL: https://arxiv.org/abs/2511.03082v1.

Commentary.

Conjecture 6.4, printed page 20: “P_n(z) has full Galois group for even n. For n = 2m + 1, the Galois group of P_n(z) is the mth hyperoctahedral group.” The displayed proposition is the second sentence, for natural m ≥ 1. Polynomial.Gal is the automorphism group of the splitting field over ℚ. Being the indicated group means the existence of an abstract multiplicative equivalence, expressed by Nonempty; disproving this also excludes an isomorphism as permutation groups.

Theorem 1.5 (The odd-index assertion is false).

Proof. Machine-checked in Lean as D5/S3/Factorization/Galois/LevensPascalian.result (✓ std3). ∎

Resolves. Problems/levens-2025-pascalian-galois-square-discriminant (refuted) by D5/S3/Factorization/Galois/LevensPascalian.result.

Source. Repository-derived.

Acknowledgement. Owen Levens (2025). Polynomials Arising from Sorted Binomial Coefficients. DOI: 10.48550/arXiv.2511.03082. URL: https://arxiv.org/abs/2511.03082v1.

Commentary.

At m = 24, put c = 63205303218876 = Nat.choose 49 24 and q(X) = ∑ j ∈ Finset.range 25, Polynomial.C ((Nat.choose 49 j : ℕ) : ℚ) * X^j. Then P 49 = (1 + X) * q.comp (X^2), and (1 + X) * q.derivative − Polynomial.C 49 * q = −Polynomial.C (25*c) * X^24. Resultant identities give q.discr = (7 * 5^23 * c^11)^2. These polynomial and rational identities are checked inside the proof.

The Vandermonde determinant of the twenty-four distinct roots of q is rational and nonzero. Every field automorphism fixes it, so its permutation of those roots has sign one. The roots of P 49 are −1 and the signed square roots of the roots of q. Encoding an automorphism by its twenty-four signs and its even permutation is injective. Consequently the Galois group has order at most 2^24 * |alternatingGroup (Fin 24)|, strictly less than the hyperoctahedral order 2^24 * 24!.

This excludes the abstract group isomorphism at n = 49. It does not determine the exact Galois group. The even-index sentence, Conjecture 6.3, and a classification of the other odd indices remain separate questions. The square-discriminant formula is classical; its general form appears in Filaseta–Moy, Lemma 3, as recorded with the source reference.

References