Existence of a Laver function at a supercompact

By F2 choose an embedding with critical point $\kappa$. F3 makes $\kappa$ measurable, and F4 makes it inaccessible. In particular $\kappa$ is regular uncountable. F5 gives $\mathrm{\mid }{V}_{\alpha }\mathrm{\mid }<\kappa$ for $\alpha <\kappa$, hence $\mathrm{\mid }{V}_{\kappa }\mathrm{\mid }=\kappa$: a union of $\kappa$ sets of size at most $\kappa$ has size at most $\kappa$, using AC and the cardinal-square theorem F13, while the ordinals below $\kappa$ give the reverse bound. If a critical-$\kappa$ embedding is given, it fixes $V_{\kappa }$ pointwise. Indeed enumerate any $y\in V_{\kappa }$ by $e:\beta \to y$ with $\beta <\kappa$. Then $j(y)=j(e)\mathrm{‘}\mathrm{‘}\beta =j\mathrm{‘}\mathrm{‘}y$, and induction on membership fixes all its members. AC is used for these set enumerations and subsequent cardinal comparisons.

We establish a closure observation. Let $M$ be a transitive class model of ZFC containing all ordinals and closed under ambient $\mu$-sequences, where $\mu$ is infinite. Any ambient set of at most $\mu$ elements of $M$ belongs to $M$: enumerate it on an ordinal at most $\mu$, pad to length $\mu$, use closure, and restrict internally; the empty case is immediate. Moreover $H_{{\mu }^{+}}\subseteq M$, with F10's root-inclusive convention. For $x\in H_{{\mu }^{+}}$, choose a bijection from an ordinal $\beta \le \mu$ to $\mathrm{TC}(\{x\})$, and code membership as a relation on $\beta$. The relation is a set of at most $\mu$ ordinal pairs, hence belongs to $M$ by the preceding observation and the cardinal-square theorem F13. It is well-founded and extensional in $M$, since it is so externally and $M$ is transitive. Its internal collapse is a set and is also an external collapse. F9's uniqueness identifies its distinguished root with $x$. The same argument gives agreement of cardinal comparisons at or below $\mu$ and of hereditary-size classes $H_{{\eta }^{+}}$ for $\eta \le \mu$: all relevant injections, bijections and their graphs belong to $M$.

Here is the exact factor comparison. Suppose $j:V\to M$ is $\theta$-closed, with $\theta \ge \kappa$ infinite cardinal and $j(\kappa )>\theta$. Put $I=P_{\kappa }(\theta )$, $s=j\mathrm{‘}\mathrm{‘}\theta$, and derive $U=\{A\subseteq I:s\in j(A)\}$ by F2. Let $j_0:V\to M_0$ be its collapsed normal fine ultrapower, supplied by F2 and F8. For a set function $f:I\to V$ define $k({\pi }_U([f{]}_U))=j(f)(s)\mathrm{.}$ Equality is preserved and reflected: its coordinate equality set belongs to $U$ precisely when its $j$-image contains $s$, precisely when the two evaluations agree. The same calculation for each fixed formula, using F7 and elementarity of $j$, proves that $k$ is a well-defined elementary injection. Constant functions show $k\circ j_0=j$. All maps are definable with the stated set parameters; restrictions are sets by Replacement. F6 identifies the seed $s_0=j_0\mathrm{‘}\mathrm{‘}\theta$ with the collapsed identity class, so $k(s_0)=s$.

Use AC to fix a set well-order $W$ of $V_{\kappa }$. Define $\mathrm{\ell }:\kappa \to V_{\kappa }$ by the following bounded recursion. At regular uncountable $\gamma <\kappa$, consider cardinals $\gamma \le \eta <\kappa$ and $x\in V_{\kappa }\cap H_{{\eta }^{+}}$ for which no normal fine $\gamma$-complete measure on $P_{\gamma }(\eta )$ has $j_U(\mathrm{\ell }\upharpoonright \gamma )(\gamma )=x$. If there are such pairs, take the least $\eta$ and the $W$-least corresponding $x$ as $\mathrm{\ell }(\gamma )$; otherwise put $\mathrm{\ell }(\gamma )=\mathrm{\varnothing }$. At other $\gamma$ also put empty. This is a uniquely specified set-valued rule on all histories, with an empty fallback for malformed histories. F11 supplies the function. Ultrapower evaluation is a definable set-collapse predicate by F8, so the rule is first-order in set parameters. It does not quantify over arbitrary elementary class embeddings. The explicit cutoff $\eta <\kappa$ and range $V_{\kappa }$ avoid assuming any reflection bound on unbounded failures at smaller stages.

For every $\alpha \le \theta$, the set $s_0\cap j_0(\alpha )=j_0\mathrm{‘}\mathrm{‘}\alpha$ has ordinal order type $\alpha$. Apply $k$ to the definable order-type operation: $k(\alpha )=\mathrm{otp}(s\cap j(\alpha ))=\alpha$. In particular $k$ fixes $\kappa$, including when $\theta =\kappa$. F2 says $M_0$ is $\theta$-closed, so step 1.2 puts $H_{{\theta }^{+}}$ inside $M_0$. Given $y$ in that hereditary class, an enumeration $e:\beta \to y$ with $\beta \le \theta$ belongs to $M_0$ by closure. Since $k$ fixes the indexing ordinal pointwise, $k(y)=k(e)\mathrm{‘}\mathrm{‘}\beta =k\mathrm{‘}\mathrm{‘}y$. Membership induction on $\mathrm{TC}(\{y\})$ now gives $k(y)=y$. Thus the factor fixes every anticipated object of hereditary size at most $\theta$, not just small ordinals.

