Alphabeta Math
Session-authored (Fable 5 assisted)
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.

6 results · all verified · 6 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; all 6 also cleared it.

Euclidean Ordinary Differential Equations with Smooth Dependence: Examples

1 · Prerequisites

2 · Summary

These examples make the flow and smooth-dependence statements concrete: constant and linear systems, the harmonic oscillator, a compactly supported field with global trajectories, parameter dependence in x˙=λx, and the standard reduction of a nonautonomous equation to an autonomous system in one higher dimension.

3 · Logical flowchart

4 · Definitions, theorems and proofs

None yet.

5 · Examples, counterexamples and false statements

ExampleConstruction: Literature-sourcedVerification: AI-generatedprecheck passjudge pass (gpt-5.6-terra)audited 2026-08-29Open item page →

A constant vector field has translation solutions

Example

Fix vRn. The constant vector field V(x)=v has solutions

x(t)=x0+tv.

Thus its flow is translation by tv.

Facts & Assumptions

Given: A fixed vector vRn and the autonomous equation x=v.

[L1]

Autonomous smooth ODEs have unique local smooth flows (The fundamental theorem for autonomous smooth ODEs).

Verification

technique · direct
1.1

The curve x(t)=x0+tv satisfies x(0)=x0 and x(t)=v for every t, so [given] it solves the ODE.

given
2.1

By [L1], the local solution through x0 is unique, so the displayed [L1, step 1.1] affine curve is the solution and the time-t map is translation by tv.

L1step 1.1
ExampleConstruction: Literature-sourcedVerification: AI-generatedprecheck passjudge pass (gpt-5.6-terra)audited 2026-08-29Open item page →

A linear system and its fundamental matrix

Example

Consider the linear planar system

x(t)=Ax(t),A=(1001).

Its solution through (x10,x20) is x(t)=(etx10,etx20), and a fundamental matrix is

Φ(t)=(et00et).

Facts & Assumptions

Given: The constant matrix A=diag(1,1).

[F1]

The variational equation along a solution is a linear matrix ODE (The variational equation along an ODE solution).

[L1]

Linear matrix ODEs have unique solutions on compact intervals (Linear matrix ODEs have unique global solutions on a fixed interval).

[L2]

A fundamental matrix is invertible at every time (A fundamental matrix is invertible).

Verification

technique · direct
1.1

Differentiating the displayed formula gives [given] x(t)=(etx10,etx20)=Ax(t), and x(0)=(x10,x20). So it is a solution.

given
2.1

The matrix Φ satisfies Φ(t)=AΦ(t) and Φ(0)=I2, so by [F1, L1, L2, step 1.1] [F1] and [L1] it is the fundamental matrix of this system. Its determinant is etet=1, which is consistent with [L2].

F1L1L2step 1.1
3.1

Therefore the linear system has the stated solution operator and [step 2.1] fundamental matrix.

step 2.1
ExampleConstruction: Literature-sourcedVerification: AI-generatedprecheck passjudge pass (gpt-5.6-terra)audited 2026-08-29Open item page →

The harmonic oscillator as a first-order system

Example

The second-order equation

q+q=0

becomes the first-order system

(qp)=(0110)(qp).

Its solutions are

q(t)=q0cost+p0sint,p(t)=q0sint+p0cost.

Facts & Assumptions

Given: The matrix A=(0110).

[L1]

Autonomous smooth ODEs have unique local solutions (The fundamental theorem for autonomous smooth ODEs).

[L2]

The linear-system example shows how to read a first-order matrix system and its solution operator (A linear system and its fundamental matrix).

Verification

technique · direct
1.1

Setting p=q turns q+q=0 into the displayed first-order system, and [given] conversely differentiating the first equation and substituting the second recovers q+q=0.

given
2.1

Differentiating the displayed sine-cosine formulas gives [L1, L2, step 1.1] q=p and p=q, so they solve the first-order system with (q(0),p(0))=(q0,p0). By [L1] the solution is unique, and [L2] identifies the system as the oscillator written in first-order form.

