TheoremStatement: Literature-sourcedProof: AI-adaptedPipeline-generated

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 transverse pseudo-arclength section has a locally quadratic Newton corrector

Statement

Let $n \geq 1$ , let $U \subseteq R^{n + 1}$ be open, and let $F : U \to R^{n}$ be $C^{2}$ . Suppose $z_{*} \in U$ satisfies $F (z_{*}) = 0$ and $A : = D F (z_{*})$ has rank $n$ . Let $t \in \ker A$ be a unit vector, let $τ \in R^{n + 1}$ be a unit vector with $∣ τ^{T} t ∣ \geq c$ for some $0 < c \leq 1$ , and let $z_{p}$ satisfy $τ^{T} (z_{*} - z_{p}) = 0$ . Define $G (z) : = (F (z), τ^{T} (z - z_{p})) .$ Let $K_{A} \geq 0$ satisfy $∥ (A ∣_{t^{⊥}})^{- 1} u ∥_{2} \leq K_{A} ∥ u ∥_{2} (u \in R^{n}),$ and set $β_{*} : = \sqrt{K_{A}^{2} (1 + c^{- 1})^{2} + c^{- 2}} .$ The derivative $D G (z_{*})$ is invertible and $∥ D G (z_{*})^{- 1} ∥_{o p} \leq β_{*}$ . There is a local regular unit-speed solution-curve chart through $z_{*}$ , and after shrinking it, the hyperplane $τ^{T} (z - z_{p}) = 0$ has exactly one intersection with that chart.

Suppose also that for some $R > 0$ and $L \geq 0$ the closed ball ${\overline{B}}_{2} (z_{*}, R)$ lies in $U$ and $∥ D F (u) - D F (v) ∥_{o p} \leq L ∥ u - v ∥_{2} (u, v \in {\overline{B}}_{2} (z_{*}, R)) .$ Then there are $ρ \in (0, R]$ and $K > 0$ such that each exact-Jacobian Newton update for $G$ started in ${\overline{B}}_{2} (z_{*}, ρ)$ is defined, remains in that ball, and satisfies $∥ z_{k + 1} - z_{*} ∥_{2} \leq C ∥ z_{k} - z_{*} ∥_{2}^{2}, C : = K L / 2,$ where $C ρ \leq 1 / 2$ (if $L = 0$ , any sufficiently small $ρ$ works). Continuing the exact recurrence indefinitely gives convergence to $z_{*}$ ; a finite update budget may stop first, and its root status means only that the residual tolerance was met. Separately, whenever the hypotheses of A bounded residual and derivative error give a local root certificate hold for $G$ on a proposed closed ball, that theorem certifies exactly one zero there and its stated residual-to-root error bound. These conclusions are local and imply no global branch-completeness claim.

Facts & Assumptions

Given: $n, U, F, z_{*}, A, t, τ, z_{p}, K_{A}, c, R, L$ and the hypotheses in the Statement.

[F1]

