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

Curves sharing too many points share a component

Statement

Assume the Axiom of Choice, inherited from the cited local-length, smoothness or Bezout suppliers.

Let $C, D$ be plane projective curves of degree $d \geq 1$ over the algebraically closed field $k$ . If $C \cap D$ contains more than $d^{2}$ distinct points, then $C$ and $D$ share a component. Equivalently, two distinct curves of degree at most $d$ cannot meet in more than $d^{2}$ distinct points without a common component.

Facts & Assumptions

Given: AC The Axiom of Choice, plane projective curves $C, D$ of degree $d \geq 1$ over the algebraically closed field $k$ .

[F1]

For degrees $d_{C}, d_{D} \geq 1$ , if $C, D$ have no common component, then $\sum_{p \in C \cap D} I_{p} (C, D) = d_{C} d_{D}$ , a finite sum over the finitely many intersection points; when both degrees equal $d$ , the sum is $d^{2}$ Bezout's theorem for plane projective curves, Two plane projective curves meet.

[F2]

Whenever $I_{p} (C, D)$ is finite, it is a positive integer at points of $C \cap D$ and zero at points outside the intersection Symmetry, additivity and local nature of intersection multiplicity. Under the no-common-component hypothesis, [F1] ensures this finiteness at every intersection point.

Proof

1.1F1F2algebra

Suppose $C$ and $D$ had no common component and let $S \subseteq C \cap D$ be a set of pairwise distinct intersection points with $∣ S ∣ > d^{2}$ . By [F2] each $p \in S$ contributes $I_{p} (C, D) \geq 1$ to the Bezout sum, so $\sum_{p \in C \cap D} I_{p} (C, D) \geq ∣ S ∣ > d^{2}$ , contradicting the Bezout identity of [F1]. Hence a common component must exist.

2.1step 1.1F1algebra∎

Equivalently, if $C$ and $D$ are distinct curves of degrees $d_{C} \leq d$ and $d_{D} \leq d$ meeting in more than $d^{2} \geq d_{C} d_{D}$ distinct points, then the same counting argument with the product $d_{C} d_{D}$ in place of $d^{2}$ forces a common component; specialising to $d_{C} = d_{D} = d$ gives the first formulation, The equal-degree formulation is therefore a special case of the degree-bounded one.

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

41 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

William Fulton, Algebraic Curves: An Introduction to Algebraic Geometry (2008 electronic edition; Internet Archive copy of the author's PDF) (standard reference, not scraped)
Michael Artin, MIT 18.721 Notes for a Course in Algebraic Geometry (January 26, 2022 version), Chapter 1 (standard reference, not scraped)