Fine-measure coordinates avoiding small supports

Put $\theta =\kappa +\lambda$ and let $\rho$ be its Hartogs number. Then $\rho >\theta$: otherwise inclusion would inject $\rho$ into $\theta$. Also $\rho$ is an initial ordinal. A bijection from $\rho$ to some $\eta <\rho$, followed by an injection of $\eta$ into $\theta$ supplied by minimality of $\rho$, would contradict its defining property. Thus $\rho$ is a cardinal above $\kappa$. Set $I=P_{\kappa }(\rho )$ and take a fine $\kappa$-complete ultrafilter $U$ by F1. It is nonprincipal: for each $x\in I$ there is $\xi \in \rho \setminus x$, since $\mathrm{\mid }x\mathrm{\mid }<\kappa \le \rho$; its point cone is in $U$ and omits $x$, so $\{x\}\mathrm{\notin }U$.

For $\alpha <\lambda$ put $t_{\alpha }=\kappa +\alpha$ and define $f_{\alpha }(x)=\mathrm{otp}(x\cap t_{\alpha })$, using the inherited ordinal order. F4 gives $\kappa \le t_{\alpha }<\theta <\rho$ and $t_{\alpha }<t_{\beta }$ for $\alpha <\beta$. F6 makes each value unique; Separation and Replacement give all functions and their indexed family. Every value is below $\kappa$: the order isomorphism gives it the cardinality of $x\cap t_{\alpha }$, which is below $\kappa$; an ordinal at least the initial ordinal $\kappa$ cannot have that cardinality. For the empty index $x=\mathrm{\varnothing }$ every value is zero.

If $\alpha <\beta <\lambda$ and $t_{\alpha }\in x$, then $x\cap t_{\alpha }$ is exactly the proper initial segment below the element $t_{\alpha }$ of the well-order $x\cap t_{\beta }$. Under the order isomorphism of F6 its order type is therefore an ordinal strictly below the order type of $x\cap t_{\beta }$. The point cone at $t_{\alpha }$ belongs to $U$ by fineness, so upward closure gives $\{x:f_{\alpha }(x)<f_{\beta }(x)\}\in U$.

Fix $\delta <\kappa$. Intersect the point cones at all $\xi \le \delta$. This is a $U$-member by F3, since $\delta +1<\kappa$. For finite $\delta$ this follows from uncountability. For infinite $\delta$, the new last point can be sent to zero, each natural number shifted to its successor, and each ordinal in $[\omega ,\delta )$ fixed; this injects $\delta +1$ into $\delta$, so $\delta +1$ cannot reach the initial ordinal $\kappa$. At an index in this intersection, $\delta +1\subseteq x\cap t_{\alpha }$, because $t_{\alpha }\ge \kappa$. In fact $\delta +1$ is an initial segment there. Restricting the order isomorphism of F6 shows $f_{\alpha }(x)\ge \delta +1>\delta$. Upward closure proves the second displayed assertion, including $\delta =0$ and $\alpha =0$.

For fixed $\alpha <\lambda$, intersect $\{x:f_{\alpha }(x)>\delta \}$ over $\delta \in S$. The inherited ordinal order on $S\subseteq \kappa$ has order type below $\kappa$, by the same initial-cardinal argument as in step 2.1, so F3 applies without choosing an enumeration. The intersection lies in $U$ and is contained in $\{x:f_{\alpha }(x)\mathrm{\notin }S\}$. For finite $F$, intersect these avoidance sets and the finitely many comparison sets from step 3.1 for ordered pairs $\alpha <\beta$ in $F$. This $U$-member is contained in $H(F,S)$, proving the conclusion by upward closure. If $F$ is empty then $H(F,S)=I$; if $S$ is empty its avoidance intersections are $I$; a singleton $F$ requires no pair comparisons. Neither this construction nor its proof uses normality or any restriction on $\mathrm{cf}(\lambda )$.