Alphabeta Math
Pipeline-generated
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

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

DefinitionDefinition: Literature-sourcedProof: Not applicableaudited 2026-09-06Open item page →

Semilinear and quasilinear first-order Cauchy problems on a parametrised hypersurface

Definition

Let n1 and VRn1 be open, let γ:VRn and ϕ:VR be C1, with rankDγ(y)=n1 for every yV, and let a:ORn and b:OR be smooth on an open set ORn×R. Assume that (γ(y),ϕ(y))O for every yV. The Cauchy problem for the quasilinear equation is

a(x,u(x))Du(x)=b(x,u(x)),u(γ(y))=ϕ(y).

It is semilinear when a=a(x) is independent of u. At y0V, a classical local solution is a C1 function u on an open neighbourhood Ω of γ(y0) such that (x,u(x))O and the PDE holds for every xΩ, and such that there is a neighbourhood WV of y0 with γ(W)Ω and u(γ(y))=ϕ(y) for every yW. 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.

DefinitionDefinition: Literature-sourcedProof: Not applicablejudge pass (gpt-5.6-terra)audited 2026-09-06Open item page →

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 (X,Z)(s,y) satisfying

X˙=a(X,Z),Z˙=b(X,Z),(X,Z)(0,y)=(γ(y),ϕ(y)).

Here s is the characteristic parameter and yV labels the initial point. The system concerns only (X,Z); no differential equation for a putative gradient is included in this definition.

LemmaStatement: Literature-sourcedProof: AI-generatedjudge pass (gpt-5.6-terra)audited 2026-09-06Open item page →

Local solvability and C1 parameter dependence for the augmented characteristic ODE

Statement

At every y0V, the system in The augmented characteristic system for a quasilinear first-order PDE has, after shrinking to s<ϵ and a neighbourhood W of y0, a unique common solution (X,Z) for yW. It is C1 in (s,y).

Facts & Assumptions

Given: The smooth coefficients and C1 initial strip in the definition, and y0V.

Proof

technique · direct
1.1

Put Y:=(X,Z) and G(x,z):=(a(x,z),b(x,z)). The coefficients in the defining Cauchy problem are smooth, so G is smooth.

givenconstruct
2.1

Apply Smooth dependence of ODE solutions on parameters to Y=G(Y) with initial value Y(0,y)=(γ(y),ϕ(y)). It gives a common local interval, uniqueness, and C1 dependence on y; including the ODE variable gives C1 dependence on (s,y).

step 1.1given
LemmaStatement: Literature-sourcedProof: AI-generatedaudited 2026-09-06Open item page →

A quasilinear solution lifts to augmented characteristics

Statement

Let uC1(Ω) solve a(x,u)Du=b(x,u). If X solves X˙=a(X,u(X)) while it stays in Ω, then Z:=u(X) satisfies Z˙=b(X,Z). Thus (X,Z) solves the augmented characteristic ODE system.

Facts & Assumptions

Given: A C1 solution u, a differentiable curve X with the stated ODE, and Z=uX.

Proof

technique · direct
1.1

The chain rule gives Z˙=Du(X)X˙.

givenalgebra
2.1

Substitute X˙=a(X,u(X)) and the PDE: Z˙=Du(X)a(X,u(X))=b(X,u(X))=b(X,Z).

step 1.1givenalgebra
LemmaStatement: Literature-sourcedProof: AI-generatedaudited 2026-09-06Open item page →

Compatibility of a characteristic strip with Cauchy data

Statement

If a C1 solution has u(γ(y))=ϕ(y) and p0(y):=Du(γ(y)), then

p0(y)Dγ(y)=Dϕ(y),p0(y)a(γ(y),ϕ(y))=b(γ(y),ϕ(y)).

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 C1 Cauchy data and a C1 solution attaining them.

Proof

technique · direct
1.1

Differentiate uγ=ϕ with respect to y to obtain Du(γ)Dγ=Dϕ.

givenalgebra
2.1

Evaluate a(x,u)Du=b(x,u) at x=γ(y) and use u(γ(y))=ϕ(y) to obtain the second identity.

