Normalizing a scale at existing least upper bounds

Fix the choice function of A1. For every $u\in P$ there is an index $\xi <\lambda$ with $u{<}^{\ast }{g}_{\xi }$: by F1 first weakly dominate $u$ by a scale term and then use its successor term, which exists below infinite $\lambda$. Choose the least such index when needed. Given fewer than $\lambda$ product functions and a stage $\alpha <\lambda$, the least dominating indices have supremum below $\lambda$ by F3–F4. Thus there is $\beta >\alpha$ below $\lambda$ whose scale term strictly dominates every function in that family, by taking $\beta$ above those indices as well. For the empty family the least eligible index is simply the least $\beta >\alpha$.

Define $f$ by the following rule at each $\alpha <\lambda$. The preceding values form a family of size at most $\mathrm{\mid }\alpha \mathrm{\mid }<\lambda$. If $\mathrm{cf}(\alpha )>\omega$ and that family has a least upper bound in $P$, let $f_{\alpha }$ be the fixed choice from its nonempty set of least-bound representatives. Otherwise set $f_{\alpha }=g_{\beta }$ for the least $\beta >\alpha$ strictly dominating all preceding $f$ values, which exists by step 1.1. The sets of representatives are subsets of the set $P$, and the least eligible index is uniquely specified, so F5 implements the rule. Each output belongs to $P$ by construction; in particular at $\alpha =0$ the fallback applies and gives $f_0=g_1$.

At a fallback stage, strict domination of all predecessors is part of the rule. At a least-bound stage $\alpha$, F4 implies $\alpha$ is a limit. For every $\gamma <\alpha$ we have $\gamma +1<\alpha$. Once strictness holds for earlier stages, $f_{\gamma }{<}^{\ast }{f}_{\gamma +1}{\le }^{\ast }{f}_{\alpha }$, and composing outside the union of the two finite exceptional sets gives $f_{\gamma }{<}^{\ast }{f}_{\alpha }$. This proves strictness at each stage by induction: if a first failure existed, the appropriate fallback or least-bound calculation just given would rule it out using only earlier stages. At every successor stage $\alpha =\xi +1$, the fallback applies because its cofinality is one. It gives $f_{\xi +1}=g_{\beta }$ for some $\beta >\xi +1$, so $g_{\xi }{<}^{\ast }{f}_{\xi +1}$. Given $u\in P$, choose $\xi$ with $u{\le }^{\ast }{g}_{\xi }$ by F1; then $u{<}^{\ast }{f}_{\xi +1}$. Hence $f$ is cofinal as well as strict.

Whenever the stated uncountable-cofinality initial segment has a least bound in $P$, the first branch of step 2.1 selected a representative of exactly that set of least bounds. Thus the normalization clause holds, without any assertion that the first branch always applies at such limits. Step 3.1 proves that the selected representatives still form a scale on the original $B$. Finally F2 supplies at least one such $B$ and input scale, so the unconditional existence consequence also follows. QED.