ExampleConstruction: AI-adaptedVerification: AI-adaptedPipeline-generatedprecheck passjudge pass (gpt-6-sol)audited 2026-09-30

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.

Pontryagin forms from a real connection

Example

Let $M$ be a finite-dimensional Hausdorff second-countable smooth manifold, possibly empty or with boundary, let $E \to M$ be a smooth real vector bundle of finite rank $r$ , and let $\nabla$ be a real connection on $E$ with curvature $Ω$ . Use the conventions of Chern, Pontryagin, and Euler characteristic forms for the complexified connection $\nabla_{C}$ on $E_{C} = E \otimes_{R} C$ , the Chern forms $c_{j}$ , the Pontryagin forms $p_{j}$ , and the Euler form $e$ . Then:

$p_{1} (\nabla) = - c_{2} (\nabla_{C})$ .
If $\nabla$ is compatible with a Euclidean metric, then in every local orthonormal frame $tr Ω = 0$ and $p_{1} (\nabla) = - \frac{tr (Ω \land Ω)}{8 π^{2}} .$
If in addition $r = 2$ , the bundle is oriented, and $Ω = (\begin{array}{cc} 0 & - F \\ F & 0 \end{array})$ for a real $2$ -form $F$ in a positively oriented orthonormal frame, then $p_{1} (\nabla) = \frac{F \land F}{4 π^{2}} = e (\nabla) \land e (\nabla) .$

For every real connection the second determinant coefficient is $c_{2} (\nabla_{C}) = \frac{tr (Ω \land Ω) - tr Ω \land tr Ω}{8 π^{2}},$ so clause 2 uses metric compatibility exactly to delete the $(tr Ω)^{2}$ term; the trace formula without that correction is false for general real connections, as the witness below shows. No integral or topological equality is claimed. The Euler form is defined only in even rank, so clause 3 is restricted to rank two.

Facts & Assumptions

Given: The manifold, bundle, connection and curvature of the three clauses; in clause 2 a Euclidean metric compatible with $\nabla$ ; in clause 3 an orientation and a positively oriented orthonormal frame in which the curvature matrix has the displayed form.

[F1]

In a real bundle the total Chern form of a complex connection is the determinant $c (\nabla) = \det ⁣ (I - \frac{Ω}{2 π i}) = \sum_{j} c_{j} (\nabla)$ , with $c_{j}$ of degree $2 j$ , and the complexified connection on $E_{C} = E \otimes_{R} C$ is the complexification of the real one (Chern, Pontryagin, and Euler characteristic forms).

[F2]

For a real connection, $p_{j} (\nabla) = (- 1)^{j} c_{2 j} (\nabla_{C})$ is a real form of degree $4 j$ , and $p_{j} = 0$ whenever $2 j > r$ (Chern, Pontryagin, and Euler characteristic forms).

[F3]

For an oriented Euclidean bundle of even rank with a metric-compatible connection, the Euler form is $e (\nabla) = Pf ⁣ (\frac{Ω}{2 π})$ in an ordered oriented orthonormal frame, with the normalization $Pf ⁣ (\begin{matrix} 0 & a \\ - a & 0 \end{matrix}) = a$ (Chern, Pontryagin, and Euler characteristic forms).

[F4]

A real connection on a Euclidean vector bundle is Euclidean-compatible when it obeys the identity $X h (s, t) = h (\nabla_{X} s, t) + h (s, \nabla_{X} t)$ for all smooth sections $s, t$ and vector fields $X$ (Complex-linear and metric-compatible bundle connections).

[F5]

In a local frame the curvature matrix of a connection obeys the structure equation $Ω = d ω + ω \land ω$ (Curvature two-form structure equation).

Verification

Given: The objects and hypotheses above, and the standard coordinates on $R^{4}$ in step 3.1.

1.1F1F2givenalgebra

The second determinant coefficient. In a real frame $e_{1}, \dots, e_{r}$ the complexified connection restricts to $\nabla$ on $E \otimes 1$ and is complex-linear in the scalar factor, so it has the same connection matrix and hence the same curvature matrix $Ω$ over $C$ . Put $A = - Ω / (2 π i)$ . Its entries are $2$ -forms and therefore commute, so the usual expansion $\det (I + A) = 1 + e_{1} (A) + e_{2} (A) + \dots$ in principal minors is valid, with $e_{1} (A) = tr A$ and $e_{2} (A) = \frac{1}{2} ((tr A)^{2} - tr (A \land A))$ by Newton's identity. Since $(2 π i)^{2} = - 4 π^{2}$ , $c_{2} (\nabla_{C}) = \frac{tr (Ω \land Ω) - tr Ω \land tr Ω}{8 π^{2}},$ and [F2] turns this into $p_{1} (\nabla) = - c_{2} (\nabla_{C}) = [(tr Ω)^{2} - tr (Ω \land Ω)] / (8 π^{2})$ . For $r \leq 1$ the rank cutoff gives $c_{2} = 0 = p_{1}$ .

