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

Gaussian conditioning with singular state covariance

Statement

Assume AC. Let $Z = (Z_{1}, Z_{2}) \sim N_{2} (0, I_{2})$ , where $I_{2}$ is the $2 \times 2$ identity matrix, and set $X = (Z_{1}, Z_{1})$ and $Y = Z_{1} + Z_{2}$ . The state covariance is singular, $Var (Y) = 2 > 0$ , and the conditional law at every $y \in R$ is $X ∣ Y = y \sim N_{2} ((y / 2, y / 2), (\begin{array}{cc} 1 / 2 & 1 / 2 \\ 1 / 2 & 1 / 2 \end{array})) .$

Facts & Assumptions

Given: AC, $Z \sim N_{2} (0, I_{2})$ , and the definitions of $X$ and $Y$ in the Statement.

[A1]

AC is assumed by the multivariate-normal construction and conditional-law theorem. The Axiom of Choice.

[F1]

Under AC, $N_{d} (m, Σ)$ exists for every positive-semidefinite covariance, has the stated mean and covariance, and is characterized by its Gaussian linear projections. Multivariate normal law, including singular covariance.

[F2]

If a jointly Gaussian pair has block covariance $(\begin{array}{cc} A & C \\ C^{T} & B \end{array})$ with $B$ positive definite, its conditional kernel has mean $a + C B^{- 1} (y - b)$ and covariance $A - C B^{- 1} C^{T}$ , which may be singular. Conditional law of a jointly Gaussian block with positive-definite observed covariance.

Verification

Given: AC and the Gaussian vector and affine definitions in the Statement, with facts [A1], [F1], [F2].

1.1A1F1givenalgebra

For any $u_{1}, u_{2}, v \in R$ , $u_{1} X_{1} + u_{2} X_{2} + v Y = (u_{1} + u_{2} + v) Z_{1} + v Z_{2}$ is Gaussian by [F1]. Its mean is zero. Computing covariances from $Cov (Z) = I_{2}$ gives $A = (\begin{array}{cc} 1 & 1 \\ 1 & 1 \end{array})$ , $C = (\begin{array}{c} 1 \\ 1 \end{array})$ , and $B = (2)$ . Since $\det A = 0$ , the state covariance is singular.

2.1step 1.1algebra

The observed block $B = (2)$ is positive definite. Its inverse is $(1 / 2)$ , so $A - C B^{- 1} C^{T} = (\begin{array}{cc} 1 / 2 & 1 / 2 \\ 1 / 2 & 1 / 2 \end{array})$ and $C B^{- 1} (y - 0) = (y / 2, y / 2)$ . The conditional covariance is also singular, with determinant zero.

3.1A1F2step 2.1given∎

Apply [F2] with these blocks. It gives the displayed conditional Gaussian kernel for every $y$ , despite singularity of $A$ and the conditional covariance; no inverse or pseudoinverse of either is used.

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

20 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

Gelman et al., Bayesian Data Analysis, 3rd ed., §3.5 and Appendix A (standard reference, not scraped)
Simo Särkkä, Bayesian Filtering and Smoothing, Appendix A.1, Lemma A.2 (standard reference, not scraped)