Alphabeta Math
ExampleConstruction: AI-generatedVerification: AI-generatedPipeline-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 nonzero-residual stationary point gives only linear Gauss-Newton convergence

Example

Consider the scalar-parameter residual r(x)=(x,  1/2+x2/2)T. At x∗=0, the objective is stationary but the residual is nonzero. The exact Gauss-Newton update is x+=x x2−12(1+x2). For every nonzero ∣x∣<1 the iterates converge to 0, and ∣x+∣/∣x∣→1/2 while ∣x+∣/∣x∣2→+∞. Thus the local rate is linear and cannot be quadratic.

Facts & Assumptions

Given: The residual model and exact Gauss-Newton iteration in the Example.

[F2]

Gauss-Newton linearized least-squares step with QR/SVD rank safeguards: for a full-column-rank scalar Jacobian, the exact step minimizes the linearized residual norm.

[F3]

Gauss-Newton contracts linearly under a controlled residual-curvature bound: for m,n≥1, a C2 residual on an open set, a stationary point x∗ and a closed ball of radius R>0 inside that set, suppose the Jacobian has smallest singular value at least σ>0, satisfies ∥J(x)∥2≤M and is L-Lipschitz on the ball, and ∥S(x)∥2≤κ. If q=(κ+MLR)/σ2<1, exact Gauss-Newton steps supplied with exact reduced QR factors satisfy ∥x+p(x)−x∗∥2≤q∥x−x∗∥2.

Verification

1.1givenF1algebra

Here J(x)=(1,x)T, so J(x)TJ(x)=1+x2>0 for every x. Also J(x)Tr(x)=x+12x+12x3=32x+12x3, which vanishes at x∗=0 while r(0)=(0,1/2)T has norm 1/2.

2.1F2step 1.1algebra

For each x, the exact reduced QR supplied to the algorithm is Q(x)=11+x2[1x] and R(x)=1+x2, so Q(x)TQ(x)=1 and J(x)=Q(x)R(x). The scalar normal equation is (1+x2)p=−32x−12x3, so p=−x(3+x2)/(2(1+x2)); the supplied QR branch returns this unique least-squares step. Adding x gives x+=x(x2−1)/(2(1+x2)). For 0<∣x∣<1, ∣x+∣/∣x∣=(1−x2)/(2(1+x2))<1/2, so every such iterate stays in the interval and converges to zero.

2.2givenF3step 1.1algebra

The residual is polynomial, hence C2 on U=R, with n=1, m=2, and stationary point x∗=0 by step 1.1. On B=[−1/10,1/10], both ∥J(x)∥2 and ∥J(x)T∥2 are at most 11/10, both are 1-Lipschitz, and ∥J(x)v∥2≥∣v∣; also S(x)=1/2+x2/2≤101/200. Thus the local contraction theorem [F3] applies with R=1/10, M=11/10, L=1, σ=1, κ=101/200, and q=123/200<1.

3.1F3step 2.1step 2.2algebra∎

As x→0 through nonzero values, ∣x+∣/∣x∣→1/2, whereas ∣x+∣/∣x∣2=(1−x2)/(2∣x∣(1+x2))→+∞. No finite quadratic error constant can therefore hold near the stationary point. This exact example shows that the linear rate in [F3] cannot generally be strengthened when the residual is nonzero.

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

24 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