Realization Calculus

Download original file

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

Read the typeset paper

1 \section{The global projected connection}\label{supp6:section:001}
2 Let $M$ be a smooth real manifold without boundary, $F$ a complete normed real vector space and $P:M\to\End(F)$ a smooth family of bounded idempotents. For smooth range sections $s$, define
3 \[
4 \nabla_Xs=P\,\dd s[X].
5 \]
6 The proof begins by constructing the range bundle from $P$. Its local connection formulas glue, and the actual covariant commutator satisfies
7 \[
8 \boxed{(\nabla_X\nabla_Y-\nabla_Y\nabla_X-\nabla_{[X,Y]})s
9 =P\bigl(\dd P[X]\dd P[Y]-\dd P[Y]\dd P[X]\bigr)P\,s.}
10 \]
11 The derivative and Lie bracket are Mathlib's actual manifold operators. No global coordinate chart is assumed. The result requires idempotence, not an additional orthogonality hypothesis.
12 
13 
14 \section{Local products constructed from the projector}\label{supp6:section:002}
15 The fiber over $x$ is the actual fixed subspace
16 \[
17 \mathcal E_x=\{v\in F:P(x)v=v\}=\Ran P(x).
18 \]
19 The total space is the subset $\mathcal E=\{(x,v):P(x)v=v\}\subseteq M\times F$, with the induced topology. The construction provides local homeomorphisms of this total space as well as the transition functions between them.
20 
21 \subsection{An invertible intertwiner near each anchor}
22 For idempotents $p,q$, set
23 \[
24 T(p,q)=pq+(I-p)(I-q).
25 \]
26 Lean proves $T(p,p)=I$ and $pT(p,q)=T(p,q)q$. For an anchor $a\in M$, define
27 \[
28 U_a=\{x:T(P(x),P(a))\text{ is invertible}\}.
29 \]
30 The invertible elements form an open subset of the algebra of bounded operators. Consequently $U_a$ is open and contains $a$. The family $(U_a)$ covers the whole base. Invertibility is \emph{derived locally}, not assumed at every pair of points.
31 
32 \subsection{The mutually inverse local maps}
33 Write $T_a(x)=T(P(x),P(a))$. For $x\in U_a$,
34 \[
35 B_a(x):\mathcal E_a\longrightarrow\mathcal E_x,
36 \quad v\longmapsto T_a(x)v,
37 \]
38 \[
39 A_a(x):\mathcal E_x\longrightarrow\mathcal E_a,
40 \quad w\longmapsto P(a)T_a(x)^{-1}w.
41 \]
42 The intertwining identity and its inverse counterpart show that the displayed targets are correct. Lean proves both inverse laws, continuity, linearity in the fiber and smooth dependence on the base. Thus
43 \[
44 \mathcal E|_{U_a}\ \cong\ U_a\times\mathcal E_a
45 \]
46 is a local product homeomorphism that preserves the base point.
47 
48 \subsection{Smooth overlap maps and rank}
49 The coordinate transition is $g_{ab}(x)=A_b(x)B_a(x)$. It is smooth on $U_a\cap U_b$, agrees with the actual change between local homeomorphisms, and satisfies
50 \[
51 g_{aa}=I,\qquad g_{bc}g_{ab}=g_{ac}.
52 \]
53 A continuous linear equivalence between $\mathcal E_a$ and $\mathcal E_x$ also gives local constancy of fiber dimension. No single constant rank across disconnected components is assumed.
54 
55 
56 
57 
58 
59 \section{A connection on the constructed bundle}\label{supp6:section:003}
60 The global formula is defined using the actual manifold derivative:
61 \[
62 \nabla_Xs(x)=P(x)\,D_Ms(x)[X(x)].
63 \]
64 Here $D_M$ is represented by \path{mvfderiv}. A second definition, \path{GlobalConnection.covariant}, has values in the actual fiber:
65 \[
66 \nabla s(x):T_xM\longrightarrow\mathcal E_x.
67 \]
68 It is not only an ambient expression asserted to land in the range.
69 
70 \subsection{Connection axioms and smoothness}
71 The formal proofs establish range preservation, additivity in the section, linearity over functions in the vector field argument, and the scalar Leibniz identity
72 \[
73 \nabla_X(fs)=\dd f[X]\,s+f\nabla_Xs.
74 \]
75 Smooth $P$, smooth sections and smooth vector fields give smooth covariant derivatives. Equality of section germs gives equality of covariant derivatives at the point, so the operation is local.
76 
77 \subsection{Smoothness of sections in bundle coordinates}
78 Let $x\in U_a$. If $P(y)s(y)=s(y)$ in a neighborhood of $x$, then
79 \[
80 s\text{ is smooth at }x
81 \quad\Longleftrightarrow\quad
82 \bigl(y\mapsto A_a(y)s(y)\bigr)\text{ is smooth at }x.
83 \]
84 The range condition is only local. The proof uses the actual inverse local maps and equality of germs. It follows that smoothness in bundle coordinates does not depend on the chosen chart.
85 
86 \subsection{The local connection and its change of coordinates}
87 For a coordinate function $u$ valued in $\mathcal E_a$, define
88 \[
89 \nabla^{(a)}_Xu=A_a\bigl(P\,D_M(B_a u)[X]\bigr).
90 \]
91 For every overlap point, Lean proves the operator identity
92 \[
93 \boxed{\nabla^{(b)}_X(g_{ab}u)=g_{ab}\nabla^{(a)}_Xu.}
94 \]
95 This is proved for arbitrary local coordinate functions. It does not assume that $u$ was obtained from a globally smooth section or that a smooth extension has been supplied. Together with the local smoothness criterion, this closes the gluing step left open in the fifth block.
96 
97 
98 
99 
100 
101 \section{From differentiated projectors to the two-form}\label{supp6:section:004}
102 The curvature is defined by the covariant commutator, including the \emph{actual manifold Lie bracket}. It is not defined to equal the desired projector expression.
103 
104 \subsection{The flat ambient identity is proved in charts}
105 For a smooth vector-valued function $s$, the proof identifies directional derivatives with the pullback into each extended chart. It then proves
106 \[
107 D_Ms([X,Y])=D_M(D_Ms[Y])[X]-D_M(D_Ms[X])[Y].
108 \]
109 This uses the chart pullback of the actual vector fields and the ordinary differential identity, then transfers the result back to the manifold. The auxiliary module works locally at a point, so the argument applies within arbitrary open chart domains.
110 
111 \subsection{Projector and section identities are derived}
112 Differentiating $P^2=P$ in a tangent direction $v$ yields
113 \[
114 (\dd P[v])P+P\dd P[v]=\dd P[v],
115 \qquad P\dd P[v]P=0.
116 \]
117 Differentiating $Ps=s$ gives
118 \[
119 \dd s[v]=\dd P[v]s+P\dd s[v].
120 \]
121 Both statements are consequences of actual derivative rules. They are not additional assumptions.
122 
123 \subsection{Cancellation of the second derivatives}
124 The product rule and the identity for the ambient Lie bracket reduce curvature to
125 \[
126 R^\nabla(X,Y)s=P\dd P[X]\dd s[Y]-P\dd P[Y]\dd s[X].
127 \]
128 Substitute the identity obtained by differentiating the range condition for the section. The terms containing $P\dd P[v]P$ vanish, leaving
129 \[
130 R^\nabla(X,Y)s=
131 P\bigl(\dd P[X]\dd P[Y]-\dd P[Y]\dd P[X]\bigr)P s.
132 \]
133 Lean also proves that this depends only on $X(x)$, $Y(x)$ and $s(x)$, not on their extensions. The operator-valued form is alternating, additive and homogeneous, and lands in the actual fiber. Constant projector bundles have zero curvature form.
134 
135 
136 
137 
138 
139 \subsection{Geometry and scalar conventions}
140 The main global curvature theorem uses a smooth real manifold without boundary, modeled on a complete normed real space, and bounded real-linear endomorphisms of a complete normed real space. Finite-dimensional parameter and quantum spaces fall within the corresponding real differential calculus. Complex quantum spaces can be viewed through their underlying real normed spaces. This block does not introduce a separate typeclass wrapper for complex bundles.
141 
142 The atlas and global connection constructions also support the more general infrastructure for models with corners wherever their hypotheses apply. The \emph{curvature completion claim} concerns the stated theorem for manifolds without boundary. Extending that curvature result to boundaries or corners requires further work.
143 
144 \subsection{An explicit smooth atlas}
145 The implementation exposes the actual total space, local product homeomorphisms, linear transitions, smoothness proofs and cocycle laws. It does not register these as a \path{ContMDiffVectorBundle} instance. This is an interface choice. The range bundle atlas, local trivializations, overlap identities, and curvature formula are all constructed or proved from the stated inputs.
146 
147 The equivalence for smooth sections and the gauge law make the atlas usable intrinsically. The connection is also defined with values in \path{fiber (P x)}. Six constructed objects that contain proof fields, including both local equivalences and the derivative with values in the fiber, have separate axiom audits.
148 

Back to source controls

Back to Realization Calculus