LemmaStatement: Literature-sourcedProof: AI-adaptedPipeline-generatedjudge 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.

A regular solution curve has a unique local arclength chart and a quadratic predictor defect

Statement

Let $n \geq 1$ , let $U \subseteq R^{n + 1}$ be open, and let $F : U \to R^{n}$ be $C^{2}$ . Suppose $F (z_{0}) = 0$ and $rank D F (z_{0}) = n$ . Let $t \in \ker D F (z_{0})$ be a unit vector. There is an interval about $0$ and a unique local $C^{2}$ curve $γ (r)$ satisfying $F (γ (r)) = 0, γ (0) = z_{0}, t^{T} (γ (r) - z_{0}) = r .$ There is a neighborhood $V$ of $z_{0}$ in which every solution $z$ of $F (z) = 0$ has the form $z = γ (t^{T} (z - z_{0}))$ . It has $γ^{'} (0) = t$ . After reparameterization by Euclidean arclength, the same local curve is represented by a $C^{1}$ unit-speed curve $c (s)$ with $c (0) = z_{0}$ and $c^{'} (0) = t$ .

Let $K \subseteq U$ be convex, let $c (s)$ and the segment from $c (s)$ to $c (s) + h c^{'} (s)$ lie in $K$ for a step $h > 0$ , and suppose $∥ D F (u) - D F (v) ∥_{o p} \leq L ∥ u - v ∥_{2} (u, v \in K) .$ For $z_{p} : = c (s) + h c^{'} (s)$ , the augmented pseudo-arclength residual $G_{s, h} (z) : = (F (z), c^{'} (s)^{T} (z - z_{p}))$ satisfies $∥ G_{s, h} (z_{p}) ∥_{2} = ∥ F (z_{p}) ∥_{2} \leq \frac{\sqrt{n} L}{2} h^{2} .$ Thus the predictor defect is quadratic in the step length on the stated tube.

Facts & Assumptions

Given: $U, F, z_{0}, t, K, L$ and the hypotheses in the Statement.

[F1]

Invertibility and a norm bound for the pseudo-arclength bordered matrix: if $A : R^{n + 1} \to R^{n}$ has rank $n$ , $t$ is a unit kernel vector, and $τ$ is unit, then $[\begin{array}{c} A \\ τ^{T} \end{array}]$ is invertible exactly when $τ^{T} t \neq 0$ .

[F2]

The parametrized implicit function theorem with $C^{k}$ regularity: for a $C^{2}$ equation whose derivative in the solved variables is invertible, there is a unique local $C^{2}$ implicit solution, and every nearby zero of the equation is on its graph.

[F3]

The chain rule for total derivatives: $D (g \circ f) (a) = D g (f (a)) \circ D f (a)$ : the derivative of a composite is the composite of the derivatives.

[F4]

A continuous function on $[a, b]$ is Riemann integrable, by Heine-Cantor and Riemann's criterion and Newton–Leibniz needs only continuity on $[a, b]$ , differentiability on $(a, b)$ , and a Riemann-integrable extension of the interior derivative: a scalar $C^{1}$ function on a compact interval equals its initial value plus the integral of its derivative.

[F5]

If $f \leq g$ on $[a, b]$ and both are integrable then $\int_{a}^{b} f \leq \int_{a}^{b} g$ ; and $m (b - a) \leq \int_{a}^{b} f \leq M (b - a)$ : pointwise bounds between integrable real functions pass to their integrals.

[F6]

Cauchy-Schwarz $∣ ⟨ x, y ⟩ ∣ \leq ∥ x ∥_{2} ∥ y ∥_{2}$ with its equality case, the triangle inequality for $∥ \cdot ∥_{2}$ , the parallelogram law and polarisation: a coordinate of a vector has absolute value at most its Euclidean norm.

[F7]

The Euclidean inverse function theorem: a $C^{1}$ map with invertible derivative at a point has a local $C^{1}$ inverse.

[F8]

$C^{k}$ Euclidean maps and diffeomorphisms: $C^{2}$ means each scalar component has continuous coordinate partial derivatives through order two.

[F9]

The total (Fréchet) derivative $D f (a)$ as the linear first-order approximation with $o (∥ h ∥_{2})$ remainder: $D F (z)$ is the linear map in the first-order approximation $F (z + h) = F (z) + D F (z) h + o (∥ h ∥_{2})$ .

[F10]

Rank and nullity of a linear map with finite-dimensional domain: rank is the dimension of the image of a linear map with finite-dimensional domain.

[F11]

Rank-nullity: $\dim_{F} V = nullity T + rank T$ : the kernel dimension plus the image dimension equals the domain dimension.

[F12]

The first fundamental theorem: if $f$ is integrable on $[a, b]$ and continuous at $c$ , then $F^{'} (c) = f (c)$ ; in particular a continuous $f$ has $F$ as a primitive: the integral function of a continuous scalar integrand has derivative equal to that integrand.

[F13]

For $a < c < b$ : $f$ is integrable on $[a, b]$ if and only if it is integrable on $[a, c]$ and on $[c, b]$ , and then $\int_{a}^{b} f = \int_{a}^{c} f + \int_{c}^{b} f$ ; with the oriented form for arbitrary $a, b, c$ in its oriented form and The integral with oriented limits: $\int_{a}^{a} f : = 0$ and $\int_{b}^{a} f : = - \int_{a}^{b} f$ : $\int_{a}^{r} v - \int_{a}^{0} v = \int_{0}^{r} v$ , including negative $r$ .

Proof

Given: The data and hypotheses in the Statement.

1.1F1F2F3F8F9F10F11given

Define $Φ (z, r) : = (F (z), t^{T} (z - z_{0}) - r)$ . Its derivative in $z$ at $(z_{0}, 0)$ is $[\begin{array}{c} D F (z_{0}) \\ t^{T} \end{array}]$ , which is invertible by [F1] because $D F (z_{0}) t = 0$ and $∥ t ∥_{2} = 1$ . Apply [F2] with parameter $r$ to obtain the unique local $C^{2}$ solution $z = γ (r)$ and the stated normalization. For each nearby zero $z$ of $F$ , setting $r = t^{T} (z - z_{0})$ makes $Φ (z, r) = 0$ , so the local uniqueness clause in [F2] places $z$ on this graph. Differentiating the equations at $r = 0$ using [F3] gives $D F (z_{0}) γ^{'} (0) = 0$ and $t^{T} γ^{'} (0) = 1$ ; rank-nullity [F11] gives $\dim \ker D F (z_{0}) = (n + 1) - n = 1$ , so the kernel and unit length of $t$ force $γ^{'} (0) = t$ .

2.1F3F4F5F7F12F13step 1.1algebra

The speed $v (r) : = ∥ γ^{'} (r) ∥_{2}$ is continuous and positive on a smaller interval because $v (0) = 1$ . Set $ℓ (r) : = \int_{0}^{r} v (u) d u$ . On a compact subinterval $[a, b]$ with $a < 0 < b$ , continuity makes $v$ integrable by [F4]. Set $H (r) = \int_{a}^{r} v$ ; [F12] gives $H' (r) = v (r)$ . By [F13], $ℓ (r) = H (r) - H (0)$ on both sides of zero, so $ℓ' (r) = v (r) > 0$ ; [F7] therefore gives a local inverse $r = r (s)$ . The curve $c (s) : = γ (r (s))$ is $C^{1}$ , satisfies $∥ c^{'} (s) ∥_{2} = 1$ , and has $c (0) = z_{0}$ , $c^{'} (0) = t$ .

3.1F3F4F5F6F8F9givenstep 2.1

Fix an admissible $s, h$ and put $e : = h c^{'} (s)$ . Differentiating the identity $F (c (r)) = 0$ at $r = s$ by the chain rule gives $D F (c (s)) c^{'} (s) = 0$ , hence $D F (c (s)) e = 0$ . For each coordinate $0 \leq i < n$ , apply [F3] and [F4] to $u \mapsto F_{i} (c (s) + u e)$ and subtract the zero linear term $D F_{i} (c (s)) e$ to obtain $F_{i} (c (s) + e) = \int_{0}^{1} (D F_{i} (c (s) + u e) - D F_{i} (c (s))) e d u .$ The Lipschitz bound, [F6], and $∥ e ∥_{2} = h$ bound the integrand in absolute value by $L u h^{2}$ ; [F5] then gives the coordinate bound $L h^{2} / 2$ .

4.1step 3.1algebra∎

Combining the $n$ coordinate bounds gives $∥ F (z_{p}) ∥_{2} \leq \sqrt{n} L h^{2} / 2$ . The last coordinate of $G_{s, h} (z_{p})$ is zero by the definition of $z_{p}$ , proving the augmented residual bound.

Depends on

Used by

Dependency tree · two levels

85 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

Eugene L. Allgower and Kurt Georg, Numerical Continuation Methods: An Introduction, Springer Series in Computational Mathematics 13 (1990) (standard reference, not scraped)
K. A. Cliffe, A. Spence, and S. J. Tavener, The numerical analysis of bifurcation problems with application to fluid mechanics, Acta Numerica 9 (2000), 39–131 (standard reference, not scraped)