givenalgebra
LemmaStatement: Literature-sourcedProof: AI-generatedjudge pass (gpt-5.6-terra)audited 2026-09-06Open item page →

Jacobian of a characteristic strip at its initial surface

Statement

For the local strip (X,Z), the derivative of Ψ(s,y):=X(s,y) at s=0 is

D(s,y)Ψ(0,y)=[a(γ(y),ϕ(y)),Dγ(y)].

Consequently D(s,y)Ψ(0,y) is invertible exactly when this n×n matrix has rank n.

Facts & Assumptions

Given: The C1 local strip supplied by the preceding lemma.

Proof

technique · direct
1.1

Its initial condition gives DyX(0,y)=Dγ(y), and its ODE gives sX(0,y)=a(γ(y),ϕ(y)).

givenalgebra
2.1

These are precisely the first and remaining columns of D(s,y)Ψ(0,y), proving the formula; an n×n derivative is invertible exactly when it has rank n.

step 1.1algebra
TheoremStatement: Literature-sourcedProof: AI-generatedjudge pass (gpt-5.6-terra)audited 2026-09-06Open item page →

Local quasilinear characteristic graph construction

Statement

At y0V, suppose [a(γ(y0),ϕ(y0)),Dγ(y0)] has rank n. Then, after shrinking the characteristic strip, Ψ(s,y)=X(s,y) is a C1 diffeomorphism onto an open set U, and

u(x):=Z(Ψ1(x))

is the unique C1 function obtained by this inverse-projection construction. It attains u(γ(y))=ϕ(y); the next lemma verifies its PDE.

Facts & Assumptions

Given: The smooth coefficients, C1 data, and the stated full-rank condition at y0.

Proof

technique · direct
1.1

The local ODE lemma supplies a C1 strip, and the Jacobian lemma makes DΨ(0,y0) invertible.

givenalgebra
2.1

By The Euclidean inverse function theorem, shrink to a neighbourhood on which Ψ has a C1 inverse. Define u=ZΨ1 there.

step 1.1construct
3.1

At s=0, Ψ(0,y)=γ(y) and Z(0,y)=ϕ(y), hence u(γ(y))=ϕ(y). Any inverse-projected function from this strip has the same formula and is therefore identical to u.

step 2.1given
LemmaStatement: Literature-sourcedProof: AI-generatedjudge pass (gpt-5.6-terra)audited 2026-09-06Open item page →

The inverse-projected characteristic graph satisfies the quasilinear PDE

Statement

The function u=ZΨ1 constructed in Local quasilinear characteristic graph construction satisfies a(x,u(x))Du(x)=b(x,u(x)) on its local domain.

Facts & Assumptions

Given: The local inverse-projected graph and its characteristic identities Xs=a(X,Z) and Zs=b(X,Z).

Proof

technique · direct
1.1

The identity u(X(s,y))=Z(s,y) differentiates in s to Du(X)Xs=Zs.

givenalgebra
2.1

Substitute the two characteristic identities to get Du(X)a(X,Z)=b(X,Z).

step 1.1givenalgebra
3.1

Since X=Ψ(s,y) ranges over the local domain and Z=u(X), this is a(x,u(x))Du(x)=b(x,u(x)) for every x there.

step 2.1given
DefinitionDefinition: Literature-sourcedProof: Not applicablejudge pass (gpt-5.6-terra)audited 2026-09-06Open item page →

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 (s,y)X(s,y) loses local rank or local one-to-one graphing. It is a failure of the projection needed to define u=ZX1, not a claim that the lifted ODE (X,Z) has reached its maximal lifespan. For a forward-time family, a first crossing time is an infimum in [0,], with value when the relevant set is empty.

LemmaStatement: Literature-sourcedProof: AI-generatedaudited 2026-09-06Open item page →

The Burgers slope obeys a Riccati law along characteristics

Statement

Let uC2(Ω) solve ut+uux=0 on an open ΩR2. Let I be an open interval containing zero and XC1(I) satisfy (t,X(t))Ω and X˙=u(t,X). Then q(t):=ux(t,X(t)) satisfies