2.1F4F5step 1.1algebra

Metric connections. Let $\nabla$ be Euclidean-compatible and let $e_{1}, \dots, e_{r}$ be a local orthonormal frame, so $h (e_{i}, e_{j}) = δ_{i j}$ . Applying [F4] to these frame sections gives $0 = X h (e_{i}, e_{j}) = h (\nabla_{X} e_{i}, e_{j}) + h (e_{i}, \nabla_{X} e_{j}) = ω_{j i} (X) + ω_{i j} (X)$ for every vector field $X$ , hence $ω^{T} = - ω$ . Transposing [F5] and using $(ω \land ω)^{T} = - ω^{T} \land ω^{T}$ together with the anticommutativity of one-form coefficients gives $Ω^{T} = d (ω^{T}) - ω^{T} \land ω^{T} = - Ω$ . Thus every diagonal entry of $Ω$ vanishes and $tr Ω = 0$ . Step 1.1 then gives $c_{2} (\nabla_{C}) = tr (Ω \land Ω) / (8 π^{2})$ and $p_{1} (\nabla) = - tr (Ω \land Ω) / (8 π^{2})$ .

3.1step 1.1step 2.1givenalgebra

The correction term is genuine. On the trivial rank-two real bundle over $R^{4}$ take the standard frame, let $ω = diag (x_{2} d x_{1}, x_{4} d x_{3})$ , and let $\nabla = d + ω$ . Then $ω \land ω = 0$ and $Ω = d ω = diag (d x_{2} \land d x_{1}, d x_{4} \land d x_{3})$ . Hence $tr Ω = d x_{2} \land d x_{1} + d x_{4} \land d x_{3}$ is nonzero, while $tr (Ω \land Ω) = (d x_{2} \land d x_{1})^{2} + (d x_{4} \land d x_{3})^{2} = 0$ . Step 1.1 gives $c_{2} (\nabla_{C}) = - \frac{tr Ω \land tr Ω}{8 π^{2}} = - \frac{d x_{1} \land d x_{2} \land d x_{3} \land d x_{4}}{4 π^{2}} \neq 0,$ whereas the uncorrected expression $- tr (Ω \land Ω) / (8 π^{2})$ of step 2.1 evaluates to $0$ ; the trace formula therefore requires metric compatibility.

3.2F3step 2.1algebra

Rank two. Let $r = 2$ , let the bundle be oriented, and let $Ω = (\begin{array}{cc} 0 & - F \\ F & 0 \end{array})$ in a positively oriented orthonormal frame. Then $Ω \land Ω = (\begin{array}{cc} - F \land F & 0 \\ 0 & - F \land F \end{array})$ , so $tr (Ω \land Ω) = - 2 F \land F$ and step 2.1 gives $p_{1} (\nabla) = F \land F / (4 π^{2})$ . By [F3] and the $2 \times 2$ normalization, $e (\nabla) = Pf (Ω / (2 π)) = - F / (2 π)$ , hence $e (\nabla) \land e (\nabla) = F \land F / (4 π^{2}) = p_{1} (\nabla)$ .

4.1F1F2F3F4step 1.1step 2.1step 3.1step 3.2cases∎

Boundary cases. If $M$ is empty then every form space is zero and the identities hold trivially. If $r = 0$ or $r = 1$ , then $c_{2} = p_{1} = 0$ in clause 1 by the rank cutoff; for $r = 1$ and a Euclidean-compatible connection, step 2.1 makes the $1 \times 1$ curvature matrix skew-symmetric, hence zero, so $p_{1} = - tr (Ω \land Ω) / (8 π^{2}) = 0$ . The Euler form is defined only in even rank, so clause 3 has no rank-one case. If $Ω = 0$ , then both sides of each displayed identity in clauses 2 and 3 vanish, with $F = 0$ there. All three clauses are pointwise local statements in frame coefficients, so they restrict to boundary charts unchanged; no choice principle, parameter, or limiting process occurs, clause 2 assumes metric compatibility while clause 1 does not, and no converse of clause 2 is asserted.

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

18 results within two dependency steps of this one, each drawn at its shortest distance from it. An arrow runs from a result to what uses it, so the chart reads left to right and ends at this result, which carries a heavier outline. Every node is a link to that result. Click elsewhere on the chart to enlarge it.

Sources

Stefan Haller, The Atiyah–Singer Index Theorem, Vienna lecture notes (2013) (standard reference, not scraped)
John W. Milnor and James D. Stasheff, Characteristic Classes (standard reference, not scraped)