Stratified Universality

Download original file

This is the original TeX manuscript source. Use the paper’s PDF for typeset equations.

Read the typeset paper

1 \section{Relative semantic quotients and behavioral cores}
2 \label{sec:block17-semantic-quotients}
3 
4 The preceding parts fix resolved signatures, profile-preserving realizations, normalized strata, typed bridges, and descent data.  A second question remains inside each such setting: which distinctions must a representation retain for a declared family of future observations?  This section formalizes that question without replacing the existing preservation-profile machinery.  The central object is a behavioral quotient computed relative to a carrier doctrine, a continuation grammar, and an observation category.
5 
6 \subsection{Semantic slices and resolved observational systems}
7 \label{subsec:block17-semantic-slices}
8 
9 \begin{definition}[Semantic slice]
10 \label{def:block17-semantic-slice}
11 A \emph{semantic slice} is a tuple
12 \[
13  \Sigma=(\mathcal A,\mathcal G,\mathcal V,\mathcal O)
14 \]
15 consisting of:
16 \begin{enumerate}[label=\textup{(\roman*)}]
17 \item a carrier doctrine \(\mathcal A\), which specifies how alternatives, routes, or packets combine;
18 \item a continuation grammar \(\mathcal G\), presented here by a monoid \(M\) or by a chosen generating family of admissible endomorphisms;
19 \item an observation category \(\mathcal V\), such as \(\mathbf{Set}\), \(R\text{-}\mathbf{Mod}\), or \(K\text{-}\mathbf{Vect}\);
20 \item a declared family \(\mathcal O=(o_j)_{j\in J}\) of observations in \(\mathcal V\).
21 \end{enumerate}
22 The slice belongs to the stratum passport.  It does not replace the preservation profile \(\Pi\).  The profile specifies which constructions a bridge preserves, while the slice specifies which future distinctions define the current semantic task.
23 \end{definition}
24 
25 \begin{definition}[Resolved observational system]
26 \label{def:block17-observational-system}
27 Let \(X\) be an object equipped with an action
28 \[
29  \rho:M\longrightarrow \End(X)
30 \]
31 of a continuation monoid and with observations
32 \[
33  o_j:X\longrightarrow Y_j\qquad(j\in J).
34 \]
35 The tuple
36 \[
37  \mathsf S=(X,M,\rho,(o_j)_{j\in J})
38 \]
39 is a \emph{resolved observational system}.  When the indicated product exists, its behavior map is
40 \[
41  \Beh_{\mathsf S}:X\longrightarrow
42  \prod_{(m,j)\in M\times J}Y_j,
43  \qquad
44  x\longmapsto\bigl(o_j(\rho(m)x)\bigr)_{m,j}.
45 \]
46 The \emph{relative behavioral object} is the coimage
47 \[
48  Q_{\mathsf S}:=\operatorname{Coim}(\Beh_{\mathsf S})
49 \]
50 whenever that coimage exists.
51 \end{definition}
52 
53 In \(\mathbf{Set}\), the behavior map identifies states exactly when every declared future observation agrees.  In a module category, the same object can be constructed directly from the intersection of kernels, without assuming that the possibly infinite product is part of the ambient profile.
54 
55 \begin{definition}[Behavioral congruence and linear behavioral kernel]
56 \label{def:block17-behavioral-kernel}
57 In \(\mathbf{Set}\) or a variety of algebras, put
58 \[
59  x\equiv_{\mathsf S}y
60  \quad\Longleftrightarrow\quad
61  o_j(\rho(m)x)=o_j(\rho(m)y)
62  \quad\text{for every }m\in M,\ j\in J.
63 \]
64 Write \(\Theta_{\mathsf S}\) for this relation.  In \(R\text{-}\mathbf{Mod}\), define
65 \[
66  N_{\mathsf S}
67  :=
68  \bigcap_{m\in M}\bigcap_{j\in J}
69  \ker(o_j\rho(m)).
70 \]
71 Then
72 \[
73  Q_{\mathsf S}=X/N_{\mathsf S}.
74 \]
75 \end{definition}
76 
77 \begin{theorem}[Universal behavioral coimage]
78 \label{thm:block17-universal-behavioral-coimage}
79 Assume the relevant effective quotient or module quotient exists.  Then \(Q_{\mathsf S}\) preserves every declared future observation.  Moreover, if
80 \[
81  q:X\twoheadrightarrow Z
82 \]
83 is any surjective representation through which every map \(o_j\rho(m)\) factors, there is a unique map
84 \[
85  \overline q:Z\longrightarrow Q_{\mathsf S}
86 \]
87 with \(\overline q\,q:X\to Q_{\mathsf S}\) equal to the canonical quotient map.  Thus \(Q_{\mathsf S}\) is the coarsest exact representation for the declared semantic slice.
88 \end{theorem}
89 
90 \begin{proof}
91 In the relational setting, the kernel pair of \(q\) is contained in \(\Theta_{\mathsf S}\), because equality under \(q\) forces equality under every factorized future observation.  The universal property of the quotient by \(\Theta_{\mathsf S}\) gives the unique map.  In the module setting,
92 \[
93  \ker q\subseteq
94  \bigcap_{m,j}\ker(o_j\rho(m))=N_{\mathsf S},
95 \]
96 so the ordinary quotient universal property gives the same conclusion.
97 \end{proof}
98 
99 \begin{boundary}[No observer-independent minimum]
100 \label{bnd:block17-no-absolute-minimum}
101 The phrase ``minimal representation'' is meaningful only after the carrier, continuation grammar, observation category, and task have been declared.  Changing any one of these data can change the quotient.  In particular, equality of residual functions in \(\mathbf{Set}\) and linear dependence of residual functions in \(K\text{-}\mathbf{Vect}\) are different minimization problems.
102 \end{boundary}
103 
104 \subsection{The maximal stable invisible core}
105 \label{subsec:block17-stable-core}
106 
107 Let
108 \[
109  K_0:=\bigcap_j\kerpair(o_j)
110 \]
111 in the relational setting and
112 \[
113  N_0:=\bigcap_j\ker(o_j)
114 \]
115 in the linear setting.
116 
117 \begin{theorem}[Behavioral core theorem]
118 \label{thm:block17-behavioral-core}
119 The behavioral relation \(\Theta_{\mathsf S}\) is the greatest continuation-stable congruence contained in \(K_0\).  In the module setting, \(N_{\mathsf S}\) is the greatest \(\rho(M)\)-invariant submodule contained in \(N_0\).
120 \end{theorem}
121 
122 \begin{proof}
123 The identity continuation gives \(\Theta_{\mathsf S}\subseteq K_0\) and \(N_{\mathsf S}\subseteq N_0\).  If \(x\equiv_{\mathsf S}y\), then for every \(n,m\in M\) and every \(j\),
124 \[
125  o_j\rho(m)\rho(n)x
126  =o_j\rho(mn)x
127  =o_j\rho(mn)y
128  =o_j\rho(m)\rho(n)y,
129 \]
130 so the relation is stable.  The same calculation proves invariance of \(N_{\mathsf S}\).
131 
132 Conversely, let \(R\subseteq K_0\) be continuation stable.  If \(xRy\), then \(\rho(m)x\,R\,\rho(m)y\) for every \(m\), and membership in \(K_0\) forces
133 \[
134  o_j\rho(m)x=o_j\rho(m)y
135 \]
136 for every \(j\).  Hence \(R\subseteq\Theta_{\mathsf S}\).  The submodule statement is identical with relations replaced by differences.
137 \end{proof}
138 
139 \begin{remark}[Comparison with holonomy]
140 The maximal path-flat core in \cref{sec:strata-bridges-obstructions} intersects fixed spaces of closed transport words.  The behavioral core intersects kernels of future observation words.  Both constructions extract the greatest subobject on which a declared family of transformations becomes semantically invisible.  They answer different questions and are not identified without a typed comparison map.
141 \end{remark}
142 
143 \subsection{Greatest-fixed-point construction and finite recognition}
144 \label{subsec:block17-fixed-point}
145 
146 Assume \(M\) is generated by a family \(A\).  On congruences or submodules define
147 \[
148  \Phi(R)
149  :=
150  K_0\cap\bigcap_{a\in A}\rho(a)^{-1}(R),
151 \]
152 with the corresponding submodule formula in the linear setting.
153 
154 \begin{theorem}[Coinductive characterization]
155 \label{thm:block17-coinductive-characterization}
156 The behavioral core is the greatest fixed point of \(\Phi\):
157 \[
158  \Theta_{\mathsf S}=\nu R.\Phi(R),
159  \qquad
160  N_{\mathsf S}=\nu N.\Phi(N).
161 \]
162 \end{theorem}
163 
164 \begin{proof}
165 Every fixed point is invisible and stable under every generator, hence under
166 the generated monoid, so it is contained in the behavioral core by
167 \cref{thm:block17-behavioral-core}.  Conversely, the behavioral core is a fixed
168 point: stability gives its inclusion in its image under \(\Phi\), while
169 membership in \(\Phi\) of that core makes the identity observation invisible
170 and makes every first-generator successor behaviorally invisible, hence makes
171 every continuation word invisible.  Its maximality therefore proves the
172 asserted greatest-fixed-point identities.
173 \end{proof}
174 
175 \begin{corollary}[Finite certification]
176 \label{cor:block17-finite-certification}
177 For finite \(X\), descending partition refinement stabilizes after finitely many strict refinements.  For finite-dimensional \(X\) over a field, the chain
178 \[
179  N^{(0)}=N_0,
180  \qquad
181  N^{(r+1)}=
182  N_0\cap\bigcap_{a\in A}\rho(a)^{-1}(N^{(r)})
183 \]
184 stabilizes after at most \(\dim X\) strict dimension drops.  At stabilization it equals \(N_{\mathsf S}\).
185 \end{corollary}
186 
187 \begin{proof}
188 The iteration is descending and every strict inclusion of finite-dimensional subspaces lowers dimension by at least one.  The behavioral core lies in \(N^{(0)}\), and monotonicity of \(\Phi\), together
189 with its fixed-point property, preserves this inclusion at every stage.  Thus
190 the stabilized fixed point contains the behavioral core.  Greatest-fixed-point
191 maximality gives the reverse inclusion, proving equality.
192 \end{proof}
193 
194 \subsection{The task--congruence Galois connection}
195 \label{subsec:block17-task-galois}
196 
197 Fix a universe \(\mathscr Q(X)\) of admissible queries on \(X\).  For \(\mathcal Q\subseteq\mathscr Q(X)\), define
198 \[
199  \Ind(\mathcal Q)
200  :=
201  \bigcap_{q\in\mathcal Q}\kerpair(q).
202 \]
203 For an equivalence relation or congruence \(R\), define
204 \[
205  \Def(R)
206  :=
207  \{q\in\mathscr Q(X):R\subseteq\kerpair(q)\}.
208 \]
209 
210 \begin{theorem}[Task--congruence Galois connection]
211 \label{thm:block17-task-galois}
212 For every query family \(\mathcal Q\) and relation \(R\),
213 \[
214  \mathcal Q\subseteq\Def(R)
215  \quad\Longleftrightarrow\quad
216  R\subseteq\Ind(\mathcal Q).
217 \]
218 Consequently,
219 \[
220  \Cl(\mathcal Q):=\Def(\Ind(\mathcal Q))
221 \]
222 is a closure operator on query families, and
223 \[
224  \operatorname{Sat}(R):=\Ind(\Def(R))
225 \]
226 is the observational saturation of \(R\) relative to the admitted query universe.
227 \end{theorem}
228 
229 \begin{proof}
230 Both conditions say that every query in \(\mathcal Q\) is constant on every \(R\)-class.  The closure laws follow from the standard identities associated with an antitone Galois connection.
231 \end{proof}
232 
233 \begin{definition}[Extensional task]
234 \label{def:block17-extensional-task}
235 An \emph{extensional task} is a closed query theory, equivalently a query family modulo equality of the closure \(\Cl\).  When the admitted query universe separates the desired quotients, an extensional task can equivalently be represented by its observationally definable congruence.
236 \end{definition}
237 
238 \begin{corollary}[Task strengthening]
239 \label{cor:block17-task-strengthening}
240 Adding continuations or observations can only refine behavioral indistinguishability.  Thus
241 \[
242  M\subseteq M',\qquad \mathcal O\subseteq\mathcal O'
243  \quad\Longrightarrow\quad
244  \Theta_{M',\mathcal O'}\subseteq\Theta_{M,\mathcal O},
245 \]
246 and there is a canonical forgetting map
247 \[
248  Q_{M',\mathcal O'}\longrightarrow Q_{M,\mathcal O}.
249 \]
250 \end{corollary}
251 
252 \begin{boundary}[Definable tasks form a closure system]
253 \label{bnd:block17-task-lattice}
254 All continuation-stable congruences form a complete lattice.  Congruences definable by the chosen query universe are always closed under arbitrary meets.  Closure under joins requires an additional richness or quotient-completeness hypothesis on the query universe and is not asserted automatically.
255 \end{boundary}
256 
257 \subsection{Semantic quotient lattice}
258 \label{subsec:block17-quotient-lattice}
259 
260 \begin{theorem}[Semantic quotient classification, classical]
261 \label{thm:block17-semantic-quotient-classification}
262 Let \(X\) be an algebra in a variety.  Surjective semantic maps
263 \[
264  q:X\twoheadrightarrow Q
265 \]
266 up to isomorphism of codomains are classified by congruences on \(X\) through
267 \[
268  q\longmapsto\ker q.
269 \]
270 Moreover, a quotient \(q\) maps to a quotient \(r\) exactly when \(\ker q\subseteq\ker r\).
271 \end{theorem}
272 
273 \begin{proof}
274 This is the first isomorphism theorem and the universal property of quotient algebras.  It is included to fix the direction of the information order used below.
275 \end{proof}
276 
277 \begin{corollary}[Combined and shared semantics]
278 \label{cor:block17-combined-shared-semantics}
279 For semantic quotients with kernels \(N\) and \(M\):
280 \begin{enumerate}[label=\textup{(\roman*)}]
281 \item the least common refinement has kernel \(N\cap M\);
282 \item the greatest common coarsening has kernel the generated congruence join \(N\vee M\);
283 \item in a module category, \(N\vee M=N+M\).
284 \end{enumerate}
285 \end{corollary}
286 
287 \subsection{The two-view semantic diamond}
288 \label{subsec:block17-semantic-diamond}
289 
290 Let \(X\) be an \(R\)-module and let
291 \[
292  s:X\twoheadrightarrow S,
293  \qquad
294  t:X\twoheadrightarrow T
295 \]
296 be surjective linear semantic maps.  Put
297 \[
298  N=\ker s,
299  \qquad
300  M=\ker t,
301  \qquad
302  J=X/(N\cap M),
303  \qquad
304  C=X/(N+M).
305 \]
306 
307 \begin{theorem}[Semantic diamond and exact compatibility sequence]
308 \label{thm:block17-semantic-diamond}
309 The canonical square
310 \[
311 \begin{CD}
312  J @>>> T\\
313  @VVV @VVV\\
314  S @>>> C
315 \end{CD}
316 \]
317 is a pullback in \(R\text{-}\mathbf{Mod}\).  Equivalently,
318 \[
319  J\cong S\times_C T.
320 \]
321 There is also a canonical short exact sequence
322 \[
323  0\longrightarrow X/(N\cap M)
324  \xrightarrow{\alpha}
325  X/N\oplus X/M
326  \xrightarrow{\beta}
327  X/(N+M)
328  \longrightarrow0,
329 \]
330 where
331 \[
332  \alpha(x+N\cap M)=(x+N,x+M)
333 \]
334 and
335 \[
336  \beta(a+N,b+M)=a-b+(N+M).
337 \]
338 \end{theorem}
339 
340 \begin{proof}
341 The map \(\alpha\) is injective because its kernel is \(N\cap M\).  The formula for \(\beta\) is well defined and surjective.  Clearly \(\beta\alpha=0\).  If \(\beta(a+N,b+M)=0\), then
342 \[
343  a-b=n+m
344 \]
345 for some \(n\in N\) and \(m\in M\).  Set \(x=a-n=b+m\).  Then
346 \[
347  (a+N,b+M)=(x+N,x+M)=\alpha(x+N\cap M).
348 \]
349 Thus \(\ker\beta=\im\alpha\), proving exactness.  The kernel description of the fiber product is the same calculation.
350 \end{proof}
351 
352 \begin{figure}[htbp]
353 \centering
354 \includegraphics[width=.76\textwidth]{block17_semantic_diamond.pdf}
355 \caption{The semantic diamond.  The joint representation \(J\) retains both views.  The common quotient \(C\) is the compatibility interface over which the separate coordinates glue.}
356 \label{fig:block17-semantic-diamond}
357 \end{figure}
358 
359 \begin{definition}[Relative semantic residual]
360 \label{def:block17-relative-residual}
361 The information needed to augment \(S\) so that it also retains \(T\) is
362 \[
363  R_{T\mid S}
364  :=
365  \ker(J\to S)
366  \cong
367  N/(N\cap M)
368  \cong
369  (N+M)/M.
370 \]
371 \end{definition}
372 
373 \begin{corollary}[Factorization criterion]
374 \label{cor:block17-factorization-criterion}
375 The following are equivalent:
376 \[
377  t\text{ factors through }s,
378  \qquad
379  N\subseteq M,
380  \qquad
381  R_{T\mid S}=0,
382  \qquad
383  J\to S\text{ is an isomorphism}.
384 \]
385 Moreover,
386 \[
387  0\longrightarrow R_{T\mid S}
388  \longrightarrow J
389  \longrightarrow S
390  \longrightarrow0
391 \]
392 is exact.
393 \end{corollary}
394 
395 \begin{boundary}[Residuals need not split]
396 \label{bnd:block17-residual-splitting}
397 The exact sequence above does not canonically identify \(J\) with \(S\oplus R_{T\mid S}\).  Vector-space extensions split noncanonically.  Module, integral, semiring, filtered, or topological extensions may fail to split.  A residual packet presented as an independent coordinate therefore requires an explicit splitting theorem or constructor passport.
398 \end{boundary}
399 
400 \subsection{Exact change of task}
401 \label{subsec:block17-task-change}
402 
403 \begin{theorem}[Task-change exact sequence]
404 \label{thm:block17-task-change}
405 Let a stronger task have behavioral kernel \(N_s\), and let a weaker task have behavioral kernel \(N_w\), with
406 \[
407  N_s\subseteq N_w.
408 \]
409 Then
410 \[
411  0\longrightarrow N_w/N_s
412  \longrightarrow X/N_s
413  \longrightarrow X/N_w
414  \longrightarrow0
415 \]
416 is exact.  Thus \(N_w/N_s\) is the exact semantic information discarded when the task is weakened.
417 \end{theorem}
418 
419 \begin{proof}
420 Apply the third isomorphism theorem to the chain \(N_s\subseteq N_w\subseteq X\).
421 \end{proof}
422 
423 \begin{corollary}[Composition of task loss]
424 \label{cor:block17-task-loss-composition}
425 For
426 \[
427  N_1\subseteq N_2\subseteq N_3,
428 \]
429 there is an exact sequence
430 \[
431  0\longrightarrow N_2/N_1
432  \longrightarrow N_3/N_1
433  \longrightarrow N_3/N_2
434  \longrightarrow0.
435 \]
436 Hence task loss composes as extension data rather than as a canonically split sum.
437 \end{corollary}
438 
439 \begin{resultbox}
440 \textbf{Semantic quotient result.}
441 Inside a fixed doctrine, declared future tasks are represented by continuation-stable congruences or subobjects.  Behavioral minimization extracts the maximal stable invisible core.  Task strengthening induces canonical forgetting maps, joint tasks form semantic diamonds, and relative task loss is measured by exact quotient objects.  The construction is relative to the semantic slice and does not define an observer-independent minimum.
442 \end{resultbox}

Back to source controls

Back to Stratified Universality