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 with and . There are analytic coordinates with near a. For an analytic scalar equation , , the derivative of its transformed equation with respect to the pure normal m-jet equals the principal symbol of its linearization evaluated at . 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 , 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.
Nonsingular analytic coordinate maps have analytic local inverses and nonsingular scalar equations have analytic implicit branches. (Real analytic inverse and implicit functions).
Highest-order coefficients transform by the inverse-transpose differential. (The principal symbol depends only on the first derivative of a smooth coordinate change).
Analytic higher derivatives are symmetric multilinear derivatives. (Continuous mixed partials of order are invariant under permutations).
Proof
After relabeling coordinates take . The map has determinant . F1 supplies an analytic inverse , and the initial surface is exactly t=0.
For any derivative of order m, repeated chain rule shows the coefficient of is : 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 , the principal symbol of its linearization. This agrees with F2 applied to that linearized operator.
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.
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 at its positive root. Thus is analytic. The map 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, . 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.
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
- Gantumur, Math 580 Lecture Notes 2: The Cauchy-Kovalevskaya Theorem (standard reference, not scraped)
- Ageno, Part III: Analysis of Partial Differential Equations (standard reference, not scraped)