ExampleConstruction: Literature-sourcedVerification: AI-adaptedPipeline-generatedjudge 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.

The Hodge index theorem on a product of projective lines

Example

Assume the Axiom of Choice. Let $k$ be a field and let $X = P_{k}^{1} \times_{Spec k} P_{k}^{1}$ with ruling classes $ℓ, m$ as in The Picard group and intersection form of a product of projective lines, so that $Pic (X) = Z ℓ \oplus Z m$ , $ℓ^{2} = m^{2} = 0$ and $ℓ \cdot m = 1$ . Then:

The class $H : = ℓ + m$ satisfies $H \cdot H = 2 > 0$ , so the Hodge index theorem The Hodge index theorem for smooth projective surfaces applies to $H$ .
$H^{⊥} = R (ℓ - m)$ inside $N_{R}^{1} (X)$ and $(ℓ - m)^{2} = - 2 < 0$ ; the primitive part is negative definite of rank one, in agreement with Negative definiteness of the primitive part of the Neron-Severi space.
The intersection form on $N_{R}^{1} (X)$ has matrix $(\begin{array}{cc} 0 & 1 \\ 1 & 0 \end{array})$ in the basis $(ℓ, m)$ ; it is nondegenerate of signature $0$ and index $(1, 1)$ , so it is not negative definite on the whole space. In particular the equality case in the Hodge index theorem is visible here: $(ℓ - m) \cdot H = 0$ and $(ℓ - m)^{2} = - 2 < 0$ , while no nonzero class orthogonal to $H$ has square zero.

Facts & Assumptions

Given: a field $k$ , the surface $X = P_{k}^{1} \times_{k} P_{k}^{1}$ , its ruling classes $ℓ, m$ , and the class $H = ℓ + m$ .

[F1]

By the structure and Picard computation for the product of two projective lines, $X$ is an integral smooth projective surface over $k$ , $Pic (X) = Z ℓ \oplus Z m$ , and the intersection form is given by $ℓ \cdot ℓ = m \cdot m = 0$ , $ℓ \cdot m = 1$ ; the intersection product is symmetric and $Z$ -bilinear (The Picard group and intersection form of a product of projective lines, Intersection numbers of Cartier divisors on a smooth projective surface, The surface intersection product is symmetric and bilinear, Invertible sheaves).

[F2]

Numerical space and definiteness data: the real Neron-Severi space is the extension of scalars of $Pic (X)$ modulo numerical equivalence, with the bilinear extension of the intersection form and the inertia, rank and signature conventions of Positive and negative definiteness, the inertia $(p, q, r)$ , rank $p + q$ , and signature $p - q$ of a real symmetric bilinear or quadratic form (Numerical equivalence and the Neron-Severi space of a surface).

[F3]

Hodge index theorem and its corollary: for invertible sheaves with $H \cdot H > 0$ and $L \cdot H = 0$ one has $L \cdot L \leq 0$ , with equality exactly for numerically trivial $L$ ; the form is negative definite on the primitive part $h^{⊥}$ for $h = [H]$ with $h \cdot h > 0$ (The Hodge index theorem for smooth projective surfaces, Negative definiteness of the primitive part of the Neron-Severi space).

Verification

Given: the surface $X$ , its ruling classes $ℓ, m$ , and $H = ℓ + m$ .

1.1F1F3

Positive self-intersection. By bilinearity and [F1], $H \cdot H = (ℓ + m) \cdot (ℓ + m) = ℓ \cdot ℓ + 2 (ℓ \cdot m) + m \cdot m = 0 + 2 + 0 = 2 > 0$ ; hence $H$ is not numerically trivial and the Hodge index theorem [F3] applies to $H$ .

2.1F1F3step 1.1

The primitive part. Let $x = a ℓ + b m$ be a real class. By [F1], $x \cdot H = x \cdot (ℓ + m) = a (m \cdot ℓ) + b (ℓ \cdot m) = a + b$ , so $x \cdot H = 0$ if and only if $b = - a$ , that is $x \in R (ℓ - m)$ . Hence $H^{⊥} = R (ℓ - m)$ , and $(ℓ - m)^{2} = ℓ \cdot ℓ - 2 (ℓ \cdot m) + m \cdot m = - 2 < 0$ by [F1]; the primitive part is therefore negative definite of rank one, in agreement with [F3]. For $t \neq 0$ the class $t (ℓ - m)$ has square $- 2 t^{2} \neq 0$ , so no nonzero class orthogonal to $H$ has square zero.

3.1F1F2step 2.1

The intersection matrix and its signature. The classes $ℓ, m$ form a basis of the real Neron-Severi space, since they span by the Picard computation [F1], and pairing a relation $a ℓ + b m = 0$ with $ℓ$ and $m$ gives $b = 0$ and $a = 0$ by the intersection matrix [F1]; in this basis the Gram matrix of the intersection form is $(\begin{array}{cc} ℓ \cdot ℓ & ℓ \cdot m \\ m \cdot ℓ & m \cdot m \end{array}) = (\begin{array}{cc} 0 & 1 \\ 1 & 0 \end{array})$ , which is nondegenerate with eigenvalues $\pm 1$ , hence of inertia $(1, 1, 0)$ , index $(1, 1)$ and signature $0$ (Positive and negative definiteness, the inertia $(p, q, r)$ , rank $p + q$ , and signature $p - q$ of a real symmetric bilinear or quadratic form). In particular the form is not negative definite on the whole space.

4.1step 1.1step 2.1step 3.1∎

Conclusion. Step 1.1 gives $H \cdot H = 2 > 0$ ; step 2.1 computes $H^{⊥} = R (ℓ - m)$ with $(ℓ - m)^{2} = - 2 < 0$ and shows no nonzero orthogonal class has square zero; step 3.1 computes the matrix and its signature and index. This verifies all three claims.

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

70 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

Ravi Vakil, The Rising Sea: Foundations of Algebraic Geometry, pre-publication version 2025-10-21 (standard reference, not scraped)