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.

A compressed classifier can differ from its trained predictor off the sample

Example

Let $X = {0, 1}$ and $Y = {1, 2}$ , both with the discrete sigma-algebra, and let $P {(0, 1)} = P {(1, 2)} = 1 / 2$ . Define $ρ (t) = \max {0, t}$ and the two-class score maps $f (x) = (10 ρ (1 - x), ρ (x)), g (x) = (10, 0), x \in X .$ Both maps can be realized by one-hidden-layer feedforward networks with ReLU hidden activation and identity output activation. Take the training score map to be constant, $F (S, x) = f (x)$ for every length-one sample, and take a constant selector into a fixed one-code codebook with $q = 1$ and $r = 1$ , whose decoder is $g$ . For the one-point training sample $S = ((0, 1))$ , the scores agree exactly, so $g$ is a $1 / 10$ -score compression of $f$ on $S$ . Their least-index argmax classifiers agree at the observed input $0$ and differ at the unobserved input $1$ . Their population zero-one risks are $R_{P} (h_{f}) = 0$ and $R_{P} (h_{g}) = 1 / 2$ . This is only a single-sample witness: the fixed code does not meet the theorem's almost-sure compression hypothesis for this $P$ , because it fails on the other possible one-point sample $((1, 2))$ .

Example references

Finite feedforward computation graphs and layered MLPs: a finite acyclic computation graph evaluates hidden activations in topological order and uses identity output activations in a layered MLP.

Margin-preserving compression of score classifiers: a fixed helper and codebook can be paired with a sample-dependent code whose decoded scores are close on the observed inputs.

Finite-description compression bound for trained classifiers: its high-probability conclusion bounds the selected compressed classifier under an almost-sure compression hypothesis.

Facts & Assumptions

Given: The two-point measurable classification problem, the law $P$ , the one-point sample $S = ((0, 1))$ , the constant training map $F (S, x) = f (x)$ , the scores $f, g$ , and the fixed one-code family described in the Example.

[F1]

A feedforward computation graph is a finite directed acyclic graph evaluated in a topological order; a layered MLP has hidden activations and identity output activations. Finite feedforward computation graphs and layered MLPs

[F2]

A finite score codebook is fixed independently of the sample, while its measurable selector may depend on the sample; compression on $S$ requires coordinatewise score error at most the stated tolerance on each observed input. Margin-preserving compression of score classifiers

[F3]

Under the theorem's almost-sure compression hypothesis, the conclusion bounds the decoded classifier $h_{s, α (S)}$ , and makes no claim for the original classifier without separate all-domain loss preservation. Finite-description compression bound for trained classifiers

Verification

Given: The finite instance space $X = {0, 1}$ , labels $Y = {1, 2}$ , equal-mass law $P$ , and score maps from the Example.

1.1givenF1constructalgebra

Let the two hidden ReLU units for $f$ be $u_{1} (x) = ρ (x)$ and $u_{2} (x) = ρ (1 - x)$ , with output coordinates $(10 u_{2}, u_{1})$ . Let $g$ use one hidden unit $u_{1} (x) = ρ (x)$ , output weights zero, and output biases $(10, 0)$ . These are finite one-hidden-layer graphs with hidden activation $ρ$ and identity output activation, as in [F1]. Direct evaluation gives $f (0) = g (0) = (10, 0)$ and $f (1) = (0, 1)$ , $g (1) = (10, 0)$ .

2.1givenstep 1.1algebra

The least-index argmax rule predicts class $1$ for both maps at $x = 0$ ; at $x = 1$ , $f$ predicts class $2$ and $g$ predicts class $1$ . Under $P$ , $f$ is correct on both support points, while $g$ errs exactly at $(1, 2)$ , so $R_{P} (h_{f}) = 0$ and $R_{P} (h_{g}) = 1 / 2$ . Also $P^{1} {S = ((0, 1))} = 1 / 2$ .

3.1givenF2F3step 2.1algebra∎

Let $A = {a_{0}}$ with one parameter slot whose only possible value is $a_{0}$ , fix the helper string, decode $a_{0}$ to $g$ , and let the compressor choose $a_{0}$ on every sample. On $S = ((0, 1))$ , the maximum coordinate error is $0 \leq 1 / 10$ , so this sample is compressed and the predictions agree on the observed point. On $S^{'} = ((1, 2))$ , the maximum coordinate error is $10 > 1 / 10$ , so this fixed compressor fails the almost-sure premise of the theorem under $P$ . Therefore this example establishes only that single-sample agreement can coexist with different off-sample predictions and population risks; it does not contradict or invoke the theorem's high-probability conclusion.

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

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