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.

Convergence of the Goursat majorant

Statement

For integers d,N≥1 and M,r>0, choose 0<ρ≤1 with a=1−dNMρ/r>0 and put b=dNρ/r. The equation aq−bq2=M/(1−y/r)−M has a unique analytic branch q=g(y) through (0,0) with nonnegative coefficients. The solution of v′(σ)=g(σ/ρ+Nv(σ)), v(0)=0, is analytic with nonnegative coefficients. Setting Uj(t,x)=v(t+ρ∑ixi) gives a convergent majorant system solution of the preceding lemma, with U(0,0)=DxU(0,0)=0. Its initial trace U(0,x) is nonnegative coefficientwise but need not vanish identically.

Facts & Assumptions

Given: The positive parameters M,r, the finite positive integers N,d, and the prescribed Goursat majorant equation in the statement. A convergence proof and a choice of rho are required.

[F1]

A nonzero implicit derivative gives a local analytic branch. (Real analytic inverse and implicit functions).

[F2]

An analytic ODE has a unique analytic germ and preserves nonnegative coefficients with zero initial data. (Analytic ODE systems from majorants).

[F3]

An analytic positive-trace majorant with zero origin jet dominates the formal zero-data solution. (Positive majorants dominate the Cauchy recursion).

Proof

1.1givenF1algebra

Admissible choices exist: ρ=min⁡(1,r/(2dNM)) gives a≥1/2. Fix any rho allowed by the statement, so a>0. The analytic function P(y,q)=aq−bq2−M/(1−y/r)+M vanishes at (0,0) and has Pq(0,0)=a>0. F1 gives g. Writing g=∑k≥1ckyk yields ck=(b/a)∑i=1k−1cick−i+(M/a)r−k. At k=1 the sum is empty and c1=M/(ar)>0; successive coefficients are nonnegative.

2.1step 1.1F2

The function g(σ/ρ+Nv) is analytic near zero, and its power-series coefficients in sigma,v are nonnegative by the finite binomial expansion and step 1.1. F2 therefore gives an analytic v with nonnegative coefficients. Moreover v′(0)=g(0)=0. Choose a positive sigma-radius small enough that ∣σ/ρ+Nv(σ)∣ is inside the actual convergence radius of g and less than r, and that ∣bv′(σ)∣<1. These inequalities hold by continuity and their zero origin values.

3.1step 1.1step 2.1F3algebra

Put q=v′(σ) and y=σ/ρ+Nv(σ). The algebraic identity of step 1.1 is equivalent to (q+M)(1−bq)=M/(1−y/r), hence q=M/((1−y/r)(1−bq))−M on the neighborhood of step 2.1. With σ=t+ρ∑ixi we have ∂tUj=q, ∂xiUj=ρq, ∑jUj=Nv, and ∑i,j∂xiUj=dNρq. Substitution gives exactly the system G of F3.

4.1step 2.1step 3.1F3∎

On a sufficiently small polydisc in (t,x), ∣t∣+ρ∑i∣xi∣ is smaller than the radius selected in step 2.1, so this substitution converges absolutely. The coefficients of U and of its trace are nonnegative because those of v and the linear form are nonnegative. At the origin, Uj=v(0)=0 and ∂xiUj=ρv′(0)=0. Thus every hypothesis on U in F3 holds and U dominates the formal zero-data solution.

Source notes

Gantumur, §4 equations (47)–(52) and Remark 19, printed p. 10.

Depends on

Used by

Dependency tree · two levels

11 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