Alphabeta Math
TheoremStatement: Literature-sourcedProof: 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.

The d, partial and dbar identities

Statement

Let U⊆Cn be open and let all forms below be smooth and complex-valued. Then d=∂+∂ˉ,∂2=0,∂ˉ2=0,∂∂ˉ+∂ˉ∂=0. For η∈Ωp,q(U) and θ∈Ωr,s(U), ∂(η∧θ)=∂η∧θ+(−1)p+qη∧∂θ,∂ˉ(η∧θ)=∂ˉη∧θ+(−1)p+qη∧∂ˉθ. The identities hold at bidegree endpoints as well, with components outside 0≤p,q≤n interpreted as zero.

Facts & Assumptions

Given: The open set U⊆Cn and smooth complex-valued forms on U.

[F1]

Complex forms decompose uniquely by bidegree, and ∂ and ∂ˉ are the two bidegree components of d (Bigraded complex forms and the Dolbeault operators).

[F2]

The published exterior derivative satisfies d2=0 on smooth differential forms (The exterior derivative squares to zero).

[F3]

For homogeneous real forms, the published exterior derivative obeys the graded product rule (The exterior derivative is a graded derivation).

Proof

technique · direct
1.1F1F2givenalgebra

Write a complex form ξ=ξ1+iξ2 with real forms ξ1,ξ2. The coordinate formula defining d on complex coefficients is the complex-linear extension of the real exterior derivative, so d2ξ=d2ξ1+i d2ξ2=0 by [F2].

1.2F1F3givenalgebra

The real graded product rule [F3] extends to complex forms: write each complex form as real part plus i times imaginary part, expand the wedge product by complex bilinearity, and apply [F3] to each real pair. The coordinate definition of d in [F1] is complex-linear, so the resulting identity is the same signed rule for complex forms.

2.1F1step 1.1givenalgebra

For a pure type form η∈Ωp,q(U), [F1] gives dη=∂η+∂ˉη and hence 0=d2η=∂2η+(∂∂ˉ+∂ˉ∂)η+∂ˉ2η by step 1.1. These three terms have respective bidegrees (p+2,q), (p+1,q+1), and (p,q+2); the direct sum uniqueness in [F1] forces each component to vanish, including when an endpoint component is zero by convention.

2.2F1step 1.2givenalgebra

Let η∈Ωp,q(U) and θ∈Ωr,s(U). Wedge products add the two bidegrees (and vanish if a repeated differential occurs). In the complex graded-derivation identity from step 1.2, the terms involving ∂ have bidegree (p+r+1,q+s) and those involving ∂ˉ have bidegree (p+r,q+s+1). Projecting onto these distinct summands yields the two displayed Leibniz identities.

3.1F1step 2.1step 2.2givenalgebra∎

Every smooth complex form is a finite sum of its bidegree components, and both operators and wedge product are additive. Applying step 2.2 componentwise proves the graded Leibniz rules for all homogeneous forms; applying step 2.1 componentwise proves all three square and anticommutation identities for arbitrary forms.

Depends on

Used by

Dependency tree · two levels

14 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