How statement and proof provenance work
The first chip identifies the source of the statement or construction; the second identifies the source of its local proof or verification.
- Literature-sourced: the exact statement appears in a cited source; only wording and notation differ.
- AI-adapted: a semantically identical restatement of literature-sourced material, modulo indexing, notation, and boundary cases adopted by the library.
- AI-generated: a genuinely novel statement formulated by AI, with no source for the claim itself.
These labels describe origin, not correctness: citations and verification chips remain separate evidence.
Holonomy and discrete geometric interfaces — flat local transport with global holonomy
Statement
Let , write for the standard embedding coordinates on , and set . With real coordinates on , define
The global frame , , , is an orthonormal tetrad for with signature . Here is the restriction of the indicated ambient vector field to , where it is tangent because it is orthogonal to . Orient by this ordered frame and time-orient it by . Let be the constant matrix with , , and . Assume the convention in Local Lorentz tetrad and connection. Define and the affine connection on this frame by
For a real matrix , denotes the matrix series , which converges absolutely in any fixed submultiplicative matrix norm.
This is a flat Lorentz connection. On any coordinate arc of with angular coordinate , transport between endpoints is , independent of the chosen path inside that arc. Around the once-around loop it is , although the curvature is zero; the loop is not thin-contractible.
Statement references
Facts & Assumptions
Given: The manifold, metric, tetrad, and matrix-valued one-form in the statement; use the connection and transport conventions of the linked A-page items.
Assume as required by Local Lorentz tetrad and connection.
Local Lorentz tetrad and connection: a Lorentz connection matrix is -skew, has curvature , and in this signature uses .
Connection path transport: transport solves with initial value .
The once-around circle path is not thin-contractible: the once-around loop in is not the identity class in the thin path groupoid.
A smooth differential -form: a smooth one-form is a smooth section of the cotangent bundle.
A regular level set is an embedded submanifold: a nonempty regular level set of a smooth real-valued function is a smooth embedded submanifold of codimension one.
The exterior derivative by the invariant vector-field formula: for a one-form , .
The pullback of a differential form: the pullback evaluates the ambient form on tangent vectors after applying the differential of the embedding.
Pullback of forms is smooth functorial and preserves wedges: pullback along a smooth map sends smooth differential forms to smooth differential forms.
The invariant exterior-derivative formula is -multilinear: the invariant exterior-derivative formula is alternating and -multilinear and defines a smooth form. In particular is a two-form, determined by its values on pairs from a tangent frame.
Proof
The function has derivative on , so [F5] gives its usual smooth one-dimensional submanifold structure. Let be the product inclusion, put on , and interpret the stated form as , defined by [F7] and smooth by [F8], hence a smooth cotangent section by [F4]. On the global frame, and ; the frame fields commute pairwise. By [F9], is a smooth two-form. Thus [F6] gives for every , so intrinsically on . Also and it vanishes on the other frame vectors, so the displayed frame is orthonormal for ; it is smooth and is future-directed. In the plane the matrix is the standard skew rotation generator, so . The displayed formula for is linear over smooth functions in , additive in the vector field argument, and satisfies by the ordinary product rule; hence it defines a smooth affine connection with tetrad matrix . Its curvature is , since and . It is -skew and flat, so it is a Lorentz connection under [F1].
On an angular arc, . The matrix starts at ; termwise differentiation of the defining series, whose derivative series converges uniformly on compact parameter intervals, gives . By [F2] it is the transport by uniqueness, and it depends only on the endpoints on that arc. For the path , its endpoint is . Since on , separating the even and odd terms of the series gives on that plane, so it is not the identity. If the once-around loop in were thin-contractible, composing that homotopy with the smooth projection would preserve fixed endpoints, the finite smooth-triangle subdivision, and rank at most one, and would contract the once-around circle loop, contrary to [F3]. Thus its loop class is nontrivial despite .
Depends on
Local Lorentz tetrad and connection
Connection path transport
The once-around circle path is not thin-contractible
A regular level set is an embedded submanifold
A smooth differential -form
The exterior derivative by the invariant vector-field formula
The invariant exterior-derivative formula is -multilinear
The pullback of a differential form
Pullback of forms is smooth functorial and preserves wedges