Realization Calculus

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
• core-layout.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: finite algebraic core.}}\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: Chapters 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}{Mathematical text}
134 \KomorebiSetup
135 \input{atlas-definitions.tex}
136 \usepackage{titlesec}
137 \input{core-layout.tex}
138 
139 % Publication-design overrides. Mathematical bodies retain their source text.
140 \CoreLayout
141 \colorlet{accent}{pubTeal}\colorlet{teal}{pubTeal}\colorlet{ink}{pubInk}\colorlet{muted}{pubMuted}\colorlet{pale}{pubWash}\colorlet{light}{pubWash}
142 \makeatletter
143 \@ifundefined{KomorebiCover}{}{\renewcommand{\KomorebiCover}{%
144 \clearpage\hypersetup{pageanchor=false}\thispagestyle{empty}\begingroup\setlength{\parindent}{0pt}%
145 {\sffamily\fontsize{8.5}{11}\selectfont\color{pubTeal}REALIZATION CALCULUS\par}%
146 \vspace{27pt}%
147 {\sffamily\fontsize{9}{12}\selectfont\color{pubTeal}\MakeUppercase{\KomorebiSeries}\par}%
148 \vspace{22pt}%
149 {\normalfont\fontsize{29}{35}\selectfont\color{pubNavy}\raggedright\KomorebiTitle\par}%
150 \vspace{17pt}%
151 {\normalfont\fontsize{17}{23}\selectfont\color{pubMuted}\raggedright\KomorebiSubtitle\par}%
152 \vspace{22pt}\noindent\textcolor{pubCopper}{\rule{42pt}{.8pt}}\par%
153 \vspace{20pt}%
154 \@ifundefined{KomorebiCoverBlurb}{}{\normalfont\fontsize{11.4}{16.2}\selectfont\color{pubMuted}\raggedright\KomorebiCoverBlurb\par}%
155 \vfill%
156 {\normalfont\fontsize{14}{18}\selectfont\color{pubInk}Komorebi P.\par}%
157 \vspace{9pt}{\sffamily\fontsize{9}{13}\selectfont\color{pubMuted}\KomorebiKind\par}%
158 \endgroup\clearpage\pagenumbering{roman}\hypersetup{pageanchor=true}\color{pubInk}\normalfont\pagestyle{empty}}}
159 \makeatother
160 
161 \begin{document}
162 \KomorebiCover
163 \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.
164 
165 Part I develops the finite algebraic core under its declaration-level formal contract. Part II gives the nonlinear and analytic development with ordinary proofs. The accompanying formal development 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 identified 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.}
166 \begin{abstract}
167 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.
168 \end{abstract}
169 The chapter 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 formal companion gives the exact source and scope of each formal verification.
170 \tableofcontents
171 \listoffigures
172 \clearpage\pagenumbering{arabic}
173 \input{chapters/01_finite_coordinates.tex}
174 \input{chapters/02_connections_obstructions.tex}
175 \input{chapters/03_nonlinear_coordinates.tex}
176 \input{chapters/04_correction_transport.tex}
177 \clearpage
178 \appendix
179 \section{Visual atlas}\label{app:visual-atlas}
180 The plates give exact finite models for the algebraic constructions in this volume. Their stable labels run from Plate III.1 to Plate III.24. Each plate names the related statements in the chapter. These models make the hypotheses and map directions visible. They do not extend the finite Lean contract to the analytic results of Part II.
181 \begin{readerroadmap}[title={Three routes through the atlas}]
182 For typed transfer, read Plate III.3 to Plate III.8. For coordinates, connections, and gauge, read Plate III.9 to Plate III.18, followed by Plate III.23. For candidate witnesses and trees, read Plate III.19 to Plate III.22, followed by Plate III.24. Plate III.1 and Plate III.2 introduce the objects and the questions they answer.
183 \end{readerroadmap}
184 Products act in traversal order. The first edge traversed is the rightmost operator. Rows represent targets and columns represent sources.
185 \clearpage
186 \begingroup
187 \setstretch{1.01}\fontsize{10}{12}\selectfont
188 \setlength{\parskip}{3pt}\setlength{\abovedisplayskip}{6pt}\setlength{\belowdisplayskip}{6pt}
189 \input{visual_atlas.tex}
190 \endgroup
191 \clearpage
192 \begingroup\small\setstretch{1}
193 \bibliographystyle{plain}
194 \bibliography{references}
195 \endgroup
196 \end{document}

Back to source controls

Back to Realization Calculus