q˙=q2,q(t)=q(0)1+tq(0)

for every tI; in particular 1+tq(0) cannot vanish in I.

Facts & Assumptions

Given: A C2 classical Burgers solution and one of its projected characteristics.

Proof

technique · direct
1.1

Put r(t,x)=ux(t,x). Differentiate ut+uux=0 in x to obtain rt+urx+r2=0; equality of mixed partials holds since u is C2.

givenalgebra
2.1

Along X˙=u, the total-derivative chain rule gives q˙=rt(t,X)+u(t,X)rx(t,X), so q˙=q2.

step 1.1givenalgebra
3.1

Set c=q(0) and h(t)=(1+tc)q(t)c. Then h(0)=0 and h=qh, so differentiation shows h(t)exp(0tq(s)ds) is constant and hence zero. Thus (1+tc)q(t)=c. If c=0, this gives q=0; if c0, the identity rules out a zero denominator in I and yields the displayed formula.

step 2.1algebra
TheoremStatement: Literature-sourcedProof: AI-generatedjudge pass (gpt-5.6-terra)audited 2026-09-06Open item page →

Inviscid Burgers characteristic formula and first crossing time

Statement

For ut+uux=0 with C1 datum u(0,ξ)=u0(ξ), every classical characteristic has

u(t,X(t,ξ))=u0(ξ),X(t,ξ)=ξ+tu0(ξ).

Thus Xξ=1+tu0(ξ) and its first forward crossing time is

T:=inf{t0:ξ, 1+tu0(ξ)=0}[0,],

where the infimum of the empty set is .

Facts & Assumptions

Given: A classical Burgers solution with the stated C1 initial datum.

Proof

technique · direct
1.1

Along X˙=u(t,X), the chain rule and the PDE give d(u(t,X))/dt=ut+uux=0.

givenalgebra
2.1

The initial condition makes u(t,X)=u0(ξ), hence X˙=u0(ξ) and integration from X(0,ξ)=ξ gives X=ξ+tu0(ξ).

step 1.1givenalgebra
3.1

Differentiating in ξ gives Xξ=1+tu0(ξ), so the definition of caustic gives exactly the displayed set and its stated infimum convention.

step 2.1given
CorollaryStatement: Literature-sourcedProof: AI-generatedjudge pass (gpt-5.6-terra)audited 2026-09-06Open item page →

Monotone Burgers data have no forward characteristic crossing

Statement

If u0(ξ)0 for all ξ, then 1+tu0(ξ)1 for t0. Hence the Burgers projection has no forward crossing. This says nothing about any unrelated global lifespan condition.

Facts & Assumptions

Given: The characteristic formula and u00.

Proof

technique · direct
1.1

For t0, multiplication gives tu0(ξ)0.

givenalgebra
2.1

Therefore 1+tu0(ξ)1, so the zero set defining T is empty and the projection has no forward crossing.

step 1.1given
TheoremStatement: Literature-sourcedProof: AI-generatedjudge pass (gpt-5.6-terra)audited 2026-09-06Open item page →

Uniqueness of a classical quasilinear solution before characteristic crossing

Statement

Let u,vC1 solve the same quasilinear Cauchy problem. On a connected region where their common characteristic projection from the data is a diffeomorphism, u=v.

Facts & Assumptions

Given: Two C1 solutions with identical data, and a connected region on which the common projection is a diffeomorphism.

Proof

technique · direct
1.1

The lifting lemma sends the restrictions of both solutions along each data-labelled characteristic to the same augmented initial-value problem.

givenconstruct
2.1

Uniqueness of that ODE gives equal lifted values u(X(s,y))=v(X(s,y)) on the strip.

step 1.1given
3.1

The diffeomorphic projection represents every point of the region as one X(s,y), so step 2.1 gives u=v there.

step 2.1given
DefinitionDefinition: Literature-sourcedProof: Not applicablejudge pass (gpt-5.6-terra)audited 2026-09-06Open item page →

