Metadata

slug: brown-george-2025-degree-polynomial-root-bound
bibkey: browngeorge2025degree
doi: 10.48550/arXiv.2505.04882
url: https://arxiv.org/abs/2505.04882v1
triage: theorem
motivation_gids:
  - D5/S3/Zeros/DegreeRoots/Result.result

Brown–George’s argument-dependent degree-root bound

Problem

J. I. Brown and I. C. George, On the roots of degree polynomials, Australasian Journal of Combinatorics 92(2), 164–183, Conjecture 4.1, p. 180, states:

If z is a nonzero degree root of a graph of order n with argument arg(z) ∈ (−π, π], then |z| ≤ (n − 1)^{|arg(z)/π|}.

Section 1 defines $D (G; x) = \sum_{v \in V (G)} x^{d e g (v)}$ . The arXiv version is The Degree Polynomial, arXiv:2505.04882v1. The settled proposition is

$\forall n \geq 1 \forall G simple on Fin (n) \forall z \in C, z \neq = 0 \land D (G; z) = 0 ⟹ ∣ z ∣ \leq (n - 1)^{∣ a r g z ∣/ π} .$

Statement echo

Source clause	Lean counterpart	Fidelity
Graph of positive order $n$	Natural `n`, `1 ≤ n`, `SimpleGraph (Fin n)` in `claim`	The preregistered simple-graph convention; empty graphs are excluded
Degree polynomial	`degreePolynomial`, the sum of `Polynomial.X ^ G.degree v` over every vertex	Includes degree-zero vertices
Nonzero degree root	Complex `z`, `z ≠ 0`, polynomial evaluation equal to zero	Both hypotheses retained
$ar g z \in (- π, π]$	`Complex.arg z`	Pinned Mathlib branch convention
Modulus and power	Complex norm and real power	$π > 0$ gives $∣ ar g (z) / π ∣ = ∣ ar g z ∣/ π$
All nonzero roots	`result : claim`	Universal inequality; no extra root hypothesis

The public definitions degreePolynomial and claim reproduce the two preregistered expressions literally. Positive order is explicit: at order zero the vertex sum is the zero polynomial, so a universal root bound would have a different meaning.

Motivation

Preregistration #19987 selects Conjecture 4.1. The settling declaration is D5.S3.Zeros.DegreeRoots.Result.result, with admission basis open-problem-resolution (#19987; Proved). Its proof uses the general D5.S3.Zeros.DegreeRoots.EscapeWitness.normalized_escape_bound.

Gap

The source’s Theorem 3.2 gives the real-root bound $n - 1$ and Proposition 3.5 gives the imaginary-root bound $n - 1$ . Conjecture 4.1 interpolates these bounds through the root’s argument. The published version retains the conjecture. The source and literature checks recorded in #19987 cover the article, arXiv version, George’s thesis, and title/identifier searches; no settlement was located in that searched scope. Literature completeness is ASSUMED-UNVERIFIED.

Route

