The first primes with explicit constructive bounds

G021: every supplied natural bound has an actual larger prime; no nonempty list or prime-search witness is supplied.

Finite decidable scanning either finds the actual least prime above a or proves every such prime exceeds the scanned interval.

Euclid unboundedness terminates the finite least-prime scan without any unbounded-search axiom.

The least prime above any natural is uniquely determined by its minimality, not by its code.

Bertrand's theorem bounds the actual consecutive prime, rather than only producing a sparse prime subsequence.

Least-prime search is a total, uniquely valued constructive relation for every natural input.

The one-entry initial prime chain is an actual beta code of the prime two.

Appending the actual next prime preserves every old decoded entry and every minimal-successor edge.

Every initial segment retains the same genuine least-prime transitions.

Every decoded terminal entry of an initial-prime chain is genuinely prime, including the first entry two.

Construct the first k+1 primes with their actual terminal value strictly below the witnessed power 2^(k+2).

For every positive k, construct exactly the first k primes and both power witnesses proving p_k < 2^(2^k).

Every earlier decoded prime is strictly smaller than the terminal prime; repetitions and descending lists are excluded.

Every prime no larger than a decoded terminal prime occurs in the actual prefix; no smaller prime is omitted.

Every positive-length first-prime list exposes its actual final index and minimal-successor chain.

Every entry of every first-prime list is prime, with the empty-list boundary proved vacuously.

The first-prime list is exhaustive below each of its entries, with an explicit bounded index witnessing every smaller prime.

Every first-prime list is strictly increasing at all valid index pairs, not merely at its last transition.

Every finite number of initial primes has a real beta-coded list, including the empty list at zero.