LemmaStatement: AI-adaptedProof: 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.

Localization: vanishing integrals or fluxes force a continuous function to vanish

Statement

Assume the Axiom of Countable Choice ( ${A C}_{ω}$ , The Axiom of Countable Choice ( ${A C}_{ω}$ )).

Integral form. Let $n, m \geq 1$ , let $U \subseteq R^{n}$ be open, and let $g : U \to R^{m}$ be continuous. Write $g_{i} (x) : = g (x) (i)$ for $0 \leq i < m$ , using the canonical function coordinates of The Euclidean inner product $⟨ x, y ⟩ = \sum_{k < n} x_{k} y_{k}$ on $R^{n}$ . For a measurable $V \subseteq U$ write, componentwise,

$\int_{V} g d λ_{n} : = (\int g_{0} χ_{V} d λ_{n}, \dots, \int g_{m - 1} χ_{V} d λ_{n}),$

each component $0 \leq i < m$ , when integrable, being the Lebesgue integral of $g_{i}$ on $V$ , extended by zero outside $V$ (Integrable real and complex functions, and their integrals, Integral over a measurable subset). A ball $V \subseteq U$ is compactly contained in $U$ when its closure is a compact subset of $U$ ; for a Euclidean ball this means $\overline{V} \subseteq U$ . If $\int_{V} g d λ_{n} = 0$ for every ball $V$ compactly contained in $U$ , then $g = 0$ on $U$ .

Disc form. Let $W \subseteq R^{3}$ be open and let $F : W \to R^{3}$ be continuous. Write $F_{i} (x) : = F (x) (i)$ for $0 \leq i < 3$ and $e_{0} = (1, 0, 0)$ , $e_{1} = (0, 1, 0)$ , $e_{2} = (0, 0, 1)$ , the canonical standard vectors of The standard list $e : n \to F^{n}$ with $e_{i} (i) = 1_{F}$ and $e_{i} (j) = 0_{F}$ for $j \neq i$ is an ordered basis of $F^{n}$ ; hence $\dim_{F} F^{n} = n$ , and $F^{0}$ is the zero space with basis $\emptyset$ and dimension $0$ . Extend the basis labels cyclically by $e_{j} : = e_{j m o d 3}$ for $j \geq 3$ . Thus $e_{i + 1} \times e_{i + 2} = e_{i}$ for each $i \in {0, 1, 2}$ . For such $i$ , $q \in W$ and $r > 0$ put

$φ_{i, q} (s, t) : = q + s e_{i + 1} + t e_{i + 2}, D_{r} : = {(s, t) \in R^{2} : s^{2} + t^{2} < r^{2}},$

with $\overline{D_{r}}$ the closed disc. If for every $i$ , every $q \in W$ and every $r > 0$ with $φ_{i, q} (\overline{D_{r}}) \subseteq W$ one has

$\int_{\overline{D_{r}}} (F_{i} \circ φ_{i, q}) d λ_{2} = 0,$

then $F = 0$ on $W$ .

Conventions. The displayed disc condition is the vanishing of the flux of $F$ through the flat disc $φ_{i, q} (\overline{D_{r}})$ in the orientation with unit normal $e_{i}$ : the affine parametrization is a regular patch whose tangent vectors $e_{i + 1}, e_{i + 2}$ have cross product $e_{i}$ of norm one (Regular parametrized surface patches on compact Jordan parameter regions, The cross product in $R^{3}$ , The standard list $e : n \to F^{n}$ with $e_{i} (i) = 1_{F}$ and $e_{i} (j) = 0_{F}$ for $j \neq i$ is an ordered basis of $F^{n}$ ; hence $\dim_{F} F^{n} = n$ , and $F^{0}$ is the zero space with basis $\emptyset$ and dimension $0$ ), so the flux of Unit normal fields, orientations, and flux through a regular surface patch is the Riemann integral $\int_{\overline{D_{r}}} (F_{i} \circ φ_{i, q}) d (s, t)$ ; that integral equals the displayed Lebesgue integral because the integrand is continuous on the compact Jordan region $\overline{D_{r}}$ (A closed disc of radius $r \geq 0$ has Jordan content $π r^{2}$ , The Riemann integral of a bounded function over a bounded Jordan measurable set, A continuous real function on a compact Jordan measurable set is Riemann integrable over that set, Borel Darboux integrands in finite dimension). Both clauses are pointwise conclusions on their open domains. The first clause is the converse from universal integral relations to a pointwise equation; a single vanishing integral over one ball or one disc supplies no conclusion, and the hypothesis ranges over the full family described.