Fully nonlinear first-order PDEs and complete integrals

Definition

Let F:ORn×R×RnR. A general first-order equation has the form F(x,u,Du)=0; it is fully nonlinear when its dependence on the highest-order variable p=Du is not affine after (x,u) is fixed. A local complete integral on open sets U,ARn is a C2 family S:U×AR such that (x,S(x;α),DxS(x;α))O,F(x,S(x;α),DxS(x;α))=0,detDxα2S(x;α)0 for every (x,α)U×A. Thus the n parameters enter essentially rather than merely labelling repeated copies of one solution. A stationary envelope is a value u(x)=S(x;α(x)) selected by Sα(x;α(x))=0. This definition asserts neither global representation nor differentiability of an envelope.

LemmaStatement: Literature-sourcedProof: AI-generatedjudge pass (gpt-5.6-terra)audited 2026-09-06Open item page →

A nondegenerate stationary envelope solves the Hamilton–Jacobi equation

Statement

If Sα(x0;α0)=0 and Sαα(x0;α0) is invertible, then locally Sα(x;α(x))=0 defines a C1 parameter α(x). The envelope u=S(x;α(x)) has Du=Sx(x;α(x)) and satisfies F(x,u,Du)=0.

Facts & Assumptions

Given: A C2 complete integral, a stationary point, and an invertible parameter Hessian there.

Proof

technique · direct
1.1

Apply the implicit function theorem to G(x,α)=Sα(x;α); its derivative in α is the invertible Sαα.

givenconstruct
2.1

The chain rule gives Du=Sx+SαDα=Sx on the stationary branch.

step 1.1givenalgebra
3.1

The complete-integral identity F(x,S,Sx)=0, evaluated at α(x) and using step 2.1, is F(x,u,Du)=0.

step 2.1given
DefinitionDefinition: Literature-sourcedProof: Not applicablejudge pass (gpt-5.6-terra)audited 2026-09-06Open item page →

The Lagrange–Charpit characteristic system

Definition

For FC2(O) on ORn×R×Rn, the Lagrange–Charpit system is

X˙=Fp,Z˙=PFp,P˙=FxPFz,

with all derivatives evaluated at (X,Z,P). The alternative contact normalization Z˙=PFpF agrees with this one only along F=0; it is not silently substituted off that constraint.

LemmaStatement: Literature-sourcedProof: AI-generatedjudge pass (gpt-5.6-terra)audited 2026-09-06Open item page →

The Charpit flow preserves the PDE constraint

Statement

Along a Charpit curve,

ddsF(X,Z,P)=0.

Consequently an initial point in F=0 remains in F=0 while the curve exists.

Facts & Assumptions

Given: A C1 Charpit curve for a C2 function F.

Proof

technique · direct
1.1

The chain rule gives F˙=FxX˙+FzZ˙+FpP˙.

givenalgebra
2.1

Substitute X˙=Fp, Z˙=PFp, and P˙=FxPFz; the three terms cancel pairwise.

step 1.1givenalgebra
3.1

Hence F(X,Z,P) is constant, so an initial zero stays zero.

step 2.1given
LemmaStatement: Literature-sourcedProof: AI-generatedjudge pass (gpt-5.6-terra)audited 2026-09-06Open item page →

Charpit contact compatibility is preserved

Statement

Let (X,Z,P)(s,y) be a C1 Charpit strip lying in F=0. If Zy(0,y)=P(0,y)Xy(0,y), then

Zy(s,y)=P(s,y)Xy(s,y)

while the strip exists.

Facts & Assumptions

Given: A C1 Charpit strip, its initial contact identity, and the constraint F(X,Z,P)=0.

Proof

technique · direct
1.1

Set D:=ZyPXy. Differentiate the Charpit equations in y and apply the product and chain rules to obtain Ds=FyFzD.

givenalgebra
2.1

Differentiating F(X,Z,P)=0 in y gives Fy=0, so Ds=FzD and D(0,y)=0.

step 1.1givenalgebra
3.1

Multiplication by the integrating factor exp(0sFz(r,y)dr) makes D constant; its initial value is zero, hence D=0.

