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.

Rank-deficient data do not identify both parameters, while LM has a unique damped step

Example

Let r(a,b)=(a+b−1,  2(a+b−1))T. The data depend only on a+b, so they do not identify a and b separately. At (0,0) the Gauss-Newton Jacobian is rank deficient and its linearized least-squares problem has many minimizers. With D=I, damping λ=1 gives a unique trial step. For trust radius Δ=1, ratio thresholds η1=1/4,η2=3/4, lower damping λmin⁡=1/2, update factor γ=2, and one allowed trial, that step is accepted with ratio 1.

Facts & Assumptions

Given: The residual model, starting point (0,0), and LM parameters in the Example.

[F1]

Gauss-Newton linearized least-squares step with QR/SVD rank safeguards: with a supplied exact reduced QR factorization, a zero triangular diagonal returns rank-deficient rather than an asserted unique Gauss-Newton step.

[F2]

Finite-budget Levenberg-Marquardt with a trust-ratio safeguard: with a supplied exact reduced QR factorization of the augmented matrix, a feasible LM trial with positive predicted reduction and ρ≥η1 is accepted; a high-ratio boundary step is the only accepted branch that decreases damping.

[F3]

A damped least-squares step solves a scaled trust-region model: with nonsingular D and λ>0, the damped normal system has a unique step and its predicted reduction is positive when JTr≠0.

[F4]

The Euclidean inner product ⟨x,y⟩=∑k<nxkyk on Rn: ∥(u,v)∥2=u2+v2 in two dimensions.

Verification

1.1givenF1algebra

At (0,0), r=(−1,−2)T, J=[1122], and JTJ=[5555]. The two columns of J coincide, so its rank is 1<2. Supply the exact reduced QR Q=15[1−221] and R=[5500], which satisfies QTQ=I and QR=J. The exact QR branch therefore returns rank-deficient. The objective is 52(a+b−1)2, whose minimizers are the full line a+b=1; hence the parameters are not separately identifiable. The linearized problem at (0,0) is minimized whenever p1+p2=1, so it has no unique Gauss-Newton step.

2.1givenF2F3F4algebra∎

For D=I and λ=1, the augmented matrix and residual are A1=[J;I] and s1=[r;0]. Supply the exact reduced QR Q=[1/61/662/62/661/6−5/6606/66] and R=[65/6066/6], which satisfies QTQ=I and A1=QR. The damped system is [6556]p=(5,5)T, whose unique solution is p=(5/11,5/11)T. The linear model residual is r+Jp=(−1/11,−2/11)T, so m0(0)=5/2, m0(p)=5/242, and pred⁡=300/121>0. Since the residual is affine, the true residual at (0,0)+p equals that linear model residual; therefore ared⁡=pred⁡ and ρ=1. Also ∥p∥2=52/11<1=Δ, so the trial is feasible and is not a boundary step. By [F2]–[F3] it is accepted and λ stays 1.

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

31 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