Facts & Assumptions

Given: The Axiom of Countable Choice; integers $n, m \geq 1$ ; an open $U \subseteq R^{n}$ and a continuous $g : U \to R^{m}$ with $\int_{V} g d λ_{n} = 0$ for every ball $V$ compactly contained in $U$ ; an open $W \subseteq R^{3}$ and a continuous $F : W \to R^{3}$ satisfying the disc condition of the Statement, with canonical indices $0 \leq i < m$ for $g_{i}$ and $0 \leq i < 3$ for $F_{i}, e_{i}$ ; and, inside the contradiction argument below, either a point $p \in U$ with $g (p) \neq 0$ or a point $x \in W$ with $F (x) \neq 0$ .

[F1]

Metric balls and continuity at a point: $B_{X} (a, ρ) = {y \in X : d_{X} (y, a) < ρ}$ , and $f$ is continuous at $a$ when for every real $ε > 0$ there is $δ > 0$ with $f [B_{X} (a, δ)] \subseteq B_{Y} (f (a), ε)$ (Open ball, closed ball and sphere in a metric space, Continuity of a map between metric spaces, at a point and globally, in the $ε$ - $δ$ form).

[F2]

Open subsets of a metric space: $U$ is open exactly when every $x \in U$ has $r > 0$ with $B (x, r) \subseteq U$ (The metric topology: a set is open when every one of its points has a ball around it inside the set; closed means open complement).

[F3]

Under ${A C}_{ω}$ , every Euclidean ball $B (x, r)$ with $r > 0$ is Lebesgue measurable with $0 < λ (B (x, r)) < \infty$ (Euclidean balls have positive finite Lebesgue measure).

[F4]

Integral of signed and nonnegative functions: for measurable real $u$ with at most one of $\int u^{+}$ , $\int u^{-}$ equal to $+ \infty$ one sets $\int u d λ : = \int u^{+} d λ - \int u^{-} d λ$ , and $u$ is integrable when both are finite, equivalently $\int ∣ u ∣ d λ < \infty$ ; then $\int (- u) d λ = - \int u d λ$ ; and for nonnegative measurable $f$ the integral over $E$ is $\int_{E} f d λ = \int f χ_{E} d λ$ (Integrable real and complex functions, and their integrals, Integral over a measurable subset).

[F5]

Monotonicity and nonnegative homogeneity for the nonnegative integral: if $0 \leq f \leq h$ are measurable then $\int f d λ \leq \int h d λ$ , and if $c > 0$ then $\int c f d λ = c \int f d λ$ (Monotonicity and nonnegative homogeneity of the nonnegative integral).

[F6]

Simple integral: for a nonnegative simple measurable function $s = \sum_{j \leq N} c_{j} χ_{E_{j}}$ one has $\int s d λ = \sum_{j \leq N} c_{j} λ (E_{j})$ with $0 \cdot \infty = 0$ , and the nonnegative integral of a nonnegative simple measurable function equals its simple integral; hence $\int c χ_{E} d λ = c λ (E)$ for $c \geq 0$ and measurable $E$ (The integral of a nonnegative simple function, The nonnegative integral agrees with the simple integral on simple functions).

[F7]

Measurability: every continuous map $R^{n} \to R^{m}$ is Borel measurable under ${A C}_{ω}$ ; the Borel $σ$ -algebra is generated by the open sets, so indicators of open sets are Borel (Continuous functions on Euclidean spaces are Borel measurable, The Borel sigma-algebra of a topological space).

[F8]

Closed bounded Euclidean sets are compact (Heine-Borel in $R^{n}$ : with the Euclidean metric a subset of $R^{n}$ is compact if and only if it is closed and bounded, and the proof by bisection uses no choice principle; the same holds on the real line). Extreme values: a continuous real function on a nonempty compact metric space is bounded above and below and attains a maximum and a minimum (A continuous real-valued function on a nonempty compact metric space is bounded and attains a greatest and a least value).

[F9]

