For an extender $F$ of minimal length witnessing the coherence condition of a Martin-Steel Doddage, $\kappa_F = \iota_F$ This question of mine comes from Woodin's "In Search of Ultimate-L" article on page $36$.
Let $\mathcal{E}$ be a Martin-Steel Doddage and $(\alpha, \beta)\in \mbox{dom}(\mathcal{E})$ and assume $E \in \mathcal{E}^\alpha_\beta$ and let $F$ be an extender of minimal length which witnesses the coherence conditions below:

*

*$\alpha < \rho(F)$ and $\rho(F)$ is inaccessible


*$E = F|\alpha$


*(shortness) $\alpha \le j_F(\kappa_F)$


*$j_F(\mathcal{E})|(\alpha+1, 0) = \mathcal{E}|(\alpha, \beta)$.
Also here we define: $\nu_F = \sup\{\xi+1: \xi \mbox{ is a generator}\}$, $\iota_F=\sup\{\eta: j_F(\eta) < \nu_F\}$ and also $\rho(F) = \sup\{\eta: V_\eta \subset \mbox{Ult}(V; F)\}$. So $\kappa_F \le \iota_F$ by definition. And in this case we want to show that $\kappa_F =\iota_F$. In what follows, for ease of notation I will drop the subscripts.
Now I can say that I have partially proven this, but I need help with the rest. First assume towards a contradiction that $\kappa < \iota$. We will find an extender of shorter length which also satisfies the coherence conditions. Note that the hardest condition to insure is that $\rho(F')$ is inaccessible, as the other conditions either will be immediate or will follow from the fact that we will let $F'$ be a large enough proper initial segment of $F$.
Now if $\rho(F) \le \xi$ for some generator $\xi$, then by looking at the factor map induced by the initial segment $F|\xi$ and the fact that $\rho(F)$ is inaccessible, one may see that $\rho(F|\xi) = \rho(F)$ and so we may take $F' = F|\xi$ and we have a contradiction.
Otherwise assume $\rho(F) \ge \nu$ and by our base assumption $\kappa < \iota$, we have that $$j(\kappa) < \xi < \nu \le \rho(F)$$ for some generator $\xi$ and this is the case where I'm stuck.
Now I intuitively suspect that in this case $\xi$ is probably inaccessible by looking at the factor maps and probably $\rho(F|\xi) = \xi$ which also would contradict the statement, but I can't fill in the details. Is this true? Or is there another way to reach a contradiction in this circumstance?
 A: I also don't see how to fully prove the lemma, in particular in the case that you mention, or maybe a subcase thereof. In that case I only see how to prove a weaker version, that we can replace $F$ with an extender $F'$ of the same length and satisfying the requirements, plus $\kappa_{F'}=\iota_{F'}$. (In fact, if there is an instance with $\alpha=j_F(\kappa_F)$ then as far as I can see the lemma fails, and I don't see how to rule this possibility out.) However, it seems we also need an observation to see why condition (d) of the coherence conditions is preserved, so I give a more or less complete argument below and fill this in, though it will repeat some of what you did in the original post. (When I say (a), (b), (c), (d), I am referring to the conditions in the definition of coherence, which are the statements you bullet-pointed in your question, in order.)
Let $F$ be an extender of minimum length witnessing the condition. Suppose that $\alpha<j_F(\kappa_F)$. Suppose $\kappa_F<\iota_F$. In particular then, $\kappa_F<\mathrm{lh}(F)$. Let $F'$ be the (short) restriction of $F$ to length $j_F(\kappa_F)$. Then $F'$ also satisfies the conditions, contradicting the minimality. For $j_{F'}(\kappa_{F'})=j_F(\kappa_F)$ and $E$ is short, so (b) and (c) are clear. For (a), if $\rho(F)\leq j_F(\kappa_F)$ then $\rho(F')=\rho(F)$, which easily suffices. So suppose $j_F(\kappa_F)<\rho(F)$. Then $V_{j_F(\kappa_F)+1}\subseteq\mathrm{Ult}(V,F)$ and $V_{j_F(\kappa_F)}\subseteq\mathrm{Ult}(V,F')$ but $V_{j_F(\kappa_F)+1}\not\subseteq\mathrm{Ult}(V,F')$, so $\rho(F')=j_F(\kappa_F)=j_{F'}(\kappa_{F'})$. Also note here that since $\kappa_F$ is inaccessible,
$M=\mathrm{Ult}(V,F)\models$"$j_F(\kappa_F)$ is inaccessible", but then since $j_F(\kappa_F)<\rho(F)$, $j_F(\kappa_F)$ is really inaccessible (in $V$), so $\rho(F')$ is inaccessible, as desired. For (d): Because $\mathscr{E}(\alpha_0,\beta_0)$ is a set of extenders of length $\alpha_0$ (for all $\alpha_0,\beta_0\in\mathrm{dom}(\mathscr{E})$), and for each $\beta_1<\beta_0$,
$\mathscr{E}(\alpha_0,\beta_0)\neq\mathscr{E}(\alpha_0,\beta_1)$ (by the novelty condition), it follows that $\beta_0<$ the next inaccessible $\mu>\alpha_0$, and that $\mathscr{E}\upharpoonright(\alpha_0+1,0)\in V_\mu$. Applying this in $\mathrm{Ult}(V,F)$ to $\alpha$, where $j_F(\mathscr{E})\upharpoonright(\alpha+1,0)=\mathscr{E}\upharpoonright(\alpha,\beta)$, we get that (as by assumption $\alpha<j_F(\kappa_F)$) $\beta<j_F(\kappa_F)$. But then considering the factor map $\mathrm{Ult}(V,F')\to\mathrm{Ult}(V,F)$, condition (d) follows.
But now suppose that $\alpha=j_F(\kappa_F)$. I don't see how to rule this possibility out (and it is expressly allowed by condition (c)). But in this case, by (a), $\alpha<\rho(F)$, so $j_F(\kappa_F)<\rho(F)$, which requires that $F$ is not short, i.e. $\kappa_F<\iota_F$. So I don't see how to prove the lemma in this case. However, a weaker conclusion is: There is an extender $F'$ which is short, has the same (minimal) length as does $F$, and which also satisfies the conditions. To see this, let $F_0=F$ and $M_0=V$ and $M_1=\mathrm{Ult}(M_0,F_0)$ and $F_1=j_{F_0}(F_0)$ and $M_2=\mathrm{Ult}(M_1,F_1)$. Let $k:M_0\to M_2$ be the composition of the ultrapower maps. Let $F'$ be the (short) extender derived from $k$ with length $\mathrm{lh}(F')=\rho(F)$. Claim: $F'$ satisfies the coherence conditions, and $\mathrm{lh}(F)=\mathrm{lh}(F')=\rho(F)$, so $F'$ also has minimal length. Proof: We have $\mathrm{lh}(F)=\rho(F)$ because $\mathrm{lh}(F)\geq\rho(F)$ as usual, and letting $F''$ be the restriction of $F$ to $\rho(F)$, one can see much as in the previous case that $F''$ also satisfies the conditions, so by minimality, $\mathrm{lh}(F)=\rho(F)$. We have $\mathrm{lh}(F')=\rho(F)$ by definition. So we just need to see that $F'$ satisfies conditions (a)-(d) of coherence. Note that since $V_{\rho(F)}\subseteq M_1$ and $M_1\models$"$\rho(F_1)=j_{F}(\rho_F)$", we have $V_{\rho(F)}\subseteq M_2$, so $\rho(F')\geq\rho(F)$, and in fact therefore $\rho(F')=\rho(F)$. Conditions (a), (b) and (c) for $F'$ are now clear, and in fact we have $\alpha<j_{F'}(\kappa_{F'})$ since in fact $\rho(F)<j_{F'}(\kappa_{F'})$. For (d), since $j_F(\mathscr{E})\upharpoonright(\alpha+1,0)=\mathscr{E}\upharpoonright(\alpha,\beta)$, and $F_1=j_F(F)\in j_F(\mathscr{E})_{j_F(\alpha),j_F(\beta)}$ and $\alpha=j_F(\kappa_F)<j_F(j_F(\kappa_F))=j_F(\alpha)$, we get $k(\mathscr{E})\upharpoonright(j_F(\alpha)+1,0)=j_F(\mathscr{E})\upharpoonright(j_F(\alpha),j_F(\beta))$, so $k(\mathscr{E})\upharpoonright(\alpha+1,0)=j_F(\mathscr{E})\upharpoonright(\alpha+1,0)=\mathscr{E}\upharpoonright(\alpha,\beta)$. But since $\alpha=j_F(\kappa_F)<\rho(F)$ and $\rho(F)$ is inaccessible (in $V$ and hence $M_2$), we have $\beta<\rho(F)$
and $\mathscr{E}\upharpoonright(\alpha,\beta)\in V_{\rho(F)}$. Considering the factor map $\ell:\mathrm{Ult}(V,F')\to M_2$, we get $\ell(\mathscr{E}\upharpoonright(\alpha,\beta))=\mathscr{E}\upharpoonright(\alpha,\beta)$, and $j_{F'}(\mathscr{E})\upharpoonright(\alpha+1,0)=\mathscr{E}(\alpha,\beta)$, as desired.
