TheoremStatement: AI-adaptedProof: AI-generatedprecheck passaudited 2026-08-30

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 standard flat function is smooth and flat at zero

Statement

The standard flat function $β$ is smooth on $R$ , and $β^{(n)} (0) = 0$ for every $n \in N_{0}$ .

Facts & Assumptions

Given: The standard flat function $β$ .

[F1]

The standard flat function is $0$ on $(- \infty, 0]$ and is $\exp (- 1 / t)$ on $(0, \infty)$ (The standard flat function).

[L1]

For every $m \in N$ , one has $β (t) / t^{m} \to 0$ as $t \to 0^{+}$ (Exponential decay dominates every inverse power near zero).

[L2]

The derivative of $\exp$ is $\exp$ , and one-variable derivatives satisfy the chain rule and algebra rules (The exponential function is smooth and $(\exp)^{'} = \exp$ , The chain rule, in one line from Carathéodory: if $g$ is differentiable at $c$ and $f$ is differentiable at $g (c)$ , then $f \circ g$ is differentiable at $c$ with $(f \circ g)^{'} (c) = f^{'} (g (c)) g^{'} (c)$ , Sums, scalar multiples, products and quotients: $(f + g)^{'} (c) = f^{'} (c) + g^{'} (c)$ , $(α f)^{'} (c) = α f^{'} (c)$ , $(f g)^{'} (c) = f^{'} (c) g (c) + f (c) g^{'} (c)$ , and $(f / g)^{'} (c) = (f^{'} (c) g (c) - f (c) g^{'} (c)) / g (c)^{2}$ when $g (c) \neq 0$ ).

[A1]

For each $n \in N_{0}$ there is a polynomial $P_{n}$ such that $β^{(n)} (t) = P_{n} (1 / t) \exp (- 1 / t)$ for every $t > 0$ .

Proof

technique · direct

1.1

Repeatedly applying [L2] on $(0, \infty)$ proves [A1] by a routine induction on $n$ .

L2given

2.1

For each $n$ , both $β^{(n)} (t)$ and $β^{(n)} (t) / t$ are finite linear combinations of terms $β (t) / t^{m}$ , so both tend to $0$ as $t \to 0^{+}$ by [L1] and step 1.1.

L1step 1.1A1

3.1

We prove recursively that $β$ is $C^{n}$ , that $β^{(n)}$ vanishes on $(- \infty, 0]$ , and that $β^{(n)} (0) = 0$ . The case $n = 0$ is [F1]. If the claim holds for $n$ , then the left derivative of $β^{(n)}$ at $0$ is $0$ because $β^{(n)}$ is zero on $(- \infty, 0]$ , and the right derivative is $\lim_{t \to 0^{+}} β^{(n)} (t) / t = 0$ by step 2.1. Thus $β^{(n + 1)} (0)$ exists and equals $0$ , and step 2.1 also gives continuity at $0$ .

F1step 2.1

4.1

Hence $β$ is smooth on $R$ and all of its derivatives vanish at $0$ .

step 3.1∎

Depends on

Used by

The standard smooth step function Definition
The standard compactly supported bump on the line Example
The piecewise exponential flat function is not analytic at zero False statement

Dependency tree · two levels

24 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

John M. Lee, Introduction to Smooth Manifolds (standard reference, not scraped)
Will J. Merry, Differential Geometry (standard reference, not scraped)
Nigel Hitchin, Differentiable Manifolds (standard reference, not scraped)