Canonical coordinates: $R^{m}$ consists of functions on $m = {0, \dots, m - 1}$ , $z_{i} = z (i)$ for $i < m$ , and $⟨ z, w ⟩ = \sum_{i < m} z_{i} w_{i}$ with $∥ z ∥_{2} = \sqrt{⟨ z, z ⟩}$ (The Euclidean inner product $⟨ x, y ⟩ = \sum_{k < n} x_{k} y_{k}$ on $R^{n}$ ). The standard vectors $e_{i}$ , $i < m$ , have coordinate $1$ at $i$ and $0$ at the other coordinates (The standard list $e : n \to F^{n}$ with $e_{i} (i) = 1_{F}$ and $e_{i} (j) = 0_{F}$ for $j \neq i$ is an ordered basis of $F^{n}$ ; hence $\dim_{F} F^{n} = n$ , and $F^{0}$ is the zero space with basis $\emptyset$ and dimension $0$ ). Hence $∣ z_{i} ∣ \leq ∥ z ∥_{2}$ , since $z_{i}^{2} \leq \sum_{k < m} z_{k}^{2}$ , and $⟨ z, e_{i} ⟩ = z_{i}$ ; applying the bound to differences shows that every component of a continuous vector map is continuous.

Proof

technique · contradiction; assume the Statement fails, and contradict in turn a nonzero value of $g$ (cases (A)) and, under the disc hypothesis, a nonzero value of $F$ (case (B))

1.1givenassume-contra

Suppose the Statement fails. Then either (A) $g (p) \neq 0$ for some $p \in U$ , or (B) the disc condition holds and $F (x) \neq 0$ for some $x \in W$ ; if neither holds then $g = 0$ on $U$ and, whenever the disc condition holds, $F = 0$ on $W$ , which is exactly the Statement. We contradict (A) and (B) in turn.

2.1step 1.1F1F2F4F9givenalgebra

In case (A): choose a component index $i < m$ with $g_{i} (p) \neq 0$ and put $u : = g_{i}$ , continuous by [F9]. Replacing the $i$ -th component of $g$ by its negative preserves the hypothesis, since $\int_{V} (- g_{i}) d λ = - \int_{V} g_{i} d λ$ by [F4], and does not change whether $g$ vanishes; hence we may suppose $u (p) = 2 c$ with $c : = u (p) / 2 > 0$ . By [F1] applied to the continuous $u$ at $p$ with $ε = c$ there is $δ_{0} > 0$ with $∣ u (y) - u (p) ∣ < c$ for all $y \in B (p, δ_{0})$ ; by [F2] and $p \in U$ there is $δ_{2} > 0$ with $B (p, δ_{2}) \subseteq U$ ; put $δ : = \min {δ_{0}, δ_{2}} > 0$ . Then the ball $V : = B (p, δ / 2)$ satisfies $\overline{V} \subseteq B (p, δ) \subseteq U$ , so $V$ is compactly contained in $U$ , and $u (y) > u (p) - c = c$ for every $y \in V$ . The hypothesis gives $\int_{V} g d λ_{n} = 0$ , whose $i$ -th component is $\int u χ_{V} d λ = 0$ .

2.2step 1.1F1F2F9givenalgebra

