Alphabeta Math
LemmaStatement: 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.

Analytic ODE systems from majorants

Statement

For an analytic map H(t,v) near (0,v0)∈R×RN, N≥1, the problem v′=H(t,v), v(0)=v0, has a unique analytic solution germ. If v0=0 and all Taylor coefficients of H at (0,0) are nonnegative, then the solution has nonnegative Taylor coefficients.

Facts & Assumptions

Given: H(t,v) is analytic near (0,v0) in 1+N real variables, N≥1. The optional positivity assertion assumes v0=0 and nonnegative Taylor coefficients of H.

[F1]

A finite analytic family has a common rational geometric majorant. (Geometric majorants for analytic germs).

[F2]

Zero-constant substitution preserves coefficient majorisation. (Operations preserving coefficient majorisation).

[F3]

An analytic equation with nonzero derivative in its unknown has a unique local analytic branch. (Real analytic inverse and implicit functions).

[F4]

Geometrically bounded coefficients define a holomorphic sum with termwise derivatives. (An absolutely convergent multi-indexed power series is holomorphic and differentiates termwise).

Proof

1.1givenF2

Put w=v−v0, adjoin z0=t, and write z=(z0,w)∈RN+1. The autonomous system is z′=A(z)=(1,H(z0,v0+w)), z(0)=0. A formal series z=∑q≥1aqtq has the unique recursion (q+1)aq+1=[tq]A(z). This coefficient depends only on a1,…,aq: each substituted series has zero constant term, so no positive-degree factor can use aq+1. Its zeroth coordinate is exactly t.

1.2givenF1F3algebra

With L=N+1, F1 supplies M≥1,r>0 majorising every component of A by M/(1−∑i=0NZi/r). The scalar equation W−L2rW2=Mt, W(0)=0, has an analytic branch by F3: the derivative in W at zero is one. Its coefficient recursion W=Mt+L2rW2 gives [t]W=M and every subsequent coefficient nonnegative. Differentiating the identity yields W′=M/(1−LW/r) near zero, since the denominator there is one. Solving this quadratic on the branch through zero gives W=(r/L)(1−1−2LMt/r). The square root is the analytic branch with value one at zero, so a positive convergence neighborhood is explicit; its positive real endpoint t∗=r/(2LM) is singular, since differentiating W−LW2/(2r)=Mt there would give 0=M if W extended analytically through it. No entire majorant is claimed.

2.1step 1.1step 1.2F2

Compare the recursion in step 1.1 with the vector whose L components are W. At degree zero the initial coefficients agree. If ∣[tj]zi∣≤[tj]W for j≤q, F2 bounds [tq]Ai(z) by [tq]M/(1−LW/r)=(q+1)[tq+1]W. Dividing by q+1>0 gives the next coefficient bound. This induction proves zi≪W at every degree.

3.1step 1.1step 2.1F2F4∎

Choose s>0 strictly inside the convergence radius of W. Its coefficients obey [tq]W≤Cs−q, where C=∑q[tq]Wsq<∞. Step 2.1 transfers this bound to z. F4 and F2 show the series sums and its compositions differentiate as in the formal recursion on a smaller interval, so z′−A(z)=0. The recursion also forces the Taylor series of every analytic solution; hence two such germs coincide. Finally, for the original nonnegative H with v0=0, the recursion (q+1)[tq+1]v=[tq]H(t,v) consists solely of nonnegative sums and products from its zero initial coefficient, so every coefficient of v is nonnegative.

Source notes

Gantumur, §3 equations (26)–(34), printed pp. 7–8, Theorem 15. The autonomous augmentation and quadratic majorant below avoid the misnormalized scalar formula (18).

Depends on

Used by

Dependency tree · two levels

33 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