LemmaStatement: Literature-sourcedProof: 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.

Heat-ball chains reach earlier points

Statement

Assume Countable Choice. Let $Ω \subseteq R^{n}$ be open, let $0 < t_{1} < t_{0} \leq T < \infty$ , and let $γ : [0, 1] \to Ω$ be a Lipschitz path with compact image $K$ . Then there is $ρ > 0$ such that $E_{ρ} (P) \subseteq Ω \times (0, T]$ for every $P \in K \times [t_{1}, t_{0}]$ , and for every $s \in [t_{1}, t_{0})$ there are $N \geq 1$ and points $P_{0} = (γ (0), t_{0}), P_{1}, \dots, P_{N} = (γ (1), s)$ , all lying in $K \times [t_{1}, t_{0}]$ , with $P_{j + 1} \in E_{ρ} (P_{j})$ for all $0 \leq j < N$ .

Facts & Assumptions

Given: Countable Choice, an open set $Ω \subseteq R^{n}$ , times $0 < t_{1} < t_{0} \leq T < \infty$ , a Lipschitz path $γ : [0, 1] \to Ω$ with compact image $K$ , and $s \in [t_{1}, t_{0})$ .

[A1]

Countable Choice is the ambient hypothesis (The Axiom of Countable Choice ( ${A C}_{ω}$ )).

[F1]

Heat balls are enclosed in a spatial ball and a time interval: $E_{r} (t, x) \subseteq \overline{B} (x, \frac{r}{2} \sqrt{2 n / π e}) \times [t - r^{2} / 4 π, t]$ for all $(t, x)$ and $r > 0$ (Heat balls and their time slices).

[F6]

For $0 < τ < r^{2} / (4 π)$ the time slice of $E_{r} (t, x)$ at depth $τ$ is the closed ball of radius $ρ_{n} (τ) = \sqrt{2 n τ \log \frac{r^{2}}{4 π τ}}$ (Heat balls and their time slices).

[F2]

For nonempty $A$ , put $d_{A} (x) = \inf_{z \in A} ∣ x - z ∣$ . The triangle inequality gives $d_{A} (x) \leq ∣ x - y ∣ + d_{A} (y)$ and its reverse, hence $∣ d_{A} (x) - d_{A} (y) ∣ \leq ∣ x - y ∣$ . Thus this distance is $1$ -Lipschitz and continuous. A continuous real function on a nonempty compact set attains its minimum (Lipschitz map, $α$ -Hölder map for rational $0 < α \leq 1$ , and contraction, A continuous real-valued function on a nonempty compact metric space is bounded and attains a greatest and a least value, Open cover, subcover, compact metric space, and compact subset of a metric space).

[F3]

$\log : (0, \infty) \to R$ is strictly increasing and onto $R$ (Order, continuity, range, and the product, quotient, and reciprocal laws for the natural logarithm).

[F4]

Archimedean property: for every real $x$ there is a natural number $n \geq 1$ with $x < n$ ; and for every $ε > 0$ there is $n \geq 1$ with $1 / n < ε$ (Every complete ordered field is Archimedean, For every $ε > 0$ in a complete ordered field there is a natural $n \geq 1$ with $1 / n < ε$ ).

[F5]

Balls in a metric space are the sets $B (x, r) = {y : d (x, y) < r}$ (Open ball, closed ball and sphere in a metric space), and a Lipschitz path satisfies $∣ γ (u) - γ (v) ∣ \leq L ∣ u - v ∣$ for its Lipschitz constant $L$ (Lipschitz map, $α$ -Hölder map for rational $0 < α \leq 1$ , and contraction).

Proof

Given: Countable Choice, an open $Ω \subseteq R^{n}$ , times $0 < t_{1} < t_{0} \leq T < \infty$ , a Lipschitz path $γ$ with compact image $K$ , and $s \in [t_{1}, t_{0})$ .

1.1A1F2F5given

The image $K$ is nonempty. If $A : = R^{n} ∖ Ω$ is nonempty, [F2] makes $d_{A}$ continuous and gives an attained minimum $d = \min_{K} d_{A} > 0$ : each $x \in K \subseteq Ω$ has a ball $B (x, r_{x}) \subseteq Ω$ , so $d_{A} (x) \geq r_{x} > 0$ , including at a minimum point. If $A$ is empty, set $d = 1$ .

2.1step 1.1F1F4given

Choose $ρ > 0$ with $\frac{ρ}{2} \sqrt{2 n / π e} < d$ and $ρ^{2} / (4 π) < t_{1}$ (possible by [F4]); then for every $P = (x, t) \in K \times [t_{1}, t_{0}]$ , [F1] gives $E_{ρ} (P) \subseteq \overline{B} (x, \frac{ρ}{2} \sqrt{2 n / π e}) \times [t - ρ^{2} / 4 π, t]$ , and the spatial ball lies in $Ω$ because its radius is less than $d \leq d_{A} (x)$ when $A$ is nonempty, and the inclusion is automatic otherwise, while $t - ρ^{2} / 4 π \geq t_{1} - ρ^{2} / 4 π > 0$ and $t \leq t_{0} \leq T$ ; hence $E_{ρ} (P) \subseteq Ω \times (0, T]$ .

3.1step 2.1F3F4F5F6given

Let $L$ be a Lipschitz constant of $γ$ and put $δ : = (t_{0} - s) / N > 0$ and $P_{j} : = (γ (j / N), t_{0} - j δ)$ for $0 \leq j \leq N$ , so $P_{0} = (γ (0), t_{0})$ and $P_{N} = (γ (1), s)$ . By [F5], $∣ γ ((j + 1) / N) - γ (j / N) ∣ \leq L / N$ , so $P_{j + 1} \in E_{ρ} (P_{j})$ holds by [F6] as soon as $L^{2} / N^{2} \leq 2 n δ \log \frac{ρ^{2}}{4 π δ}$ , which is implied by $L^{2} \leq 2 n (t_{0} - s) \log \frac{ρ^{2} N}{4 π (t_{0} - s)} = : R (N)$ together with $δ < ρ^{2} / (4 π)$ ; by [F3] the map $N \mapsto R (N)$ is unbounded above and $N > (4 π (t_{0} - s)) / ρ^{2}$ for all large $N$ , so [F4] supplies such an $N$ .

4.1step 2.1step 3.1given∎

The $ρ$ of step 2.1 and the chain of step 3.1, together with the fact that $s \in [t_{1}, t_{0})$ was arbitrary, are exactly the assertions of the lemma; the chain points $P_{j} = (γ (j / N), t_{0} - j δ)$ lie on the graph of the path, hence in $K \times [s, t_{0}] \subseteq K \times [t_{1}, t_{0}]$ , and since $Ω$ is open and every two points of a connected component of $Ω$ are joined by a polygonal, hence Lipschitz, path (Every connected component of an open subset of $R^{n}$ is open and polygonally connected), the chain hypothesis is never vacuous for such points.

Depends on

Used by

Strong parabolic maximum principle Theorem

Dependency tree · two levels

86 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

Gerald Teschl, Partial Differential Equations: From Classical to Modern (2025 archived author manuscript, AMS Graduate Studies in Mathematics) (standard reference, not scraped)
John K. Hunter, Notes on Partial Differential Equations (revised 18 June 2014, UC Davis) (standard reference, not scraped)