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 flattening and the normal principal coefficient

Statement

Let ϕ be real analytic near aRd+1 with ϕ(a)=0 and dϕ(a)0. There are analytic coordinates (x,t) with t=ϕ near a. For an analytic scalar equation P(z,(Dαu)αm)=0, m1, the derivative of its transformed equation with respect to the pure normal m-jet equals the principal symbol of its linearization evaluated at dϕ. At a compatible m-jet where that scalar is nonzero the equation has a unique local analytic solved branch for the pure normal m-jet. Euclidean normal data mean Dju(X(x))[ν(x),,ν(x)], and can instead be flattened using analytic normal-line coordinates.

Facts & Assumptions

Given: An analytic hypersurface at p and an analytic scalar order-m equation with a compatible initial jet at which its normal principal symbol is nonzero, as specified in the statement.

[F1]

Nonsingular analytic coordinate maps have analytic local inverses and nonsingular scalar equations have analytic implicit branches. (Real analytic inverse and implicit functions).

[F2]

Highest-order coefficients transform by the inverse-transpose differential. (The principal symbol depends only on the first derivative of a smooth coordinate change).

[F3]

Analytic higher derivatives are symmetric multilinear derivatives. (Continuous mixed partials of order k are invariant under permutations).

Proof

1.1

After relabeling coordinates take zd+1ϕ(a)0. The map Ψ(z)=(z1a1,,zdad,ϕ(z)) has determinant zd+1ϕ(a). F1 supplies an analytic inverse z=Φ(x,t), and the initial surface is exactly t=0.

givenF1algebra
2.1

For any derivative Dzαu of order m, repeated chain rule shows the coefficient of tm(uΦ) is (dϕ)α: obtaining m derivatives on u requires that each differentiation hit u, while differentiation of a coordinate coefficient leaves lower order on u. All transformed jet expressions are analytic and linear in the top-order jets. Differentiating the transformed nonlinear P in the pure t-jet therefore gives α=mPuα(dϕ)α, the principal symbol of its linearization. This agrees with F2 applied to that linearized operator.

step 1.1F2algebra
3.1

At the specified compatible jet P=0, and step 2.1 makes its derivative in the selected scalar slot nonzero. F1 gives a unique analytic branch expressing this slot in terms of the remaining jets and (x,t). The remaining derivatives all have total order at most m and normal order strictly less than m. This proves the claimed solved form only near the selected compatible jet.

givenstep 2.1F1
4.1

For normal data, step 1.1 gives an analytic parametrization X of the surface. The nonvanishing analytic gradient has an analytic positive length: apply F1 to s2ϕ2=0 at its positive root. Thus ν=ϕ/ϕ is analytic. The map Θ(x,t)=X(x)+tν(x) has independent tangent columns and its unit normal column, hence invertible derivative, so F1 again gives an analytic inverse. By F3 and the fact that Theta is affine in t, tj(uΘ)(x,0)=Dju(X(x))[ν(x),,ν(x)]. The conormal dt in these coordinates is proportional to dphi on the surface; homogeneity of the degree-m symbol preserves its nonvanishing. Thus this flattening handles exactly the stated Euclidean normal data.

step 1.1step 2.1F1F3

Source notes

Gantumur, §5 equations (61)–(68), printed pp. 12–13. The linearization and analytic normal-line extensions are derived locally.

Depends on

Used by

Dependency tree · two levels

13 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