ExampleConstruction: Literature-sourcedVerification: AI-generatedprecheck pass

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.

A charge-one BPST saddle and its formal sector weight

Physical scope

Conditional classical SU(2) Euclidean Yang–Mills example on compactified oriented S4; the displayed exponential is only a formal single-saddle factor, not a continuum observable or measured value.

Example

Assume full AC, meaning that every family of nonempty sets has a choice function; in particular, countable choice holds. Let $S^{4} = {z \in R^{5} : ∣ z ∣ = 1}$ have its unit round metric. Put $p_{\infty} = (0, 0, 0, 0, - 1)$ and $p_{0} = (0, 0, 0, 0, 1)$ . Specify the inverse stereographic maps $κ_{N} : R^{4} \to U_{N} : = S^{4} ∖ {p_{\infty}}$ and $κ_{S} : R^{4} \to U_{S} : = S^{4} ∖ {p_{0}}$ by $κ_{N} (x) = (2 x / (1 + ∣ x ∣^{2}), (1 - ∣ x ∣^{2}) / (1 + ∣ x ∣^{2}))$ and $κ_{S} (y) = (2 y / (1 + ∣ y ∣^{2}), (∣ y ∣^{2} - 1) / (1 + ∣ y ∣^{2}))$ . Here $x$ and $y$ denote their inverse coordinates on $U_{N}$ and $U_{S}$ , respectively; orient $S^{4}$ so $d x^{1} \land d x^{2} \land d x^{3} \land d x^{4} > 0$ . In the north chart put $r^{2} = \sum_{μ = 1}^{4} (x^{μ})^{2}$ ; the metric is $4 (1 + r^{2})^{- 2} \sum_{μ} (d x^{μ})^{2}$ . In the south chart put $y = x / r^{2}$ ; the metric is $4 (1 + ∣ y ∣^{2})^{- 2} \sum_{μ} (d y^{μ})^{2}$ . Define $S U (2) = {U \in M_{2} (C) : U^{*} U = I_{2}, \det U = 1}$ , with Lie algebra $s u (2) = {X \in M_{2} (C) : X^{*} = - X, {tr}_{2} X = 0}$ and commutator bracket; for $U \in S U (2)$ set ${Ad}_{U} X : = U X U^{- 1}$ . Use the Pauli matrices $σ_{1} = (\begin{array}{cc} 0 & 1 \\ 1 & 0 \end{array})$ , $σ_{2} = (\begin{array}{cc} 0 & - i \\ i & 0 \end{array})$ , $σ_{3} = (\begin{array}{cc} 1 & 0 \\ 0 & - 1 \end{array})$ and anti-Hermitian generators $T_{a} = - i σ_{a} / 2$ with ${tr}_{2} (T_{a} T_{b}) = - \frac{1}{2} δ_{a b}$ . Let $ϵ_{i j k}$ be totally antisymmetric with $ϵ_{123} = 1$ , set $η_{a i j} = ϵ_{a i j}$ , $η_{a i 4} = δ_{a i}$ , ${\overset{ˉ}{η}}_{a i j} = - ϵ_{a i j}$ , and ${\overset{ˉ}{η}}_{a i 4} = δ_{a i}$ for $i, j \in {1, 2, 3}$ , and extend both arrays antisymmetrically in their last two indices. For any $ρ > 0$ , put $u (x) = (x^{4} I_{2} - i x^{j} σ_{j}) / r$ on the overlap, and glue two trivial right $S U (2)$ bundles with local sections satisfying $s_{S} = s_{N} u^{- 1}$ . Call the resulting bundle $P$ , require its sector code $[P]$ to belong to the Euclidean model's admitted set $Σ$ , and supply this $P$ as that sector's representative in the compact branch. The local connection potentials are

$A_{N} = \frac{2 η_{a μ ν} x^{ν}}{r^{2} + ρ^{2}} T_{a} d x^{μ}, A_{S} = - \frac{2 ρ^{2} {\overset{ˉ}{η}}_{a μ ν} y^{ν}}{1 + ρ^{2} ∣ y ∣^{2}} T_{a} d y^{μ} .$

