ExampleConstruction: AI-generatedVerification: AI-generatedPipeline-generatedprecheck pass

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.

A feature outside the assumed norm bound

Example

Take a one-round horizon $n = 1$ , $d = 2$ , $λ = 1$ , $L = 1$ , and $m_{2} = 0$ . Let $Ω = {ω_{0}}$ , $F = {\emptyset, Ω}$ , $P (Ω) = 1$ , and $F_{t} = F$ for all times. Use a single context $c$ , a single available action $\overset{ˉ}{a}$ , and feature map $ψ (c, \overset{ˉ}{a}) = a = (2, 0)$ . Let $θ^{*} = (0, 0)$ and $η_{1} = 0$ , so the reward is $X_{1} = 0$ . The coordinate Euclidean norm is $∥ a ∥_{2} = \sqrt{a_{1}^{2} + a_{2}^{2}}$ . This candidate violates the model's feature bound, although the matrix update formula still gives $V_{1} = diag (5, 1)$ .

Example references

Finite-dimensional linear contextual bandit model: every candidate feature must have Euclidean norm at most $L$ .

Tor Lattimore and Csaba Szepesvári, Bandit Algorithms, §19.3

Facts & Assumptions

Given: The finite-dimensional linear contextual bandit model and the one-round data in the Example.

[F1]

Finite-dimensional linear contextual bandit model: candidate features satisfy $∥ a ∥_{2} \leq L$ ; the information matrix is $V_{1} = λ I_{2} + a a^{T}$ .

[F2]

Rectangular matrix multiplication and the identity matrix $I_{n}$ , including zero-sized shapes: matrix products and the identity use their usual coordinate formulas.

Verification

1.1givenF1algebra

The feature has norm $∥ a ∥_{2} = \sqrt{2^{2} + 0^{2}} = 2 > 1 = L$ , so it violates the model's candidate-feature hypothesis. The zero parameter and zero noise do not repair that failed assumption.

2.1F1F2step 1.1algebra∎

Its outer product is $a a^{T} = (\begin{array}{cc} 4 & 0 \\ 0 & 0 \end{array})$ and $V_{0} = I_{2}$ , hence $V_{1} = I_{2} + a a^{T} = (\begin{array}{cc} 5 & 0 \\ 0 & 1 \end{array})$ . Thus the algebraic ridge update is defined, while the feature-norm premise used by the regret theorem is absent.

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

14 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

Tor Lattimore and Csaba Szepesvári, Bandit Algorithms (standard reference, not scraped)