The PFA-to-superstrong-cardinal conjecture in the uB derived model
PFA-to-superstrong-cardinal conjecture. Under these hypotheses, there is a superstrong cardinal in HODL(uBg,Rg)\operatorname{HOD}^{L({{\sf{uB}}}_g,\mathbb{R}_g)}HODL(uBg,Rg).
MathDB