HOD-Pair Capturing Under Determinacy and No Long Extenders

Definitions and mathematical statement

The supplied record uses $\mathrm{AD}^{+}$ for a strengthened axiom of determinacy, $\mathrm{NLE}$ for the no-long-extenders hypothesis described below, and $\mathrm{HPC}$ for HOD-pair capturing. Here HOD denotes the class of hereditarily ordinal-definable sets. The record does not supply the axiom package defining $\mathrm{AD}^{+}$ or the quantified definition of HOD-pair capturing.

As stated in the source record, $\mathrm{NLE}$ asserts that there is no countable pure extender mouse containing a long extender that admits an $\omega_1$-iteration strategy. Its logical form is \[ \neg\exists M\,\exists\Sigma\;\left[ M\text{ is a countable pure extender mouse} \ \land\ M\text{ contains a long extender} \ \land\ \Sigma\text{ is an }\omega_1\text{-iteration strategy for }M \right]. \] The technical conventions for mice, long extenders, and iteration strategies, including the interpretation of iteration length $\omega_1$, are not specified in the supplied record.

Conjecture as recorded. Does the implication \[ \left(\mathrm{AD}^{+}\land\mathrm{NLE}\right) \ \Longrightarrow\ \mathrm{HPC} \] hold?

This preserves the recorded conjecture, but is not a self-contained formal statement: an underlying set-theoretic theory, the exact definition of $\mathrm{AD}^{+}$, the definition and quantifiers of HOD-pair capturing, and the relevant inner-model-theoretic conventions must be supplied before the implication can be formulated precisely. No additional hypotheses or conventions are imposed here.

Short English statement

The recorded conjecture asks whether strengthened determinacy together with the absence of an $\omega_1$-iterable countable pure extender mouse containing a long extender implies HOD-pair capturing. Essential technical definitions and background assumptions are missing from the supplied record, so this is a statement-only draft requiring mathematical review.

Sources

• Local UnsolvedMath registry, supplied complete record: permanent ID $30003405$, source problem code catalogue entry, title HOD-Pair Capturing Under Determinacy and No Long Extenders. The record gives proposed year 2017 and names no proposer.
• Supplied source citation: Set Theory (2018), Oberwolfach Reports, pp. 527--589, DOI 10.4171/owr/2017/11. https://doi.org/10.4171/owr/2017/11. The record describes Oberwolfach Reports as documenting mathematical workshops and their open-problem discussions.
• Supplied literature source, labelled "Oberwolfach report": https://ems.press/content/serial-article-files/46674.
• Supplied literature source, labelled "Steel": https://math.berkeley.edu/~steel/papers/short.strategycompare.pdf.
• Supplied literature source, labelled "Sargsyan--Steel": https://par.nsf.gov/servlets/purl/10221774.
• Literature assessment dated 2026-08-21: the supplied curation labels the conjecture open and reports that localization and conditional results are available while the general HOD analysis retains the capturing hypothesis. This is supplied dated curation derived from the OWR record, not an independently verified literature assessment; its status and cited claims require independent verification.
• The registry labels the statement corrected_verified and reports that the official Oberwolfach report was checked directly to restore definitions and remove source-dependent wording. This is a supplied verification claim; no source was independently visited or verified in preparing this draft.