Realization Calculus: twin edition

Download original file

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

Included manuscript sections

• claim_table.tex

1 \chap{Notation and formal correspondence}\label{app:concordance}
2 \subsection{Notation}
3 \begin{longtable}{@{}p{.25\linewidth}p{.7\linewidth}@{}}
4 \toprule
5 Symbol & Meaning\\\midrule\endhead
6 \(\V,F_v,f^*\) & A declared view category, its fibers, and contravariant restrictions.\\
7 \(\Gamma(F)\) & The strict set of coherent global families.\\
8 \(\Gamma_U(F),\Ext_U(s)\) & Partial sections on a full patch and their global extension fiber.\\
9 \(\delta,\partial,d,D\) & Respectively the view differential, tower differential, a model residual, and a Hilbert defect operator. Each target is declared where used.\\
10 \(p,p_U,p_L\) & A protected observable, restriction to prescribed views, and an innovation observable depending on the splitting.\\
11 \(\mathfrak o_U,H_U\) & The existence obstruction and the group of invisible coherent changes. Additive and nonabelian conventions are stated separately.\\
12 \(C_j,J_j,Q_N,S_N\) & Coarsener, chosen lift, restored coarse remainder, and retained finite reconstruction.\\
13 \(c_f,a_v\) & Coherent nonabelian transition labels and gauge values.\\
14 \(\mathfrak K_G,J_{\rm comp}\) & The cocycle patch groupoid and its composition-support topology.\\
15 \(\mathcal E_b(R)\) & Realizations equipped with an actual identification of their boundary with \(b\).\\
16 \(T_i,K_{ij},R_p\) & Transport to the root, the corresponding root loop operator, and reconstruction from the root.\\
17 \(\mathcal H,q,P\) & Root residual, an orthogonal kernel projector, and the explicitly defined model repair. A graph repair need not be orthogonal in the global maximum norm.\\
18 \(\pi_{W,U},H_U\) & The map forgetting part of the prescription and the corresponding invisible coherent ambiguity.\\
19 \(\phi,\operatorname{EventualHom}\) & A monotone source schedule and transport classes modulo eventual equality.\\
20 \(\chi_A,M=SA-BC\) & Split exact/residual coordinates and the mismatch between chosen repair lifts.\\
21 \(\omega,Q_n,C_n,b_n\) & A residual, its prefix-product rate, movement coefficient, and summable step budget. Here $Q_n$ is not the dyadic remainder operator $Q_N$.\\
22 \(\nu_B,d_W,d_W^{\mathrm{sym}}\) & Residual floor, extended directed transport distance, and its symmetric maximum.\\
23 \(c(x,y),\kappa(x,y)\) & The two-bit pair phase and its antisymmetric scalar-gauge invariant.\\
24 \(H,T,r\) & In the budget chapters, $H=\ker p$ with its inherited Hilbert metric, $T=d|_H$, and $r=df$ for the true raw residual. Measured data are declared separately.\\
25 \(\beta_{T,r}(M),a_\alpha\) & Minimum residual at correction budget $M$, and the quadratic regularized correction.\\
26 \(C,b,q\) & Closure of the correction image, its projection of the residual, and the irreducible residual floor.\\
27 \(v,g,e,\mathcal D_\alpha\) & Fit residual, Hilbert normal residual, optimizer error, and regularized dual objective in the solver chapters.\\
28 \(B,G,q\) & Kernel basis, its Gram matrix, and the coordinate normal covector. This $q$ is not the scalar residual floor used earlier.\\
29 \(\simeq,\simeq_L\) & A specified equivalence, and a continuous linear equivalence. Neither notation alone asserts an isometry.\\
30 \bottomrule
31 \end{longtable}
32 
33 \subsection{From the text to the formal source}
34 The table below locates the foundational results in the accompanying Lean development. Numbered locations refer to results in the main text. Page references locate discussions without a separate numbered statement. Module names are relative to the \path{KomorebiSpace} directory in the \path{lean/} source tree. A row may collect several declarations that together express the displayed result.
35 
36 The table is a navigation aid. A declaration's full type specifies its quantifiers, hypotheses, and conclusion. Those types are the authority for formal coverage. The correspondence does not assign a separate machine-checked counterpart to every explanatory sentence or illustrative calculation. Appendix~\ref{app:written} gives the complementary map for bounded realization, budgets, regularization, and certificates.
37 
38 \input{claim_table}
39 
40 \subsection{Using the correspondence}
41 For a proof involving a restriction or a change of representation, compare the source and target spaces before identifying two displayed formulas. For an analytic estimate, check the norm, the permitted correction space, and the operator whose adjoint is used. The declarations preserve these distinctions explicitly. A continuous linear equivalence alone is not an isometry, and a coordinate equation alone does not fix the metric of its residual.
42 
43 The source contains further definitions, lemmas, and examples beyond this table. The Lean guide explains its organization and the formal treatment of the principal analytic results. Verification records retain the exact source inventories and declaration types from the accepted compilation.

Back to source controls

Back to Realization Calculus: twin edition