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

The orthogonal-design Lasso is coordinatewise soft thresholding

Example

Let $n \geq d \geq 1$ , let $X \in R^{n \times d}$ satisfy $X^{T} X = n I_{d}$ , and let $Y \in R^{n}$ be any response. Set $Z = X^{T} Y / n$ and use the penalty $τ > 0$ from Lasso estimator for fixed design. The unique Lasso minimizer has coordinates ${\hat{θ}}_{j} = S_{τ} (Z_{j})$ .

In particular, if $Z_{0} \in R^{d}$ is an observation from the sparse Gaussian sequence model of Gaussian sequence model with sparse means and $Y = X Z_{0}$ , then $Z = Z_{0}$ , so the same formula applies coordinatewise to that sequence observation. The square case $n = d$ , $X = \sqrt{n} I_{d}$ , and $Y = \sqrt{n} Z_{0}$ is included.

Facts & Assumptions

Given: Integers $n \geq d \geq 1$ , a design $X \in R^{n \times d}$ with $X^{T} X = n I_{d}$ , a response $Y \in R^{n}$ , $Z = X^{T} Y / n$ , and $τ > 0$ . For the Gaussian specialization, $Z_{0}$ is an observation from the stated Gaussian sequence model, with its Axiom of Choice hypothesis, and $Y = X Z_{0}$ .

[F1]

The Lasso objective is $n^{- 1} ∥ Y - X θ ∥_{2}^{2} + 2 τ ∥ θ ∥_{1}$ (Lasso estimator for fixed design).

[F2]

The Gaussian sequence observation has the form $(Z_{0})_{j} = θ_{j}^{*} + σ ξ_{j} / \sqrt{n}$ with independent standard normal $ξ_{j}$ (Gaussian sequence model with sparse means).

[F3]

The soft-threshold map is $S_{τ} (z) = z - τ$ for $z > τ$ , $0$ for $- τ \leq z \leq τ$ , and $z + τ$ for $z < - τ$ (Soft-thresholding map).

[F4]

For every response, the minimizer set of the Lasso objective is nonempty (The Lasso objective has a nonempty compact convex minimizer set).

Verification

1.1F1givenalgebra

Expanding [F1] and using $X^{T} X = n I_{d}$ and $X^{T} Y / n = Z$ gives $Q_{Y} (θ) = ∥ Y ∥_{2}^{2} / n - 2 Z^{T} θ + ∥ θ ∥_{2}^{2} + 2 τ ∥ θ ∥_{1}$ . Hence $Q_{Y} (θ) = c (Y) + \sum_{j = 1}^{d} ((Z_{j} - θ_{j})^{2} + 2 τ ∣ θ_{j} ∣)$ , where $c (Y) = ∥ Y ∥_{2}^{2} / n - ∥ Z ∥_{2}^{2}$ is independent of $θ$ . The objective therefore separates into one-coordinate objectives plus a constant.

1.2F3algebracases

For a scalar $z$ , on $θ \geq 0$ completing the square gives $(z - θ)^{2} + 2 τ θ = (θ - (z - τ))^{2} + 2 τ z - τ^{2}$ , whose constrained minimum is at $\max {z - τ, 0}$ . On $θ \leq 0$ , $(z - θ)^{2} - 2 τ θ = (θ - (z + τ))^{2} - 2 τ z - τ^{2}$ , whose constrained minimum is at $\min {z + τ, 0}$ . If $z > τ$ , the positive candidate has value $2 τ z - τ^{2}$ and is below the negative-branch boundary value $z^{2}$ by $(z - τ)^{2}$ ; if $z < - τ$ , the negative candidate is below the positive-branch boundary value by $(z + τ)^{2}$ ; if $∣ z ∣ \leq τ$ , both constrained minima occur uniquely at $0$ . Thus the unique scalar minimizer is $S_{τ} (z)$ .

2.1F1F2F4givenstep 1.1step 1.2algebra∎

By [F4] the minimizer set is nonempty. Since each coordinate term in step 1.1 has the unique minimizer from step 1.2, their vector of minimizers is the unique global minimizer, and its coordinates satisfy ${\hat{θ}}_{j} = S_{τ} (Z_{j})$ for every $j$ . In the Gaussian specialization, $Y = X Z_{0}$ gives $Z = X^{T} X Z_{0} / n = Z_{0}$ , so the formula applies pointwise to every realization of [F2]. When $n = d$ and $X = \sqrt{n} I_{d}$ , this response is $Y = \sqrt{n} Z_{0}$ , recovering the square case.

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

10 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

Philippe Rigollet, 18.S997 High-Dimensional Statistics, Chapter 2, Sections 2.3–2.4 (standard reference, not scraped)
Philippe Rigollet and Jan-Christian Hütter, High-Dimensional Statistics: Lecture Notes, Chapter 2 (standard reference, not scraped)