For $λ > 0$ and $t \geq 0$ , put $F_{λ} (t) = e^{- λ t} (cos t + λ sin t)$ . The private damped_trig_bound proves $F_{λ} (t) \geq - e^{- λπ}$ . On $0 \leq t \leq π$ , the proof uses the derivative of $q (u) = e^{λ u} (cos u - λ sin u)$ : $q^{'} (u) = - (1 + λ^{2}) e^{λ u} sin u \leq 0$ on $[0, π]$ , with $u = π - t$ . For $t \geq π$ , put $u = t - π$ ; the estimates $cos u \leq 1$ , $sin u \leq u$ , and $1 + λ u \leq e^{λ u}$ give the same lower bound.

Suppose $a_{i} \geq 0$ , $a_{0} > 0$ , $k_{i} \in N$ , $r = ∣ z ∣ > 1$ , and $a_{0} + \sum_{i} a_{i} z^{- k_{i}} = 0$ . For $θ = ar g z > 0$ , take $λ = lo g r / θ$ . Multiplication by $1 + iλ$ and real parts give

$0 = a_{0} + i \sum a_{i} F_{λ} (k_{i} θ) \geq a_{0} - e^{- λπ} i \sum a_{i} .$

Thus $e^{λπ} \leq (\sum_{i} a_{i}) / a_{0}$ and $r \leq ((\sum_{i} a_{i}) / a_{0})^{θ / π}$ . Nonnegativity excludes argument zero; conjugation handles negative argument. This is the public normalized_escape_bound over an arbitrary finite index type, with no fixed cardinality or exponent bound.

For a graph, let $d$ be its maximum degree, $m$ the number of vertices of degree $d$ , and $S$ the remaining vertices. Dividing $D (G; z) = 0$ by $z^{d}$ gives $m + \sum_{v \in S} z^{- (d - d e g v)} = 0$ . Here $m \geq 1$ and $m + ∣ S ∣ = n$ , so $∣ S ∣/ m \leq n - 1$ . The general estimate proves the exterior-root case. For $n \geq 2$ , the right-hand side of the conjectured bound is at least one; this handles $∣ z ∣ \leq 1$ . For $n = 1$ , the polynomial is one and has no roots.

Falsifier

A mismatch in the vertex sum, positive-order restriction, argument branch, real-power convention, or universal quantifiers invalidates source fidelity. A graph, nonzero root, and strict violation would refute the encoded conjecture. Numerical checks provide finite evidence only.

Evidence

The kernel-checked settling theorem is D5.S3.Zeros.DegreeRoots.Result.result. The supporting general estimate is D5.S3.Zeros.DegreeRoots.EscapeWitness.normalized_escape_bound. The axiom closure of every public declaration is contained in {propext, Classical.choice, Quot.sound}.

Experiment

The program is in the experiments repository at fa30318aef455ef7e0ce6e6dc2fd3ff06391a669, file check.py. The pinned blob exists (git cat-file -e, exit 0). Its SHA-256 is 8758cc1cdc8b1fd6cd469277528e9390a64a25b6485a696145a0a31380d19f1e. The command python3 /Users/auric/.sshx/3725ce750c618c117ba5ef82/attempt-1/experiment-check.py executes that blob extracted without changes, with exit 0. It tests all labelled simple graphs on 2–6 vertices and 20,000 seeded random graphs on 7 vertices, counting 142,065 nonzero numerical roots. The largest bound ratio is 1.000000000000; the largest real-root ratio against $n - 1$ is 1.000000000000. For stars of orders 3–11 the displayed candidate roots have residual at most $6.47 \times 1 0^{- 15}$ and ratio 1.000000000000. These are floating-point results with the script’s $1 0^{- 9}$ acceptance tolerance, not exact certificates or exhaustive results for order seven or larger.

Triage

What the settlement shows

Item	Status and evidence kind	Result and boundary
Conjecture 4.1	Proved; kernel-checked `Result.result`	All positive orders, simple graphs, and nonzero degree roots
Decisive rotated-real-part mechanism	Proved; kernel-checked `EscapeWitness.normalized_escape_bound`, using its private `damped_trig_bound`	The uniform damped-trigonometric lower bound yields the argument-dependent estimate
Nominated Lemma 2 in normalized finite-sum form	Proved; kernel-checked `EscapeWitness.normalized_escape_bound`	Arbitrary finite nonnegative real weights and natural exponents, positive constant, root norm greater than one
Nonnegative-coefficient polynomial form of Lemma 2	Proved in prose below	No new public polynomial wrapper theorem
Loopless multigraph extension	Proved in prose below	A mathematical consequence for finite degree sequences; no multigraph Lean theorem
Star equality	Proved in prose below; not formalized as an equality theorem	All star orders at least three
Uniqueness of extremal graphs	Open	No classification of equality cases
Source’s real and imaginary bounds	Proved in prose below as consequences	No additional public corollary theorem
Canonical Scribe, registration and admission follow-up	Open for the four-slot audit; canonical source, Scribe and freeze delivered	One Proved resolution claim on `Result.result`; remaining audit obligations are in #20929
Four-slot escape registration	Open; missing registration evidence	Both public theorem targets remain in #20929; no Reg mirror or validated registration is asserted
Graph and star numerical checks	Computed; the experiment above, exit 0 and recorded script SHA-256	Exactly its finite sample and numerical tolerances
Literature screen	Open; literature reading recorded in #19987	No settlement located in the checked sources; completeness `ASSUMED-UNVERIFIED`

Polynomial consequence (proved in prose). Write $P (X) = \sum_{j = 0}^{d} a_{j} X^{j}$ with $a_{j} \geq 0$ , $a_{d} > 0$ , and $A = \sum_{j < d} a_{j}$ . If $P (z) = 0$ and $∣ z ∣ > 1$ , then $z \neq = 0$ and $a_{d} + \sum_{j < d} a_{j} z^{- (d - j)} = 0$ after division by $z^{d}$ . The general finite-sum estimate gives $∣ z ∣ \leq (A / a_{d})^{∣ a r g z ∣/ π}$ . For the remaining nonzero roots $∣ z ∣ \leq 1$ , this implies the uniform form $∣ z ∣ \leq max (1, (A / a_{d})^{∣ a r g z ∣/ π})$ by the unit-disk branch. A constant positive polynomial has no roots, so the empty lower-degree sum creates no exception.

Multigraph consequence (proved in prose). For a nonempty finite loopless multigraph, choose the largest vertex degree $d$ , let $m \geq 1$ count its occurrences, and let $S$ contain the other vertices. Degrees remain natural numbers even when edges have multiplicity. The same normalized equation and $∣ S ∣/ m \leq n - 1$ hold because each vertex contributes one monomial. Neither adjacency simplicity nor an upper bound on $d$ is used in this argument. Order one has constant degree polynomial one. This establishes the stated multigraph bound mathematically; the delivered Lean result retains the preregistered simple-graph domain.

Stars (proved in prose). For $n \geq 3$ , $D (K_{1, n - 1}; X) = X^{n - 1} + (n - 1) X$ . Put $r = (n - 1)^{1/ (n - 2)}$ and $z = r exp (iπ / (n - 2))$ . Then $z^{n - 2} = - (n - 1)$ , hence $D (K_{1, n - 1}; z) = 0$ and $z \neq = 0$ . Its principal argument is $π / (n - 2)$ and $(n - 1)^{∣ a r g z ∣/ π} = r = ∣ z ∣$ . The numerical experiment checks orders 3–11 separately. This derivation neither classifies other extremizers nor adds a kernel-checked equality theorem.

Source consequences (proved in prose). A nonzero negative real root has $∣ ar g z ∣ = π$ ; substituting gives $∣ z ∣ \leq n - 1$ . A positive real number cannot be a root of the nonzero nonnegative coefficient sum. A nonzero purely imaginary root has $∣ ar g z ∣ = π /2$ , yielding $∣ z ∣ \leq n - 1$ . These recover the source’s two directional bounds. The settlement does not supply an equality classification or strengthen unrelated source statements.

ASSUMED-UNVERIFIED

Literature completeness and absence of every possible dominating external theorem are unverified. The numerical experiment has floating-point accuracy and its stated finite scope. Uniqueness of extremizers and both four-slot registrations are open. The prose polynomial, multigraph and star consequences are distinguished from the delivered kernel statements.

Keyboard shortcuts

trureturing — Discovering truth