Alphabeta Math
AlgorithmAlgorithm: AI-adaptedProof: Not applicablePipeline-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.

Finite-budget computed Francis Schur reduction with explicit statuses

Definition

Input a real or complex square matrix A∈Fn×n with n≥1, a finite nonnegative deflation tolerance τ, a nonnegative integer sweep budget N, a positive integer stagnation period h, a finite family of exceptional-shift tables Ta,b indexed by original contiguous index intervals [a,b]⊆[1,n] with a<b, optional exact rational/dyadic encodings of its stored real values, optionally a terminating exact evaluator of Exact sign predicate for a real 2x2 characteristic discriminant, and optionally a terminating outward evaluator for nonnegative expressions and Frobenius norms. The outward evaluator's upadd, upmul, and upsqrt calls return finite nonnegative represented upper bounds for the exact sum, product, and square root, while upnormF(X) returns a finite represented upper bound for ∥X∥F; any call may instead return unavailable. In the declared scalar-cost model, each upadd, upmul, and upsqrt call has unit cost and upnormF(X) makes one pass over the entries of X with a fixed number of such calls per real component. The evaluator acts only on certificate bookkeeping. A formation breakdown is propagated with the operation index and partial factors. Every scalar operation in the main procedure is evaluated in the operationwise model of Operationwise real and complex floating point arithmetic with rounded square roots and fused multiply-add. Any invalid, overflow, or underflow operation in the main procedure returns range-failure with the operation index and partial factors.

Each complex table entry is a finite represented scalar μ∈C; each real table entry is a pair of finite represented real coefficients (s,t) for z2−sz+t. Each table is an ordered finite list, possibly empty; an omitted interval has the empty list. These descriptors use the field of A. Tables support direct indexed lookup by interval and cursor; unused entries are not scanned. All interval-state updates use a single ordered pass over the current partition. Counters and table indices are exact integers. Maintain state (ca,b,qa,b), initially (0,0), for each current maximal diagonal interval separated by exact zero subdiagonals: c counts completed ordinary block sweeps since the last reset and q counts exceptional descriptors already consumed. After a split, discard the parent state and initialize every new child interval to (0,0), using its own table. An unchanged interval retains its state. Completed one-by-one blocks, and real two-by-two blocks with verified negative discriminant, require no shift.

Start with H=A and the empty factor product Q=I. Set the completed global sweep count to k=0 after initialization. Before attempting any sweep, and after every completed sweep, perform steps 2 and 5, in that order. If neither returns, snapshot the remaining active intervals in increasing left endpoint, and perform steps 3 and 4 once for each snapshotted interval in that order. No deflation scan or repartition occurs during this pass. After all its intervals finish, increment k by one and repeat the scan and stopping test. All intervals in a pass use their current diagonal block when reached; previously applied similarities on disjoint blocks do not reschedule a block.

Before every real or complex formation in steps 1 and 4, test the target vector componentwise for exact zero, including an external initial polynomial vector. If it is zero, mark the stage identity, copy all affected matrix entries unchanged, skip formation and both left and right updates, append the embedded identity Pj=I to the product representation, and record Ej=0 and arithmetic coefficient αj=αˉj=0. Do not evaluate P(v) or a stored-vector norm in this branch. For a matrix target its column is already zero, so its target zero writes change nothing; for an external vector no matrix column is overwritten. Continue with the invariant checks, sweep counters and stopping tests specified below. Record and process every deflation write separately exactly as specified below; this branch does not discard a deflation perturbation. These identity instructions take precedence over the formation/update instructions in steps 1 and 4.