On the overlap the potentials obey $A_{S} = {Ad}_{u} A_{N} + u d (u^{- 1})$ , with the right-action section convention above. Their curvature representatives are $F_{N} = d A_{N} + \frac{1}{2} [A_{N} \land A_{N}]$ and $F_{S} = d A_{S} + \frac{1}{2} [A_{S} \land A_{S}]$ , using the alternating wedge–Lie bracket normalized by $\frac{1}{2} [A \land A] (Y, Z) = [A (Y), A (Z)]$ ; the transition makes them representatives of one global adjoint-bundle-valued curvature $F$ . For smooth $s u (2)$ -valued forms $α = \sum_{a} T_{a} α^{a}$ and $β = \sum_{b} T_{b} β^{b}$ with real coefficient forms, use $κ (α \land β) = \sum_{a, b} κ (T_{a}, T_{b}) α^{a} \land β^{b}$ , where $κ (X, Y) = - 2 {tr}_{2} (X Y)$ . The conditional Euclidean action is $S_{E} = (2 g_{Y M}^{2})^{- 1} \int_{S^{4}} κ (F \land * F)$ , and the compactified charge $ν = - (8 π^{2})^{- 1} \int_{S^{4}} {tr}_{2} (F \land F)$ , for fixed $g_{Y M} > 0$ . For this specified smooth two-chart connection, the charge is $ν = 1$ , the curvature is self-dual, and $S_{E} = 8 π^{2} / g_{Y M}^{2}$ . A classical saddle means a smooth admissible connection whose first variation of $S_{E}$ vanishes for every smooth compactly supported adjoint-bundle-valued one-form variation preserving the supplied data. This connection is a classical saddle, and its nonzero charge and self-duality make it an instanton saddle. If the formal sector expression includes the dimensionless theta coupling $θ$ , the corresponding formal single-saddle factor is $e^{- 8 π^{2} / g_{Y M}^{2} + i θ}$ . This factor is not an evaluated continuum path integral.

Example references

Tong, §§1.1.1–1.1.2, self-duality bound and charge-one solution

Vandoren and van Nieuwenhuizen, §2, charge, bound, and theta term

Belavin, Polyakov, Schwartz, and Tyupkin, pp. 85–87, original charge-one solution

Facts & Assumptions

Given: Full AC; the conditional Euclidean SU(2) model and compactified charge convention of the assigned Definition; $g_{Y M} > 0$ ; the oriented round $S^{4}$ charts, Pauli matrices, symbols, scale $ρ > 0$ , two-chart gluing, and local potentials in the Example.

[A1]

Full AC means that every family of nonempty sets has a choice function; it implies the ${A C}_{ω}$ model hypothesis and the full-choice hypotheses of the charge, action-bound, and BPST suppliers. The Axiom of Choice, Trace-normalized instanton number and self-dual sectors, Euclidean Yang–Mills self-dual action bound, Explicit charge-one BPST connection on the round four-sphere

[A2]

The Definition assumes ${A C}_{ω}$ for its smooth gauge data and connections, fixes the Euclidean action as $S_{E} = (2 g_{Y M}^{2})^{- 1} \int κ (F \land * F)$ with positive invariant $κ = - 2 {tr}_{2} = 2 B_{t o p}$ , and defines a saddle by vanishing first variation under smooth compactly supported connection variations. Euclidean Yang–Mills sectors and instanton interpretation

[F1]

The explicitly specified two-chart BPST connection obeys $A_{S} = {Ad}_{u} A_{N} + u d (u^{- 1})$ , so its potentials define a smooth global connection on the glued bundle; it has $F = * F$ , $q_{B} = 1$ in the stated orientation and trace normalization, and $S_{B} (g) = g^{- 2} \int_{S^{4}} B_{t o p} (F \land * F) = 8 π^{2} / g^{2} < \infty$ . Explicit charge-one BPST connection on the round four-sphere

[F2]

The charge supplier defines $q_{B} = (8 π^{2})^{- 1} \int_{X} B_{t o p} (F \land F)$ with $B_{t o p} = - {tr}_{2}$ in the defining SU(2) representation. Trace-normalized instanton number and self-dual sectors