A regular solution curve has a unique local arclength chart and a quadratic predictor defect: at a root where $D F$ has rank $n$ , a unit kernel vector determines a unique locally normalized solution curve, which has a $C^{1}$ unit-speed reparameterization $c (s)$ with $c (0) = z_{*}$ and $c^{'} (0) = t$ ; every sufficiently nearby solution lies on this curve.

[F2]

A transverse predictor hyperplane selects one nearby point of a regular branch: if $τ^{T} c^{'} (s) \geq κ > 0$ on a short two-sided chart interval and the signed predictor offset lies between $0$ and $κ$ times its forward length, the hyperplane intersects that entire local branch segment exactly once.

[F3]

Invertibility and a norm bound for the pseudo-arclength bordered matrix: for rank- $n$ $A$ with unit kernel $t$ , the matrix $[\begin{array}{c} A \\ τ^{T} \end{array}]$ is invertible when $∣ τ^{T} t ∣ \geq c > 0$ and its inverse norm is at most $\sqrt{K_{A}^{2} (1 + c^{- 1})^{2} + c^{- 2}}$ .

[F4]

Updated-Jacobian Newton has local quadratic convergence at a simple root: if a $C^{2}$ square residual has an exact zero with invertible Jacobian and a Lipschitz Jacobian on a closed ball, there is a smaller invariant ball on which every exact Newton update is defined and satisfies the quadratic error recurrence; an infinite recurrence converges, while finite-budget root status records only a residual tolerance.

[F5]

Finite-budget Newton for a square vector residual specifies the residual, trial-domain, singularity and budget branches. Its correction-call bound is proved in Finite-budget Newton preserves its domain and returns a status in bounded outer work; budget exhaustion may precede tolerance attainment.

[F6]

A bounded residual and derivative error give a local root certificate: under its certified residual/Jacobian error, inverse, Lipschitz and strict contraction hypotheses, a square residual has exactly one zero in the proposed ball and the distance from its center is at most $β ρ_{g} / (1 - q)$ , where $ρ_{g}$ is its certified residual upper bound.

[F7]

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 composition of derivatives.

[F8]

$C^{k}$ Euclidean maps and diffeomorphisms: $C^{2}$ means each 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 of a map with finite-dimensional domain is the dimension of its image.

Proof

Given: The data and hypotheses in the Statement.

1.1F1F2F8F9F10givenchoose

Apply [F1] to obtain a $C^{1}$ unit-speed branch chart $c (s)$ with $c (0) = z_{*}$ and $c^{'} (0) = t$ . Set $\tilde{τ} : = τ$ if $τ^{T} t > 0$ and $\tilde{τ} : = - τ$ if $τ^{T} t < 0$ ; it is a unit vector, its hyperplane is unchanged, and ${\tilde{τ}}^{T} c^{'} (0) = ∣ τ^{T} t ∣ \geq c$ . By continuity of $c^{'}$ , shrink the chart to $[- r, r]$ so that ${\tilde{τ}}^{T} c^{'} (s) \geq c / 2$ . For $g (s) : = {\tilde{τ}}^{T} (c (s) - z_{p})$ the offset in [F2] is zero because $z_{*}$ lies on the hyperplane. The $d = 0$ case of [F2] gives exactly one intersection on this chart segment, at $s = 0$ .

1.2F3F7F9F10givenalgebra

By [F7], the derivative of $G$ at $z_{*}$ is the bordered matrix $D G (z_{*}) = [\begin{array}{c} A \\ τ^{T} \end{array}] .$ The rank, kernel, angle and complement-inverse hypotheses let [F3] give its invertibility and the stated bound $β_{*}$ .

2.1F4F8F9F10givenstep 1.2algebra

The last component of $G$ is affine, so for $u, v$ in the ball, $∥ D G (u) - D G (v) ∥_{o p} = {∥ [\begin{array}{c} D F (u) - D F (v) \\ 0 \end{array}] ∥}_{o p} \leq L ∥ u - v ∥_{2} .$ Also $G (z_{*}) = 0$ by $F (z_{*}) = 0$ and the section equation. Apply [F4] to the square map $G$ on this ball. It supplies a smaller radius $ρ$ , a uniform inverse bound $K$ , and the quadratic estimate with $C = K L / 2$ ; its induction also ensures every attempted update stays in the invariant ball.

3.1F5F6step 2.1given∎

The finite procedure in [F5] uses exactly these updates and its own residual, domain, singularity and budget checks. Hence any update it attempts from the invariant ball has the bound of step 2.1; if it stops for the iteration budget before reaching tolerance, no exact-zero conclusion follows. For a separately supplied approximate residual/Jacobian tuple satisfying [F6], that certificate gives the stated unique local zero and error bound for this same augmented map $G$ .

Depends on

Used by

Dependency tree · two levels

49 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)