Having done that, I compared with something I tried to model earlier.

I compared the Layer0 refactor with the old refactor writeup from Mark Miller (https://github.com/erights/tc39pr-refactor-ModuleRecord) and the most significant difference is:

We separate into a distinct ModuleInitialization object the bookkeeping needed to guide module instantiation, linking, initialization, etc. Thus, once the initialization process completes, this bookkeeping state is no longer present. This helps us reason about post-initialization state separately.

Which was introduced to make CyclicModuleRecord cleaner. I think it could also remove the need for bidirectional reference between Module and SourceTextModuleRecord if introduced to Layer 0 refactor.