ExampleConstruction: AI-generatedVerification: AI-adaptedPipeline-generatedjudge 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 two-class one-layer spectral-margin calculation

Example

Assume the axiom of choice. Take one layer with input width $1$ , output width $2$ , identity activation with Lipschitz constant $ρ_{1} = 1$ , reference matrix $M_{1} = 0$ , and layer matrix $A_{1} = (1, - 1)^{⊤}$ . Let the input distribution be the point mass at $(x, y) = (1, 1)$ , so a sample of size $n = 1$ always has $X = (1)$ and label $1$ . At margin level $γ = 1$ and confidence $δ = 1 / 10$ , the score vector is $(1, - 1)$ , its margin is $2$ , its empirical margin loss and population error are both zero, and the spectral network complexity is $R_{A} = 2$ . The simultaneous theorem's right-hand side is $8 + 3 \sqrt{Q / 2}$ , where $Q = \log 60 + 2 \log 3 + 2 \log 3 + 2 \log 4 + 2 \log (2 + \sqrt{2}) \approx 13.72,$ so the bound evaluates to approximately $15.86$ . The example records the exact margin and complexity and shows the small-sample bound is valid but loose.

Example references

Spectral network complexity with reference matrices: defines the spectral complexity formula and induced operator norm.

Multiclass margins, ramp loss, and empirical margin loss: defines multiclass margin, empirical margin loss, and population error.

A simultaneous spectral margin bound for multiclass networks: supplies the simultaneous probability bound and its confidence expression.

Facts & Assumptions

Given: The one-layer network, point-mass distribution, sample size, margin level, and confidence parameter in the Example.

[F1]

The spectral norm is the induced Euclidean operator norm, the transpose-difference mixed norm sums its column Euclidean norms, and $R_{A}$ is their prescribed spectral-complexity expression. Spectral network complexity with reference matrices

[F2]

The margin is true-label score minus the largest competing score; empirical margin loss counts examples with margin at most the threshold, and population error is zero-one classification error. Multiclass margins, ramp loss, and empirical margin loss

[F3]

Under the stated iid and choice assumptions, the simultaneous theorem has an additive $8 / n$ term, a leading term proportional to $\log n$ , and confidence term $3 \sqrt{Q / (2 n)}$ . A simultaneous spectral margin bound for multiclass networks

Verification

technique · direct

1.1F1givenalgebra

The only column of $A_{1}$ has Euclidean norm $\sqrt{2}$ , so its induced operator norm is $\sqrt{2}$ . The transpose $A_{1}^{⊤} = (1, - 1)$ has two scalar columns of absolute values $1$ and $1$ , so $∥ A_{1}^{⊤} - M_{1}^{⊤} ∥_{2, 1} = 2$ . Also $∥ X ∥_{F} = 1$ .

2.1F2givenstep 1.1algebra

Applying the network map to $x = 1$ gives scores $(1, - 1)$ ; [F2] therefore gives margin $1 - (- 1) = 2$ , empirical margin loss $1 {2 \leq 1} = 0$ , and zero population error under the point-mass law.

3.1F1F3step 1.1step 2.1algebra∎

Substitution into the spectral-complexity definition yields $R_{A} = \sqrt{2} {((2 / \sqrt{2})^{2 / 3})}^{3 / 2} = 2.$ For $n = 1$ the leading term in [F3] vanishes because $\log 1 = 0$ , and $8 / n = 8$ . Substituting $δ = 1 / 10$ , $γ = 1$ , $∥ X ∥_{F} = 1$ , $L = 1$ , $∥ A_{1}^{⊤} - M_{1}^{⊤} ∥_{2, 1} = 2$ , and $∥ A_{1} ∥_{σ} = \sqrt{2}$ into the theorem's $Q$ gives the displayed expression. The inequality is $0 \leq 8 + 3 \sqrt{Q / 2} \approx 15.86$ .

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

Bartlett, Foster, and Telgarsky, Spectrally-normalized margin bounds for neural networks, Definition (1.2) and Theorem 1.1 (standard reference, not scraped)