Alphabeta MathHow 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.
The Rosenbrock factorization and stage procedures terminate with finite work
Statement
For every finite dimension , finite stored matrix, unit roundoff with , and finite collection of stored right-hand sides and nonnegative residual tolerances in the input domains of Reusable Householder QR solve for a shifted matrix with residual status, Finite-precision one-stage Rosenbrock step with residual status, and Two-stage second-order Rosenbrock W-method with shared factorization, assume each called field-evaluation, domain-membership, exact-storage, and certificate-evaluation routine returns in finite work. Then the factorization operation, every requested solve operation, and each step procedure terminate after finitely many elementary operations with one of their stated success or failure statuses. Termination does not imply that the factorization is nonsingular, a residual is certified, or a step succeeds. No asymptotic runtime bound is claimed.
Facts & Assumptions
Given: Finite dimension and finite input data in the procedures' stated domains.
Scaled Householder reflector formation and application: its loops range over the finite active column and trailing block, and every elementary operation returns a finite value or a failure status.
Reusable Householder QR solve for a shifted matrix with residual status: factorization uses one reflector call per column; each solve uses a finite reflector list, triangular substitution, a finite residual check, and finitely many terminating certificate-evaluator calls.
Forward and backward substitution for triangular linear systems: back substitution is a descending finite recursion over the diagonal indices.
Operationwise real and complex floating point arithmetic with rounded square roots and fused multiply-add: each attempted arithmetic operation either returns a finite value or its declared failure status.
Finite-precision one-stage Rosenbrock step with residual status: a one-stage step performs one factorization and at most one solve.
Two-stage second-order Rosenbrock W-method with shared factorization: a two-stage step performs one factorization and at most two solves, with no iterative stage loop.
Proof
Given: The finite input data in the Statement.
In dimension , the QR factor routine calls the Householder procedure for at most the column indices . Each call has finite active vector and block dimensions, so [F1] makes each call finite or returns its first failure.
On a successful factorization, each solve applies at most stored reflectors, performs at most back-substitution stages by [F3], computes dot products and residual differences, and makes finitely many certificate-evaluator requests. Each loop has a finite index set, so [F2]–[F4] and the stated evaluator termination assumption imply that the solve also terminates with a stated result or failure.
By [F5], the one-stage procedure makes one factorization call and at most one solve call; by [F6], the two-stage procedure makes one factorization call and at most two solve calls. Each call terminates by steps 1.1–1.2, and the remaining work consists of finite vector operations and tests, including the stage-domain test performed by the assumed terminating domain-membership routine.
Thus the factorization call, every solve call in the finite request collection, and each step procedure execute finitely many operations and return the first encountered failure or a declared terminal status. This proves finite-work termination without a success or complexity assertion.
Depends on
- Reusable Householder QR solve for a shifted matrix with residual status
- Finite-precision one-stage Rosenbrock step with residual status
- Two-stage second-order Rosenbrock W-method with shared factorization
- Scaled Householder reflector formation and application
- Forward and backward substitution for triangular linear systems
- Operationwise real and complex floating point arithmetic with rounded square roots and fused multiply-add
Used by
Nothing in the library uses this result yet.
Dependency tree · two levels
16 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
- Daniel Kressner, Advanced Numerical Analysis, §3.5 Rosenbrock methods (standard reference, not scraped)
- David Bindel, CS 6210 Matrix Computations, Lecture 4 (standard reference, not scraped)