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.
Quasilinear Characteristics and Cauchy Kovalevskaya
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
- Partial Differential Equations and Characteristics
- 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 Inverse and Implicit Function Theorems
- 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
Starting with a quasilinear Cauchy problem, this page separates ODE solvability from the inverse-projection step that actually constructs a PDE graph. It then makes projection failure precise through Burgers caustics, develops both Charpit invariants for fully nonlinear equations, and records the analytic Cauchy–Kovalevskaya theorem exactly without using its omitted proof.
3 · Logical flowchart
4 · Definitions, theorems and proofs
Semilinear and quasilinear first-order Cauchy problems on a parametrised hypersurface
Definition
Let and be open, let and be , with for every , and let and be smooth on an open set . Assume that for every . The Cauchy problem for the quasilinear equation is
It is semilinear when is independent of . At , a classical local solution is a function on an open neighbourhood of such that and the PDE holds for every , and such that there is a neighbourhood of with and for every . This specializes the first-order classification in Linear, semilinear, quasilinear, and fully nonlinear partial differential equations; the word noncharacteristic will be tested by the rank calculation below, rather than by importing the space-time transport convention of Noncharacteristic Cauchy surfaces for first-order transport.
The augmented characteristic system for a quasilinear first-order PDE
Definition
For the problem in Semilinear and quasilinear first-order Cauchy problems on a parametrised hypersurface, its augmented characteristic strip is a map satisfying
Here is the characteristic parameter and labels the initial point. The system concerns only ; no differential equation for a putative gradient is included in this definition.
Local solvability and C1 parameter dependence for the augmented characteristic ODE
Statement
At every , the system in The augmented characteristic system for a quasilinear first-order PDE has, after shrinking to and a neighbourhood of , a unique common solution for . It is in .
Facts & Assumptions
Given: The smooth coefficients and initial strip in the definition, and .
Proof
Put and . The coefficients in the defining Cauchy problem are smooth, so is smooth.
Apply Smooth dependence of ODE solutions on parameters to with initial value . It gives a common local interval, uniqueness, and dependence on ; including the ODE variable gives dependence on .
A quasilinear solution lifts to augmented characteristics
Statement
Let solve . If solves while it stays in , then satisfies . Thus solves the augmented characteristic ODE system.
Facts & Assumptions
Given: A solution , a differentiable curve with the stated ODE, and .
Proof
The chain rule gives .
Substitute and the PDE: .
Compatibility of a characteristic strip with Cauchy data
Statement
If a solution has and , then
The first condition is tangential compatibility. The rank condition for the projected strip is a separate hypothesis; it is not derived from this identity.
Facts & Assumptions
Given: The Cauchy data and a solution attaining them.
Proof
Differentiate with respect to to obtain .
Evaluate at and use to obtain the second identity.
Jacobian of a characteristic strip at its initial surface
Statement
For the local strip , the derivative of at is
Consequently is invertible exactly when this matrix has rank .
Facts & Assumptions
Given: The local strip supplied by the preceding lemma.
Proof
Its initial condition gives , and its ODE gives .
These are precisely the first and remaining columns of , proving the formula; an derivative is invertible exactly when it has rank .
Local quasilinear characteristic graph construction
Statement
At , suppose has rank . Then, after shrinking the characteristic strip, is a diffeomorphism onto an open set , and
is the unique function obtained by this inverse-projection construction. It attains ; the next lemma verifies its PDE.
Facts & Assumptions
Given: The smooth coefficients, data, and the stated full-rank condition at .
Proof
The local ODE lemma supplies a strip, and the Jacobian lemma makes invertible.
By The Euclidean inverse function theorem, shrink to a neighbourhood on which has a inverse. Define there.
At , and , hence . Any inverse-projected function from this strip has the same formula and is therefore identical to .
The inverse-projected characteristic graph satisfies the quasilinear PDE
Statement
The function constructed in Local quasilinear characteristic graph construction satisfies on its local domain.
Facts & Assumptions
Given: The local inverse-projected graph and its characteristic identities and .
Proof
The identity differentiates in to .
Substitute the two characteristic identities to get .
Since ranges over the local domain and , this is for every there.
Characteristic crossing and caustic for a first-order PDE
Definition
For a characteristic strip, a crossing or caustic is a point or time at which the projected map loses local rank or local one-to-one graphing. It is a failure of the projection needed to define , not a claim that the lifted ODE has reached its maximal lifespan. For a forward-time family, a first crossing time is an infimum in , with value when the relevant set is empty.
The Burgers slope obeys a Riccati law along characteristics
Statement
Let solve on an open . Let be an open interval containing zero and satisfy and . Then satisfies
for every ; in particular cannot vanish in .
Facts & Assumptions
Given: A classical Burgers solution and one of its projected characteristics.
Proof
Put . Differentiate in to obtain ; equality of mixed partials holds since is .
Along , the total-derivative chain rule gives , so .
Set and . Then and , so differentiation shows is constant and hence zero. Thus . If , this gives ; if , the identity rules out a zero denominator in and yields the displayed formula.
Inviscid Burgers characteristic formula and first crossing time
Statement
For with datum , every classical characteristic has
Thus and its first forward crossing time is
where the infimum of the empty set is .
Facts & Assumptions
Given: A classical Burgers solution with the stated initial datum.
Proof
Along , the chain rule and the PDE give .
The initial condition makes , hence and integration from gives .
Differentiating in gives , so the definition of caustic gives exactly the displayed set and its stated infimum convention.
Monotone Burgers data have no forward characteristic crossing
Statement
If for all , then for . Hence the Burgers projection has no forward crossing. This says nothing about any unrelated global lifespan condition.
Facts & Assumptions
Given: The characteristic formula and .
Proof
For , multiplication gives .
Therefore , so the zero set defining is empty and the projection has no forward crossing.
Uniqueness of a classical quasilinear solution before characteristic crossing
Statement
Let solve the same quasilinear Cauchy problem. On a connected region where their common characteristic projection from the data is a diffeomorphism, .
Facts & Assumptions
Given: Two solutions with identical data, and a connected region on which the common projection is a diffeomorphism.
Proof
The lifting lemma sends the restrictions of both solutions along each data-labelled characteristic to the same augmented initial-value problem.
Uniqueness of that ODE gives equal lifted values on the strip.
The diffeomorphic projection represents every point of the region as one , so step 2.1 gives there.
Fully nonlinear first-order PDEs and complete integrals
Definition
Let . A general first-order equation has the form ; it is fully nonlinear when its dependence on the highest-order variable is not affine after is fixed. A local complete integral on open sets is a family such that for every . Thus the parameters enter essentially rather than merely labelling repeated copies of one solution. A stationary envelope is a value selected by . This definition asserts neither global representation nor differentiability of an envelope.
A nondegenerate stationary envelope solves the Hamilton–Jacobi equation
Statement
If and is invertible, then locally defines a parameter . The envelope has and satisfies .
Facts & Assumptions
Given: A complete integral, a stationary point, and an invertible parameter Hessian there.
Proof
Apply the implicit function theorem to ; its derivative in is the invertible .
The chain rule gives on the stationary branch.
The complete-integral identity , evaluated at and using step 2.1, is .
The Lagrange–Charpit characteristic system
Definition
For on , the Lagrange–Charpit system is
with all derivatives evaluated at . The alternative contact normalization agrees with this one only along ; it is not silently substituted off that constraint.
The Charpit flow preserves the PDE constraint
Statement
Along a Charpit curve,
Consequently an initial point in remains in while the curve exists.
Facts & Assumptions
Given: A Charpit curve for a function .
Proof
The chain rule gives .
Substitute , , and ; the three terms cancel pairwise.
Hence is constant, so an initial zero stays zero.
Charpit contact compatibility is preserved
Statement
Let be a Charpit strip lying in . If , then
while the strip exists.
Facts & Assumptions
Given: A Charpit strip, its initial contact identity, and the constraint .
Proof
Set . Differentiate the Charpit equations in and apply the product and chain rules to obtain .
Differentiating in gives , so and .
Multiplication by the integrating factor makes constant; its initial value is zero, hence .
The Charpit momentum equation from differentiating Hamilton–Jacobi
Statement
If solves , put and let . Then
so the momentum equation is forced by differentiating the PDE.
Facts & Assumptions
Given: A classical solution and the stated projected characteristic.
Proof
Differentiate in to get .
Along , the chain rule gives .
Combining the two identities and gives .
Local fully nonlinear Charpit graph construction
Statement
Let be open and . Let be open, let , and let , , and be maps such that , , and for every . Suppose also that Then the Charpit strip through projects locally to a classical graph satisfying . It is unique while that projection is locally invertible among graphs obtained by inverse-projecting this fixed Charpit strip.
Facts & Assumptions
Given: The stated equation, compatible strip data, and full-rank condition at .
Proof
The Charpit vector field is because , hence locally Lipschitz. Continuous dependence gives a unique common local strip through the initial data .
The -dependence theorem makes this strip in . Its projected derivative at has columns , hence is invertible by the rank hypothesis.
The inverse function theorem supplies a local inverse of ; define .
Constraint preservation gives , while contact preservation gives ; the identity is . Since is invertible, these identities imply .
Substitution in the preserved constraint gives . The fixed strip and its local inverse determine this inverse-projected graph uniquely while the projection remains locally invertible.
Characteristics do not select a post-crossing weak solution
A crossing makes the characteristic projection fail to define a single-valued classical graph. It does not by itself choose a continuation: entropy conditions for conservation laws and viscosity inequalities for Hamilton–Jacobi equations are extra selection principles. No such weak-solution theorem is claimed here.
Cauchy–Kovalevskaya for a noncharacteristic analytic Cauchy problem
For an analytic th-order PDE posed on an analytic hypersurface and locally solved for the th derivative in a noncharacteristic normal direction, analytic data prescribing the normal derivatives through order determine a unique local analytic solution. The existence and uniqueness are within the analytic class and are local. This is a recorded external theorem, not a smooth-data theorem and not a result proved or used by this page.
The proof boundary of Cauchy–Kovalevskaya
Cauchy–Kovalevskaya for a noncharacteristic analytic Cauchy problem ‡ is recorded without its majorant-series proof. In particular, this page does not extend it to arbitrary smooth coefficients or data, and no later item may use the recorded theorem as a dependency.
5 · Examples, counterexamples and false statements
None yet.