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.
A polynomial ring in n variables over a field has dimension n
Statement
Let be a field and let . Then
Facts & Assumptions
Given: A field and an integer .
Every nonzero finite-type -domain is module-finite and hence integral over a polynomial subring (Noether normalisation yields module finiteness over a polynomial subring). Comparable primes in an integral extension with equal contraction are equal (Comparable primes with the same contraction are equal under an integral map).
Finite transcendence degree is additive in field towers, so algebraic extensions preserve transcendence degree (Transcendence degree is additive in finite towers).
Proof
Let be any finite-type -domain and primes of . Set , a nonzero finite-type -domain, and , a nonzero prime of . By [L1], fix a module-finite normalization . Its fraction field extension is algebraic, so [L2] gives .
By incomparability in [L1], is nonzero: otherwise would be comparable primes of with the same contraction in . If , then is a field and has no nonzero proper prime, so the assumed strict pair cannot exist. For a strict pair one therefore has . A nonzero polynomial gives a nontrivial algebraic relation among the images of in the domain . Among this finite set of images, take a maximal algebraically independent subset; because the full set is dependent, it has at most members. Maximality makes each omitted image algebraic over the field generated by the subset. Since all images generate , this proves .
The quotient is integral over , hence its fraction field is algebraic over . By [L2] and step 2.1, . Thus transcendence degree drops at least one along every strict prime inclusion in a finite-type domain.
Apply this drop to any strict chain in . The fraction field of the initial quotient is generated by at most images of variables, so its transcendence degree is at most ; the final transcendence degree is nonnegative. Hence . For , the coordinate ideals are prime and form a chain of length . When , the sole prime is and both bounds are zero. Therefore for every .