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.

One streaming least-squares SGD update

Example

Let $Y$ be equally likely to be $- 1$ or $1$ on a filtered space with trivial $F_{0}$ and $F_{1} = σ (Y)$ . Set $ℓ (x, Y) = \frac{1}{2} (x - Y)^{2}$ and define the streaming least-squares objective $f (x) = E [ℓ (x, Y)]$ . From $x_{0} = 0$ , use the one-sample gradient $G_{0} = \partial_{x} ℓ (x_{0}, Y)$ and step $α_{0} = \frac{1}{2}$ . Compute the mean gradient, first iterate, and objective gap.

Facts & Assumptions

Given: The two-point finite probability space, the loss and objective in the Example, initial point $x_{0} = 0$ , and step $α_{0} = 1 / 2$ .

[A1]

The Axiom of Choice: AC is used for the canonical conditional-expectation interface.

[F1]

Finite probability spaces, outcome weights, events, and event probabilities: each of the two outcomes $Y = - 1, 1$ has weight $1 / 2$ .

[F2]

Expectation of a nonnegative or integrable random variable: on this finite space, expectation is the weighted finite sum.

[F3]

Filtration-adapted stochastic-gradient oracles and Robbins–Monro updates: the sample gradient is the oracle value, and the SGD step is $x_{1} = x_{0} - α_{0} G_{0}$ .

[F4]

The Euclidean inner product $⟨ x, y ⟩ = \sum_{k < n} x_{k} y_{k}$ on $R^{n}$ : on $R$ , $∥ x ∥_{2}^{2} = x^{2}$ .

[F5]

The derivative $f^{'} (c) = \lim_{x \to c} \frac{f (x) - f (c)}{x - c}$ of $f : A \to R$ at a point $c \in A$ that is a limit point of $A$ , and differentiability on a set: the derivative is the limit of the difference quotient.

[F6]

Conditional variance: $Var (G_{0} ∣ F_{0}) = E [(G_{0} - E [G_{0} ∣ F_{0}])^{2} ∣ F_{0}]$ .

Verification

1.1A1F1F2F3F5F6givenalgebra

By [F1]–[F2], $f (x) = \frac{1}{4} (x + 1)^{2} + \frac{1}{4} (x - 1)^{2} = \frac{1}{2} (x^{2} + 1) .$ Its difference quotient at $x$ is $(f (x + h) - f (x)) / h = x + h / 2$ , so [F5] gives $\nabla f (x) = x$ . Likewise $(ℓ (h, Y) - ℓ (0, Y)) / h = h / 2 - Y$ , so $G_{0} = - Y$ . Its conditional mean given the trivial $F_{0}$ is zero, equal to $\nabla f (0)$ , and [F6] with [F1]–[F2] gives conditional variance $E [Y^{2}] = 1$ .

2.1F3F4step 1.1algebra∎

The update in [F3] gives $x_{1} = Y / 2$ . Since $Y^{2} = 1$ , $f (x_{1}) = \frac{1}{2} (1 / 4 + 1) = 5 / 8$ , whereas $f (0) = 1 / 2$ is the minimum because $f (x) - f (0) = x^{2} / 2 \geq 0$ . Hence the realized objective gap after this one sample is exactly $1 / 8$ .

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

43 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.