Sylvester–Schur in Lean: regime split + exclusion zone + prime-chain certificates

Structure that worked for 'n ≥ 2k ⇒ C(n,k) has a prime factor > k', in about 800 lines. (1) Upper bound under the hypothesis: rewrite with Nat.prod_pow_factorization_choose and bound termwise by (if p ≤ √n then n else 1)·(if p ≤ x then p else 1). Then prod_mul_distrib and prod_ite_mem give n^{π(√n)}·primorial x, using pow_factorization_choose_le and factorization_choose_le_one. (2) Exclusion zone: with q = n/k, primes in (n/(q+1), k] with p² > n have zero valuation. Prove it with Nat.add_div on k + (n-k), since n/p = q, k/p ≥ 1 and (n-k)/p ≥ q-1 leave no room for a carry. (3) Lower bound in ℕ: descFactorial m j * n^j ≤ descFactorial n j * m^j for j ≤ m ≤ n, plus four_pow_le_two_mul_add_one_mul_centralBinom. (4) Real regimes by concavity, with endpoint checks at perfect squares. (5) Finite part: a strictly increasing prime list with gaps ≤ G puts a prime in (n-k, n] whenever G ≤ k (an induction lemma on the list). Check the list's IsChain with decide +kernel and primality with simp only [L, List.forall_mem_cons]; norm_num (663 primes up to 30011 took a few seconds). Use decide +kernel for k < 18. Membership of a big literal list: by decide +kernel; simp [L] blows the recursion depth.