L1L2step 1.1
3.1

Therefore the harmonic oscillator fits the first-order smooth-ODE framework [step 2.1] exactly as claimed.

step 2.1
ExampleConstruction: Literature-sourcedVerification: AI-generatedprecheck passjudge pass (gpt-5.6-terra)audited 2026-08-29Open item page →

A compactly supported vector field with global solutions

Example

Let ρ:Rn[0,1] be a smooth bump function supported in the closed unit ball, and fix vRn. Then

V(x):=ρ(x)v

is a compactly supported smooth vector field, so all of its maximal solutions are global.

Facts & Assumptions

Given: A smooth bump function ρ supported in B(0,1) and a vector vRn.

[L1]

Every compactly supported smooth Euclidean vector field is complete (A compactly supported smooth Euclidean vector field is complete).

Verification

technique · direct
1.1

The support of V(x)=ρ(x)v is contained in the compact support of ρ, [given] and V is smooth because it is a scalar multiple of the constant vector v by a smooth scalar function.

given
2.1

Therefore [L1] applies and makes every maximal trajectory of V global. [L1, step 1.1] Outside the support of ρ, the field vanishes and the solution is locally constant, which is consistent with that completeness conclusion.

L1step 1.1
ExampleConstruction: Literature-sourcedVerification: AI-generatedprecheck passjudge pass (gpt-5.6-terra)audited 2026-08-29Open item page →

Smooth dependence in an ODE with a parameter

Example

For the parameter-dependent ODE

x(t)=λx(t),x(0)=x0,

the solution is

x(t;λ,x0)=eλtx0.

It depends smoothly on both the initial value x0 and the parameter λ.

Facts & Assumptions

Given: The parameter-dependent scalar ODE x=λx, x(0)=x0.

[L1]

Smooth parameter-dependent ODEs depend smoothly on the parameter (Smooth dependence of ODE solutions on parameters).

[L2]

Smooth autonomous ODEs depend smoothly on initial data (Smooth dependence of solutions on initial data).

Verification

technique · direct
1.1

The curve x(t)=eλtx0 satisfies x(0)=x0 and [given] x(t)=λeλtx0=λx(t), so it solves the ODE.

given
2.1

Differentiating the explicit formula gives [L1, L2, step 1.1] x0x(t;λ,x0)=eλt and λx(t;λ,x0)=teλtx0, and higher derivatives are again polynomial multiples of eλt. Thus the solution depends smoothly on both data variables, exactly as [L1] and [L2] predict.

L1L2step 1.1
3.1

So this ODE is a concrete instance of smooth dependence on initial data and [step 2.1] parameters.

step 2.1
ExampleConstruction: Literature-sourcedVerification: AI-generatedprecheck passjudge pass (gpt-5.6-terra)audited 2026-08-29Open item page →

A nonautonomous equation made autonomous by adjoining time

Example

The nonautonomous scalar equation

x(t)=tx(t),x(t0)=x0,

becomes autonomous after adjoining the time variable:

s(t)=1,x(t)=s(t)x(t),(s(0),x(0))=(t0,x0).

Its explicit solution is

s(t)=t+t0,x(t)=x0e(t+t0)2/2t02/2=x0e(t2+2t0t)/2.

Equivalently, in the original time variable τ=t+t0, x(τ)=x0e(τ2t02)/2.

Facts & Assumptions

Given: The scalar equation x=tx with initial data (t0,x0).

[L1]

The nonautonomous smooth-ODE theorem is proved by adjoining the time variable as an autonomous one (The fundamental theorem for nonautonomous smooth ODEs).

Verification

technique · direct
1.1

The augmented system has s(t)=t+t0 because s=1 and s(0)=t0. Then [given] x=s(t)x=(t+t0)x, so solving this linear scalar equation gives the displayed exponential formula.

given
2.1

Writing τ=t+t0 turns the displayed solution into [L1, step 1.1] x(τ)=x0e(τ2t02)/2, which is exactly the solution of the original nonautonomous equation. This is the concrete reduction promised by [L1].

L1step 1.1

Sources