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.
DPLR structured state-space parameterization
Definition
An -state single-input, single-output complex linear state-space model has , state equation , and output ; its direct term is set to zero in the S4 convolution convention. Here denotes conjugate transpose; a square complex matrix is normal when ; and a square matrix is unitary when . A matrix is in diagonal-plus-low-rank (DPLR) form of rank if
where is diagonal and . It is in normal-plus-low-rank (NPLR) form of rank if
where is unitary, is diagonal, and . The unitary state change converts this NPLR representation to DPLR form and changes to , respectively.
For a step size such that is invertible, the bilinear recurrent matrices are With initial state , the discrete recurrence is , . Its length- impulse kernel is the vector . For a nonzero direct term , the output has the additional separate skip term .
For a filter evaluation of transform length , the output vector for the length- truncated generating function is . A filter procedure may receive as given data; an operation count for evaluating the filter from this transformed vector does not include the separate work of forming it from .
Depends on
Used by
- S4 state-space recurrence and convolution procedure Algorithm
- A scalar state-space layer has matching recurrent and convolutional outputs Example
- DPLR SSM filter values reduce to Cauchy products Lemma
- A fixed-rank DPLR bilinear recurrent step has linear arithmetic cost Theorem
- HiPPO LegS, LegT, and LagT matrices have normal-plus-low-rank form after specified similarities Theorem
- S4 convolution-filter arithmetic and numerical cost Theorem
Dependency tree · two levels
7 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, §§2.1, 2.3, 3.2, Appendix C.3 (standard reference, not scraped)