LemmaStatement: Literature-sourcedProof: AI-adaptedPipeline-generatedjudge pass (gpt-6-luna)

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 zero set of a nonzero real polynomial is Lebesgue null

Statement

Assume Countable Choice. For every integer $d \geq 1$ , if

$P (x_{1}, \dots, x_{d}) = \sum_{α \in N_{0}^{d}} c_{α} x_{1}^{α_{1}} \dots x_{d}^{α_{d}},$

is a nonzero real polynomial with finitely many nonzero coefficients, then its zero set ${x \in R^{d} : P (x) = 0}$ is Lebesgue measurable and has $d$ -dimensional Lebesgue measure zero.

Statement references

Leshno et al., proof of Theorem 1, polynomial-activation obstruction

Facts & Assumptions

Given: Countable Choice, $d \geq 1$ , and a nonzero real polynomial $P$ in $d$ variables.

[F1]

A nonzero univariate real polynomial has only finitely many distinct real roots (A nonzero real polynomial of degree $n$ has no more than $n$ distinct real roots).

[F2]

Tonelli's theorem computes the measure of a Borel set by integrating the measures of its coordinate sections (Tonelli's theorem for nonnegative measurable functions on a sigma-finite product).

[F3]

Product Lebesgue measure agrees with Euclidean Lebesgue measure on Borel sets (On Borel subsets of R^{m+n}, the product lambda_m times lambda_n agrees with lambda_{m+n}).

[F4]

Countable subsets of Euclidean space are Lebesgue null under Countable Choice, and Lebesgue measure is countably subadditive (Every at most countable subset of $R^{n}$ is Lebesgue null; in particular $λ_{1} (Q) = 0$ , Finite and countable subadditivity of measures).

[F5]

Under Countable Choice every Borel subset of $R^{d}$ is Lebesgue measurable (Assuming countable choice, every Borel subset of $R^{n}$ is Lebesgue measurable).

[F6]

Under Countable Choice, Lebesgue measure in every positive dimension is $σ$ -finite: $R^{m} = ⋃_{r = 1}^{\infty} [- r, r]^{m}$ , and each box has finite measure $(2 r)^{m}$ (A box in $R^{n}$ with parameters $a_{i} \leq b_{i}$ is Lebesgue measurable of measure $\prod_{i < n} (b_{i} - a_{i})$ , whichever of its faces are included).

[A1]

Countable Choice means every sequence of nonempty sets has a function choosing one element from each (The Axiom of Countable Choice ( ${A C}_{ω}$ )).

Proof

1.1givenF1F4A1base

Base case $d = 1$ : [F1] makes the zero set finite, hence countable and null by [F4].

1.2givenF1F4A1IH

Inductive step: let $d \geq 2$ and assume the claim in dimension $d - 1$ . Write $P (x^{'}, t) = \sum_{j = 0}^{m} Q_{j} (x^{'}) t^{j}$ , where $x^{'} \in R^{d - 1}$ and the highest coefficient $Q_{m}$ is a nonzero polynomial. By the induction hypothesis, $Z = {x^{'} : Q_{m} (x^{'}) = 0}$ is null. For every $x^{'} \notin Z$ , the section $t \mapsto P (x^{'}, t)$ is a nonzero univariate polynomial, so its zero set is finite by [F1] and null by [F4].

2.1step 1.2F2F3F5F6A1

Fix $R \geq 1$ . The set ${(x^{'}, t) \in [- R, R]^{d} : P (x^{'}, t) = 0}$ is Borel because $P$ is continuous. Its section has measure at most $2 R$ when $x^{'} \in Z$ and measure zero otherwise. Both Lebesgue factors are $σ$ -finite by [F6], so Tonelli [F2] shows that its product measure is zero, since $Z$ is null; [F3] identifies this with its Euclidean Lebesgue measure.

3.1step 1.1step 1.2step 2.1F4F5A1discharge-induction∎

The full zero set is the countable union of these Borel null intersections over integers $R \geq 1$ . Countable subadditivity [F4] makes it measurable and null. The base case and induction step prove the assertion for every $d \geq 1$ .

Depends on

Used by

Dependency tree · two levels

50 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

Leshno, Lin, Pinkus, and Schocken, Multilayer Feedforward Networks With a Non-Polynomial Activation Function Can Approximate Any Function, proof of Theorem 1, Step 1 (standard reference, not scraped)