Chapter 6 - The internal theory of LSA HOD mice

Summary

This chapter studies internal theory of lsa hod mice. Suppose $(\mathcal{P},\Sigma)$ is a hod pair of an sts hod pair, $X$ is a self-wellordered set such that $\mathcal{P}\in X$, and $\mathcal{N}$ is a $\Sigma$ or $\Sigma$-sts mouse over $X$. The main theorem of this chapter shows that N is $\Sigma$-closed and has fullness preserving iteration strategy, then $\Sigma \restriction \mathcal{N}[g]$ is definable in $\mathcal{N}[g]$ for any generic $g$ over $\mathcal{N}$ . The main idea behind the proof is that the branch of an iteration tree $\mathcal{T}$ on $\mathcal{P}$ can be identified by the authentication process introduced in Chapter 3.