TheoremStatement: Literature-sourcedProof: AI-adaptedPipeline-generatedjudge pass (gpt-6-luna)

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 fixed-rank DPLR bilinear recurrent step has linear arithmetic cost

Statement

Let $N, r \geq 1$ , let $A = Λ - P Q^{*}$ with diagonal $Λ \in C^{N \times N}$ and $P, Q \in C^{N \times r}$ , where $^{*}$ denotes conjugate transpose, let $B, C \in C^{N}$ , and let $Δ > 0$ . If $G = I - Δ A / 2$ is invertible, then one bilinear recurrent update and its scalar output can be computed using $O (N (r + 1)^{2} + (r + 1)^{3})$ exact complex arithmetic operations and $O (N (r + 1) + (r + 1)^{2})$ working space. For fixed $r$ , this is $O (N)$ operations and $O (N)$ space. When the diagonal base $I - Δ Λ / 2$ is invertible, the required $r \times r$ Woodbury correction is invertible. When that diagonal base is singular but $G$ is invertible, the bordered correction in the recurrent algorithm is invertible and has size at most $2 r$ .

Statement references

Gu, Goel, and Ré, “Efficiently Modeling Long Sequences with Structured State Spaces,” Theorem 2 and Appendix C.2

Facts & Assumptions

Given: The dimensions, DPLR matrices, step size, and invertibility hypothesis from the Statement.

[F1]

DPLR structured state-space parameterization: $A = Λ - P Q^{*}$ and $G = I - Δ A / 2$ ; the recurrent right-hand side is $(I + Δ A / 2) x + Δ B u$ and the output is $C^{*} x^{'}$ after solving for $x^{'}$ .

[F2]

Woodbury inverse for a diagonal-plus-low-rank update: if $D$ is invertible, then $D + U V^{*}$ is invertible exactly when $I + V^{*} D^{- 1} U$ is invertible, and its inverse is $D^{- 1} - D^{- 1} U (I + V^{*} D^{- 1} U)^{- 1} V^{*} D^{- 1}$ .

[F3]

S4 state-space recurrence and convolution procedure: for a singular diagonal base, the algorithm partitions its zero and nonzero coordinates and solves the displayed bordered system of dimension $r + ∣ Z ∣$ , then sets $x_{J} = D_{J}^{- 1} (b_{J} - α P_{J} z)$ .

Proof

1.1F1givenalgebra

Put $α = Δ / 2$ and $D = I - α Λ$ . For a current state $x$ and input $u$ , form $b = (I + α A) x + Δ B u = x + α Λ x - α P (Q^{*} x) + Δ B u$ . Diagonal scaling costs $O (N)$ operations, the two low-rank products cost $O (N r)$ , and the remaining vector additions cost $O (N)$ . The solve is $G x^{'} = b$ with $G = D + α P Q^{*}$ .

2.1F2step 1.1algebra

If every diagonal entry of $D$ is nonzero, apply [F2] with $U = α P$ and $V = Q$ . Since $G$ is invertible, the correction $W = I_{r} + α Q^{*} D^{- 1} P$ is invertible, and $x^{'} = D^{- 1} b - D^{- 1} (α P) W^{- 1} Q^{*} D^{- 1} b$ . Forming $D^{- 1} P$ and $W$ costs $O (N r^{2})$ operations and $O (N r + r^{2})$ space; factoring $W$ costs $O (r^{3})$ . Applying the inverse to one right-hand side costs $O (N r + r^{2})$ operations. Thus this branch meets the stated bounds.

2.2givenF1step 1.1algebra

Otherwise let $Z = {j : D_{j j} = 0}$ , $J = {0, \dots, N - 1} ∖ Z$ , and $s = ∣ Z ∣$ . The rows of $G$ indexed by $Z$ are those of $α P_{Z} Q^{*}$ , whose rank is at most $r$ . If $s > r$ , these $s$ rows are linearly dependent, so $G$ is singular, contrary to the hypothesis. Hence $s \leq r$ .

3.1givenF3step 2.2algebra

Suppose $s \leq r$ and consider a homogeneous solution $(z, x_{Z})$ of the bordered system in [F3]. Set $x_{J} = - α D_{J}^{- 1} P_{J} z$ . The first bordered row gives $z = Q_{J}^{*} x_{J} + Q_{Z}^{*} x_{Z} = Q^{*} x$ , while its lower row gives $α P_{Z} z = 0$ . Therefore the $J$ rows of $G x$ equal $D_{J} x_{J} + α P_{J} Q^{*} x = 0$ , and the $Z$ rows equal $α P_{Z} Q^{*} x = α P_{Z} z = 0$ . Invertibility of $G$ implies $x = 0$ , hence $z = Q^{*} x = 0$ and $x_{Z} = 0$ . The square bordered matrix has trivial kernel and is therefore invertible.

4.1F1F3step 2.2step 3.1algebra∎

For any right-hand side, solve the bordered system, define $x_{J} = D_{J}^{- 1} (b_{J} - α P_{J} z)$ , and keep the solved $x_{Z}$ . Its first row states $z = Q^{*} x$ ; the upper coordinate equations then give $(G x)_{J} = b_{J}$ , and the lower row gives $(G x)_{Z} = α P_{Z} z = b_{Z}$ . Thus $x = x^{'}$ is the unique solution to $G x^{'} = b$ . The bordered dimension is $r + s \leq 2 r$ ; forming it and its right-hand side costs $O (N r^{2})$ operations and $O (N r + r^{2})$ space, and factoring/solving it costs $O (r^{3})$ . Computing $C^{*} x^{'}$ adds $O (N)$ . Both branches satisfy the claimed fixed-rank linear bounds.

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

6 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

Gu, Goel, and Ré, Efficiently Modeling Long Sequences with Structured State Spaces, Theorem 2 and Appendix C.2 (standard reference, not scraped)