ExampleConstruction: AI-adaptedVerification: AI-adaptedPipeline-generatedprecheck passjudge 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.

An AR(1) covariance forecast and general-RHS Toeplitz solve

Statement

Assume a real, mean-zero, weakly stationary process $X_{t}$ satisfies the causal AR(1) model $X_{t} = \frac{1}{2} X_{t - 1} + ε_{t}$ in $L^{2}$ , where $ε_{t}$ is centered with variance $3 / 4$ , is uncorrelated with $X_{s}$ for every $s < t$ , and the process is weakly stationary. Here “AR(1)” means precisely this first-order autoregression; the stated uncorrelatedness is the innovation orthogonality used below. Then its autocovariance function (ACVF) is $γ (h) = 2^{- ∣ h ∣}$ . The order-two Durbin–Levinson output is $ϕ_{2} = (1 / 2, 0)^{T}$ and $ν_{2} = 3 / 4$ . Separately, for $T = (\begin{array}{cc} 1 & 1 / 2 \\ 1 / 2 & 1 \end{array})$ and $b = (1, 1)^{T}$ , the general-RHS Hermitian Toeplitz solver returns $T^{- 1} b = (2 / 3, 2 / 3)^{T}$ by the Gohberg–Semencul formula.

Facts & Assumptions

Given: The process and innovation hypotheses in the Statement, the Durbin–Levinson covariance-input procedure, and the exact Hermitian Toeplitz solver.

[F1]

Weak stationarity supplies a constant mean and an ACVF $γ (h) = Cov (X_{t + h}, X_{t})$ depending only on lag. Strict and weak stationarity for integer-indexed time series Autocovariance and sample autocovariance

[F2]

Covariance is symmetric and bilinear for finite linear combinations of square-integrable variables. Moments, variance, and covariance on a probability space Variance and covariance identities for random variables

[F3]

The real Durbin–Levinson recursion computes $ϕ_{k}, ν_{k}$ from $γ (0), \dots, γ (k)$ when the leading covariance blocks are positive definite. Durbin–Levinson forecast recursion

[F4]

Under those leading-block hypotheses, $ϕ_{k}$ solves the prediction equations and $ν_{k} = γ (0) - r_{k}^{T} ϕ_{k}$ . Durbin–Levinson solves the successive prediction equations

[F5]

The Hermitian Toeplitz solver constructs the endpoint inverse columns and applies the exact Gohberg–Semencul formula. General-RHS Hermitian Toeplitz solve by reflection recursion and Gohberg–Semencul The Hermitian positive-definite Gohberg–Semencul formula is exact and quadratic

Proof

1.1givenF1F2algebra

Centering and weak stationarity give $E [X_{t}] = 0$ and $γ (0) = Var (X_{t})$ for every $t$ . From the autoregression and innovation orthogonality, $γ (0) = Var (\frac{1}{2} X_{t - 1} + ε_{t}) = \frac{1}{4} γ (0) + \frac{3}{4},$ so $γ (0) = 1$ .

1.2givenF5algebra

For the separate general-RHS solve, set $T = (\begin{array}{cc} 1 & 1 / 2 \\ 1 / 2 & 1 \end{array})$ as in the Statement. For each nonzero $z \in C^{2}$ , $z^{*} T z = ∣ z_{1} + z_{2} / 2 ∣^{2} + 3 ∣ z_{2} ∣^{2} / 4 > 0$ , so $T$ is Hermitian positive definite. Its first lag data are $t_{0} = 1, t_{1} = 1 / 2$ , hence $α_{1} = t_{1} / t_{0} = 1 / 2$ , $ϕ_{1} = α_{1} = 1 / 2$ , and $ν_{1} = t_{0} (1 - ∣ α_{1} ∣^{2}) = 3 / 4$ . The endpoint columns from [F5] are $v = (- 2 / 3, 4 / 3)^{T}, u = J_{2} v = (4 / 3, - 2 / 3)^{T}, u_{0} = 4 / 3 > 0.$ The lower triangular Toeplitz products are $L (u) L (u)^{*} = (\begin{array}{cc} 16 / 9 & - 8 / 9 \\ - 8 / 9 & 20 / 9 \end{array}), L (Z_{2} v) L (Z_{2} v)^{*} = (\begin{array}{cc} 0 & 0 \\ 0 & 4 / 9 \end{array}) .$ Therefore the formula in [F5] gives $T^{- 1} = (\begin{array}{cc} 4 / 3 & - 2 / 3 \\ - 2 / 3 & 4 / 3 \end{array}), T^{- 1} b = (2 / 3, 2 / 3)^{T} .$ Direct multiplication also verifies $T (2 / 3, 2 / 3)^{T} = (1, 1)^{T}$ .

2.1givenF1F2step 1.1induction

For each integer $h \geq 1$ , covariance bilinearity and $Cov (ε_{t}, X_{t - h}) = 0$ give $γ (h) = Cov (X_{t}, X_{t - h}) = \frac{1}{2} γ (h - 1) .$ Induction yields $γ (h) = 2^{- h}$ for $h \geq 0$ ; covariance symmetry gives $γ (- h) = γ (h)$ .

3.1givenF3F4step 1.1step 1.2step 2.1algebra

The order-one recursion gives $κ_{1} = γ (1) / γ (0) = 1 / 2$ , $ϕ_{1} = (1 / 2)$ and $ν_{1} = 1 (1 - 1 / 4) = 3 / 4$ . At order two, $κ_{2} = \frac{γ (2) - ϕ_{1, 1} γ (1)}{ν_{1}} = \frac{1 / 4 - (1 / 2) (1 / 2)}{3 / 4} = 0,$ so $ϕ_{2} = (ϕ_{1, 1} - κ_{2} ϕ_{1, 1}, κ_{2})^{T} = (1 / 2, 0)^{T}$ and $ν_{2} = ν_{1} (1 - κ_{2}^{2}) = 3 / 4$ . By steps 1.1 and 2.1, $Γ_{1} = [1]$ and $Γ_{2} = T$ . Step 1.2 proves $T$ Hermitian positive definite, so the real leading covariance blocks are positive definite; [F3] applies and [F4] identifies this vector as the unique prediction solution.

4.1step 3.1step 1.2algebra∎

The first calculation reuses the published real covariance prediction recursion, while the second is a distinct arbitrary-right-hand-side Hermitian Toeplitz solve; the computed vector satisfies its stated system.

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

22 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

Ralf Hiptmair, Numerical Methods for Computational Science and Engineering, Lecture Document, §4.5.3 (standard reference, not scraped)
MIT OpenCourseWare 6.341, Discrete-Time Signal Processing, Lecture 13: The Levinson-Durbin Recursion (standard reference, not scraped)