ExampleConstruction: Literature-sourcedVerification: AI-adaptedPipeline-generatedprecheck passjudge pass (gpt-6.1-sol)

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.

Primitive one-forms and the Weil star sign

Example

With the form-side conventions of Compact Kähler and rational Hodge polarization conventions: let $V$ be the oriented Euclidean two-plane with positively oriented orthonormal basis $e, f$ , Kähler form $ω = e \land f$ , and compatible complex structure $J$ , acting by pullback on forms, with $J e = - f, J f = e$ (equivalently $f = - J e$ ). Then the type- $(1, 0)$ form $u = e + i f$ is primitive and satisfies $* u = - i u$ . Its positive norm density is $u \land * \overset{ˉ}{u} = 2 e \land f .$

Facts & Assumptions

Given: The oriented Euclidean two-plane $V$ with its positively oriented orthonormal basis $e, f$ , the form $ω = e \land f$ , the compatible complex structure $J$ with $J e = - f$ , $J f = e$ , and $u = e + i f$ .

[F1]

These are the form-side conventions of Compact Kähler and rational Hodge polarization conventions: $J$ acts on forms by pullback, the $(p, q)$ decomposition is by the eigenspaces of $J$ , $ω$ is the fundamental form, and the orientation is the one for which $ω$ is positive; for $n = k = 1$ every $1$ -form is primitive because $Λ$ lowers degree by two.

[F2]

The complementary-basis formula for the Hodge star on a positively oriented orthonormal basis, and the characterization of the star by $α \land * \overset{ˉ}{β} = h (α, β) vol$ on complexified forms (obtained by complexifying the real basis formula), are those of The Hodge star exists uniquely and is given by the complementary-basis formula in an oriented orthonormal basis.

[F3]

For a primitive form of type $(p, q)$ and degree $k$ , the pointwise Weil star identity reads $* u = ϵ (k) i^{q - p} L^{n - k} u / (n - k)!$ (Hermitian exterior Lefschetz decomposition and Weil star identity), with $L = ω \land$ and $ϵ (k) = (- 1)^{k (k - 1) / 2}$ .

Verification

1.1F1givenalgebra

Since $J$ is complex-linear on the complexification and $J e = - f$ , $J f = e$ , one has $J u = J e + i J f = - f + i e = i (e + i f) = i u$ , so $u$ lies in the $(1, 0)$ -eigenspace of $J$ and is of type $(1, 0)$ ; also $Λ u = 0$ because $Λ$ lowers degree by two and $u$ has degree one, so $u$ is primitive, equivalently $L u = ω \land u = 0$ in degree three.

1.2F2givenalgebra

On the positively oriented orthonormal basis $e, f$ the complementary-basis formula gives $* e = f$ (sign $+ 1$ ) and $* f = - e$ (sign $- 1$ ), hence $* u = * e + i * f = f - i e = - i (e + i f) = - i u$ .

2.1F3step 1.2givenalgebra∎

This agrees with the primitive-star formula of [F3] at $n = k = 1$ , $(p, q) = (1, 0)$ , where it reads $* u = ϵ (1) i^{0 - 1} L^{0} u / 0! = - i u$ ; since $\overset{ˉ}{u} = e - i f$ is primitive of type $(0, 1)$ , the same formula gives $* \overset{ˉ}{u} = i \overset{ˉ}{u}$ , and $u \land \overset{ˉ}{u} = (e + i f) \land (e - i f) = - 2 i e \land f$ , so $u \land * \overset{ˉ}{u} = i u \land \overset{ˉ}{u} = 2 e \land f$ , which is positive for the orientation in which $e \land f > 0$ .

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

17 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

Christian Schnell, Complex Manifolds, MAT 545 (Stony Brook, Fall 2024), Class 17 'Proof of the Kähler identities' (October 29), 4 pp.; Proposition 17.3 (Weil's identity) with its n=1 two-plane verification (standard reference, not scraped)
Christian Schnell, Complex Manifolds, MAT 545 (Stony Brook, Fall 2024), Class 18 'The Hodge decomposition' (October 31), 6 pp.; Theorem 18.15 (Hodge–Riemann bilinear relations) (standard reference, not scraped)