[F3]

For every self-dual supplied connection, the local Bianchi identity implies the source-free Euclidean equation $D_{A} (* F_{A}) = 0$ , where $D_{A} η = d η + [A \land η]$ . Euclidean Yang–Mills self-dual action bound

[F4]

Assume ${A C}_{ω}$ . If $X$ is an oriented smooth four-manifold with boundary and $η$ is a compactly supported smooth three-form, then $\int_{X} d η = \int_{\partial X} η$ ; an empty boundary contributes zero. The general Stokes theorem

[F5]

The sector expression contains the factor $e^{i θ ν}$ and is only a formal continuum notation; it supplies no measure, gauge-fixing prescription, determinant, or limiting argument. Euclidean Yang–Mills sectors and instanton interpretation

Verification

1.1givenA2F1F2

The actual two-chart construction in [F1] supplies a smooth global connection with the stated curvature and $q_{B} = 1$ . Its bundle is the supplied representative of an admitted sector by the Example, so it is admissible in the compact branch of [A2]. By [F2], its charge convention is exactly $ν = q_{B}$ of the assigned Definition, so $ν = 1$ .

1.2F1F3

Self-duality and Bianchi give $D_{A} (* F_{A}) = D_{A} F_{A} = 0$ by [F3]. Therefore the first-variation calculation below has a vanishing Euler–Lagrange term.

2.1A1F1F2step 1.1algebraA2

Since $κ = 2 B_{t o p}$ , the Euclidean action is $S_{E} = (1 / g_{Y M}^{2}) \int_{S^{4}} B_{t o p} (F \land * F)$ , which is the $S_{B} (g)$ of [F1] at $g = g_{Y M}$ . Thus $S_{E} = 8 π^{2} / g_{Y M}^{2}$ .

2.2A1F3F4step 1.2algebraA2

Let $a$ be any smooth adjoint-bundle-valued one-form on compact $S^{4}$ and vary $A_{t} = A + t a$ . Expanding $F_{A_{t}} = d A_{t} + \frac{1}{2} [A_{t} \land A_{t}]$ gives $F_{A_{t}} = F_{A} + t (d a + [A \land a]) + \frac{1}{2} t^{2} [a \land a]$ , because the bracket of two one-forms is symmetric under exchange. Symmetry of $κ$ and the two-form Hodge inner product then give ${\frac{d}{d t} ∣}_{0} S_{E} [A_{t}] = g_{Y M}^{- 2} \int_{S^{4}} κ ((d a + [A \land a]) \land * F_{A})$ . The graded product rule gives $d κ (a \land * F_{A}) = κ (d a \land * F_{A}) - κ (a \land d * F_{A})$ . Infinitesimal Ad-invariance, $κ ([X, Y], Z) = κ (X, [Y, Z])$ , gives $κ ([A \land a] \land * F_{A}) = κ (a \land [A \land * F_{A}])$ after the degree-one wedge reorder; adding the identities yields $d κ (a \land * F_{A}) = κ ((d a + [A \land a]) \land * F_{A}) - κ (a \land D_{A} * F_{A})$ . The scalar three-form $κ (a \land * F_{A})$ is globally defined since $κ$ is Ad-invariant, and is compactly supported because $S^{4}$ is compact. By [F4] its exterior derivative integrates to zero on the closed manifold; using step 1.2, the first variation is $g_{Y M}^{- 2} \int_{S^{4}} κ (a \land D_{A} * F_{A}) = 0$ . This holds for every such $a$ , proving the saddle condition in [A1].

3.1F5step 1.1step 2.1algebra∎

Substitution of $ν = 1$ and the action from steps 1.1 and 2.1 into the formal sector factor $e^{- S_{E} + i θ ν}$ in [F5] gives $e^{- 8 π^{2} / g_{Y M}^{2} + i θ}$ . The Definition supplies only a formal expression and no continuum measure, gauge fixing, determinant, or limiting argument, so this is not a partition-function value.

A charge-one BPST saddle and its formal sector weight

Example

Example references

Facts & Assumptions

Verification

Depends on

Dependency tree · 2 levels

Sources