Alphabeta Math
TheoremStatement: Literature-sourcedProof: AI-adaptedPipeline-generatedjudge pass (gpt-5.6-terra)audited 2026-09-09
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.

Cauchy–Kovalevskaya for first-order analytic systems

Statement

Let d,N1, let g:RdRN be analytic near zero, and let F be analytic near (0,0,g(0),Dg(0)). Then ut=F(t,x,u,Dxu), u(0,x)=g(x) has a unique real analytic solution germ at (0,0). Existence holds on a nonempty neighborhood; uniqueness is among analytic germs.

Facts & Assumptions

Given: An analytic first-order normal system with analytic initial data and a right side analytic at the actual initial value and spatial jet, as specified in the statement.

[F1]

Subtracting g gives an analytic zero-data system. (Subtracting analytic Cauchy jets).

[F2]

First-order analytic zero-data systems have a unique formal solution. (Formal recursion for solved analytic normal equations).

[F3]

The positive Goursat system dominates the zero-data formal solution. (Positive majorants dominate the Cauchy recursion).

[F4]

The specified positive system has a convergent analytic solution with the required origin jet. (Convergence of the Goursat majorant).

[F5]

Geometric coefficient bounds give convergence and termwise differentiation. (An absolutely convergent multi-indexed power series is holomorphic and differentiates termwise).

Proof

1.1

By F1 set w=ug(x) to obtain wt=H(t,x,w,Dxw) with zero data. Put c=H(0,0,0,0) and z=wtc. Its equation is zt=H(t,x,z+tc,Dxz)c=:K(t,x,z,Dxz), where K is analytic and K(0)=0. Its initial data remain zero. All substitutions stay inside the original analytic neighborhood after a finite shrinking.

givenF1algebra
2.1

F2 gives a unique formal z. Choose a common positive-radius coefficient bound M,r for the finite analytic family K (equivalently bound the absolute series on a smaller polydisc). F4 constructs the convergent positive Goursat majorant for these constants; F3 gives [tqxα]zj[tqxα]Uj. Choose a positive polyradius s strictly inside the convergence region of U. If C=maxjβ[Zβ]Ujsβ, then every coefficient of z is at most Csβ.

step 1.1F2F3F4
3.1

F5 makes z an analytic sum on a smaller polydisc and permits its spatial and time derivatives to be taken termwise. Shrink once more so the absolute sums of z and its spatial derivatives are inside the convergence radii of K. Expanding K then gives an absolutely convergent substitution, whose Taylor coefficients agree with the formal substitution in F2. Each coefficient of ztK(t,x,z,Dxz) is zero by the recursion; hence this function is identically zero there. All coefficients are real, so the restriction is a real analytic solution. Adding tc and g reverses step 1.1 and supplies the prescribed trace.

step 1.1step 2.1F2F5
4.1

Any other analytic solution undergoes the same subtraction in step 1.1; its Taylor series solves the identical zero-data formal problem. F2 forces equality of every coefficient with z. On a common smaller neighborhood both analytic functions equal their series and therefore coincide. Reversing the subtraction proves uniqueness of the original germ.

step 1.1step 3.1F2

Source notes

Gantumur, §4 Theorem 18, printed pp. 9–10; Corollary 20 proof, p. 11, for nonzero analytic data.

Depends on

Used by

Dependency tree · two levels

34 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