step 2.1algebra
LemmaStatement: Literature-sourcedProof: AI-generatedjudge pass (gpt-5.6-terra)audited 2026-09-06Open item page →

The Charpit momentum equation from differentiating Hamilton–Jacobi

Statement

If uC2 solves F(x,u,Du)=0, put P=Du(X) and let X˙=Fp(X,u(X),Du(X)). Then

P˙=FxPFz,

so the momentum equation is forced by differentiating the PDE.

Facts & Assumptions

Given: A C2 classical solution and the stated projected characteristic.

Proof

technique · direct
1.1

Differentiate F(x,u(x),Du(x))=0 in x to get Fx+FzDu+D2uFp=0.

givenalgebra
1.2

Along X, the chain rule gives P˙=D2u(X)X˙=D2u(X)Fp.

givenalgebra
2.1

Combining the two identities and P=Du(X) gives P˙=FxPFz.

step 1.1step 1.2algebra
TheoremStatement: Literature-sourcedProof: AI-generatedaudited 2026-09-06Open item page →

Local fully nonlinear Charpit graph construction

Statement

Let ORn×R×Rn be open and FC2(O). Let VRn1 be open, let y0V, and let γ:VRn, ϕ:VR, and p0:VRn be C1 maps such that (γ(y),ϕ(y),p0(y))O, F(γ(y),ϕ(y),p0(y))=0, and Dϕ(y)=p0(y)Dγ(y) for every yV. Suppose also that rank[Fp(γ(y0),ϕ(y0),p0(y0)),Dγ(y0)]=n. Then the Charpit strip through (γ,ϕ,p0) projects locally to a classical graph u satisfying F(x,u,Du)=0. It is unique while that projection is locally invertible among graphs obtained by inverse-projecting this fixed Charpit strip.

Facts & Assumptions

Given: The stated C2 equation, compatible C1 strip data, and full-rank condition at y0.

Proof

technique · direct
1.1

The Charpit vector field is C1 because FC2, hence locally Lipschitz. Continuous dependence gives a unique common local strip through the C1 initial data (γ,ϕ,p0).

givenconstruct
2.1

The C1-dependence theorem makes this strip C1 in (s,y). Its projected derivative at s=0 has columns [Fp,Dγ], hence is invertible by the rank hypothesis.

step 1.1givenalgebra
3.1

The inverse function theorem supplies a local inverse of (s,y)X(s,y); define u(X(s,y)):=Z(s,y).

step 2.1construct
4.1

Constraint preservation gives F(X,Z,P)=0, while contact preservation gives DyZ=PDyX; the s identity is Zs=PXs. Since D(s,y)X is invertible, these identities imply Du(X)=P.

step 3.1givenalgebra
5.1

Substitution in the preserved constraint gives F(x,u(x),Du(x))=0. The fixed strip and its local inverse determine this inverse-projected graph uniquely while the projection remains locally invertible.

step 4.1given
RemarkRemark: Literature-sourcedProof: Not applicablejudge pass (gpt-5.6-terra)audited 2026-09-06Open item page →

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.

RemarkRemark: Literature-sourcedProof: Not suppliedaudited 2026-09-06 sources checked 2026-09-06 not proved hereOpen item page →
Recorded, not proved here. This statement is included so the library can refer to it honestly, with a citation to the literature. It is not proved anywhere in this library: the track that would prove it has not been developed here yet.

Cauchy–Kovalevskaya for a noncharacteristic analytic Cauchy problem

For an analytic mth-order PDE posed on an analytic hypersurface and locally solved for the mth derivative in a noncharacteristic normal direction, analytic data prescribing the normal derivatives through order m1 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.

RemarkRemark: Literature-sourcedProof: Not applicablejudge pass (gpt-5.6-terra)audited 2026-09-06 rests on unproved materialOpen item page →
Rests on 1 statement not proved in this library. Every dependency marked below is recorded with a citation but is not established here, because the track that would prove it has not yet been developed in this library. Everything else in this proof is proved here.

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.

Sources