Pipeline-generated

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.

✓ 1 result · all verified · 1 also independently AI-judged

Every result on this page is machine-checked by a proof checker and read in full and owner-audited; the judge is an additional, independent cross-model AI review of the proofs; all 1 also cleared it.

Projective Hodge Polarization Foundations Examples

1 · Prerequisites

2 · Summary

The example performs the smallest nontrivial calculation behind the Hodge–Riemann positivity identity. On an oriented Euclidean two-plane it verifies that the type- $(1, 0)$ form $u = e + i f$ is primitive and that the Weil-star identity gives $* u = - i u$ , matching the pointwise primitive-star formula at $n = k = 1$ , and it computes the norm density $u \land * \overset{ˉ}{u} = 2 e \land f$ that underlies positivity.

3 · Logical flowchart

4 · Definitions, theorems and proofs

None yet.

5 · Examples, counterexamples and false statements

ExampleConstruction: Literature-sourcedVerification: AI-adaptedprecheck passjudge pass (gpt-6.1-sol)Open item page →

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$ .