For each nonidentity stored reflector with active indices S=(s1,…,sm), nonzero vector v∈Fm, and real computed coefficient τ^, the real or complex formation routine first performs the stated finite left application. Then perform the right application in this fixed order: for each matrix row i=1,…,n, compute di=fl⁡(∑a=1mHi,saLva) by left-to-right rounded products and additions; for a=1,…,m, compute ca=fl⁡(τ^va‾), gia=fl⁡(dica), and Hi,saR=fl⁡(Hi,saL−gia). Each complex product uses the six real operations of the arithmetic model. The exact factor appended to Q is P(v)=I−2vv∗/(v∗v); the computed right update uses τ^ as displayed and is not asserted equal to multiplication by P(v). For a matrix-target column, the formation routine's explicit zero writes are retained. In the initial polynomial-vector step there is no matrix-target column: use the entire active row panel for the left update and then apply the right update to the active columns. Record deflation writes separately, including a pure deflation with no following reflector as an identity-transform stage; a local error certificate must account for all other rounding and target-column writes.

  1. Reduce A to upper Hessenberg form with Householder similarities. For k=1,…,max⁡(n−2,0) in increasing order, use active indices S={k+1,…,n}, target x=HS,k, and trailing left panel B=HS,{k+1,…,n} with columns in increasing order. In the real branch use Scaled Householder reflector formation and application for the finite left application and overwrite; in the complex branch use Scaled complex Householder reflector step with explicit range status. Complete each similarity by the right application above on columns S. After the entire initialization loop, including when it is empty, check the resulting matrix's exact upper-Hessenberg zero pattern; on failure return bulge-chase-invariant-failure with the partial factors. Store the exact unitary reflector factors as a product representation Q0.
  2. In increasing global row index i=2,…,n, test each nonzero first-subdiagonal entry by ∣hi,i−1∣≤τ(∣hi−1,i−1∣+∣hi,i∣). For a complex entry z=a+ib, evaluate ∣z∣ by s=max⁡(∣a∣,∣b∣) and s(a/s)2+(b/s)2 when z≠0, with divisions, squares, sum, square root and final scaling rounded in the stated order; use ∣0∣=0. Return range-failure if this evaluation fails. Compute the diagonal-magnitude sum first, then multiply by τ in the operationwise model; compare the resulting finite values exactly. When the test holds, set that entry to zero and record its original value as a deflation perturbation. After the scan, form the maximal intervals separated by exact zero subdiagonals and update interval states by the rule above. The equality case deflates. Do not use the Hermitian-tridiagonal Wilkinson shift rule for a general Hessenberg matrix.
  3. For the current snapshotted interval [a,b], let L=Ha:b,a:b and ℓ=b−a+1. If ca,b=h, read entry qa,b+1 of Ta,b. If absent, return stagnation-exhausted before this block's chase. Otherwise consume it by incrementing qa,b once and use its complex scalar shift or real coefficient pair. After this exceptional block sweep completes, set ca,b=0. If ca,b<h, use the ordinary shift: in the complex branch μ=Lℓ,ℓ; in the real branch, for the trailing block (a′b′c′d′), compute s=fl⁡(a′+d′) then t=fl⁡(fl⁡(a′d′)−fl⁡(b′c′)) in that order. Return range-failure on a failed operation. After this ordinary block sweep completes, increment ca,b by one. A split at the next scan resets each new child as specified above; unchanged intervals retain these updated states.
  4. On the diagonal block L selected in step 3, apply the index pattern of Exact finite Francis single- or double-shift Hessenberg QR step, with its dimension ℓ and local indices 1,…,ℓ. In the vector formulas in this step, H means that current diagonal block. Translate every local index i to global index a+i−1; embed each factor in the full n×n identity. The left panel extends through global column n, and the right application runs through all global rows, so upper off-diagonal blocks are updated as well. For the initial single-shift vector compute x1=fl⁡(h11−μ) and xi=hi1 for i>1. For the initial real double-shift vector, compute u=He1, then w=Hu by left-to-right rounded matrix-vector products, then x=fl⁡(fl⁡(w−su)+te1) componentwise. Compute only the first r+1 components from the Hessenberg support pattern; on range failure return the operation index and partial factors. For a chase at local column j, use the globally translated active indices S=Ij, the corresponding global target column a+j−1, and the trailing left panel through global columns a+j,…,n in increasing order. Call the real or complex formation routine, write the target tail zeros exactly, complete the two-sided update by the right-kernel order above on columns S, and append the exact reflector representation to Q. In the initial polynomial-vector step there is no matrix-target column; use the full active row panel for the left update and then apply the right update to its active columns. After the block chase, perform the following exact upper-Hessenberg zero-pattern check, including when all its stages were identities. For i=1,…,n in increasing order, if a≤i≤b, test hij=0 for j=1,…,i−2 in increasing order; otherwise test hij=0 for j=a,…,min⁡(b,i−2) in increasing order. Skip every empty index range. On the first nonzero tested entry return bulge-chase-invariant-failure with the partial matrix and factors. These are precisely the below-first-subdiagonal positions whose row or column belongs to [a,b]. Enumerate only these ranges; do not scan all n2 positions and filter them. The unchanged complementary positions retain the zero values established by initialization or the previous accepted check. Deflation writes affect only the first subdiagonal and do not change those positions. Use Left and right scaled Householder errors give a concrete similarity bound to store the proved two-sided coefficient αmj=amj+bmj+amjbmj, with a the target-overwrite coefficient or separate-block coefficient as actually used and b the right separate-block coefficient. This gives ∥Ej∥F≤αmj∥H^j−1∥F when its mju<1 and range hypotheses hold. Apply the same certificate to every Hessenberg-initialization similarity. If any step lacks that certificate, retain the residual diagnostic and set the backward-error-certificate status to inconclusive.
  5. Inspect maximal intervals in increasing left endpoint. A size-one interval is completed. A complex interval of size at least two, or a real interval of size at least three, is active. For each real size-two interval determine its exact discriminant sign as below: a negative sign completes that interval, while zero or a positive sign leaves it active. Stop with Schur-computed when all intervals are completed. Use the supplied evaluator, or the finite integer recipe in Rational or dyadic stored real blocks have a finite exact discriminant-sign evaluator when exact rational/dyadic encodings are available, for each real block's discSign⁡ as defined in Exact sign predicate for a real 2x2 characteristic discriminant. If no exact sign is available, return schur-type-undecided and do not claim Schur-computed. If any active interval remains and k=N, return budget-exhausted; in particular, with N=0 return Schur-computed only when the initialized matrix already has the target block structure. Return the partial matrix and factors on every failure or nonconvergence status.