In case (B): choose $i \in {0, 1, 2}$ with $F_{i} (x) \neq 0$ and put $φ : = φ_{i, x}$ , $W^{'} : = φ^{- 1} [W] = {(s, t) : φ (s, t) \in W}$ and $h : = F_{i} \circ φ : W^{'} \to R$ , so that $h (0, 0) = F_{i} (x) \neq 0$ . Then $W^{'}$ is open in $R^{2}$ , $h$ is continuous, and for every $r > 0$ with $\overline{B} ((0, 0), r) \subseteq W^{'}$ the disc hypothesis with centre $x$ gives $\int_{\overline{B} ((0, 0), r)} h d λ_{2} = 0$ . Indeed, the standard unit vectors are orthonormal by [F9], so $∥ φ (s, t) - φ (s^{'}, t^{'}) ∥_{2} = ∥ (s, t) - (s^{'}, t^{'}) ∥_{2}$ for all $(s, t), (s^{'}, t^{'})$ ; hence $φ$ is continuous, and the inverse image of a ball contained in $W$ at $φ (s_{0}, t_{0})$ contains the parameter ball of the same radius at $(s_{0}, t_{0})$ , so $W^{'}$ is open by [F2], while for $(s_{0}, t_{0}) \in W^{'}$ and $ε > 0$ , continuity of $F_{i}$ by [F9] at $φ (s_{0}, t_{0}) \in W$ gives $ρ > 0$ with $∣ F_{i} (y) - F_{i} (φ (s_{0}, t_{0})) ∣ < ε$ whenever $d (y, φ (s_{0}, t_{0})) < ρ$ , and then $d ((s, t), (s_{0}, t_{0})) < ρ$ gives $∣ h (s, t) - h (s_{0}, t_{0}) ∣ < ε$ by the isometry identity; finally, when $\overline{B} ((0, 0), r) \subseteq W^{'}$ the disc $φ (\overline{B} ((0, 0), r))$ lies in $W$ , so the Statement's condition applies with centre $x$ and radius $r$ .

3.1step 2.1F3F4F5F6F7F8algebra

In case (A): the function $u χ_{V}$ is Borel and nonnegative, and $0 \leq c χ_{V} \leq u χ_{V}$ pointwise, because $u > c > 0$ on $V$ by step 2.1 while $u χ_{V} = 0$ off $V$ , and $u$ is continuous while $V$ is open [F7]. More explicitly, for a continuous function on open $U$ , inverse images of open real sets are relatively open, hence open in $R^{n}$ ; after multiplication by $χ_{V}$ and zero extension, inverse images are Borel (adding $R^{n} ∖ V$ when the target contains zero). Moreover $\overline{V}$ is a nonempty compact metric space, so $M : = \max_{\overline{V}} ∣ u ∣$ is finite by [F8], and $∣ u χ_{V} ∣ \leq M χ_{B (p, δ)}$ with $\int M χ_{B (p, δ)} d λ = M λ (B (p, δ)) < \infty$ by [F5], [F6] and [F3]; hence $u χ_{V}$ is integrable and $\int u χ_{V} d λ$ is a finite real number by [F4]. Monotonicity [F5] and the simple-integral rule [F6] give $\int u χ_{V} d λ \geq \int c χ_{V} d λ = c λ (V) > 0$ by [F3], contradicting $\int u χ_{V} d λ = 0$ from step 2.1. Therefore case (A) is impossible: the integral hypothesis forces $g = 0$ on $U$ .

4.1step 2.1step 2.2step 3.1F3F4F5F6F8algebra

In case (B), replace $h$ by $- h$ if necessary, which preserves every zero disc integral by [F4], so $h (0, 0) = 2 c^{'} > 0$ . Continuity and openness as in step 2.1 give $r > 0$ with $\overline{B} ((0, 0), r) \subseteq W^{'}$ and $h > c^{'}$ throughout that closed disc $C$ . It is compact by [F8] and contained in the open ball $B ((0, 0), 2 r)$ , of finite measure by [F3], so $h χ_{C}$ is integrable by the boundedness and Borel argument of step 3.1. Since $0 \leq c^{'} χ_{B ((0, 0), r)} \leq h χ_{C}$ , [F5] and [F6] give $\int_{C} h d λ_{2} \geq c^{'} λ_{2} (B ((0, 0), r)) > 0$ by [F3]. This contradicts the closed-disc integral hypothesis of step 2.2, without replacing it by an unstated open-ball hypothesis. Thus $F = 0$ on $W$ .

5.1step 3.1step 4.1discharge-contradiction∎

Cases (A) and (B) both end in contradiction, so no failure of the Statement occurs: the integral hypothesis forces $g = 0$ on $U$ , and the disc hypothesis forces $F = 0$ on $W$ .

Remarks

The proof uses, for each clause, the hypothesis only on balls centred at the point where the function is assumed nonzero and with radius half of a continuity threshold; the full family in the Statement is what makes the lemma a localization statement, but no choice from the family is made, and the argument is choice-free apart from the declared ${A C}_{ω}$ used by the surface and measurability suppliers.
The disc clause is not a statement about a single loop or box: one special disc carries no information, and the components must be tested in all three coordinate directions at all admissible centres and radii.

Localization: vanishing integrals or fluxes force a continuous function to vanish

Statement

Facts & Assumptions

Proof

Remarks

Depends on

Dependency tree · 2 levels

Sources