Laver hasA few months back, I posted a question asking about a proposed axiom of Laver's and I, unfortunately, left out a critical piece. Here is the followingfull axiom:
(*L) someSome elementary embedding $j:V_{\lambda+1}\rightarrow V_{\lambda +1}$$j:V_{\lambda+1}\prec V_{\lambda+1}$ extends to a non-trivial elementary embedding $h:HOD(ord^\lambda)\rightarrow HOD(ord^\lambda)$$h:HOD(ord^\lambda)\prec HOD(ord^\lambda)$ where it is assumed that $HOD(ord^\lambda)\models ZF +DC_\lambda + Unif(V_{\lambda+1})$.
Here $DC_\lambda$ denotes the axiom of $\lambda$-dependent choice and $Unif(V_{\lambda +1})$ is the axiom that uniformization holds for $V_{\lambda +1}$. More specifically, given any $R\subseteq V_{\lambda +1}\times V_{\lambda +1}$ there exists some function $f\subset R$ with the same domain as $R$.
This axiom is generically fragile in that any small forcing adding a real kills the axiom. This fragility is evidently a consequence of the further assumption about which axioms hold in $HOD(ord^\lambda)$, in particular $Unif(V_{\lambda +1})$.
As before, I have no indication about how this is established at the the moment and I suspect that the problem is that I don't understand what the model $HOD(ord^\lambda)$ looks like in a generic extension. I am hoping someone can give me some indication as to the kinds of "damage" HOD$HOD$-like models can undergo during a forcing.
As of now, I have the following very limited sketch:
Assume, in $V$, that some $j:V_{\lambda+1}\rightarrow V_{\lambda+1}$ extends to $h:HOD(ord^\lambda)\rightarrow HOD(ord^\lambda)$. Let $P$ be a poset of size smaller than $crit(j)$, $G\subseteq P$ which is $V$-generic and $V[G]\setminus V$ contains a new real, say $f$. Since the forcing is small, we can lift the original embedding $j$ (in $V$) in the canonical way to a $j_G$ (in $V[G]$) , i.e. set $j_G(\dot{x}_G)=j(x)_G$ for $\dot{x}$ a name. I don't see why $h$ doesn't lift in the exact same way to an $h_G$, i.e. why doesn't $h_G$ witness an elementary embedding from $HOD(ord^\lambda)$ to itself?
Supposing $h$ does lift to an $h_G$, is the generic fragility claim simply the observation that $h_G$ restricted to $V[G]_{\lambda+1}\neq j_G$? Is this even a correct observation? Is there some consequence like "$j_G(f) \neq h_G(f)$" that I just don't see?
As you can probably tell, I really only have a surface understanding of the situation. I have been trying to find literature dealing with HOD beyond the basic facts, but I am coming up with very few resources.