10.2 The four-level implementation invariant

Chapter 5 separated four operations that an implementation must not collapse. This chapter adopts that separation as its organizing invariant:

The arrows display workflow dependencies, not morphisms asserted to exist in one ambient category. When the selected enriched-sketch doctrine admits the required tensor product, \(\mathbb {A}_X\) and \(\mathbb {B}_X\) present the two typed repair families and their specified interchange laws. The maintained state \(M\) is a model of the domain theory \(\mathbb S_X\), equipped with a computational realization of those repair operations. The mixed witness \(\Theta _X(M)\) localizes a failure of the declared repair interaction on that model; it is not itself a change of theory.

A candidate local direction must next pass a finite-realization observer, also called an integration observer, \(\gamma _X\): a registered finite-horizon test of whether repeated repair forms a coherent path, rollout, continuation, groupoid action, or other application-specific finite realization. Classical Lie integrability is the sharp mathematical model, but an implementation may use a justified empirical surrogate. Only after this test does the algorithm ask which component of the maintained representational package, if any, must change. The resulting proposal is a package comparison \(\Upsilon _X:\mathfrak R_X\to \mathfrak R_X^{+}\). When the presentation or generative language changes, its presentation component is a typed map \(J_X:\mathbb {S}_X\to \mathbb {S}_X^{+}\); changes to semantics, observers, probes, doctrine, or admission occupy their own components. Transport and independent admission remain necessary in every case.

This yields three different negative outcomes. A side-coherence failure invalidates the proposed repair semantics. A mixed defect diagnoses an interaction that the current model does not explain. An integration failure shows that a locally meaningful candidate does not survive finite composition. None uniquely specifies a new object, axiom, or mechanism.

. Every executable DIAL-X method must expose four records: the tensor-product repair declaration, the localized mixed witness, the finite-realization result produced by its registered observer, and—when proto-accommodation is proposed—the package comparison, its domain-theory component when applicable, and their independently tested consequences. A one-step improvement is not a realized repair, and a realized repair is not automatically a theory extension.