Alphabeta MathHow 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 Dirichlet right-hand side gives a first-order equation with no solution
Statement refuted
Every scalar right-hand side admits a local solution. Let ; then has no solution on any nondegenerate interval, for any initial value.
Facts & Assumptions
Given: The Dirichlet field .
Every derivative has the intermediate-value property (Darboux's theorem: every derivative has the intermediate-value property).
The Dirichlet function is the indicator of the rationals (The Dirichlet function , and Thomae's function with at a rational in lowest terms with and at every irrational ).
The rationals and irrationals are both dense in (Both and are dense in , and every nonempty open subset of is uncountable).
Counterexample
By [L2] and [L3], takes only and , and takes both values on every nondegenerate interval.
Suppose a differentiable solution existed; its derivative would equal but omit every value strictly between and , contrary to [L1], so no local solution exists.
Depends on
- First-order systems, initial value problems, and solutions on intervals
- The Dirichlet function $1_{\mathbb{Q}}$, and Thomae's function $t$ with $t(x) = 1/q$ at a rational $x = p/q$ in lowest terms with $q \ge 1$ and $t(x) = 0$ at every irrational $x$
- Darboux's theorem: every derivative has the intermediate-value property
- Both $\mathbb{Q}$ and $\mathbb{R} \setminus \mathbb{Q}$ are dense in $\mathbb{R}$, and every nonempty open subset of $\mathbb{R}$ is uncountable
Used by
Nothing in the library uses this result yet.
Dependency tree · two levels
36 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, Ordinary Differential Equations and Dynamical Systems, Ch. 2 (standard reference, not scraped)
- Jiri Lebl, Basic Analysis I, Section 6.3 (standard reference, not scraped)