Sacks forcing does not always produce a minimal upper bound

Theorem. There is a countable admissible set, $\text{Ol}$, with ordinal ω^CK₁ such that if S is Sacks generic over $\text{Ol}$ then ω₁^S > ω^CK₁ and S is a nonminimal upper bound for the hyperdegrees in $\text{Ol}$. (The same holds over $\text{Ol}$ for any upper bound produced by any forcing which can be construed so that the forcing relation for Σ₁ formulas is Σ₁.) A notion of forcing, the “delayed collapse” of ω^CK₁, is defined. The construction hinges upon the symmetries inherent in how this forcing interacts with Σ₁ formulas. It also uses Steel trees to make a certain part of the generic object Σ₁ over the final inner model, $\text{Ol}$, and, indeed, over many generic extensions of $\text{Ol}$.