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

Training risk and independent test risk are different quantities

Example

Use the degree-one clamped B-spline basis p(x)=(1−x,x) on [0,1], with a single fixed training input x1=1/2 and response y1=1. The coefficient vector β^=(0,2)T is a least-squares minimizer and gives the fitted function g^(x)=2x. Let the target be g0(x)=1 and the independent test input be uniform on [0,1].

Facts & Assumptions

Given: The one-row design matrix P=(1/2,1/2), response Y=(1), and test law X′∼Unif⁡[0,1].

[F1]

The fitted training vector is the orthogonal projection onto the design column space; any least-squares coefficient representation has that same training fit (Series least squares with a spline basis).

[F2]

The risk bound in this page concerns expected empirical training-design loss, not independent test loss (Expected empirical training risk for spline series least squares).

[F3]

The clamped degree-one B-splines form a basis of the degree-one spline space, and the recurrence defines their values (B-spline spaces and knot conventions, B-spline basis properties and polynomial reproduction).

[A1]

The training input and response are 1/2 and 1, the chosen least-squares coefficient is (0,2)T, and the independent test input is uniform on [0,1].

Verification

Given: x1=1/2, y1=1, β^=(0,2)T, g0≡1, and independent X′∼Unif⁡[0,1].

1.1A1F1F3givenalgebra

On the clamped knot vector (0,0,1,1), the only nonzero degree-zero spline on (0,1) is B2,0=1; the recurrence in [F3] gives B1,1=1−x and B2,1=x, so p(1/2)=(1/2,1/2). Therefore p(1/2)Tβ^=(1/2,1/2)(0,2)T=1, the training residual and empirical training loss are zero, and the fitted vector equals the projection in [F1]. The chosen coefficient vector is one admissible representation of it.

2.1A1F2step 1.1algebra∎

The independent test squared error has expectation E{g^(X′)−g0(X′)}2=∫01(2x−1)2dx=43−2+1=13>0. Thus zero training loss does not imply zero independent test loss, consistent with the scope of [F2].

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

19 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