Fix any $\mathrm{\ell }:\kappa \to V_{\kappa }$ and cardinal $\theta \ge \kappa$, and choose an infinite cardinal $\mu \ge \mathrm{\mid }\mathcal{P}(P_{\kappa }(\theta ))\mathrm{\mid }$. Let $j:V\to M$ be $\mu$-closed with $j(\kappa )>\mu$. For each cardinal $\kappa \le \eta \le \theta$, $M$ and $V$ have exactly the same normal fine $\kappa$-complete measures on $I=P_{\kappa }(\eta )$. Indeed step 1.2 puts every small ordinal subset and hence every element of $I$ in $M$, then puts $I$, all its subsets and all subsets of its power set in $M$. This last assertion uses $\mathrm{\mid }\mathcal{P}(I)\mathrm{\mid }\le \mu$. The sequences of length below $\kappa$ and selector functions used to test completeness and normality also belong to $M$, so those tests agree in both directions. The index and its cardinal comparisons are the same by step 1.2. The same step gives agreement on $H_{{\eta }^{+}}$.

The internal and external evaluations $j_U(\mathrm{\ell })(\kappa )$ agree for each measure in step 2.2. Here are details that avoid identifying internal Scott rank codes with external ones. In a normal fine ultrapower, the function $x\mapsto \mathrm{otp}(x\cap \kappa )$ represents $\kappa$: the normal seed intersected with $j_U(\kappa )$ is $j_U\mathrm{‘}\mathrm{‘}\kappa =\kappa$, and its order type is $\kappa$. Its coordinate values are below $\kappa$. Thus the desired value is the collapse of the class of $r(x)=\mathrm{\ell }(\mathrm{otp}(x\cap \kappa ))$. Put $T=\mathrm{TC}(\{\mathrm{\ell }\})\cup \kappa \cup \{\mathrm{\varnothing }\}$. This is transitive, contains all values of $r$, and has size at most $\kappa$ by step 1.1 and the union bound there. Every function $I\to T$ belongs to $M$ by closure. Their entire collection belongs to $M$ too: writing $\nu =\mathrm{\mid }I\mathrm{\mid }\ge \kappa$, its size is at most ${\kappa }^{\nu }\le (2^{\nu }{)}^{\nu }=2^{\nu }\le \mu$. Form the ordinary set quotient of these functions by coordinate $U$-equivalence. It and its coordinate membership relation are identical internally and externally. The relation is well-founded because a descending sequence would, by countable completeness, yield a descending membership sequence at one coordinate; AC supplies sequence representatives. It is extensional: for unequal function classes, on a large set their values differ, and choosing a member of their symmetric difference gives a distinguishing predecessor; transitivity of $T$ keeps that predecessor in this same quotient. Patching by empty gives every predecessor of every class from a function into $T$. F9's unique set collapse therefore agrees in both models and with the corresponding transitive part of the universe collapse. In particular the two evaluations of $[r]$ agree. This is an assertion about the collapse value, not equality of the two Scott representative codes.

Suppose this $\mathrm{\ell }$ fails F1's requirement. A target set and requested cardinal witnessing failure give a cardinal $\theta \ge \kappa$ dominating both that cardinal and the hereditary size of that set. Any normal fine $\theta$-measure anticipating the set would give an embedding meeting the original request by F2, so there is a failure for some such $\theta$. Choose the least cardinal $\theta \ge \kappa$ for which some $x\in H_{{\theta }^{+}}$ is not anticipated by any normal fine measure on $P_{\kappa }(\theta )$. Choose $\mu$ as in step 2.2 and a $\mu$-supercompact embedding $j:V\to M$ by F2. Step 1.1 gives $j(\mathrm{\ell })\upharpoonright \kappa =\mathrm{\ell }$. Steps 2.2 and 3.1 show that $M$ computes exactly the same least failure $\theta$, including all candidate objects and every smaller cardinal. This is the required anticipation absoluteness, with a bound large enough to contain the measures themselves.

Internally $j(\kappa )$ is inaccessible and $\theta <j(\kappa )$. Every candidate $x\in H_{{\theta }^{+}}^M$ belongs to $V_{j(\kappa )}^M$: its transitive closure has internal size at most $\theta$, and well-founded induction on that closure, using regularity of $j(\kappa )$, bounds the rank of each member below $j(\kappa )$. Consequently the transformed recursion at stage $\kappa$ excludes none of these failure witnesses by its range restriction or cutoff. It selects a failing object $a\in H_{{\theta }^{+}}$ and gives $j(\mathrm{\ell })(\kappa )=a$. The order $j(W)$ need not select any externally preselected witness; the argument only requires that its selected $a$ is a failure, which steps 2.2 and 3.1 make true externally too.

Apply steps 1.3 and 2.1 to this $j$ at $\theta$, deriving a normal fine $\theta$-measure and its factor $j_0$, with $k\circ j_0=j$. The factor fixes $\kappa$ and $a$. Hence $k(j_0(\mathrm{\ell })(\kappa ))=j(\mathrm{\ell })(\kappa )=a=k(a)\mathrm{.}$ Injectivity gives $j_0(\mathrm{\ell })(\kappa )=a$, contradicting the failure asserted in step 5.1. Thus no least failure exists. For arbitrary requested $\lambda \ge \kappa$ and arbitrary set $x$, choose $\theta \ge \lambda$ dominating its hereditary size. The resulting normal fine ultrapower anticipates $x$, moves $\kappa$ above $\theta$, and is $\theta$-closed, hence also $\lambda$-closed by padding sequences. This is precisely F1, including $x=\mathrm{\varnothing }$ and $\lambda =\kappa$. All choice uses are set choices; no Global Choice or inaccessible existence beyond the given supercompact was assumed.