appendix sectionsignatures

MixML, LTG, and definedness

Finite teaching signature.: ${Mix}_{0}$ has typed finite slots, polar import/export signatures, partial merge, and an initialization state transition. Definedness growth and no-early-read are local theorems only for that signature.
Ordered trace signature.: The command and trace judgments of definition 15.6, definition 15.7 validate temporal initialization and prove no early read or repeated assignment. They are stricter than full LTG and are not used to strengthen its theorem.
Full semantic signature.: Imported MixML signatures contain type, term, and higher-order unit components, two unit locators, realizers, and absolute signatures as in definition 15.10. Template, static, lookup, and main premises meet in the deterministic link mechanism (15.2)–(15.5).
Published boundary.: Rossberg–Dreyer Theorems 7.10, 7.14, 8.1, 8.7, 9.8–9.10, Corollary 9.11, and Theorem 9.12 establish LTG safety, evidence translation, three-pass soundness/completeness, decidability, and uniqueness for their full MixML/LTG signatures and stated core-language hypotheses. LTG may reduce an early undefined dereference to $∙$ ; progress says that a non-error terminal configuration has only defined cells.
Non-transfer.: No result is asserted for Standard ML, Dreyer’s distinct recursive-module calculus, or Leroy’s module system.
Executable evidence.: artifacts/ch15-mixml-definedness/ checks five finite merge/initialization cases; it proves no metatheorem.