Countable-ordinal correctness under constructibility (source code)

= Countable-ordinal correctness under constructibility

Assuming $V=L$, every uncountable <transitive model> of <ZFC> contains all ambient <countable ordinals> and witnesses their countability internally. Its ordinal height is at least $\omega_1$, and <absoluteness of constructible levels> puts $L_{\omega_1}$ inside it. Every countability witness for a countable ordinal can be chosen in $L_{\omega_1}$ by <hereditarily countable constructible sets appear below omega-one>.