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.
Euclidean Ordinary Differential Equations with Smooth Dependence: Examples
1 · Prerequisites
- Absolute and Conditional Convergence; Rearrangement; Products
- Binary Operations, Monoids, Groups and Subgroups
- Compactness in Metric Spaces
- Completeness, Completion, and Uniform Continuity
- Connectedness
- Construction of the Natural Numbers
- Construction of the Real Numbers via Cauchy Sequences
- Construction of the Real Numbers via Dedekind Cuts
- Continuity, IVT, EVT, and Uniform Continuity
- Countability and Uncountability
- Euclidean Ordinary Differential Equations with Smooth Dependence
- Filters and Ultrafilters
- Finite Counting, Factorials and Binomial Coefficients
- Foundations of the Real Numbers for Analysis
- Limits of Real Functions
- limsup, liminf, and Subsequential Limits
- Linear Independence, Bases and Dimension
- Linear Transformations, Rank-Nullity and Quotient Spaces
- Metric Spaces
- Mixed Partials, Taylor Formulae, and Extrema
- Monotone Functions, Discontinuities, and Continuity Sets
- Monotone Sequences, Bolzano-Weierstrass, and Cauchy Completeness
- Order, Zorn's Lemma, and the Axiom of Choice
- Picard-Lindelöf and First-Order Ordinary Differential Equations
- Power Series and Real-Analytic Functions
- Properties of the Integral and the Working FTC
- Relations, Functions, and Quotients
- Rings, Subrings, Integral Domains and Fields
- Rⁿ as a Normed Space; Vector-Valued Functions
- Roots, Rational Powers, and Classical Inequalities
- Sequences and Limits
- Sequences and Series of Functions; Uniform Convergence
- Series: Convergence and the Nonnegative Tests
- Subspaces, Products, and Quotients
- Suprema and Infima
- The Derivative and the Mean Value Theorems
- The Exponential Function
- The Riemann Integral: Definition and Integrability
- The Total Derivative in ℝᵐ → ℝⁿ
- The ZFC Axioms and the Basic Set Constructions
- Topological Spaces and Continuity
- Topology of ℝ
- Vector Spaces, Linear Subspaces, Span and Direct Sums
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 , 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
A constant vector field has translation solutions
Example
Fix . The constant vector field has solutions
Thus its flow is translation by .
Facts & Assumptions
Given: A fixed vector and the autonomous equation .
Autonomous smooth ODEs have unique local smooth flows (The fundamental theorem for autonomous smooth ODEs).
Verification
The curve satisfies and for every , so [given] it solves the ODE.
By [L1], the local solution through is unique, so the displayed [L1, step 1.1] affine curve is the solution and the time- map is translation by .
A linear system and its fundamental matrix
Example
Consider the linear planar system
Its solution through is , and a fundamental matrix is
Facts & Assumptions
Given: The constant matrix .
The variational equation along a solution is a linear matrix ODE (The variational equation along an ODE solution).
Linear matrix ODEs have unique solutions on compact intervals (Linear matrix ODEs have unique global solutions on a fixed interval).
A fundamental matrix is invertible at every time (A fundamental matrix is invertible).
Verification
Differentiating the displayed formula gives [given] , and . So it is a solution.
The matrix satisfies and , so by [F1, L1, L2, step 1.1] [F1] and [L1] it is the fundamental matrix of this system. Its determinant is , which is consistent with [L2].
Therefore the linear system has the stated solution operator and [step 2.1] fundamental matrix.
The harmonic oscillator as a first-order system
Example
The second-order equation
becomes the first-order system
Its solutions are
Facts & Assumptions
Given: The matrix .
Autonomous smooth ODEs have unique local solutions (The fundamental theorem for autonomous smooth ODEs).
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
Setting turns into the displayed first-order system, and [given] conversely differentiating the first equation and substituting the second recovers .
Differentiating the displayed sine-cosine formulas gives [L1, L2, step 1.1] and , so they solve the first-order system with . By [L1] the solution is unique, and [L2] identifies the system as the oscillator written in first-order form.
Therefore the harmonic oscillator fits the first-order smooth-ODE framework [step 2.1] exactly as claimed.
A compactly supported vector field with global solutions
Example
Let be a smooth bump function supported in the closed unit ball, and fix . Then
is a compactly supported smooth vector field, so all of its maximal solutions are global.
Facts & Assumptions
Given: A smooth bump function supported in and a vector .
Every compactly supported smooth Euclidean vector field is complete (A compactly supported smooth Euclidean vector field is complete).
Verification
The support of is contained in the compact support of , [given] and is smooth because it is a scalar multiple of the constant vector by a smooth scalar function.
Therefore [L1] applies and makes every maximal trajectory of 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.
Smooth dependence in an ODE with a parameter
Example
For the parameter-dependent ODE
the solution is
It depends smoothly on both the initial value and the parameter .
Facts & Assumptions
Given: The parameter-dependent scalar ODE , .
Smooth parameter-dependent ODEs depend smoothly on the parameter (Smooth dependence of ODE solutions on parameters).
Smooth autonomous ODEs depend smoothly on initial data (Smooth dependence of solutions on initial data).
Verification
The curve satisfies and [given] , so it solves the ODE.
Differentiating the explicit formula gives [L1, L2, step 1.1] and , and higher derivatives are again polynomial multiples of . Thus the solution depends smoothly on both data variables, exactly as [L1] and [L2] predict.
So this ODE is a concrete instance of smooth dependence on initial data and [step 2.1] parameters.
A nonautonomous equation made autonomous by adjoining time
Example
The nonautonomous scalar equation
becomes autonomous after adjoining the time variable:
Its explicit solution is
Equivalently, in the original time variable , .
Facts & Assumptions
Given: The scalar equation with initial data .
The nonautonomous smooth-ODE theorem is proved by adjoining the time variable as an autonomous one (The fundamental theorem for nonautonomous smooth ODEs).
Verification
The augmented system has because and . Then [given] , so solving this linear scalar equation gives the displayed exponential formula.
Writing turns the displayed solution into [L1, step 1.1] , which is exactly the solution of the original nonautonomous equation. This is the concrete reduction promised by [L1].