LemmaStatement: Literature-sourcedProof: AI-generatedPipeline-generatedprecheck passjudge pass (gpt-6-luna)

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.

Smooth local eigenpairs for a simple characteristic spectrum

Statement

Let $f : G \to R^{m}$ be $C^{3}$ and let $\overset{ˉ}{u} \in G$ be a state at which $A (\overset{ˉ}{u}) = D f (\overset{ˉ}{u})$ has distinct real eigenvalues $λ_{1}^{0} < \dots < λ_{m}^{0}$ . For each $i$ , there is a neighborhood $N_{i}$ of $\overset{ˉ}{u}$ and $C^{2}$ functions $λ_{i} : N_{i} \to R$ and $r_{i} : N_{i} \to R^{m}$ such that $A (u) r_{i} (u) = λ_{i} (u) r_{i} (u)$ , $λ_{i} (\overset{ˉ}{u}) = λ_{i}^{0}$ , and the eigenvectors can be normalized by a fixed linear functional. After intersecting these finitely many neighborhoods, the eigenvalues remain real, simple, and ordered, and $r_{1} (u), \dots, r_{m} (u)$ form a basis at each $u$ .

Facts & Assumptions

Given: An open state domain, a $C^{3}$ flux, and a base state whose flux Jacobian has distinct real eigenvalues.

[F1]

Strictly hyperbolic conservation systems and characteristic families: $A (u) = D f (u)$ is $C^{2}$ ; strict hyperbolicity means the eigenvalues are distinct and real.

[F2]

The Euclidean implicit function theorem with derivative formula: a $C^{1}$ equation $F (x, y) = 0$ with invertible $D_{y} F$ at a zero has a unique local $C^{1}$ solution $y = φ (x)$ and derivative $D φ = - (D_{y} F)^{- 1} D_{x} F$ .

Proof

1.1givenF1algebrachoose

Fix $i$ and choose right and left eigenvectors $r_{i}^{0}, l_{i}^{0}$ for $λ_{i}^{0}$ . For a simple eigenvalue, $l_{i}^{0} \cdot r_{i}^{0} \neq 0$ : otherwise $r_{i}^{0}$ is orthogonal to the left kernel of $A (\overset{ˉ}{u}) - λ_{i}^{0} I$ , hence lies in its range; a generalized eigenvector would then force algebraic multiplicity at least two. Normalize $l_{i}^{0} \cdot r_{i}^{0} = 1$ .

2.1step 1.1algebra

Define $F_{i} (u, λ, r) = (A (u) r - λ r, l_{i}^{0} \cdot r - 1)$ . At $(\overset{ˉ}{u}, λ_{i}^{0}, r_{i}^{0})$ it vanishes. Its derivative in $(r, λ)$ sends $(v, μ)$ to $((A (\overset{ˉ}{u}) - λ_{i}^{0} I) v - μ r_{i}^{0}, l_{i}^{0} \cdot v)$ . If this is zero, pairing the first component with $l_{i}^{0}$ gives $μ = 0$ ; then $v$ is a multiple of $r_{i}^{0}$ , and the last component forces $v = 0$ . The square derivative is therefore invertible.

3.1step 2.1F1F2

Since $F_{i}$ is $C^{2}$ , [F2] gives a local $C^{1}$ eigenpair. The derivative formula in [F2] is $C^{1}$ because $D F_{i}$ is $C^{1}$ and matrix inversion is smooth on invertible matrices; hence the eigenpair is $C^{2}$ . Continuity preserves the eigenvalue gaps and reality after shrinking the neighborhood.

4.1step 3.1algebrachoose∎

Eigenvectors belonging to distinct eigenvalues are linearly independent: applying $\prod_{j \neq i} (A - λ_{j} I)$ to a linear relation isolates its $i$ th coefficient. Thus the $m$ eigenvectors form a basis. Intersecting the $m$ neighborhoods proves the simultaneous assertion.

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

Alberto Bressan, Hyperbolic Conservation Laws: An Illustrated Tutorial (standard reference, not scraped)