The recurrence coefficients of the oscillatory Gegenbauer weight (1-x²)^(λ-1/2)e^(iζ x): the closed-form conjecture of Lyu and Zhou certified for βₙ to n=13 and αₙ to n=12, and the degree conjecture of Milovanović, Cvetković and Marjanović for n ≤ 16

Compute-first gate: an independent implementation of arXiv:2607.19797v1 (2.9)-(2.10) with its initial values (2.11), run in exact rational-function arithmetic over Q(lambda,zeta), reproduces its Table 1 (alpha₀..alpha₈, beta₁..beta₉) and every polynomial of its Appendix 'symbols'(1) – X₂, X₃, X₄, X₅, X₆, X₈, X₉ with their printed normalisations 2X₃, 4X₄, 8X₅, 8X₆, 16X₈, 16X₉ – and MCM 2008's Table 1 (alpha₀, alpha₁, alpha₂, beta₁, beta₂).

Normal form of the conjecture, and the bilinear system it satisfies. With dₙ = floor(n²/4), Eₙ = X_(dₙ), Fₙ = X_(dₙ-1), cₙ = 1 (n odd) / -n(2*lambda+n-1) (n even), eₙ = (n/2)(2*lambda+n-1) (n even) / ((n-1)/4)(2*lambda+n) (n odd), the four displayed formulas of the conjecture collapse to betaₙ = cₙ Eₙ₋₁Eₙ₊₁/(zeta² Eₙ²) and alphaₙ = 2(lambda+n)/zeta + zeta(Rₙ - Rₙ₊₁) with Rₙ = eₙ Fₙ/Eₙ; substituting these into the source's own compatibility conditions (S₁) and (S₂') gives two polynomial identities in the Xⱼ alone (BilA, BilB), with no alpha, no beta and no divisions.

The conjecture of arXiv:2607.19797v1 machine-checked over Z[lambda][zeta²] on the range the source itself iterated: BilB for 1 <= n <= 9 and BilA for 1 <= n <= 9, hence alphaₙ and betaₙ in the conjectured closed form for n <= 9.

The conjecture of arXiv:2607.19797v1 machine-checked past the source's range, and composed into one theorem (Final.closed_form): the cleared (S₂') is certified for 1 <= n <= 15 and the cleared (S₁) for 1 <= n <= 12, whence – through the data-free Algebra.lean and Unique.lean – every solution of the source's Theorem 2.1 (its (2.9), (2.10) for 1 <= n <= 11 and its four initial values (2.11)) has alphaₙ for n <= 12 and betaₙ for 1 <= n <= 13 equal to the conjectured closed forms built from the certified monic tables, with lambda symbolic. beta₀ is not claimed: the source leaves it arbitrary.

MCM 2008's degree conjecture, machine-checked: for every 0 <= n <= 16 the certified table X_(floor(n²/4)) is monic of degree exactly floor(n²/4) in zeta² and X_(floor(n²/4)-1) is monic of degree exactly floor(n²/4)-1, so the Hankel determinant Hₙ = det(Pˡambdaᵢ₊ⱼ) has degree floor(n²/4) in zeta² for n <= 16.

THEOREM (verified, not formalized): the two leading-coefficient conjectures of arXiv:2607.19797v1 (its S_(k²) and S_(k(k+1)) products) are one formula, Hₙ = (-1)^(n(n-1)/2) gammaₙ X_(floor(n²/4)) with gammaₙ = prodₘ₌₁ⁿ⁻¹ cₘⁿ⁻ᵐ; verified directly for 1 <= n <= 12 at lambda = 1/3, 7/2, 5 by building MCM's Pˡambdaₖ from its own four-term recurrence, forming Hₙ = det(Pˡambdaᵢ₊ⱼ), and comparing with the X computed from arXiv:2607.19797v1 (2.9)-(2.10).

MCM 2008 p. 53 prints alpha₂ₖ = V_(k(2k+1))(zeta²)/(zeta S_(k²)(zeta²) S_(k(k+1))(zeta²)²); the exponent 2 is wrong and the denominator is zeta S_(k²) S_(k(k+1)). Settled at k = 1 from MCM's own data: V₃ * A2den = zeta * S₁ * S₂ * A2num holds identically, while the squared version fails already at (lambda, zeta) = (1, 3), the discrepancy being exactly the extra factor S₂.

Controls: every certified table is nonzero; moving one coefficient of X_(d₆) by a single unit destroys the certified (S₂') at n = 5; the n = 5 left side does not match the n = 4 right side; shifting the whole (S₁) certificate at n = 5 by one unit destroys it; the length of the table for X_(d₆) is exactly d₆ + 1 and neither d₆ nor d₆ + 2.

Data-free layer: (S₁) at n and at n+1 give arXiv:2607.19797v1 (2.10); (S₁) at n and (S₂') at n+1 give its (2.9); and two solutions of a system of that shape sharing alpha₀, alpha₁, beta₁, beta₂ agree on alpha up to index N+1 and on beta from index 1 to N+2 – beta₀ is not claimed equal, matching the source's 'Note that beta₀ can be arbitrary.'