LemmaStatement: Literature-sourcedProof: AI-adaptedPipeline-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.

Incidence alpha planes detect positive-orientation anti-self-duality

Statement

Let $E \to S^{4}$ be a smooth finite-rank complex vector bundle and let $A$ be a smooth connection on $E$ , with curvature $F_{A} = \nabla_{A}^{2} \in Ω^{2} (S^{4}, {End}_{C} E)$ . For real two-forms $η, ζ$ , let $*_{g}$ be the Hodge star characterized by $η \land *_{g} ζ = ⟨ η, ζ ⟩_{g} d {v o l}_{g}$ , and extend it complex-linearly to the form factor of $F_{A}$ . At a finite point of the positively oriented stereographic chart in the incidence geometry, evaluate $F_{A}$ complex-bilinearly on $H_{1} = \partial_{{\overset{ˉ}{z}}_{1}} - t \partial_{z_{2}}$ and $H_{2} = \partial_{{\overset{ˉ}{z}}_{2}} + t \partial_{z_{1}}$ . Then $F_{A} (H_{1}, H_{2}) = 0$ for every $t \in C$ if and only if the self-dual part $F_{A}^{+} = (F_{A} + *_{g} F_{A}) / 2$ vanishes at that point. Equivalently, $F_{A}$ restricts to zero on every alpha-plane in the full projective family $C P^{1}$ , including $t = \infty$ as represented in the second incidence chart. Vanishing on the single plane at $t = \infty$ alone is insufficient.

Statement references

Positive incidence geometry for the coupled Penrose transform

Rawnsley, §1, pp. 43–46

Donaldson, §3, pp. 4–6

Facts & Assumptions

Given: The positive orientation, metric, and horizontal vectors of the incidence definition; the complexification of a real two-form is evaluated complex bilinearly.

[F1]

The chart uses the positive orientation $d x_{0} \land d x_{1} \land d x_{2} \land d x_{3}$ , metric $4 (1 + r^{2})^{- 2} \sum d x_{μ}^{2}$ , and horizontal vectors $H_{1} = \partial_{{\overset{ˉ}{z}}_{1}} - t \partial_{z_{2}}$ , $H_{2} = \partial_{{\overset{ˉ}{z}}_{2}} + t \partial_{z_{1}}$ . Positive incidence geometry for the coupled Penrose transform

Proof

1.1givenF1algebra

Write $F_{a b} = F_{A} (\partial_{a}, \partial_{b})$ and use antisymmetry. Bilinearity gives $F_{A} (H_{1}, H_{2}) = F_{\overset{ˉ}{1} \overset{ˉ}{2}} - t (F_{1 \overset{ˉ}{1}} + F_{2 \overset{ˉ}{2}}) + t^{2} F_{12}$ . If this polynomial vanishes for every complex $t$ , each coefficient vanishes; conversely, vanishing of the three coefficients makes the polynomial zero.

2.1F1step 1.1algebra∎

In the oriented Euclidean orthonormal coframe $d x_{0}, d x_{1}, d x_{2}, d x_{3}$ , the complex two-forms $d z_{1} \land d z_{2}$ , $d {\overset{ˉ}{z}}_{1} \land d {\overset{ˉ}{z}}_{2}$ , and $d z_{1} \land d {\overset{ˉ}{z}}_{1} + d z_{2} \land d {\overset{ˉ}{z}}_{2}$ span the complexified self-dual two-forms: applying the Euclidean star to each gives itself. The metric is a positive conformal rescaling of the Euclidean metric, and on two-forms in dimension four the star is unchanged by such a rescaling. The three coefficients in step 1.1 are the components of $F_{A}$ paired with this basis, up to nonzero constants and exchange of the first two basis vectors, so their vanishing is equivalent to $F_{A}^{+} = 0$ , entrywise in ${End}_{C} E$ . In the second chart, put $u = 1 / t$ and use ${\tilde{H}}_{1} = u \partial_{{\overset{ˉ}{z}}_{1}} - \partial_{z_{2}}$ , ${\tilde{H}}_{2} = u \partial_{{\overset{ˉ}{z}}_{2}} + \partial_{z_{1}}$ . On the overlap these are $u H_{1}, u H_{2}$ , and their curvature evaluation extends as $u^{2} F_{\overset{ˉ}{1} \overset{ˉ}{2}} - u (F_{1 \overset{ˉ}{1}} + F_{2 \overset{ˉ}{2}}) + F_{12}$ to $u = 0$ . Thus the finite-parameter condition implies vanishing also at infinity, proving the full-family equivalence. At $u = 0$ alone it tests only $F_{12}$ ; for example the nonzero self-dual form $d z_{1} \land d {\overset{ˉ}{z}}_{1} + d z_{2} \land d {\overset{ˉ}{z}}_{2}$ vanishes on that plane.

Depends on

Positive incidence geometry for the coupled Penrose transform