ExampleConstruction: AI-adaptedVerification: AI-generatedprecheck passaudited 2026-08-01

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.

For every $k \geq 0$ , $x^{k} ∣ x ∣$ is $C^{k}$ but not $C^{k + 1}$

Example

For $k \in N$ , the function $f_{k} (x) = x^{k} ∣ x ∣$ is $C^{k}$ on $R$ but not $C^{k + 1}$ .

Facts & Assumptions

Given: $f_{k} (x) = x^{k} ∣ x ∣$ .

[L1]

Absolute value is piecewise $x$ and $- x$ (Absolute value in an ordered field), and powers differentiate by For a natural $n \geq 1$ the function $x \mapsto x^{n}$ is differentiable everywhere with derivative $ι (n) x^{n - 1}$ ; for $n = 0$ it is the constant $1$ , with derivative $0$ ; for a natural $n \geq 1$ the function $x \mapsto x^{- n}$ is differentiable at every $x \neq 0$ with derivative $- ι (n) x^{- n - 1}$ ; consequently every polynomial function is differentiable at every real, with the derivative computed term by term.

Verification

technique · cases

1.1

On $x > 0$ , $f_{k} = x^{k + 1}$ ; on $x < 0$ , $f_{k} = - x^{k + 1}$ .

assume-case positiveL1

2.1

Differentiating $j \leq k$ times gives constant multiples of $x^{k + 1 - j}$ with opposite signs, and both one-sided values tend to $0$ . Defining the derivative value at $0$ by the difference quotient gives matching continuous derivatives through order $k$ .

step 1.1assume-case throughkL1

2.2

The $(k + 1)$ -st one-sided derivatives are $(k + 1)!$ and $- (k + 1)!$ , so that derivative does not exist at $0$ .

assume-case nextorderstep 1.1L1

3.1

Hence $f_{k} \in C^{k} ∖ C^{k + 1}$ according to Higher derivatives and the classes $C^{k}$ and $C^{\infty}$ .

step 2.1step 2.2cases-exhaustive∎

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

26 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

MIT OpenCourseWare 18.100B Real Analysis, Spring 2025 lecture notes (standard reference, not scraped)

For every k≥0k≥0, xk∣x∣xk∣x∣ is CkCk but not Ck+1Ck+1