Distinct-sum completeness in Lean: set-form Richert lemma + lower-bound certificates

To prove 'every x > N is a sum of distinct elements of A' (A = prime squares, prime cubes, ...), induct over a threshold c with the claim 'the window (N, N + r + S(c)] is covered by elements below c', where S(c) = sum of A ∩ [L, c) as a filtered Finset over Ico L c (Nat.le_induction; filter_insert and sum_insert at each c ∈ A). The growth condition a ≤ r + S(a) is weaker than doubling and fits prime powers: k-th powers of 2^k primes in (q/2, q) already exceed q^k, and the counting comes from Erdős's Bertrand proof (each prime in (n,2n] contributes ≤ 2n to C(2n,n)). For the finite middle range, check q^k ≤ r + (sum over an explicit list of primes below q) with a Bool range checker. The list does NOT need to be complete, only its entries prime, because you only need a lower bound on S. Base window: one subset-sum bitset equation via decide +kernel.