block15_section.tex
Stratified Universality
block15_section.tex
This is the original TeX manuscript source. Use the paper’s PDF for typeset equations.
Included manuscript sections
1 \clearpage
2 \section{Universal lane transport at finite profile}
3 \label{sec:block15-universal-lane-transport}
4
5 The preceding parts of the manuscript establish packet coordinates in an
6 additive idempotent-complete setting and verify them separately in several
7 native strata. This section isolates the common finite theorem. The word
8 ``lane'' will mean a packet together with its address, its chosen splitting,
9 and its position in a declared refinement system. Thus a lane is more than a
10 subsequence or a suggestive decomposition. It carries the exact data needed
11 for analysis, synthesis, transfer, refinement, and reconstruction.
12
13 The theorem is universal only in a profiled sense. Its algebraic core applies
14 to every additive realization that preserves the finite sums, compositions,
15 split idempotents, and refinement identities used in the proof. Kernel,
16 quotient, tensor, topological, metric, and nonlinear conclusions require the
17 additional hypotheses stated where they occur.
18
19 \subsection{Finite profiled lane systems}
20 \label{subsec:block15-lane-systems}
21
22 \begin{definition}[Finite resolution shape]
23 \label{def:block15-resolution-diagram}
24 A finite resolution shape is a finite partially ordered set
25 \(\mathsf R\). We write \(s\succeq r\) when \(s\) is finer than \(r\).
26 The shape contains no address sets: object-specific addresses and their
27 refinement maps are declared in the lane system below.
28 \end{definition}
29
30 \begin{definition}[Finite profiled lane system]
31 \label{def:block15-finite-profiled-lane-system}
32 Let \(\mathcal C\) be an additive idempotent-complete category, let
33 \(X\in\mathcal C\), and let \(\mathsf R\) be a finite resolution shape. A
34 finite profiled lane system \(\mathcal L_X\) consists, for every
35 \(r\in\mathsf R\), of a finite address set \(I_{X,r}\) and a family
36 \[
37 \mathcal P_X^r=(p_{X,i}^r)_{i\in I_{X,r}}
38 \subseteq\End_{\mathcal C}(X)
39 \]
40 with
41 \[
42 (p_{X,i}^r)^2=p_{X,i}^r,
43 \qquad
44 p_{X,i}^rp_{X,j}^r=0\quad(i\ne j),
45 \qquad
46 \sum_{i\in I_{X,r}}p_{X,i}^r=1_X,
47 \]
48 together with chosen splittings
49 \[
50 X_i^r\xrightarrow{\iota_{X,i}^r}X
51 \xrightarrow{\pi_{X,i}^r}X_i^r,
52 \qquad
53 \iota_{X,i}^r\pi_{X,i}^r=p_{X,i}^r,
54 \qquad
55 \pi_{X,i}^r\iota_{X,i}^r=1_{X_i^r}.
56 \]
57 For \(s\succeq r\), the system also contains a surjection
58 \[
59 \rho^X_{sr}:I_{X,s}\twoheadrightarrow I_{X,r}
60 \]
61 such that
62 \[
63 p_{X,i}^r
64 =
65 \sum_{\rho^X_{sr}(j)=i}p_{X,j}^s,
66 \qquad
67 \rho^X_{tr}=\rho^X_{sr}\rho^X_{ts}.
68 \]
69 Here \(\rho^X_{rr}=1_{I_{X,r}}\). The address sets and refinement maps are
70 declared data; they are not inferred from their cardinalities.
71 Its verified profile contains finite biproducts, addition of morphisms,
72 composition, the displayed splittings, and these projector-sum refinement
73 identities. Any further constructor is included only after its preservation
74 has been verified.
75 \end{definition}
76
77 At resolution \(r\), write
78 \[
79 \Analysis_X^r
80 :=(\pi_{X,i}^r)_i:
81 X\longrightarrow\bigoplus_iX_i^r,
82 \qquad
83 \Synthesis_X^r
84 :=(\iota_{X,i}^r)_i:
85 \bigoplus_iX_i^r\longrightarrow X.
86 \]
87 For profiled lane systems on \(X\) and \(Y\), define the coordinate block of
88 \(f:X\to Y\) at resolutions \(r,u\) by
89 \[
90 [f]^{u,r}_{a i}
91 :=
92 \pi_{Y,a}^u f\iota_{X,i}^r:
93 X_i^r\longrightarrow Y_a^u.
94 \]
95 Its ambient corner is
96 \[
97 p_{Y,a}^u f p_{X,i}^r
98 =
99 \iota_{Y,a}^u[f]^{u,r}_{a i}\pi_{X,i}^r.
100 \]
101
102 \subsection{The universal finite transport theorem}
103 \label{subsec:block15-main-theorem}
104
105 \begin{theorem}[Universal Lane Transport Theorem, finite profiled form]
106 \label{thm:block15-universal-lane-transport}
107 Let \(\mathcal C\) be an additive idempotent-complete category. Give each of
108 the objects \(X_0,\ldots,X_m\) a finite profiled lane system. Then all of the
109 following statements hold.
110
111 \begin{enumerate}[label=\textup{(L\arabic*)}]
112 \item \textbf{Exact analysis and synthesis.} At every declared resolution,
113 \[
114 \Synthesis_X^r\Analysis_X^r=1_X,
115 \qquad
116 \Analysis_X^r\Synthesis_X^r
117 =1_{\oplus_iX_i^r}.
118 \]
119 Hence \(X\cong\bigoplus_iX_i^r\).
120
121 \item \textbf{Unique lane matrix.} Every morphism \(f:X\to Y\) is recovered
122 uniquely from its lane blocks:
123 \[
124 f
125 =
126 \sum_{a,i}p_{Y,a}^u f p_{X,i}^r
127 =
128 \sum_{a,i}\iota_{Y,a}^u
129 [f]^{u,r}_{a i}\pi_{X,i}^r.
130 \]
131 Equivalently, the assignment
132 \[
133 f\longmapsto
134 \bigl([f]^{u,r}_{a i}\bigr)_{a,i}
135 \]
136 is a bijection from \(\Hom_{\mathcal C}(X,Y)\) to the group of rectangular
137 matrices with entries in
138 \(\Hom_{\mathcal C}(X_i^r,Y_a^u)\).
139
140 \item \textbf{Composition and path law.} If \(f:X\to Y\) and \(g:Y\to Z\),
141 with the same resolution \(u\) used on the intermediate object, then
142 \[
143 [gf]^{v,r}_{c i}
144 =
145 \sum_{a\in I_{Y,u}}[g]^{v,u}_{c a}[f]^{u,r}_{a i}.
146 \]
147 More generally, a block of a composable string is the finite sum of the
148 products along all compatible intermediate address paths.
149
150 \item \textbf{Projector-sum refinement.} If \(s\succeq r\) on \(X\) and
151 \(v\succeq u\) on \(Y\), then
152 \[
153 p_{Y,a}^u f p_{X,i}^r
154 =
155 \sum_{\rho^Y_{vu}(b)=a}
156 \sum_{\rho^X_{sr}(j)=i}
157 p_{Y,b}^v f p_{X,j}^s.
158 \]
159 Coarsening a fine composite gives the same ambient morphism as composing at
160 the coarse level.
161
162 \item \textbf{Selectors and named residuals.} For
163 \(E\subseteq I_{Y,u}\times I_{X,r}\), put
164 \[
165 C_E^{u,r}(f)
166 :=\sum_{(a,i)\in E}p_{Y,a}^ufp_{X,i}^r,
167 \qquad
168 R_E^{u,r}(f):=f-C_E^{u,r}(f).
169 \]
170 As additive endomorphisms of \(\Hom_{\mathcal C}(X,Y)\),
171 \[
172 C_E^2=C_E,
173 \qquad
174 C_EC_F=C_{E\cap F},
175 \qquad
176 R_E=1-C_E,
177 \qquad
178 f=C_E(f)+R_E(f).
179 \]
180 Thus deletion of a lane block is never silent. Its complement is an exact,
181 named residual.
182
183 \item \textbf{Support transport.} If \(f=C_E(f)\) and \(g=C_F(g)\), then
184 \[
185 gf=C_{F\circ E}(gf),
186 \]
187 where \(F\circ E\) is relational composition through the intermediate
188 addresses. For arbitrary \(f,g\), writing
189 \(f_E=C_E(f)\), \(r_f=R_E(f)\), \(g_F=C_F(g)\), and
190 \(r_g=R_F(g)\), one has the exact identity
191 \[
192 gf-g_Ff_E
193 =r_gf_E+g_Fr_f+r_gr_f.
194 \]
195
196 \item \textbf{Additive realization.} Let
197 \(F:\mathcal C\to\mathcal D\) be an additive functor to another additive
198 idempotent-complete category. If the verified profile of \(F\) contains the
199 chosen splittings and refinement identities, then
200 \[
201 F([f]^{u,r}_{a i})
202 =
203 [F(f)]^{u,r}_{a i}
204 \]
205 after the declared splitting comparisons. The functor carries analysis,
206 synthesis, matrix multiplication, projector-sum refinement, selectors, and
207 named residuals to their corresponding constructions in \(\mathcal D\).
208
209 \item \textbf{Exact fold loss.} Let \(E\) be a finite set of retained lane
210 positions and set
211 \[
212 B_e:=\Hom_{\mathcal C}(X_i^r,Y_a^u)
213 \quad\text{for }e=(a,i)\in E.
214 \]
215 Let \(T\) be a finite set, let \(\kappa:E\to T\), let \(C_t\) be abelian
216 groups, and let \(\tau_e:B_e\to C_{\kappa(e)}\) be homomorphisms. With
217 \(C=\bigoplus_{t\in T}C_t\) and coordinate inclusions
218 \(j_t:C_t\to C\), the fold
219 \[
220 \Phi_{\kappa,\tau}:
221 \bigoplus_{e\in E}B_e\longrightarrow C,
222 \qquad
223 (b_e)_e\longmapsto
224 \sum_{e\in E}j_{\kappa(e)}\tau_e(b_e)
225 \]
226 has exact information-loss group \(\ker\Phi_{\kappa,\tau}\). In particular,
227 two retained lane matrices have the same folded record exactly when their
228 difference belongs to this kernel.
229
230 Suppose, more strongly, that every \(\tau_e\) is injective and that there are
231 globally typed selectors \(Q_e\in\End(C)\) satisfying, for every
232 \(e,e'\in E\) and every \(b_{e'}\in B_{e'}\),
233 \[
234 Q_ej_{\kappa(e')}\tau_{e'}(b_{e'})
235 =
236 \delta_{e,e'}j_{\kappa(e')}\tau_{e'}(b_{e'}).
237 \]
238 Then \(\Phi_{\kappa,\tau}\) is injective. If there are also homomorphisms
239 \[
240 r_e:C\longrightarrow B_e,
241 \qquad
242 r_ej_{\kappa(e)}\tau_e=1_{B_e},
243 \]
244 then
245 \[
246 L:=\bigl(r_eQ_e\bigr)_{e\in E}:C\longrightarrow\bigoplus_{e\in E}B_e
247 \]
248 is a left inverse of \(\Phi_{\kappa,\tau}\), so the fold is split lossless.
249 \end{enumerate}
250 \end{theorem}
251
252 \begin{proof}
253 For (L1), the first composite is
254 \[
255 \sum_i\iota_{X,i}^r\pi_{X,i}^r
256 =\sum_i p_{X,i}^r=1_X.
257 \]
258 The \((i,j)\)-entry of the other composite is
259 \(\pi_{X,i}^r\iota_{X,j}^r\). It is the identity when \(i=j\), and it is
260 zero otherwise because the corresponding idempotents annihilate one another.
261
262 For (L2), insert the two reconstruction identities on the two sides of
263 \(f\). Applying \(\pi_{Y,a}^u\) on the left and
264 \(\iota_{X,i}^r\) on the right proves uniqueness of every entry. For (L3),
265 insert
266 \(1_Y=\sum_a\iota_{Y,a}^u\pi_{Y,a}^u\) between \(g\) and \(f\).
267 Iteration gives the path formula.
268
269 For (L4), substitute the two projector-sum refinement identities into the
270 coarse ambient corner and distribute the finite sums. The assertion about
271 composition follows from the same substitution at the intermediate object.
272
273 For (L5), each selector either fixes an ambient block or kills it. Applying
274 two selectors therefore retains precisely the intersection. The residual
275 identities follow by subtraction. For (L6), expand each block of \(gf\)
276 through the intermediate resolution. A surviving summand supplies an
277 intermediate address in the relational product. The residual formula is the
278 finite expansion of
279 \((g_F+r_g)(f_E+r_f)-g_Ff_E\).
280
281 For (L7), additivity preserves zero maps and finite sums, functoriality
282 preserves identities and composition, and the splitting comparisons identify
283 the image of every source lane object with the declared target lane object.
284 The profile hypothesis is needed precisely for those identifications and for
285 the refinement equations.
286
287 For (L8), equality of two fold values is equivalent to the difference of the
288 two input families lying in the kernel. Under the selector hypothesis, if
289 \(\Phi_{\kappa,\tau}((b_e)_e)=0\), applying \(Q_e\) gives
290 \(j_{\kappa(e)}\tau_e(b_e)=0\). Both \(j_{\kappa(e)}\) and \(\tau_e\) are
291 injective, hence \(b_e=0\) for every \(e\). The chosen retractions compose
292 with the \(Q_e\) to give the displayed left inverse: its \(e\)-coordinate
293 on the fold is \(r_eQ_ej_{\kappa(e)}\tau_e=1_{B_e}\), while strict
294 separation kills every other coordinate.
295 \end{proof}
296
297 \begin{remark}[Why the fold selectors live in one group]
298 \label{rem:block15-global-fold-typing}
299 The endomorphisms \(Q_e\) in (L8) all act on the single group
300 \(C=\bigoplus_tC_t\). Writing separate selectors on unrelated codomains
301 would make the Kronecker relation ill-typed and would not prove injectivity of
302 the combined fold.
303 \end{remark}
304
305 \begin{proposition}[Exact visible-support loss ledger]
306 \label{prop:block15-visible-support-ledger}
307 Use the finite fold data of (L8) and fix an input family
308 \(b=(b_e)_{e\in E}\). Define
309 \[
310 S_0:=\{e\in E:b_e\ne0\},
311 \qquad
312 A_0:=\{e\in S_0:\tau_e(b_e)=0\},
313 \qquad
314 S_1:=S_0\setminus A_0,
315 \]
316 and let
317 \[
318 \Gamma:=\kappa(S_1)\subseteq T.
319 \]
320 For \(t\in T\), write the folded coordinate as
321 \[
322 \overline b_t
323 :=
324 \sum_{\substack{e\in S_1\\\kappa(e)=t}}\tau_e(b_e)
325 \in C_t,
326 \]
327 and put
328 \[
329 \operatorname{supp}(\overline b)
330 :=\{t\in T:\overline b_t\ne0\},
331 \qquad
332 K_0:=\{t\in\Gamma:\overline b_t=0\}.
333 \]
334 Then
335 \[
336 \boxed{
337 |S_0|-|\operatorname{supp}(\overline b)|
338 =
339 |A_0|
340 +\bigl(|S_1|-|\Gamma|\bigr)
341 +|K_0|.}
342 \]
343 The three terms record, respectively, annihilation by the local maps
344 \(\tau_e\), collision of surviving lane addresses under \(\kappa\), and
345 cancellation among folded values at a common address. If every \(\tau_e\) is
346 injective, then \(A_0=\varnothing\). If globally typed selectors satisfy the
347 strict separation law of (L8), then \(K_0=\varnothing\).
348 \end{proposition}
349
350 \begin{proof}
351 The first partition gives \(|S_0|=|A_0|+|S_1|\). The definition of
352 \(K_0\) gives the disjoint partition
353 \[
354 \Gamma
355 =\operatorname{supp}(\overline b)\sqcup K_0,
356 \]
357 so \(|\Gamma|=|\operatorname{supp}(\overline b)|+|K_0|\). Subtracting the
358 second equality from the first proves the formula.
359
360 Injectivity of \(\tau_e\) makes \(\tau_e(b_e)\ne0\) for every \(e\in S_0\),
361 so there is no annihilation. For strict selectors, suppose
362 \(t\in K_0\) and choose \(e\in S_1\) with \(\kappa(e)=t\). Applying \(Q_e\)
363 to
364 \[
365 j_t\overline b_t
366 =\sum_{\kappa(e')=t}j_t\tau_{e'}(b_{e'})=0
367 \]
368 leaves \(j_t\tau_e(b_e)=0\), contrary to \(e\in S_1\). Hence
369 \(K_0=\varnothing\).
370 \end{proof}
371
372 \subsection{Certified change of resolution and exact loss sequences}
373 \label{subsec:block15-coarsening-loss}
374
375 For resolutions \(s\succeq r\) on \(X\) and \(v\succeq u\) on \(Y\), let
376 \[
377 \mathsf B^{v,s}(X,Y)
378 :=
379 \bigoplus_{b\in I_{Y,v}}
380 \bigoplus_{j\in I_{X,s}}
381 \Hom_{\mathcal C}(X_j^s,Y_b^v),
382 \]
383 and define \(\mathsf B^{u,r}(X,Y)\) similarly. Analysis of a morphism gives
384 an isomorphism
385 \[
386 \mathfrak a^{v,s}_{X,Y}:
387 \Hom_{\mathcal C}(X,Y)\xrightarrow{\sim}
388 \mathsf B^{v,s}(X,Y),
389 \]
390 whose inverse is lane synthesis.
391
392 \begin{proposition}[Certified coarsening is an exact coordinate change]
393 \label{prop:block15-certified-coarsening}
394 The change from fine to coarse block coordinates, canonical relative to the
395 chosen splittings, is
396 \[
397 \Gamma^{(u,r)}_{(v,s)}
398 :=
399 \mathfrak a^{u,r}_{X,Y}
400 \bigl(\mathfrak a^{v,s}_{X,Y}\bigr)^{-1}.
401 \]
402 For a fine matrix \(h=(h_{bj})\), its \((a,i)\)-entry is
403 \[
404 \bigl(\Gamma^{(u,r)}_{(v,s)}h\bigr)_{a i}
405 =
406 \sum_{b,j}
407 \bigl(\pi_{Y,a}^u\iota_{Y,b}^v\bigr)
408 h_{bj}
409 \bigl(\pi_{X,j}^s\iota_{X,i}^r\bigr).
410 \]
411 Only descendants of \(a\) and \(i\) can contribute. The inverse is the
412 corresponding fine analysis after coarse synthesis. Consequently, changing a
413 complete lane resolution loses no information. Loss occurs only after a
414 subsequent selector, quotient, summary, or fold is applied.
415 \end{proposition}
416
417 \begin{proof}
418 The displayed definition is a composite of two isomorphisms from
419 \cref{thm:block15-universal-lane-transport}. Expanding coarse analysis after
420 fine synthesis gives the entry formula. If \(b\) is not a descendant of
421 \(a\), then
422 \(p_{Y,a}^up_{Y,b}^v=0\), hence
423 \(\pi_{Y,a}^u\iota_{Y,b}^v=0\). The source factor vanishes by the same
424 argument when \(j\) is not a descendant of \(i\). Reversing analysis and
425 synthesis produces the inverse.
426 \end{proof}
427
428 \begin{corollary}[Functorial coarsening]
429 \label{cor:block15-functorial-coarsening}
430 For \(t\succeq s\succeq r\) and compatible target resolutions,
431 the certified coordinate changes compose strictly. They also intertwine
432 matrix multiplication. Thus a finite refinement diagram gives a genuine
433 diagram of equivalent matrix-coordinate categories, not merely a family of
434 numerically similar arrays.
435 \end{corollary}
436
437 \begin{theorem}[Abelian fold-loss exact sequence]
438 \label{thm:block15-abelian-fold-exact-sequence}
439 Let \(\mathcal A\) be an abelian category. Suppose a finite family of lane
440 objects \((B_e)_{e\in E}\), target objects \((C_t)_{t\in T}\), and morphisms
441 \(\tau_e:B_e\to C_{\kappa(e)}\) is given. Let
442 \(q_e:\bigoplus_{e'\in E}B_{e'}\to B_e\) be the coordinate projection and
443 define
444 \[
445 \Phi:=\sum_{e\in E}j_{\kappa(e)}\tau_eq_e:
446 \bigoplus_{e\in E}B_e\longrightarrow
447 \bigoplus_{t\in T}C_t.
448 \]
449 Then there are canonical short exact sequences
450 \[
451 0\longrightarrow\ker\Phi
452 \longrightarrow\bigoplus_eB_e
453 \longrightarrow\im\Phi
454 \longrightarrow0
455 \]
456 and
457 \[
458 0\longrightarrow\im\Phi
459 \longrightarrow\bigoplus_tC_t
460 \longrightarrow\coker\Phi
461 \longrightarrow0.
462 \]
463 The first sequence is the exact fold-loss certificate. Suppose every
464 \(\tau_e\) is monic and there are endomorphisms
465 \(Q_e\in\End(\bigoplus_tC_t)\) satisfying
466 \[
467 Q_ej_{\kappa(e')}\tau_{e'}
468 =\delta_{e,e'}j_{\kappa(e')}\tau_{e'}
469 \quad\text{as morphisms }B_{e'}\longrightarrow\bigoplus_tC_t.
470 \]
471 Then \(\Phi\) is monic. If, in addition, there are morphisms
472 \[
473 r_e:\bigoplus_tC_t\longrightarrow B_e,
474 \qquad r_ej_{\kappa(e)}\tau_e=1_{B_e},
475 \]
476 then \(L=(r_eQ_e)_e\) is a left inverse of \(\Phi\). Thus the first exact
477 sequence splits, \(\ker\Phi=0\), and the image inclusion in the second exact
478 sequence also splits.
479 \end{theorem}
480
481 \begin{proof}
482 The two sequences are the kernel--image and image--cokernel factorizations in
483 an abelian category. The selector argument in (L8), interpreted internally
484 in \(\mathcal A\), makes \(\Phi\) monic. The displayed morphism \(L\) is a
485 left inverse by strict separation. Hence the first sequence splits;
486 moreover, \(\Phi L\) is an idempotent with image \(\im\Phi\), so the image
487 inclusion in the second sequence splits as well.
488 \end{proof}
489
490 \begin{boundary}[Coordinate coarsening versus statistic coarsening]
491 \label{bnd:block15-coordinate-vs-statistic-coarsening}
492 The complete fine and coarse block matrices are isomorphic coordinate records.
493 Replacing each coarse block by a dimension, norm, valuation, degree, support
494 bit, or color is a different map. Its kernel or fiber must be computed in the
495 native doctrine. The lane theorem does not make such a statistic complete.
496 \end{boundary}
497
498 \subsection{The matrix category carried by a lane system}
499 \label{subsec:block15-matrix-category}
500
501 \begin{definition}[Lane matrix category at a fixed resolution]
502 \label{def:block15-lane-matrix-category}
503 Let \(\mathcal L_{\mathsf R}\) be the category whose objects are objects of
504 \(\mathcal C\) equipped with full finite profiled lane systems over
505 \(\mathsf R\), with all underlying \(\mathcal C\)-morphisms allowed. For
506 \(r\in\mathsf R\), define
507 \(\operatorname{Mat}_r(\mathcal L_{\mathsf R})\) to have the tagged finite
508 families
509 \([X;(X_i^r)_{i\in I_{X,r}}]\) as objects and rectangular matrices
510 \[
511 (h_{a i}),
512 \qquad h_{a i}:X_i^r\to Y_a^r,
513 \]
514 as morphisms. Composition is matrix contraction and identities are diagonal
515 identity matrices.
516
517 For \(s\succeq r\), define
518 \[
519 \Gamma_{sr}:\operatorname{Mat}_s(\mathcal L_{\mathsf R})
520 \longrightarrow\operatorname{Mat}_r(\mathcal L_{\mathsf R})
521 \]
522 by replacing each object tag with its \(r\)-tag and sending a fine matrix to
523 the certified source-and-target coordinate change of
524 \cref{prop:block15-certified-coarsening}.
525 \end{definition}
526
527 \begin{theorem}[Fixed-resolution matrix-category equivalence]
528 \label{thm:block15-matrix-category-equivalence}
529 The functor
530 \[
531 \mathfrak M_r:\mathcal L_{\mathsf R}\longrightarrow
532 \operatorname{Mat}_r(\mathcal L_{\mathsf R}),
533 \qquad
534 X\longmapsto[X;(X_i^r)_i],
535 \qquad
536 f\longmapsto([f]_{a i}^{r,r}),
537 \]
538 is an equivalence. A quasi-inverse returns the lane-decorated object named by
539 the tag and sends a matrix to
540 \[
541 \sum_{a,i}\iota_{Y,a}^r h_{a i}\pi_{X,i}^r.
542 \]
543 For every \(s\succeq r\), the coordinate changes are functors and satisfy
544 \[
545 \Gamma_{sr}\mathfrak M_s=\mathfrak M_r.
546 \]
547 For \(t\succeq s\succeq r\), they also satisfy
548 \[
549 \Gamma_{tr}=\Gamma_{sr}\Gamma_{ts}.
550 \]
551 Thus the equivalences are compatible with every certified change of
552 resolution.
553 \end{theorem}
554
555 \begin{proof}
556 The unique lane matrix and composition clauses of
557 \cref{thm:block15-universal-lane-transport} show that \(\mathfrak M_r\) is
558 fully faithful. Every object of the displayed matrix category is, by
559 definition, the lane family of an object of \(\mathcal L_{\mathsf R}\), so it is
560 essentially surjective. Analysis and synthesis furnish the unit and counit
561 isomorphisms. Each \(\Gamma_{sr}\) is conjugation by exact analysis and
562 synthesis, so it preserves identities and matrix composition. The two
563 displayed identities follow from cancellation of adjacent analysis--synthesis
564 pairs, equivalently from functorial coarsening in
565 \cref{cor:block15-functorial-coarsening}.
566 \end{proof}
567
568 \begin{remark}[No dimension claim]
569 \label{rem:block15-address-count-not-dimension}
570 The number \(|I_{X,r}|\) counts declared addresses. A lane object can have
571 arbitrary dimension, rank, length, measure, or entropy, including zero where
572 the ambient doctrine permits it. Matrix equivalence therefore does not
573 identify address count with any of those invariants.
574 \end{remark}
575
576 \subsection{Multilinear and specified-polynomial transport}
577 \label{subsec:block15-multilinear}
578
579 The additive theorem does not automatically govern arbitrary nonlinear maps.
580 There is, however, an exact extension in the category of modules when the
581 multilinear pieces are supplied as data.
582
583 \begin{theorem}[Module multilinear lane expansion]
584 \label{thm:block15-multilinear-lane-expansion}
585 Let \(\kk\) be a commutative ring. Let
586 \[
587 X^{(1)},\ldots,X^{(d)},Y
588 \]
589 be \(\kk\)-modules with finite split lane systems, and let
590 \[
591 T:X^{(1)}\times\cdots\times X^{(d)}\longrightarrow Y
592 \]
593 be a specified \(\kk\)-multilinear map. Define
594 \[
595 T_{a;i_1,\ldots,i_d}
596 :=
597 \pi_{Y,a}T
598 (\iota_{1,i_1}-,\ldots,\iota_{d,i_d}-).
599 \]
600 Then
601 \[
602 T(x_1,\ldots,x_d)
603 =
604 \sum_{a,i_1,\ldots,i_d}
605 \iota_{Y,a}
606 T_{a;i_1,\ldots,i_d}
607 (\pi_{1,i_1}x_1,\ldots,\pi_{d,i_d}x_d).
608 \]
609 Substitution of multilinear maps is governed by finite contraction over every
610 intermediate lane address.
611
612 Separately, let \(X,Y\) be \(\kk\)-modules with finite split lane systems and
613 suppose a polynomial map is presented with specified data
614 \[
615 P(x)=T_0+T_1(x)+T_2(x,x)+\cdots+T_D(x,\ldots,x),
616 \]
617 where
618 \[
619 T_0\in Y,
620 \qquad
621 T_n:X^n\longrightarrow Y\quad(1\le n\le D)
622 \]
623 and every \(T_n\) is a supplied multilinear map. Then
624 \[
625 T_0=\sum_a\iota_{Y,a}\pi_{Y,a}(T_0),
626 \]
627 and adding this degree-zero decomposition to the displayed multilinear
628 expansions gives an exact lane expansion of \(P\).
629 \end{theorem}
630
631 \begin{proof}
632 Insert \(x_\ell=\sum_{i_\ell}p_{\ell,i_\ell}x_\ell\) in every input, use
633 multilinearity to distribute the finite sums, and insert
634 \(1_Y=\sum_a p_{Y,a}\) in the output. The coordinate formula follows from
635 the chosen splittings. Repeating the calculation after substitution gives
636 the contraction law. The degree-zero identity is output synthesis applied
637 to \(T_0\); the polynomial statement is then a finite sum of the specified
638 homogeneous pieces.
639 \end{proof}
640
641 \begin{boundary}[The nonlinear doctrine must be specified]
642 \label{bnd:block15-multilinear-boundary}
643 Over a general commutative ring, a polynomial function need not determine a
644 unique symmetric multilinear polarization. Infinite analytic expansions also
645 require a declared topology and convergence theorem. Therefore
646 \cref{thm:block15-multilinear-lane-expansion} is stated for supplied
647 multilinear maps and supplied finite polynomial data. It does not assert a
648 canonical lane calculus for every nonlinear category.
649 \end{boundary}
650
651 \subsection{Factorial lanes and residue packets}
652 \label{subsec:block15-factorial-realization}
653
654 The factorial construction is an exact arithmetic realization of the abstract
655 lane mechanism. It is useful because the addresses, refinement maps, Fourier
656 projectors, and hypergeometric coordinates can all be written explicitly.
657
658 For integers \(N\ge1\) and \(n\ge0\), define the step factorial
659 \[
660 (a)_{n;N}:=\prod_{k=0}^{n-1}(a+Nk),
661 \qquad (a)_{0;N}:=1.
662 \]
663 For a commutative ring \(A\) and a formal series
664 \(F(z)=\sum_{m\ge0}a_mz^m\in A[[z]]\), define its residue lane
665 \[
666 \mathcal P_{N,j}F(z)
667 :=
668 \sum_{\substack{m\ge0\\m\equiv j\ (\mathrm{mod}\ N)}}a_mz^m,
669 \qquad 0\le j<N.
670 \]
671
672 \begin{theorem}[Exact factorial--residue realization]
673 \label{thm:block15-factorial-residue-realization}
674 Let \(N,c,n\in\mathbb Z\) with \(N\ge1\), \(c\ge0\), and \(n\ge0\).
675 Then
676 \[
677 \boxed{
678 \frac{(Nn+c)!}{c!}
679 =
680 \prod_{r=c+1}^{c+N}(r)_{n;N}.}
681 \]
682 Each integer factor from \(c+1\) through \(c+Nn\) occurs in exactly one
683 lane. For every commutative ring \(A\), on the \(A\)-module \(A[[z]]\) the
684 operators
685 \((\mathcal P_{N,j})_{0\le j<N}\) satisfy
686 \[
687 \mathcal P_{N,j}^2=\mathcal P_{N,j},
688 \qquad
689 \mathcal P_{N,j}\mathcal P_{N,k}=0\ (j\ne k),
690 \qquad
691 \sum_{j=0}^{N-1}\mathcal P_{N,j}=1.
692 \]
693 If \(M\in\mathbb Z\) and \(M\ge1\), their exact refinement law is
694 \[
695 \mathcal P_{N,j}
696 =
697 \sum_{\ell=0}^{M-1}\mathcal P_{NM,j+\ell N}.
698 \]
699
700 Suppose further that \(K\) is a field, that \(N\) is invertible in \(K\),
701 and that \(K\) contains a primitive \(N\)-th root of unity \(\omega\). Then
702 for every \(F\in K[[z]]\),
703 \[
704 \mathcal P_{N,j}F(z)
705 =
706 \frac1N\sum_{\ell=0}^{N-1}
707 \omega^{-j\ell}F(\omega^\ell z).
708 \]
709 If, in addition, \(K\) has characteristic zero, the exponential and
710 hypergeometric series below are defined in \(K[[z]]\). Put
711 \[
712 E_{N,j}(z)
713 :=\mathcal P_{N,j}e^z
714 =\sum_{n\ge0}\frac{z^{Nn+j}}{(Nn+j)!}.
715 \]
716 If
717 \[
718 \mathbf b_{N,j}
719 :=
720 \left\{
721 \frac{j+r}{N}:1\le r\le N,
722 \ r\ne N-j
723 \right\},
724 \]
725 then
726 \[
727 E_{N,j}(z)
728 =
729 \frac{z^j}{j!}
730 {}_0F_{N-1}
731 \left(
732 \begin{matrix}-\\ \mathbf b_{N,j}\end{matrix};
733 \frac{z^N}{N^N}
734 \right).
735 \]
736 Thus coefficient-residue, root-of-unity, and hypergeometric descriptions are
737 exact additive coordinate realizations of one residue-address decomposition.
738 The step-factorial identity is an exact multiplicative companion with the
739 same address arithmetic; it is not asserted to be an additive idempotent
740 decomposition of the factorial.
741 \end{theorem}
742
743 \begin{proof}
744 Every integer \(m\) with \(c<m\le c+Nn\) has a unique representation
745 \(m=r+Nk\) with \(c+1\le r\le c+N\) and \(0\le k<n\). Multiplying these
746 disjoint factors proves the factorial identity.
747
748 The projector laws follow coefficient by coefficient. The residue classes
749 modulo \(NM\) lying over \(j\pmod N\) are precisely
750 \(j,j+N,\ldots,j+(M-1)N\), which proves refinement. Character
751 orthogonality gives the Fourier formula. Finally,
752 \[
753 (Nn+j)!
754 =
755 j!\,N^{Nn}
756 \prod_{r=1}^{N}\left(\frac{j+r}{N}\right)_n.
757 \]
758 Exactly one factor in the product is \((1)_n=n!\). Removing it leaves the
759 parameter set \(\mathbf b_{N,j}\) and gives the hypergeometric series.
760 \end{proof}
761
762 \begin{corollary}[Factorial-lane genealogy]
763 \label{cor:block15-factorial-genealogy}
764 The step-factorial split supplies an exact multiplicative partition of the
765 factor set, while the residue projectors supply an exact additive partition of
766 the coefficient series. The residue projectors instantiate
767 \cref{thm:block15-universal-lane-transport} directly. The step-factorial
768 product is realized by the supplied finite multilinear pointwise
769 multiplication map on the module of lane sequences, as in
770 \cref{thm:block15-multilinear-lane-expansion}. Their common address
771 refinement is divisibility of the modulus. Hence the additive transport law
772 and the multiplicative companion share exact address-refinement
773 combinatorics, without identifying a product factorization with an additive
774 idempotent splitting.
775 \end{corollary}
776
777 \subsection{Typed native specializations}
778 \label{subsec:block15-specializations}
779
780 The next statements identify concrete realizations and record the hypotheses
781 that make each use of the theorem legal. They do not identify the surrounding
782 strata with one another.
783
784 \subsubsection{Fourier and polyphase lanes}
785
786 \begin{proposition}[Typed polyphase realization]
787 \label{prop:block15-polyphase-specialization}
788 Let \(K\) be a field, let \(N\in\mathbb Z\) with \(N\ge1\) be invertible in \(K\), and suppose
789 \(K\) contains a primitive \(N\)-th root of unity. For
790 \(F(z)=\sum_{n\ge0}a_nz^n\in K[[z]]\), set
791 \[
792 F_j(w):=\sum_{n\ge0}a_{Nn+j}w^n.
793 \]
794 Then
795 \[
796 F(z)=\sum_{j=0}^{N-1}z^jF_j(z^N)
797 \]
798 is exact analysis and synthesis. The Fourier residue projectors and the
799 polyphase components satisfy the explicit coordinate relation
800 \[
801 \mathcal P_{N,j}F(z)=z^jF_j(z^N).
802 \]
803 For every integer \(M\ge1\), refinement from \(N\) to \(NM\) is the
804 projector-sum law of
805 \cref{thm:block15-factorial-residue-realization}.
806 \end{proposition}
807
808 \begin{proof}
809 Every exponent has a unique quotient and remainder on division by \(N\).
810 The Fourier formula in
811 \cref{thm:block15-factorial-residue-realization} identifies the same
812 coefficient sections with character projectors.
813 \end{proof}
814
815 \subsubsection{Cartier and fixed-radix lanes}
816
817 \begin{proposition}[Typed Cartier realization]
818 \label{prop:block15-cartier-specialization}
819 Let \(K\) be a field and let \(k\ge2\). Work with \(K\)-valued formal
820 series and fix the least-significant-digit-first convention. Define
821 \[
822 \Lambda_d\left(\sum_{n\ge0}a_nz^n\right)
823 :=\sum_{n\ge0}a_{kn+d}z^n,
824 \qquad
825 S_d(G):=z^dG(z^k),
826 \quad 0\le d<k.
827 \]
828 Then
829 \[
830 \Lambda_dS_e=\delta_{de}1,
831 \qquad
832 \sum_{d=0}^{k-1}S_d\Lambda_d=1.
833 \]
834 For a digit word \(w=d_0d_1\cdots d_{a-1}\), the iterated Cartier lane is
835 \[
836 \Lambda_{d_{a-1}}\cdots\Lambda_{d_1}\Lambda_{d_0}F.
837 \]
838 It selects coefficients with index
839 \[
840 k^an+[w]_k,
841 \qquad
842 [w]_k=d_0+kd_1+\cdots+k^{a-1}d_{a-1}.
843 \]
844 Concatenation gives strict radix refinement and the lane path law.
845 \end{proposition}
846
847 \begin{proof}
848 The first identities follow by coefficient extraction and unique quotient and
849 remainder. Iterating in the stated reading convention gives the displayed
850 address, and concatenation composes the affine index maps.
851 \end{proof}
852
853 \subsubsection{Holonomic lanes}
854
855 \begin{proposition}[Typed holonomic realization]
856 \label{prop:block15-holonomic-specialization}
857 Let \(K\) be a characteristic-zero field and let the \(K\)-valued sequence
858 \((u_n)\) satisfy a linear
859 recurrence with polynomial coefficients. Beyond a finite singular prefix,
860 write the recurrence as a finite-dimensional rational nonautonomous state
861 model
862 \[
863 v_{n+1}=A(n)v_n,
864 \qquad A(n)\in\operatorname{Mat}_d(K(n)).
865 \]
866 For a fixed integer \(N\ge1\) and residue \(0\le j<N\), the lane state
867 \(w_m=v_{Nm+j}\) evolves by the exact \(N\)-step rational transfer
868 \[
869 w_{m+1}
870 =
871 A(Nm+j+N-1)\cdots A(Nm+j)w_m
872 \]
873 whenever the displayed factors are defined. Equivalently, residue
874 multisection of a D-finite generating series gives D-finite lanes. The finite
875 singular prefix and any exceptional denominators remain explicit data.
876 \end{proposition}
877
878 \begin{proof}
879 Iterate the state equation \(N\) times. Closure of D-finite series under
880 scaling the variable, finite sums, and root-of-unity multisection gives the
881 equivalent generating-series statement after a field extension containing the
882 needed roots. No autonomous finite-state claim is used.
883 \end{proof}
884
885 \subsubsection{Local Newton--Mahler lanes}
886
887 \begin{proposition}[Typed local clopen realization]
888 \label{prop:block15-local-specialization}
889 Fix a prime \(p\) and an integer \(a\ge0\). For
890 \(f\in C(\mathbb Z_p,\mathbb Z_p)\), with \(q\in\mathbb Z_p\) the branch
891 coordinate, define
892 \[
893 \Analysis_{p^a}(f)
894 :=
895 \bigl(q\mapsto f(p^aq+s)\bigr)_{0\le s<p^a}.
896 \]
897 Piecewise synthesis on the disjoint clopen cosets
898 \(s+p^a\mathbb Z_p\) is its inverse. Refining from \(p^a\) to
899 \(p^{a+b}\), for every integer \(b\ge0\), gives the exact child-address and
900 mixed-radix composition law.
901 Let
902 \[
903 \mathcal M:=\mathcal M_p^{-1}:C(\mathbb Z_p,\mathbb Z_p)
904 \xrightarrow{\sim}c_0(\mathbb Z_p)
905 \]
906 be Mahler analysis from \cref{thm:block08-mahler-coordinate}, and write
907 \(R_{p^a,s}f(q):=f(p^aq+s)\). Conjugation gives the exact coefficient
908 operator
909 \[
910 \mathcal T_{p^a,s}
911 :=\mathcal M R_{p^a,s}\mathcal M^{-1}:
912 c_0(\mathbb Z_p)\longrightarrow c_0(\mathbb Z_p),
913 \]
914 whose affine kernel is computed in \cref{thm:block08-affine-transfer}. Its
915 mixed-radix composition is \cref{thm:block08-kernel-composition}.
916
917 The assertion of complete clopen analysis is restricted to these
918 prime-power packets. More general affine coefficient kernels may still
919 compose according to their declared mixed-radix law, but an arbitrary integer
920 modulus does not automatically partition \(\mathbb Z_p\) into that many
921 disjoint clopen branches.
922 \end{proposition}
923
924 \begin{proof}
925 The \(p^a\) cosets are disjoint, clopen, and cover \(\mathbb Z_p\). Restricting
926 after piecewise synthesis and synthesizing after restriction are identities.
927 Writing a child address as \(s+p^at\) proves refinement. The cited Mahler
928 isomorphism makes the displayed conjugation exact, and the two cited kernel
929 theorems give its coefficient formula and composition law.
930 \end{proof}
931
932 \subsubsection{Nonlinear tree lanes}
933
934 \begin{proposition}[Typed Fuss--Catalan realization]
935 \label{prop:block15-tree-specialization}
936 Let \(K\) be a characteristic-zero field, let \(q\in\mathbb Z\) with
937 \(q\ge2\), and let
938 \(\alpha\in K^\times\). The uniquely marked formal solution of
939 \[
940 U=z+\alpha U^q,
941 \qquad U(0)=0,
942 \]
943 has support
944 \[
945 [z^{1+(q-1)n}]U
946 =\frac{1}{(q-1)n+1}\binom{qn}{n}\alpha^n
947 \ne0
948 \qquad(n\ge0),
949 \]
950 and every other coefficient is zero. Thus its support is exactly the set of
951 degrees congruent to \(1\pmod{q-1}\).
952 For an integer packet width \(N\ge1\), set
953 \(g=\gcd(N,q-1)\). Exactly \(N/g\) residue addresses are active, namely
954 the congruence class \(1\pmod g\). Packetizing the specified multilinear
955 map \((U_1,\ldots,U_q)\mapsto U_1\cdots U_q\) gives the exact finite
956 carry-convolution system supplied by
957 \cref{thm:block15-multilinear-lane-expansion}. On a cyclic orbit of order
958 \(q-1\), the power map used for packet synthesis has
959 \[
960 \frac{q-1}{\gcd(N,q-1)}
961 \]
962 distinct images. If a fixed embedding \(K\hookrightarrow\mathbb C\) sends
963 \(\alpha\) to a positive real number and the marked branch is interpreted in
964 the smooth implicit analytic schema, its critical points and values satisfy
965 \[
966 q\alpha\tau^{q-1}=1,
967 \qquad
968 \rho=\tau-\alpha\tau^q=\frac{q-1}{q}\tau.
969 \]
970 The resulting orbit \(\rho\mu_{q-1}\) is precisely the dominant singularity
971 orbit, and packetization leaves \((q-1)/g\) distinct images.
972 \end{proposition}
973
974 \begin{proof}
975 Lagrange inversion gives the displayed coefficient formula and zero at every
976 other degree. Characteristic zero and \(\alpha\ne0\) make every displayed
977 coefficient nonzero. Their residues modulo \(N\) form the coset of the subgroup
978 generated by \(q-1\), whose size is \(N/g\). Multilinear lane expansion of
979 the product gives the packet equation, including the power of the packet
980 variable produced by the quotient in residue addition. On the cyclic group
981 of order \(q-1\), the kernel of multiplication by \(N\) has order \(g\), so
982 the image has order \((q-1)/g\). The critical equations give the displayed
983 values, while \cref{thm:block11-dominant-orbit} identifies their full orbit as
984 the dominant one under the stated analytic hypotheses.
985 \end{proof}
986
987 \subsubsection{Algebraic branch lanes}
988
989 \begin{proposition}[Typed cyclic-radical realization]
990 \label{prop:block15-algebraic-specialization}
991 Let \(K\) be a characteristic-zero field containing \(\mu_d\) and a
992 primitive \(N\)-th root of unity \(\omega\), let
993 \(d,m,N\in\mathbb Z_{\ge1}\), and choose
994 the formal branch
995 \[
996 F(z)=(1-\alpha z^m)^{-1/d},
997 \qquad \alpha\in K^\times.
998 \]
999 With \(g=\gcd(N,m)\), its nonzero coefficients occupy exactly the subgroup of
1000 \(\mathbb Z/N\mathbb Z\) generated by \(m\), which has \(N/g\) addresses.
1001 The rotated radicands
1002 \[
1003 1-\alpha\omega^{jm}z^m,
1004 \qquad 0\le j<N,
1005 \]
1006 also have exactly \(N/g\) distinct values.
1007
1008 If, in addition, their distinct Kummer classes generate a subgroup isomorphic
1009 to \((\mathbb Z/d\mathbb Z)^{N/g}\) in the Kummer quotient
1010 \[
1011 K(z)^\times/K(z)^{\times d},
1012 \]
1013 then the compositum of the corresponding radical branch fields has degree
1014 \[
1015 d^{N/g}
1016 \]
1017 over \(K(z)\). Without that independence hypothesis, the lane orbit count
1018 remains exact but the degree formula is only an upper bound.
1019 \end{proposition}
1020
1021 \begin{proof}
1022 The binomial series is supported at exponents \(mn\). The cyclic subgroup
1023 calculation gives both address and rotation counts. The degree statement is
1024 the standard Kummer independence calculation for the explicitly listed
1025 classes. A relation among the classes produces a field collision not detected
1026 by address count alone.
1027 \end{proof}
1028
1029 \subsubsection{Finite Galois lanes}
1030
1031 \begin{proposition}[Typed semisimple Galois realization]
1032 \label{prop:block15-galois-specialization}
1033 Let \(G\) be finite and let \(K\) be a characteristic-zero splitting field
1034 for \(G\). The primitive central idempotents
1035 \[
1036 e_\chi
1037 =
1038 \frac{\chi(1)}{|G|}
1039 \sum_{g\in G}\chi(g^{-1})g
1040 \in K[G]
1041 \]
1042 for \(\chi\in\operatorname{Irr}_K(G)\) form a complete
1043 pairwise-annihilating lane system on every finite-dimensional
1044 semisimple \(K[G]\)-module \(V\):
1045 \[
1046 V=\bigoplus_{\chi\in\operatorname{Irr}_K(G)} e_\chi V.
1047 \]
1048 Every \(G\)-equivariant map is block diagonal in these isotypic lanes, while
1049 an arbitrary \(K\)-linear map has the full lane matrix of
1050 \cref{thm:block15-universal-lane-transport}.
1051
1052 For a subgroup \(H\le G\), the Reynolds operator
1053 \[
1054 e_H=\frac1{|H|}\sum_{h\in H}h
1055 \]
1056 is an idempotent projector onto \(V^H\); equivalently,
1057 \((e_H,1-e_H)\) is a two-lane system on the underlying \(K\)-vector space.
1058 It is not in general a Boolean
1059 selector formed from the isotypic projectors above. Projectors belonging to unrelated
1060 subgroups need not annihilate one another, so they do not automatically form
1061 one lane system. Transport through induction, restriction, or subgroup
1062 refinement requires the corresponding Mackey or double-coset data.
1063 \end{proposition}
1064
1065 \begin{proof}
1066 Maschke semisimplicity and the character idempotent relations give the first
1067 decomposition. An equivariant map commutes with the center of \(K[G]\), hence
1068 with every \(e_\chi\). Averaging proves that \(e_H\) is idempotent with image
1069 \(V^H\). Two subgroup averages generally fail the pairwise-annihilation
1070 axiom, which proves the stated boundary.
1071 \end{proof}
1072
1073 \subsection{Descent of lane systems through a finite atlas}
1074 \label{subsec:block15-lane-descent}
1075
1076 The local theorem becomes global only when the addresses and splittings glue
1077 without address holonomy. The following statement makes those additional
1078 hypotheses explicit.
1079
1080 \begin{theorem}[Finite atlas descent for lane transport]
1081 \label{thm:block15-lane-descent}
1082 Let \(\mathfrak R\) be a finite profiled atlas whose participating chart
1083 categories are additive and idempotent-complete, with additive transition
1084 functors \(F_{UV}:\mathfrak R(U)\to\mathfrak R(V)\) on its declared
1085 overlaps. Let
1086 \[
1087 X=(X_U,\theta^X_{UV}),
1088 \qquad
1089 Y=(Y_U,\theta^Y_{UV}),
1090 \qquad
1091 Z=(Z_U,\theta^Z_{UV})
1092 \]
1093 be three compatible descent objects. Thus the transition isomorphisms satisfy
1094 the identity and cocycle equations. Let
1095 \[
1096 f=(f_U):X\longrightarrow Y,
1097 \qquad
1098 g=(g_U):Y\longrightarrow Z
1099 \]
1100 be compatible descended morphisms.
1101
1102 Fix one finite resolution shape \(\mathsf R\). Suppose every local object
1103 \(A_U\), for \(A\in\{X,Y,Z\}\), carries a finite profiled lane system over
1104 \(\mathsf R\). For every overlap, every \(r\in\mathsf R\), and every such
1105 \(A\), suppose there is an address bijection
1106 \[
1107 \lambda_{UV}^{A,r}:
1108 I_{A_U,r}\xrightarrow{\sim}I_{A_V,r}
1109 \]
1110 such that
1111 \[
1112 \lambda_{UU}^{A,r}=1,
1113 \qquad
1114 \lambda_{UT}^{A,r}
1115 =\lambda_{VT}^{A,r}\lambda_{UV}^{A,r},
1116 \]
1117 on every triple overlap \((U,V,T)\), and, for \(s\succeq r\),
1118 \[
1119 \rho_{sr}^{A_V}\lambda_{UV}^{A,s}
1120 =
1121 \lambda_{UV}^{A,r}\rho_{sr}^{A_U}.
1122 \]
1123 Require trivial address holonomy: for every \(A\) and \(r\), there is a
1124 global finite address set \(I_{A,r}\), a global refinement map
1125 \(\rho_{sr}^{A}:I_{A,s}\twoheadrightarrow I_{A,r}\), and bijections
1126 \[
1127 \mu_U^{A,r}:I_{A_U,r}\xrightarrow{\sim}I_{A,r}
1128 \]
1129 such that
1130 \[
1131 \mu_V^{A,r}\lambda_{UV}^{A,r}=\mu_U^{A,r},
1132 \qquad
1133 \mu_U^{A,r}\rho_{sr}^{A_U}
1134 =\rho_{sr}^{A}\mu_U^{A,s}.
1135 \]
1136 Assume also that the transition isomorphisms intertwine the local projectors:
1137 \[
1138 \theta^A_{UV}
1139 F_{UV}(p_{A_U,i}^r)
1140 =
1141 p_{A_V,\lambda_{UV}^{A,r}(i)}^r
1142 \theta^A_{UV},
1143 \]
1144 and that the verified transition profiles preserve the chosen splittings,
1145 finite sums, composition, and refinement equations, with coherent splitting
1146 comparisons on triple overlaps.
1147
1148 Then:
1149 \begin{enumerate}[label=\textup{(D\arabic*)}]
1150 \item after relabeling by the \(\mu_U^{A,r}\), each local lane and its chosen
1151 splitting define a lane summand in \(\Desc(\mathfrak R)\), and the global
1152 addresses carry the declared projector-sum refinement;
1153 \item the local matrices \(([f_U]_{a i})\), \(([g_U]_{c a})\), and
1154 \(([g_Uf_U]_{c i})\) glue after the prescribed address relabelings and
1155 splitting comparisons;
1156 \item the descended matrices satisfy
1157 \[
1158 [gf]_{c i}=\sum_a[g]_{c a}[f]_{a i};
1159 \]
1160 \item every compatible family of support selectors and named residuals
1161 descends, and every compatible refinement square remains a projector-sum
1162 refinement square in the descent category;
1163 \item every fold whose source objects, target objects, and structure maps are
1164 compatible descent data defines a fold in \(\Desc(\mathfrak R)\). Compatible
1165 selectors and left inverses descend, so a split-losslessness certificate
1166 descends directly from its left-inverse identity. Moreover, suppose the
1167 relevant local kernels \(K_U=\ker(\Phi_U)\) exist, every transition functor
1168 preserves them, and there are coherent comparison isomorphisms
1169 \[
1170 \eta_{UV}:F_{UV}(K_U)\xrightarrow{\sim}K_V
1171 \]
1172 compatible with the kernel inclusions and satisfying the triple-overlap
1173 cocycle. Then the global kernel exists and is computed chartwise:
1174 \[
1175 \bigl(\ker_{\Desc(\mathfrak R)}\Phi\bigr)_U
1176 \cong
1177 \ker_{\mathfrak R(U)}(\Phi_U).
1178 \]
1179 \end{enumerate}
1180 \end{theorem}
1181
1182 \begin{proof}
1183 For a global address \(i\in I_{A,r}\), use the local projector indexed by
1184 \((\mu_U^{A,r})^{-1}(i)\). The trivialization identity makes these projectors
1185 correspond under the transition isomorphisms on every overlap; its refinement
1186 identity makes their local
1187 projector-sum laws agree. The coherent splitting comparisons make the
1188 corresponding inclusions and projections descent morphisms. Finite
1189 biproducts in the descent category are computed chartwise, so local analysis
1190 and synthesis glue and remain mutually inverse.
1191
1192 Compatibility of \(f\) and \(g\), followed by the splitting comparisons,
1193 shows that their local coordinate blocks agree on overlaps after applying the
1194 specified address relabelings. Hence the matrices descend. Matrix
1195 multiplication is a finite sum of compositions, both computed chartwise, so
1196 the local path law glues to the displayed global law. The same argument
1197 applies to projector sums, selectors, and residual differences.
1198
1199 Finally, a compatible fold is a morphism in the relevant descent category.
1200 Compatible selectors and left inverses glue, and their identities can be
1201 checked chartwise. Under the additional kernel hypotheses, the objects
1202 \((K_U,\eta_{UV})\) form a descent object; compatibility with the local kernel
1203 inclusions gives a global morphism into the fold source. Its universal
1204 property is checked in each chart, which proves the displayed chartwise
1205 kernel identity. The split case needs no kernel-preservation hypothesis:
1206 the compatible local left inverses glue directly.
1207 \end{proof}
1208
1209 \begin{corollary}[Certified atlas lane transport]
1210 \label{cor:block15-certified-atlas-lane-transport}
1211 Let \(\mathfrak A_{\mathrm{cert}}\) be the certified finite atlas of this
1212 manuscript. On every subatlas whose passports include additive split-lane
1213 systems, compatible refinement maps, coherent address relabelings with
1214 trivial address holonomy, and the required preservation profile, the
1215 Universal Lane Transport Theorem holds in the descent category. Kernel
1216 claims additionally require the kernel-preservation and coherence data in
1217 \cref{thm:block15-lane-descent}. In particular, any of the typed
1218 specializations above may be transported across a certified reversible
1219 overlap after its native hypotheses, address trivializations, and splitting
1220 cocycles have been checked.
1221 \end{corollary}
1222
1223 \begin{proof}
1224 Apply \cref{thm:block15-lane-descent} to the verified subatlas. The conclusion
1225 is deliberately restricted to the overlaps whose passports contain all of
1226 the listed data.
1227 \end{proof}
1228
1229 \begin{boundary}[Descent is conditional on address coherence]
1230 \label{bnd:block15-descent-boundary}
1231 An equivalence of underlying semantic objects does not by itself identify two
1232 lane systems. Without the bijections \(\lambda_{UV}^{A,r}\), their cocycle
1233 law, compatible global trivializations \(\mu_U^{A,r}\), refinement
1234 compatibility, and coherent splitting comparisons, the local matrices need
1235 not glue as ordinary globally addressed lanes. Nontrivial address holonomy
1236 can permute lanes around a loop; then only invariant orbit sums, or lanes in a
1237 separately defined local-system-valued category, may descend. The theorem
1238 above verifies ordinary descent under trivial holonomy. It does not
1239 manufacture missing lane passports for an arbitrary heterogeneous atlas.
1240 \end{boundary}
1241
1242 \subsection{Sharp boundaries and a finite counterexample}
1243 \label{subsec:block15-boundaries}
1244
1245 \begin{proposition}[Endpoint selection does not implement refinement]
1246 \label{prop:block15-endpoint-counterexample}
1247 Let \(K\) be a field and let \(X=K^2\). At the coarse resolution use the
1248 single projector \(p=1_X\). At the fine resolution use
1249 \[
1250 p_1=
1251 \begin{pmatrix}1&0\\0&0\end{pmatrix},
1252 \qquad
1253 p_2=
1254 \begin{pmatrix}0&0\\0&1\end{pmatrix},
1255 \qquad p=p_1+p_2.
1256 \]
1257 For
1258 \[
1259 f=p_2,
1260 \]
1261 the unique coarse block is \(pfp=f\ne0\), whereas selecting the single fine
1262 endpoint \((p_1,p_1)\) gives \(p_1fp_1=0\). Therefore a coarse block is the
1263 sum over all compatible descendant source-target pairs. It cannot in general
1264 be represented by choosing one fine endpoint.
1265 \end{proposition}
1266
1267 \begin{proof}
1268 The displayed matrix multiplication gives the two values immediately. The
1269 full refinement identity recovers
1270 \(f=\sum_{a,i\in\{1,2\}}p_afp_i\), whose only nonzero term here is
1271 \(p_2fp_2\).
1272 \end{proof}
1273
1274 \begin{boundary}[Finite profiled meaning of ``universal'']
1275 \label{bnd:block15-universal-boundary}
1276 The theorem proves a common calculus for finite split lanes in additive
1277 categories and for the explicitly stated profile extensions. It does not
1278 assert any of the following:
1279 \begin{enumerate}
1280 \item that every mathematical object has a canonical or minimal lane system;
1281 \item that countably infinite lane sums converge without a topology and a
1282 convergence theorem;
1283 \item that arbitrary nonlinear, probabilistic, operator-algebraic, or
1284 homotopical constructions preserve additive lane identities;
1285 \item that address count equals vector-space dimension, module rank,
1286 information, entropy, algebraic degree, or computational complexity;
1287 \item that a support pattern, heatmap, norm profile, valuation profile, or
1288 orbit count is a complete invariant;
1289 \item that native invariants in different strata are equal merely because
1290 their formulas contain the same gcd or residue operation;
1291 \item that the theorem supplies historical novelty evidence or external
1292 validation.
1293 \end{enumerate}
1294 Each stronger conclusion requires a native theorem and a preservation
1295 certificate.
1296 \end{boundary}
1297
1298 \begin{remark}[Classical core and present synthesis]
1299 \label{rem:block15-classical-core}
1300 Finite biproduct coordinates, Peirce decompositions, block-matrix
1301 multiplication, residue filters, and polyphase identities have classical
1302 antecedents. The theorem packages that core with explicit address refinement,
1303 profile-controlled realization, named residuals, exact fold kernels, and
1304 typed descent. This manuscript treats the resulting assembly as an internal
1305 mathematical contribution. It does not infer a priority claim without a
1306 separate literature study.
1307 \end{remark}
1308
1309 \subsection{Exact finite validation and interpretation}
1310 \label{subsec:block15-validation}
1311
1312 The accompanying verifier is an exact finite regression suite for selected
1313 implementation clauses. It checks integer and rational block reconstruction,
1314 matrix composition, refinement aggregation, support and residual identities,
1315 fold collision kernels, factorial-lane partitions, residue-projector
1316 refinement, and explicit negative controls. The proofs above do not depend on
1317 finite sampling. Conversely, the symbolic proofs do not certify that a
1318 particular program implements the formulas correctly. The two records serve
1319 different purposes.
1320
1321 \IfFileExists{generated/block15_validation_table.tex}{%
1322 \input{generated/block15_validation_table.tex}%
1323 }{%
1324 \begin{table}[htbp]
1325 \centering
1326 \caption{Exact finite regression for selected Universal Lane Transport
1327 implementation clauses. The generated validation table is inserted when the
1328 verifier has been run.}
1329 \label{tab:block15-lane-transport-validation-placeholder}
1330 \begin{tabular}{@{}ll@{}}
1331 \toprule
1332 Record & Status\\
1333 \midrule
1334 Machine-readable validation & Run the Block 15 verifier\\
1335 \bottomrule
1336 \end{tabular}
1337 \end{table}%
1338 }
1339
1340 \begin{resultbox}
1341 \textbf{Universal Lane Transport result.}
1342 Finite split lane systems admit exact analysis and synthesis, unique transfer
1343 matrices, path composition, strict projector-sum refinement, Boolean support
1344 selectors, named residuals, and exact fold-loss kernels. Complete changes of
1345 resolution are coordinate equivalences. In abelian targets, fold loss sits in
1346 a canonical short exact sequence. In module targets, specified multilinear
1347 and finite polynomial operations expand lane by lane. Residue/Fourier,
1348 polyphase, Cartier, holonomic, local Newton--Mahler, Fuss--Catalan, cyclic
1349 radical, and semisimple Galois systems realize these clauses under their
1350 printed hypotheses. The step-factorial product is an exact multiplicative
1351 companion transported through a specified multilinear multiplication map,
1352 not an additive idempotent splitting. Compatible address trivializations,
1353 refinement, and splitting data make the calculus descend through a finite
1354 certified atlas when address holonomy is trivial. No claim is made beyond
1355 that finite profiled domain.
1356 \end{resultbox}
Other PDFs for this work
Original file and source record
This copy matches the recorded source file. Its publication here does not change the work’s review status.
SHA-256: c1ae8aa2472eda9df467bbbf20b3c861f1261333364af06ffaf1cd455b5ab026