For certificate bookkeeping, start before Hessenberg initialization with ρ0=upnormF⁡(A) and C0=0. If the evaluator is absent or this call is unavailable, mark the backward-error certificate inconclusive. Process each local similarity update and each deflation-only write as a separate finite stage j. For a local similarity, take the actual coefficient αj=amj+bmj+amjbmj from Left and right scaled Householder errors give a concrete similarity bound and compute αˉj=upadd⁡(upadd⁡(amj,bmj),upmul⁡(amj,bmj))≥αj; for an identity update put αˉj=0. A recorded deflation entry stores its old value, while its additive matrix Dj has entry equal to zero minus that old value at the written position. For a deflation-only stage use Pj=I, Ej=0, αˉj=0, and obtain βˉj≥∥Dj∥F by calling upnormF on the one-entry list containing the signed recorded value, whose Frobenius norm equals ∥Dj∥F; do not form or scan a dense matrix Dj; for a similarity stage set βˉj=0. With the outward evaluator compute

gj=upadd⁡(upmul⁡(αˉj,ρj−1),βˉj),ρj=upadd⁡(ρj−1,gj),Cj=upadd⁡(Cj−1,gj).

If any local coefficient certificate or evaluator call is unavailable, keep the residual diagnostic and mark the backward-error-certificate status inconclusive; this ancillary failure does not change the main algorithm status. Otherwise return CJ as the accumulated backward-error upper bound and mark that status certified. The number of recurrence calls is finite: one initialization norm, a fixed number of scalar upper-bound calls per similarity stage, and one norm call per deflation-only stage.

Let T^ be the final returned matrix. The output includes the product representation Q, residual matrix R=Q∗AQ−T^ and its Frobenius norm as diagnostics, the exact orthogonality bound 0 for that reflector product, the recorded deflation entries, and either the accumulated backward-error bound when all local certificates exist or certificate status inconclusive. Bound expressions and any claimed upper bounds are evaluated exactly or with rigorous outward allowances; uncorrected rounded residual norms are diagnostics only. A rounded dense matrix formed from Q has its own orthogonality residual and is not asserted exactly unitary. The residual diagnostic does not itself give a forward eigenvalue bound. The procedure asserts no unconditional convergence of any shift schedule.

Depends on

Used by

Dependency tree · two levels

28 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