# Full-support geometric prior: exact result and limitation

Enumerate the unresolved primes as `p_1, p_2, ...` and assign the full-support prior

`nu(p_k) = 2^{-k}`.

After exact verification of the first `N` primes, any remaining counterexample belongs to the tail. Therefore

`nu(Z) <= sum_{k>N} 2^{-k} = 2^{-N}`.

This is an exact and useful anytime upper bound on failure mass. It does not become zero for any finite `N`.

Taking `N -> infinity` gives zero only if one has established that every finite prefix verifies. A finite program run establishes this for one concrete `N`; proving it for arbitrary `N` is equivalent to proving that the verifier succeeds on every unresolved prime. Thus the limiting argument cannot supply its own universal premise.

Likewise, sampling from `nu` forever visits every individual prime almost surely, but a process that has not encountered a counterexample is not a finite proof that none exists. A counterexample would manifest as a search that never returns a witness, and nontermination is not a checkable refutation certificate.

## Valid use inside SWC

The geometric prior can support:

- an exact decreasing bound on unresolved prior mass;
- prioritized proof search;
- an anytime-valid empirical status report;
- a universal theorem after a separate symbolic tail, complete cover, mass-gap, or induction lemma is proved.

It cannot convert finite verification into a standard finite proof of an infinite universal statement by itself.
