Alphabeta Math
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.

✓ 8 results · all verified · 3 also independently AI-judged
Every result on this page is machine-checked by a proof checker and read in full and owner-audited; the judge is an additional, independent cross-model AI review of the proofs. The 5 not AI-judged were verified by owner audit (typically over a confirmed judge false positive), not failures.

Picard-Lindelöf and First-Order Ordinary Differential Equations: Examples and Counterexamples

1 · Prerequisites

2 · Summary

3 · Logical flowchart

4 · Definitions, theorems and proofs

None yet.

5 · Examples, counterexamples and false statements

ExampleConstruction: Literature-sourcedVerification: AI-adaptedprecheck passaudited 2026-08-21Open item page →

Picard iteration for y′=y, y(0)=1, recovers the exponential series

Example

For y′=y and y(0)=1, start from u0(t)=1. The Picard iterates are

um(t)=∑k=0mtkk!,

and converge uniformly on every bounded interval to exp⁡t, the unique solution.

Facts & Assumptions

Given: The scalar Picard operator (Tu)(t)=1+∫0tu(s)ds.

[L1]

The iterates ur converge to exp⁡ uniformly on every bounded interval (Picard iteration from 1 produces the exponential partial sums).

[L2]

Picard-Lindelöf gives a unique local solution of the IVP (Picard-Lindelöf local existence and uniqueness for first-order systems).

Verification

technique · direct
1.1givenL1

The cited construction gives um(t)=∑k=0mtk/k!, beginning with u0=1, and [L1] gives compact-uniform convergence to exp⁡.

2.1step 1.1L2∎

The limit satisfies the Picard equation, and [L2] identifies it with the unique solution of y′=y, y(0)=1.

ExampleConstruction: Literature-sourcedVerification: AI-adaptedprecheck passaudited 2026-08-21Open item page →

y′=y2, y(0)=1, has maximal solution y(t)=(1−t)−1 on (−∞,1)

Example

y′=y2, y(0)=1, has maximal solution y(t)=(1−t)−1 on (−∞,1). The vector field (t,y)↦y2 is nevertheless defined on all of R2.

Facts & Assumptions

Given: The scalar equation y′=y2 and initial value y(0)=1.

[L1]

If the positive maximal endpoint is finite, the solution must eventually leave every compact set (At a finite maximal time an ODE solution leaves every compact subset of the domain).

[L3]

Every Picard–Lindelöf IVP has a unique maximal solution, and every other solution through the same data is its restriction (Every Picard–Lindelöf initial value problem has one maximal solution on an open interval).

Verification

technique · direct
1.1givenL2algebra

Differentiation gives ((1−t)−1)′=(1−t)−2=y(t)2 and y(0)=1. On the connected component of a solution's nonzero set containing 0, [L2] gives (1/y)′=−1, so integration forces 1/y=1−t. If that component had a finite boundary c inside the solution interval, continuity would give y(t)→0 there and hence ∣1/y(t)∣→+∞, while the identity gives 1/y(t)→1−c∈R, a contradiction. Thus the component is the whole solution interval.

2.1step 1.1L1L3algebra∎

On every compact state interval ∣y∣,∣z∣≤R, one has ∣y2−z2∣≤2R∣y−z∣, so the polynomial field satisfies the local state-Lipschitz hypothesis of [L3]. The formula is defined on (−∞,1) and tends to +∞ as t↑1; no finite value permits continuation through 1, while the formula continues indefinitely to the left. Thus it is the unique maximal solution from [L3], consistently with the compact-escape conclusion [L1].

CounterexampleConstruction: Literature-sourcedVerification: AI-adaptedprecheck passaudited 2026-08-21Open item page →

y′=2∣y∣ has a continuum of delayed-start solutions through the origin

Statement refuted

Continuity of the right-hand side of a first-order IVP is enough for uniqueness. The continuous field f(y)=2∣y∣ refutes this: y′=2∣y∣ has distinct delayed-start solutions through the origin.

Facts & Assumptions

Given: For each c≥0, define yc(t)=0 for every t≤c and yc(t)=(t−c)2 for t≥c.

[L1]

For rational r>0, 0r=0 (Rational powers ar of a positive base).

[L2]

Local state-Lipschitz continuity requires one finite constant bounding the state difference quotient near the point (Local Lipschitz continuity in the state variable, locally uniform in time and parameters).

Counterexample

technique · direct
1.1givenL1algebra

On the first piece yc′=0=2∣yc∣ by [L1], on the second yc′=2(t−c)=2(t−c)2, and at t=c both one-sided derivatives are 0, so every yc is a solution through (0,0).

2.1step 1.1L2algebra∎

Distinct delays give distinct solutions, while ∣f(y)−f(0)∣/∣y∣=2/y for y>0, so [L2] rules out every finite local Lipschitz constant at zero.

CounterexampleConstruction: Literature-sourcedVerification: AI-adaptedprecheck passjudge pass (deepseek-v4-pro + gpt-5.6-terra)audited 2026-08-21Open item page →

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 F(t,y)=1Q(t); then y′=F(t,y) has no solution on any nondegenerate interval, for any initial value.

Facts & Assumptions

Given: The Dirichlet field F(t,y)=1Q(t).

[L1]

