ora-0055

3.10 Local identification does not automatically glue

Let \(\mathsf{Mod}_{\mathcal C}(\mathbb T)\) be the category of realizations of a sketch \(\mathbb T\) in \(\mathcal C\). Restriction along the fragment cover defines a comparison functor

\begin{equation} \Delta : \mathsf{Mod}_{\mathcal C}(\mathbb T_{\mathrm{core}}) \longrightarrow \lim _{[k]\in \boldsymbol \Delta } \prod _{i_0,\ldots ,i_k} \mathsf{Mod}_{\mathcal C}(\mathbb T_{i_0\cdots i_k}). \end{equation}
3.1

The right side is the category of compatible local realizations and coherent overlap data.

Definition 3.9 Effective core descent

The fragment cover has effective core descent in \(\mathcal C\) when \(\Delta \) is an equivalence. It has separated core descent when \(\Delta \) is fully faithful.

Effective descent says that compatible fragments can be glued and that the gluing is unique up to coherent equivalence. Separated descent gives uniqueness when a gluing exists, but not existence. Neither condition follows merely from calling the six systems a cover; it is a substantive property of the chosen sketch semantics.

Theorem 3.10 Fragment-to-core identification

Fix a target \((\mathcal C_\star ,M_\star )\), a fragment cover with effective core descent, and fair presentations of every fragment and every finite overlap. Suppose the learner identifies each local realization and its overlap comparisons coherently in the limit. Then it identifies \(M_\star \) in the limit up to core-equivalence.

Proof ▼

After local and overlap stabilization, the learner determines an object of the limit category on the right of 3.1. Effective core descent supplies a global realization, and full faithfulness makes its equivalence class unique. Hence every query invariant under core-equivalence eventually receives the target answer.

The theorem is deliberately conditional. It exposes three independent obligations: local learnability, learnability of the overlaps, and a descent theorem for the declared core semantics. The second is easily overlooked and is often the scientifically interesting part.