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.

Subtracting analytic Cauchy jets

Statement

Let m1. Suppose tmu=F(t,x,(xαtju)α+jm, j<m) is analytic near the initial jet supplied by analytic functions gj(x), 0j<m. The substitution u=v+P, P(t,x)=j=0m1tjgj(x)/j!, bijectively transforms solutions with tju(0,x)=gj(x) into solutions of a solved analytic equation with exactly the same allowed jet orders and zero Cauchy data.

Facts & Assumptions

Given: An analytic solved normal equation of order m and analytic data gj(x) for its first m normal derivatives; for the first-order vector assertion the analytic right side is evaluated at the stated initial data and gradient.

[F1]

Finite analytic sums, derivatives and substitutions remain analytic on smaller neighborhoods. (Operations preserving coefficient majorisation).

Proof

1.1

For 0j<m, differentiation gives tjP==jm1tjg(x)/(j)!. Thus tjP(0,x)=gj(x) and tmP=0. Its tangential derivatives are obtained by replacing g with xαg and are analytic by F1.

givenF1algebra
2.1

For each allowed slot (α,j) put Pα,j=xαtjP. The transformed right-hand side is F~(t,x,(Vα,j))=F(t,x,(Vα,j+Pα,j(t,x))). This finite analytic substitution is made near the actual initial jet, so after translation of that centre F1 applies to zero-constant increments. It is analytic near (0,0,0) and introduces no new derivative slot. Since tmP=0, tmu=F is exactly tmv=F~.

givenstep 1.1F1
3.1

Step 1.1 gives tjv(0,x)=tju(0,x)gj(x), so the old data hold precisely when all the new data vanish. Conversely adding P to any zero-data solution reverses step 2.1 and restores every old data function. Addition and subtraction of P are inverse maps on the solution germs.

step 1.1step 2.1algebra

Source notes

Gantumur, §4 Corollary 20 proof, printed p. 11; the finite Taylor subtraction is computed locally.

Depends on

Used by

Dependency tree · two levels

10 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