Alphabeta Math
ExampleConstruction: Literature-sourcedVerification: AI-adaptedSession-authored (Fable 5 assisted)precheck passaudited 2026-08-21
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.

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

Example

y=y2, y(0)=1, has maximal solution y(t)=(1t)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.1

Differentiation gives ((1t)1)=(1t)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=1t. 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)1cR, a contradiction. Thus the component is the whole solution interval.

givenL2algebra
2.1

On every compact state interval y,zR, one has y2z22Ryz, so the polynomial field satisfies the local state-Lipschitz hypothesis of [L3]. The formula is defined on (,1) and tends to + as t1; 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].

step 1.1L1L3algebra

Depends on

Used by

Dependency tree · two levels

20 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