ora-0120

9.7 Growing diagrams and the Beck–Chevalley defect

In a genuinely online problem the observation category may itself grow:

\[ \mathcal{O}_s\xhookrightarrow {i_{s,t}}\mathcal{O}_t, \qquad s\leq t. \]

Restriction of a later semantic construction to an earlier prefix can then be compared with constructing the semantics directly from the restricted data. The universal properties generate a canonical mate

\begin{equation} \kappa _{s,t}: \mathsf U_s(i_{s,t}^*F_t) \longrightarrow r_{s,t}^*\mathsf U_t(F_t), \end{equation}

9.3

with orientation adjusted when the declared restriction square uses the opposite variance.

Definition 9.6 Prefix-exact online UDL

An online UDL is prefix-exact when every comparison \(\kappa _{s,t}\) in 9.3 is an isomorphism and these isomorphisms satisfy the identity and composition coherences over \(r\leq s\leq t\).

Prefix exactness is the variable-shape analogue of the fixed-shape lifting theorem: it is a Beck–Chevalley condition saying that “restrict after universal decision synthesis” agrees with “restrict the evidence and then synthesize.” When \(\kappa _{s,t}\) is not invertible, its defect is not automatically an error. It measures precisely the structure introduced, destroyed, or revised by later evidence and therefore supplies the typed input to a LINCS repair declaration.