Every derivative has the intermediate-value property (Darboux's theorem: every derivative has the intermediate-value property).

Counterexample

technique · contradiction
1.1givenL2L3

By [L2] and [L3], F takes only 0 and 1, and takes both values on every nondegenerate interval.

2.1step 1.1L1assume-contradischarge-contradiction∎

Suppose a differentiable solution existed; its derivative would equal F but omit every value strictly between 0 and 1, contrary to [L1], so no local solution exists.

CounterexampleConstruction: AI-adaptedVerification: AI-adaptedprecheck passaudited 2026-08-21Open item page →

An almost-Lipschitz vector field has a unique solution through zero but is not locally Lipschitz there

Statement refuted

Local Lipschitz continuity is necessary for uniqueness through an initial point. Define f(0)=0 and, for 0<∣x∣<e−1,

f(x)=x(1+∣log⁡∣x∣∣),

with any continuous extension outside that interval. An almost-Lipschitz vector field has a unique solution through zero but is not locally Lipschitz there.

Facts & Assumptions

Given: The displayed field and the zero IVP y′=f(y), y(0)=0.

[L1]

The Osgood divergence condition gives uniqueness of solutions through the same initial value (Osgood's criterion gives uniqueness without a Lipschitz bound).

[L2]

For x>0, log⁡′(x)=1/x and log⁡x=∫1xdt/t (The natural logarithm has derivative 1/x and equals the integral from 1 to x of 1/t).

[L3]

An Osgood modulus is positive away from zero, nondecreasing, and has a divergent reciprocal integral at zero (Moduli of continuity and the Osgood divergence condition).

Counterexample

technique · direct
1.1givenL2algebra

The quotient ∣f(x)−f(0)∣/∣x∣=1+∣log⁡∣x∣∣ is unbounded as x→0 by [L2], so f is not locally Lipschitz at zero.

2.1step 1.1L1L2L3algebra∎

Define ϕ(r)=r(1−log⁡r) for 0<r≤e−1 with ϕ(0)=0, and put ρ=2ϕ on [0,e−1]. Differentiation using [L2] shows that ϕ is increasing and concave on this interval. On one side of zero, concavity with ϕ(0)=0 gives ∣ϕ(a)−ϕ(b)∣≤ϕ(∣a−b∣); on opposite sides, ∣a−b∣=∣a∣+∣b∣ and monotonicity gives ϕ(∣a∣)+ϕ(∣b∣)≤2ϕ(∣a−b∣). Since f is the odd extension of ϕ near zero, ρ is therefore a state modulus there. It has the properties in [L3], and the substitution u=1−log⁡r gives its reciprocal divergence, so [L1] makes the zero solution unique through the origin.

False statementConstruction: Literature-sourcedVerification: AI-adaptedprecheck passjudge pass (deepseek-v4-pro + gpt-5.6-terra)audited 2026-08-21Open item page →

False: continuity of the right-hand side guarantees unique ODE solutions

Statement

False claim: Every continuous right-hand side gives a unique local solution through each initial value.

Facts & Assumptions

Given: The false universal claim.

[L1]

y′=2∣y∣ has distinct delayed-start solutions through the origin (y′=2∣y∣ has a continuum of delayed-start solutions through the origin).

Refutation

technique · contradiction
1.1assume-contraL1

Suppose the false claim were true; [L1] gives a continuous right-hand side with distinct solutions through the same initial value.

2.1step 1.1discharge-contradiction∎

This contradicts the asserted uniqueness, so the claim is false.

False statementConstruction: Literature-sourcedVerification: AI-adaptedprecheck passaudited 2026-08-21Open item page →

False: a local ODE solution extends across the whole time-domain of its vector field

Statement

False claim: Every local solution extends across the whole time-domain on which its vector field is defined.

Facts & Assumptions

Given: The false universal claim.

[L1]

y′=y2, y(0)=1, has maximal solution y(t)=(1−t)−1 on (−∞,1) (y′=y2, y(0)=1, has maximal solution y(t)=(1−t)−1 on (−∞,1)).

Refutation

technique · contradiction
1.1assume-contraL1

Suppose the false claim were true; the vector field in [L1] is defined for all real times, but its solution has finite maximal endpoint 1.

2.1step 1.1discharge-contradiction∎

The asserted extension would continue this maximal solution past 1, a contradiction.

False statementConstruction: Literature-sourcedVerification: AI-adaptedprecheck passjudge pass (deepseek-v4-pro + gpt-5.6-terra)audited 2026-08-21Open item page →

False: local Lipschitz continuity is necessary for uniqueness of an ODE solution

Statement

False claim: A first-order ODE can have a unique solution through a point only if its vector field is locally Lipschitz there.

Facts & Assumptions

Given: The false necessity claim.

[L1]

An almost-Lipschitz vector field has a unique solution through zero but is not locally Lipschitz there (An almost-Lipschitz vector field has a unique solution through zero but is not locally Lipschitz there).

Refutation

technique · contradiction
1.1assume-contraL1

Suppose the false claim were true; [L1] gives uniqueness at zero while its vector field has no local Lipschitz constant there.

2.1step 1.1discharge-contradiction∎

This contradicts the asserted necessity, so the claim is false.

Sources