The displayed target

The source declares a canonical contraction map on its reconstructed kernels on $O$. Definition def:mcirc supplies the missing display for that recipe. It does not independently recover every coefficient hidden in the inherited tensor pairings or prove that the expression can be evaluated on a test crossing the retained characteristic locus.

This is the appropriate correction to D0.10: the recipe is no longer only a paraphrase. Its domain limitation remains part of the definition rather than an omitted qualification.