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.

Equal predictive risks do not identify a model label

Example

Let the candidate model labels be $M = {0, 1}$ with identical observation laws $P_{0} = P_{1} = Bernoulli (1 / 2)$ . Associate with each label the constant learning rule $A_{m, k} (z_{1}, \dots, z_{k}) = h_{m}$ for every $k$ , where $h_{0} = 0$ and $h_{1} = 1$ , and use squared loss. The labels describe distinct candidate specifications but make the same observable data law.

Facts & Assumptions

Given: The two candidate labels, their common data law, and the two constant predictors. Compare their risks and show that observations cannot recover the label.

[F1]

Risk estimation versus model identification: risk minimization chooses a label by predictive loss, whereas identification asks to recover the true data-generating label.

[F2]

Cross-validation splits and training-size risk targets: risk is expected loss on an independent test observation after training.

[F3]

Identical distribution and IID families: an IID sample has mutually independent coordinates with the common law.

[F4]

Independent random elements have product joint law: the joint law of an IID finite sample is the product of its common marginal law.

[F5]

Bernoulli random variables and binomial random variables as sums of independent Bernoulli trials: For $p \in [0, 1]$ , a Bernoulli $(p)$ random variable takes the value $1$ with probability $p$ and $0$ with probability $1 - p$ .

Verification

1.1F1F2F5algebra

Under either label, $Y \sim Bernoulli (1 / 2)$ . By [F5], the two prediction risks are $E [(0 - Y)^{2}] = 1 / 2$ and $E [(1 - Y)^{2}] = 1 / 2$ , since $Y^{2} = Y$ and $(1 - Y)^{2} = 1 - Y$ . Thus the predictive-risk objective ties the labels and any fixed tie rule selects one without separating them.

1.2F3F4algebra

For every sample size $n$ , [F3]–[F4] give the same data law $P_{0}^{\otimes n} = P_{1}^{\otimes n}$ . Therefore every measurable data-based selector has the same output distribution under labels 0 and 1. If it were model-consistent at label 0, then $P_{0} ({\hat{m}}_{n} = 0) \to 1$ , and equality of the sample laws would give $P_{1} ({\hat{m}}_{n} = 0) \to 1$ . Consistency at label 1 would also give $P_{1} ({\hat{m}}_{n} = 1) \to 1$ , impossible because these disjoint events have probabilities summing to at most one.

2.1F1step 1.1step 1.2∎

The example has equal predictive risk but no observable information that distinguishes the two labels, so risk minimization alone does not identify a true model.

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

17 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

Sylvain Arlot and Alain Celisse, A survey of cross-validation procedures for model selection, §§2.2–2.4 and 6.1 (standard reference, not scraped)
Gareth James, Daniela Witten, Trevor Hastie, and Robert Tibshirani, An Introduction to Statistical Learning, 7th printing, Chapter 5 introduction (standard reference, not scraped)