{"id":"palomar/PALOMAR-2026-09-30-000022","url":"https://github.com/elliotglazer/solid-lean/tree/337e7a5afd81ee7236c0e0dceadbc8cfc313f83f","json":"https://data.palomar-registry.org/entries/PALOMAR-2026-09-30-000022-v1.json","repo":"https://github.com/elliotglazer/solid-lean","tags":["math.LO","msc:03C62","msc:03C40","msc:03F25","msc:03E30","msc:03E55","msc:03B38","msc:03B35","set-theory","model-theory"],"score":0,"title":"solid-lean","trust":"high","domain":"math.LO","source":"palomar","authors":["Elliot Glazer"],"reviews":0,"subject":"math.LO","summary":"The tower theory H is the many-sorted first-order theory of a tower of ZFC universes Z_0, Z_1, ... cut at consecutive inaccessible cardinals, with transition maps j_n identifying Z_n with the rank segment V(kappa_n) of Z_{n+1}. H is solid in Enayat's sense. For models M, N, P, with N interpreted in M and P interpreted in N, and an M-definable isomorphism between M and P, there is an M-definable isomorphism between M and N. The registered statement (Palomar/Challenge.lean) writes out the many-sorted first-order logic of H from scratch, with structures, formulas, satisfaction and definability…","category":"research","comments":0,"disputed":false,"division":"math","mentions":0,"verified":true,"discussed":0,"published":"2026-09-30","reactions":{},"formalized":true}