LemmaStatement: Literature-sourcedProof: AI-adaptedPipeline-generatedprecheck passjudge 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.

An outward-pointing finite-dimensional map has a zero

Statement

Let $N \geq 1$ , $R > 0$ , and let $F : R^{N} \to R^{N}$ be continuous. If $F (x) \cdot x > 0$ for every $∣ x ∣ = R$ , then $F$ has a zero in the closed ball ${\overline{B}}_{R} (0)$ .

Facts & Assumptions

Given: $N \geq 1$ , $R > 0$ , and a continuous $F$ satisfying the strict outward-pointing inequality on the sphere.

[F1]

Every continuous self-map of the closed unit ball in a finite-dimensional real vector space has a fixed point (Brouwer fixed point theorem).

Proof

1.1F1givendischarge-contradictionconstruct

Suppose, for contradiction, that $F$ has no zero in ${\overline{B}}_{R} (0)$ . Then $F (x) \neq 0$ there, and $G (x) : = - R F (x) / ∣ F (x) ∣$ is a continuous map ${\overline{B}}_{R} (0) \to {\overline{B}}_{R} (0)$ whose values all lie on the sphere. After rescaling the ball to the unit ball, [F1] gives a fixed point $x = G (x)$ .

2.1F1step 1.1givendischarge-contradictionalgebra∎

Since $G (x)$ lies on the sphere, $∣ x ∣ = R$ . The fixed-point equation gives $F (x) \cdot x = F (x) \cdot (- R F (x) / ∣ F (x) ∣) = - R ∣ F (x) ∣ < 0$ , contradicting the assumed positive boundary pairing. Thus $F$ has a zero in the closed ball.

Depends on

Brouwer fixed point theorem

Used by

Dependency tree · two levels

3 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

Marvin Fritz, Monotone Operators in Nonlinear PDEs, JKU lecture notes, WS 2023/2024 (standard reference, not scraped)
Haim Brezis, Functional Analysis, Sobolev Spaces and Partial Differential Equations, Springer Universitext, 2011 (standard reference, not scraped)