KimStantonSingleDenominator
Abstract
Integer polynomial denominators of contiguous basic hypergeometric coefficients.
Definition 1.1 (gamma).
Formalization. D5/S3/Combinatorics/MotzkinHankel/KimStantonSingleDenominator.gamma (✓ std3).
Citation. Jang Soo Kim and Dennis Stanton (2021). Three families of q-Lommel polynomials. DOI: 10.48550/arXiv.2105.10096. URL: https://arxiv.org/abs/2105.10096v3.
Commentary.
Printed pages 22–23 of arXiv:2105.10096v3: Let ∑ₙ≥₀ γ′ₙ(a,b,c) zⁿ = ₂φ₁(aq,b;cq;q,z)/₂φ₁(a,b;c;q,z).
Definition 1.2 (claim).
Formalization. D5/S3/Combinatorics/MotzkinHankel/KimStantonSingleDenominator.claim (✓ std3).
Citation. Jang Soo Kim and Dennis Stanton (2021). Three families of q-Lommel polynomials. DOI: 10.48550/arXiv.2105.10096. URL: https://arxiv.org/abs/2105.10096v3.
Commentary.
Printed page 22–23 of arXiv:2105.10096v3, Conjecture 8.4. Let ∑ₙ≥₀ γ′ₙ(a,b,c) zⁿ = ₂φ₁(aq,b;cq;q,z)/₂φ₁(a,b;c;q,z). Then γ′ₙ(a,b,c)/(1−c) = P′ₙ(a,b,c)/∏ₖ₌₀ⁿ(1−cqᵏ)^⌊(n+1)/(k+1)⌋, for some polynomial P′ₙ(a,b,c) in a,b,c,q with integer coefficients. The variables a, b, c, q are the four Fin 4 polynomial variables over the integers; the coefficient index is every natural number, including zero. The series is formal over the fraction field.
Theorem 1.3 (result).
Proof. Machine-checked in Lean as D5/S3/Combinatorics/MotzkinHankel/KimStantonSingleDenominator.result (✓ std3). ∎
Resolves. Problems/ks2105-single-2phi1denom (proved) by D5/S3/Combinatorics/MotzkinHankel/KimStantonSingleDenominator.result.
Source. Repository-derived.
Acknowledgement. Jang Soo Kim and Dennis Stanton (2021). Three families of q-Lommel polynomials. DOI: 10.48550/arXiv.2105.10096. URL: https://arxiv.org/abs/2105.10096v3.
Commentary.
The recurrence puts the ratio coefficients in the localization generated by the lower-parameter factors. The pole onset bounds clear their floor exponent denominator; localization descent supplies an integer polynomial in all four variables.
References
- Truth anchor:
D5/S3/Combinatorics/MotzkinHankel/KimStantonSingleDenominator.claim - Truth anchor:
D5/S3/Combinatorics/MotzkinHankel/KimStantonSingleDenominator.gamma - Truth anchor:
D5/S3/Combinatorics/MotzkinHankel/KimStantonSingleDenominator.result - Dependency: D5/S3/Combinatorics/MotzkinHankel/KimStantonDenominatorCore