# Shelah's eventual categoricity and the prescribed-threshold obstruction

The following describes the scope of the Lean formalization related to the following accompanying paper(s):

- [A CH obstruction to a prescribed categoricity threshold](../../preprints/A-CH-Obstruction-to-a-Prescribed-Categoricity-Threshold-September-24-2026/paper.pdf)

## Scope

Under the continuum hypothesis, the formalized result refutes the proposed transfer of categoricity down to the Hanf threshold. It gives an abstract elementary class in a countable relational language, with Löwenheim–Skolem number $\aleph_0$, that has two nonisomorphic models at $\beth_{\omega_2}=h(\aleph_0)$ but is categorical in every cardinal at least $\beth_{(2^{\aleph_1})^+}$.

No amalgamation, joint embedding, tameness, or absence-of-maximal-models assumption is imposed. The later canonical-point obstruction and the separate eventual-categoricity theorem are not included.

## Comparator links

| Result | Comparator statement |
| --- | --- |
| CH categoricity-threshold obstruction | [CHObstruction.lean](../ComparatorChallenges/CHObstruction.lean) |