CounterexampleConstruction: Literature-sourcedVerification: AI-adaptedPipeline-generatedjudge pass (gpt-5.6-terra)audited 2026-09-07

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 ambient affine-space hypothesis matters

Statement refuted

False claim: for irreducible closed subsets $P, Q$ of any irreducible classical ambient variety $W$ , every nonempty component of $P \cap Q$ has dimension at least $\dim P + \dim Q - \dim W$ .

Work over a fixed algebraically closed field $k$ , with the Axiom of Choice. Classical varieties are separated and admit finite affine covers; they may be reducible or empty unless irreducibility is specified. Irreducible means nonempty. All fibres and points below are classical closed-point fibres and points.

Facts & Assumptions

Given: The objects and hypotheses in the statement refuted, for the explicit witness below.

[F1]

Let $X$ be irreducible affine and $0 \neq f \in k [X]$ be a nonunit. Then $V_{X} (f)$ is nonempty and every irreducible component has dimension $\dim X - 1$ , hence codimension one. Work over a fixed algebraically closed field $k$ , with the Axiom of Choice. Classical varieties are separated and admit finite affine covers; they may be reducible or empty unless irreducibility is specified. Irreducible means nonempty. All fibres and points below are classical closed-point fibres and points. (A nontrivial principal section has pure codimension one).

[F2]

For every integer $n \geq 0$ , $\dim A_{k}^{n} = \dim P_{k}^{n} = n$ . Work over a fixed algebraically closed field $k$ , with the Axiom of Choice. Classical varieties are separated and admit finite affine covers; they may be reducible or empty unless irreducibility is specified. Irreducible means nonempty. All fibres and points below are classical closed-point fibres and points. (Affine and projective n-space have dimension n).

[F3]

For irreducible closed $X, Y \subseteq A_{k}^{n}$ , every nonempty irreducible component $Z$ of $X \cap Y$ satisfies $\dim Z \geq \dim X + \dim Y - n$ . Work over a fixed algebraically closed field $k$ , with the Axiom of Choice. Classical varieties are separated and admit finite affine covers; they may be reducible or empty unless irreducibility is specified. Irreducible means nonempty. All fibres and points below are classical closed-point fibres and points. (Affine intersection bound via the diagonal).

Counterexample

1.1

Let $W = V (x_{1} x_{4} - x_{2} x_{3}) \subseteq A^{4}$ . The polynomial is irreducible: viewing it as a primitive polynomial in $x_{4}$ over $k [x_{1}, x_{2}, x_{3}]$ , its coefficients $x_{1}$ and $- x_{2} x_{3}$ have no nonunit common factor, and over the fraction field it is linear. Gauss reduction proves irreducibility in the polynomial ring; equivalently a factor independent of $x_{4}$ would divide both coefficients and be a unit. Thus $W$ is irreducible, and the principal theorem in affine four-space gives $\dim W = 3$ .

F1F2

2.1

The subspaces $P = V (x_{2}, x_{4})$ and $Q = V (x_{1}, x_{3})$ lie in $W$ and are affine planes, each of dimension two. Their intersection is exactly the origin, of dimension zero. The claimed ambient bound would require $0 \geq 2 + 2 - 3 = 1$ , which is false. The valid affine-space bound instead uses ambient $A^{4}$ and gives $0 \geq 2 + 2 - 4 = 0$ .

F2F3step 1.1∎

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

13 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

Milne Remark 5.37(b) (standard reference, not scraped)