C Notation and formal correspondence
On this page · Permalink · Source line 1
C.1 Notation
On this page · Permalink · Source line 2
| Symbol | Meaning |
|---|---|
| \({\mathcal V},F_v,f^*\) | A declared view category, its fibers, and contravariant restrictions. |
| \(\Gamma(F)\) | The strict set of coherent global families. |
| \(\Gamma_U(F),{\operatorname{Ext}}_U(s)\) | Partial sections on a full patch and their global extension fiber. |
| \(\delta,\partial,d,D\) | Respectively the view differential, tower differential, a model residual, and a Hilbert defect operator. Each target is declared where used. |
| \(p,p_U,p_L\) | A protected observable, restriction to prescribed views, and an innovation observable depending on the splitting. |
| \(\mathfrak o_U,H_U\) | The existence obstruction and the group of invisible coherent changes. Additive and nonabelian conventions are stated separately. |
| \(C_j,J_j,Q_N,S_N\) | Coarsener, chosen lift, restored coarse remainder, and retained finite reconstruction. |
| \(c_f,a_v\) | Coherent nonabelian transition labels and gauge values. |
| \(\mathfrak K_G,J_{\rm comp}\) | The cocycle patch groupoid and its composition-support topology. |
| \(\mathcal E_b(R)\) | Realizations equipped with an actual identification of their boundary with \(b\). |
| \(T_i,K_{ij},R_p\) | Transport to the root, the corresponding root loop operator, and reconstruction from the root. |
| \(\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. |
| \(\pi_{W,U},H_U\) | The map forgetting part of the prescription and the corresponding invisible coherent ambiguity. |
| \(\phi,\operatorname{EventualHom}\) | A monotone source schedule and transport classes modulo eventual equality. |
| \(\chi_A,M=SA-BC\) | Split exact/residual coordinates and the mismatch between chosen repair lifts. |
| \(\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\). |
| \(\nu_B,d_W,d_W^{\mathrm{sym}}\) | Residual floor, extended directed transport distance, and its symmetric maximum. |
| \(c(x,y),\kappa(x,y)\) | The two-bit pair phase and its antisymmetric scalar-gauge invariant. |
| \(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. |
| \(\beta_{T,r}(M),a_\alpha\) | Minimum residual at correction budget \(M\), and the quadratic regularized correction. |
| \(C,b,q\) | Closure of the correction image, its projection of the residual, and the irreducible residual floor. |
| \(v,g,e,\mathcal D_\alpha\) | Fit residual, Hilbert normal residual, optimizer error, and regularized dual objective in the solver chapters. |
| \(B,G,q\) | Kernel basis, its Gram matrix, and the coordinate normal covector. This \(q\) is not the scalar residual floor used earlier. |
| \(\simeq,\simeq_L\) | A specified equivalence, and a continuous linear equivalence. Neither notation alone asserts an isometry. |
C.2 From the text to the formal source
On this page · Permalink · Source line 33
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 KomorebiSpace directory in the lean/ source tree. A row may collect several declarations that together express the displayed result.
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 D gives the complementary map for bounded realization, budgets, regularization, and certificates.