A condition consists of a finite sequence and an infinite reservoir of allowed future values. A stronger condition extends the sequence, shrinks the reservoir, and takes all newly appended values from the old reservoir. Stem values may repeat. The union of the generic stems is an unbounded real over a model: for every ground-model function and every threshold , the conditions whose stem already has some with form a dense subset of a forcing order. An infinite subset of always supplies a sufficiently large value.
Let be the finite stem of a condition , and define
The stems of two conditions in the generic filter agree on their common domain, because they have a common stronger extension. Hence this union is a function. For every , the set of conditions with is dense: append values from the nonempty infinite reservoir until the desired length is reached. Genericity therefore makes total on . The generic stems, and thus their union, are available in .
Fix and . In form the set
We show that it is a dense subset of a forcing order. Given , put . Fill the new positions with any fixed element of , and choose with for the new position . This is possible because an infinite subset of is unbounded. Let be the resulting stem of length , and keep the reservoir unchanged. Then
Every new stem value came from the old reservoir, exactly as required by the extension relation. The construction is performed in , so and is internally dense.
Genericity gives a condition in . Its witnessing coordinate remains fixed in every later stem and hence in , so some satisfies . Since this holds for every , there are infinitely many such . As was arbitrary,
Thus this infinite-reservoir stem forcing produces an unbounded real over a model, which is precisely the stipulated meaning of bounding .