Prime Witnesses and Eventual Alternating–Symmetric Galois Groups in a Jacobi Family

For a fixed nonintegral rational number a/b in lowest terms, with b >= 2, we determine the Galois group of J_n(x,a/b) = sum_{j=0}^n binom(a/b+j, j) x^j for all sufficiently large n, with an effective bound. The group contains A_n and equals S_n for odd n. For even n, it equals A_n precisely when (-1)^(n/2)(a+b)(a+b(n+1)) is a nonnegative integer square. The alternating degrees lie in a quadratic sequence, and the symmetric degrees have density one. For the central-binomial partial sums f_n(x) = sum_{j=0}^n binom(2j, j) x^j, we prove Sun's conjecture that f_n is irreducible over Q for every n >= 1; for all sufficiently large n, the Galois group is A_n exactly when n = 2r(r+1) with r >= 1, and is S_n otherwise. This establishes, in large degree, the experimental pattern of Katz and Rivin for this family and a conjecture of Sun on the reductions of f_n modulo primes. We also prove effective eventual irreducibility, show that the group is S_n in every sufficiently large prime degree, and give, for every denominator, infinite rays of parameters along which irreducibility holds in every degree. The proof combines prime witnesses, Newton polygons, tame inertia, primitivity, and Müller's classification of primitive groups containing an element with two cycles. Files: main.pdf (27 pages) and supplementary.zip, which contains anc/lean (a complete Lean 4 formalization, built on Mathlib, of the irreducibility of f_n for every n >= 1) and anc/checks (scripts for the finite computations). Version 2 rewrites the exposition of version 1 (61 pages). The results, arguments and explicit constants are unchanged, apart from a new remark (Remark 9.6) on Sun's conjecture in OEIS A224416. The use of AI tools is described in the AI provenance statement at the end of the paper.