Realization
A model that type-checks is not yet a running system. Two things stand between the source and a database that answers questions: the executor must know it can evaluate the program at all, with a cost it can name, and the program must become an artifact a runtime loads and replays. Argon settles the first before the second. A program declares how hard it is to reason about, the classifier verifies that claim, and only a program the executor can run reaches the artifact.