What does this research mean for the field?

The dominant coefficient of a polynomial continued fraction is strictly positive for all-positive polynomial families, but can vanish for polynomials with sign-varying transients, disproving the universal claim that it is non-zero for all polynomials with a positive leading coefficient. Novelty: ClaimNovelty.CONTRADICTORY. Consensus alignment: ConsensusAlignment.CHALLENGES_CONSENSUS.

June 8, 2026Open Access

When does the dominant coefficient of a polynomial continued fraction vanish? A monotone positivity criterion (machine-checked core), an unconditional bound for a positive family, and an explicit vanishing witness

Key Points

The aim is to explore conditions under which the dominant coefficient of a polynomial continued fraction vanishes, particularly focusing on positivity criteria and bounds.
Analyzed polynomial behavior using continued fractions with given definitions and limits.
Applied a positivity-persistence lemma with verification through Lean 4 for machine-checked proofs.
Utilized explicit examples to demonstrate the failure of universal claims regarding the coefficient.
The positivity criteria established that if certain conditions are met, the dominant coefficient is non-zero (C>0).
An explicit polynomial example was provided showing that the dominant coefficient can indeed vanish (C=0).
Verification processes confirmed the findings, while disproving the universal claim that C is always non-zero.

Abstract

For a real polynomial b of degree d with leading coefficient βd>0, let qₙ be the continuant denominators with q₀=1, q₁=b (1), qₙ=b (n) qₙ-1+qₙ-2. With Pₙ=∏ₖ≤nb (k) and Qₙ=qₙ/Pₙ, the scaled limit C=R_∞=lim Qₙ is the dominant (connection) coefficient of the seed (1, b (1) ) ; C≠0 iff q is not minimal. Results. (1) A ratio criterion: once b>0 on a tail and two consecutive q are positive, qₙ/qₙ-1>b (n) →+∞, so q is dominant and C≠0 (elementary). (2) A positivity-persistence lemma: if uₙ=1/ (b (n-1) b (n) ) >0 from some index and the scaled sequence is then positive, Qₙ is nondecreasing and C≥QN0>0; the monotone–bounded core is verified in Lean 4 (Mathlib) with a clean axiom cone (no sorryAx). Corollary: b (n) >0 for all n≥1 forces C≥1; in particular the family b (n) =An²+Bn+C₀, integers A, B, C₀≥1, has C≥1 unconditionally, recovering the strict positivity δ=log R_∞>0 of the companion quadratic growth-law deposit. (3) Sharpness (falsification-first): the universal claim "C≠0 for every βd>0" is FALSE — an explicit quadratic b (n) =n²−6. 2803109563277…n+8. 4205764270426… has C=0 to more than forty digits at 50-digit precision, with dominant scale ∏|b|>10⁴3000 at the same index (a genuine minimal seed). The vanishing is produced by the sign-varying transient (b (2), b (3) 0 does not imply C≠0. Only ≥1 zero is claimed: (α, β) ↦R_∞ has genuine poles wherever b has an integer root, so a sign-change count is not a zero count; the witness sits in a verified pole-free bracket with a single monotone crossing. Epistemic status (SIARC four-class). PROVEN — the monotone/bounded-below engine and the Casoratian identity are machine-checked in Lean 4 (cones ⊆ propext, Classical. choice, Quot. sound, no sorryAx). STRUCTURAL — the ratio criterion and the shifted (N0>1) form of the lemma are complete elementary hand proofs, not yet formalized; the all-positive C≥1 bound is the Lean engine plus a one-line reduction. VERIFIED — the vanishing witness and the no-seed-index-leak check are mpmath at 50 digits, reported above the floor. FALSE — the universal C≠0 claim, disproved by the witness. Open: whether C=0 implies the associated generating function is entire requires a separate unique-nearest-singularity analysis (stated, not claimed) ; literature locators (Perron, Pincherle, Frobenius radius bound) are flagged unverified and no result depends on them.

Read Full Paperexternally

Mark Helpful

Bookmark

Relay

View Full Paper