Paper III: Typed Transfer, Nonlinear Packets, and Obstruction Theory

Download original file

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

Included manuscript sections

• atlas-definitions.tex
• 01_finite_coordinates.tex
• 02_connections_obstructions.tex
• 03_nonlinear_coordinates.tex
• 04_correction_transport.tex
• references.bib
• visual_atlas.tex

Read the typeset paper

1 \documentclass[11pt,letterpaper]{article}
2 \usepackage[a4paper,margin=23mm,includeheadfoot,headheight=15pt,headsep=15pt,footskip=22pt]{geometry}
3 \usepackage[nopatch=footnote]{microtype}
4 \usepackage{amsmath,amssymb,amsthm,mathtools,amscd,aliascnt}
5 \usepackage{booktabs,longtable,array,tabularx,enumitem,fancyhdr,graphicx}
6 \usepackage[table]{xcolor}\usepackage{setspace,needspace,listings,caption,titlesec,etoolbox,bm,float}
7 \usepackage{xurl}\usepackage{hyperref}\usepackage[nameinlink,noabbrev]{cleveref}\usepackage{bookmark}
8 \definecolor{accent}{HTML}{137668}\definecolor{muted}{HTML}{536568}
9 \definecolor{leanblue}{RGB}{20,72,135}\definecolor{roadmapgray}{RGB}{86,86,86}
10 \frenchspacing\emergencystretch=3em\clubpenalty=10000\widowpenalty=10000\raggedbottom
11 \titleformat{\section}{\sffamily\bfseries\large\color{accent}}{\thesection}{.7em}{}
12 \titleformat{\subsection}{\sffamily\bfseries\normalsize}{\thesubsection}{.7em}{}
13 \titlespacing*{\section}{0pt}{1.4\baselineskip}{.55\baselineskip}
14 \captionsetup{font=small,labelfont={sf,bf},labelsep=period}
15 \pretocmd{\section}{\Needspace{7\baselineskip}}{}{}\pretocmd{\subsection}{\Needspace{5\baselineskip}}{}{}
16 \allowdisplaybreaks\setstretch{1.055}\setlength{\parskip}{.3em}\setlength{\parindent}{1.35em}
17 \setlist[itemize]{topsep=.35em,itemsep=.15em,leftmargin=1.6em}\setlist[enumerate]{topsep=.35em,itemsep=.15em,leftmargin=1.8em}
18 \graphicspath{{figures/}}
19 \hypersetup{pdftitle={Projector-Resolved Seed Calculus III: Typed Transfer, Nonlinear Packets and Obstruction Theory},pdfauthor={Komorebi P.},colorlinks=true,linkcolor=accent,citecolor=accent,urlcolor=accent}
20 \pagestyle{fancy}\fancyhf{}
21 \fancyhead[L]{\sffamily\fontsize{8}{10}\selectfont\color{muted}KOMOREBI MATHEMATICS / PAPER III}
22 \fancyhead[R]{\sffamily\fontsize{8}{10}\selectfont\color{muted}TRADITIONAL PAPER}
23 \fancyfoot[L]{\sffamily\fontsize{8}{10}\selectfont\color{muted}Projector-resolved seed calculus}\fancyfoot[R]{\sffamily\small\color{accent}\thepage}
24 \lstset{basicstyle=\ttfamily\footnotesize,breaklines=true,frame=single,showstringspaces=false,columns=fullflexible,keepspaces=true}
25 \newtheorem{theorem}{Theorem}[section]
26 \theoremstyle{plain}
27 \newaliascnt{proposition}{theorem}
28 \newtheorem{proposition}[proposition]{Proposition}
29 \aliascntresetthe{proposition}
30 \crefname{proposition}{proposition}{propositions}
31 \newaliascnt{lemma}{theorem}
32 \newtheorem{lemma}[lemma]{Lemma}
33 \aliascntresetthe{lemma}
34 \crefname{lemma}{lemma}{lemmas}
35 \newaliascnt{corollary}{theorem}
36 \newtheorem{corollary}[corollary]{Corollary}
37 \aliascntresetthe{corollary}
38 \crefname{corollary}{corollary}{corollaries}
39 \theoremstyle{definition}
40 \newaliascnt{definition}{theorem}
41 \newtheorem{definition}[definition]{Definition}
42 \aliascntresetthe{definition}
43 \crefname{definition}{definition}{definitions}
44 \newaliascnt{example}{theorem}
45 \newtheorem{example}[example]{Example}
46 \aliascntresetthe{example}
47 \crefname{example}{example}{examples}
48 \newaliascnt{construction}{theorem}
49 \newtheorem{construction}[construction]{Construction}
50 \aliascntresetthe{construction}
51 \crefname{construction}{construction}{constructions}
52 \newaliascnt{standardfact}{theorem}
53 \newtheorem{standardfact}[standardfact]{Standard Fact}
54 \aliascntresetthe{standardfact}
55 \crefname{standardfact}{standard fact}{standard facts}
56 \theoremstyle{remark}
57 \newaliascnt{remark}{theorem}
58 \newtheorem{remark}[remark]{Remark}
59 \aliascntresetthe{remark}
60 \crefname{remark}{remark}{remarks}
61 \newaliascnt{boundary}{theorem}
62 \newtheorem{boundary}[boundary]{Boundary}
63 \aliascntresetthe{boundary}
64 \crefname{boundary}{boundary}{boundaries}
65 \newaliascnt{roadmap}{theorem}
66 \newtheorem{roadmap}[roadmap]{Formalization target}
67 \aliascntresetthe{roadmap}
68 \crefname{roadmap}{formalization target}{formalization targets}
69 \crefname{theorem}{theorem}{theorems}
70 \newcommand{\bbk}{\Bbbk}
71 \newcommand{\N}{\mathbb N}
72 \newcommand{\cA}{\mathcal A}
73 \newcommand{\cC}{\mathcal C}
74 \newcommand{\cE}{\mathcal E}
75 \newcommand{\cG}{\mathcal G}
76 \newcommand{\cH}{\mathcal H}
77 \newcommand{\cO}{\mathcal O}
78 \newcommand{\cP}{\mathcal P}
79 \newcommand{\cQ}{\mathcal Q}
80 \newcommand{\cS}{\mathcal S}
81 \newcommand{\cT}{\mathcal T}
82 \newcommand{\cW}{\mathcal W}
83 \newcommand{\End}{\operatorname{End}}
84 \newcommand{\Hom}{\operatorname{Hom}}
85 \newcommand{\im}{\operatorname{im}}
86 \newcommand{\id}{\mathrm{id}}
87 \newcommand{\Ob}{\operatorname{Ob}}
88 \newcommand{\Hol}{\operatorname{Hol}}
89 \newcommand{\Coord}{\operatorname{Coord}}
90 \newcommand{\ev}{\operatorname{ev}}
91 \newcommand{\src}{\operatorname{src}}
92 \newcommand{\tgt}{\operatorname{tgt}}
93 \newcommand{\Walk}{\operatorname{Walk}}
94 \newcommand{\supp}{\operatorname{supp}}
95 \newcommand{\op}{\mathrm{op}}
96 \newcommand{\leanname}[1]{\nolinkurl{#1}}
97 \newcommand{\Acal}{\mathcal A}
98 \newcommand{\Ccal}{\mathcal C}
99 \newcommand{\Fcal}{\mathcal F}
100 \newcommand{\Hcal}{\mathcal H}
101 \newcommand{\Kcal}{\mathcal K}
102 \newcommand{\Lcal}{\mathcal L}
103 \newcommand{\Ocal}{\mathcal O}
104 \newcommand{\Pcal}{\mathcal P}
105 \newcommand{\Qcal}{\mathcal Q}
106 \newcommand{\Rcal}{\mathcal R}
107 \newcommand{\Scal}{\mathcal S}
108 \newcommand{\Tcal}{\mathcal T}
109 \newcommand{\Ucal}{\mathcal U}
110 \newcommand{\Vcal}{\mathcal V}
111 \newcommand{\Ker}{\operatorname{Ker}}
112 \newcommand{\coker}{\operatorname{coker}}
113 \newcommand{\Cone}{\operatorname{Cone}}
114 \newcommand{\Lip}{\operatorname{Lip}}
115 \newcommand{\dist}{\operatorname{dist}}
116 \newcommand{\rank}{\operatorname{rank}}
117 \newcommand{\MC}{\operatorname{MC}}
118 \newcommand{\gr}{\operatorname{gr}}
119 \newcommand{\Span}{\operatorname{span}}
120 \newcommand{\tr}{\operatorname{tr}}
121 \newcommand{\Ad}{\operatorname{Ad}}
122 
123 \newcolumntype{L}[1]{>{\raggedright\arraybackslash}p{#1}}
124 \newcolumntype{Y}{>{\raggedright\arraybackslash}X}
125 \newcommand{\statusleanthree}[1]{\par\smallskip\noindent\begin{minipage}{\linewidth}{\color{leanblue}\textbf{Formal contract: Paper III v1.0.1.}}\par\begingroup\small\raggedright\leanname{#1}\par\endgroup\end{minipage}\par\smallskip}
126 \newcommand{\statusleanprior}[1]{\par\smallskip\noindent\begin{minipage}{\linewidth}{\color{leanblue}\textbf{Inherited formal contract: Papers I--II.}}\par\begingroup\small\raggedright\leanname{#1}\par\endgroup\end{minipage}\par\smallskip}
127 \newcommand{\statusroadmap}[1]{\par\smallskip\noindent{\color{roadmapgray}\textbf{Outside the finite formal contract.}}\ #1\par\smallskip}
128 
129 
130 \usepackage{tikz,multicol}
131 \usetikzlibrary{arrows.meta,decorations.pathreplacing,patterns,calc}
132 \usepackage{komorebi-monograph}
133 \renewcommand{\KomorebiKind}{Modern Monograph}
134 \KomorebiSetup
135 \input{atlas-definitions.tex}
136 \begin{document}
137 \KomorebiCover
138 \KomorebiOpeningNote{Begin with typed edge words and exact coordinate transport. A chosen connection introduces defects, holonomy, and packet obstruction witnesses. Part II develops nonlinear packet jets, tree expansions, correction complexes, filtered lifting, elimination, and smooth transport.
139 
140 Part I retains the finite v1.0.1 formal contract. Part II gives the strengthened nonlinear and analytic development with ordinary proofs. The release also verifies exact nonlinear coordinates, continuous packet jets on actual projector ranges, and the decorated composition and structural support laws in Lean. The integral Taylor remainder and the later analytic and obstruction results retain their ordinary proof status. Formal coverage stays attached to the released declarations. The visual atlas at the end of this volume provides twenty-four worked plates. The separate Lean guide explains the formal contract and its evidence.}
141 \begin{abstract}
142 Finite projector packets turn linear transfer into typed walks and arbitrary maps into exact coordinate representations. Canonical coordinate transport satisfies an exact cocycle law. A chosen connection can fail to compose, producing holonomy and packet obstruction witnesses. Nonlinear packet jets lead to higher composition, convergent rooted tree expansions, graded operations, and nonlinear refinement defects. A specified correction map produces a canonical cokernel obstruction. Relative exact sequences, mapping cones, Hilbert splitting, nonlinear correction, and filtered lifting describe how these obstructions behave. Exact elimination produces Schur formulas, and finite transport reduces gluing to fundamental cycle holonomy. For smooth orthogonal packet families, direct packet rotations converge in operator norm to canonical unitary transport. The finite formal contract and the broader ordinary proof development retain their separate scopes throughout.
143 \end{abstract}
144 This release presents the mathematical development together with worked examples, a visual atlas, and a separate guide to the formal proof evidence. The packet norm estimate distinguishes the actual range jet from its ambient extension. The support statements keep external packet profiles and intermediate composition witnesses explicitly typed. The accompanying release record gives the exact source and scope of each formal verification.
145 \tableofcontents
146 \listoffigures
147 \clearpage\pagenumbering{arabic}
148 \input{chapters/01_finite_coordinates.tex}
149 \input{chapters/02_connections_obstructions.tex}
150 \input{chapters/03_nonlinear_coordinates.tex}
151 \input{chapters/04_correction_transport.tex}
152 \clearpage
153 \appendix
154 \section{Visual atlas}\label{app:visual-atlas}
155 The plates give exact finite models for the algebraic constructions in this volume. Their stable labels run from V1 to V24. Each plate names the related statements in the paper. These models make the hypotheses and map directions visible. They do not extend the finite Lean contract to the analytic results of Part II.
156 \begin{readerroadmap}[title={Three routes through the atlas}]
157 For typed transfer, read V3 to V8. For coordinates, connections, and gauge, read V9 to V18, followed by V23. For candidate witnesses and trees, read V19 to V22, followed by V24. V1 and V2 introduce the objects and the questions they answer.
158 \end{readerroadmap}
159 Products act in traversal order. The first edge traversed is the rightmost operator. Rows represent targets and columns represent sources.
160 \clearpage
161 \begingroup
162 \setstretch{1.01}\fontsize{10}{12}\selectfont
163 \setlength{\parskip}{3pt}\setlength{\abovedisplayskip}{6pt}\setlength{\belowdisplayskip}{6pt}
164 \input{visual_atlas.tex}
165 \endgroup
166 \clearpage
167 \begingroup\small\setstretch{1}
168 \bibliographystyle{plain}
169 \bibliography{references}
170 \endgroup
171 \end{document}

Back to source controls

Back to Paper III: Typed Transfer, Nonlinear Packets, and Obstruction Theory