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.

Separated supports saturate the ideal discriminator

Example

Let $X = {a, b}$ with counting measure $μ (E) = ∣ E ∣$ . Let $P_{d a t a}$ put mass $1$ at $a$ and $P_{G}$ put mass $1$ at $b$ , so their densities are $p (a) = 1$ , $p (b) = 0$ , $q (a) = 0$ , and $q (b) = 1$ . The ideal discriminator is $D^{*} (a) = 1$ and $D^{*} (b) = 0$ , the density-defined Jensen–Shannon divergence is $\ln 2$ , and the optimized minimax value is $C (P_{d a t a}, P_{G}) = 0$ . Thus disjoint supports give a saturated ideal discriminator; this calculation makes no claim about finite-network gradient behavior.

Example references

Optimal discriminator and Jensen–Shannon identity

Density-defined Jensen–Shannon divergence

Goodfellow et al., §4.1, Proposition 1 and Theorem 1, equations (2)–(6), complete 9-page paper

Li, §1.2, equations (4), (10)–(11), complete 6-page lecture note

Facts & Assumptions

Given: $X = {a, b}$ , counting measure $μ (E) = ∣ E ∣$ , $P_{d a t a} ({a}) = 1$ , $P_{G} ({b}) = 1$ , and zero mass at the other point for each law.

[F1]

Optimal discriminator and Jensen–Shannon divergence in the unrestricted GAN game: $D^{*} = p / (p + q)$ when $p + q > 0$ , $D^{*} = 1 / 2$ when $p + q = 0$ , and $C = - \ln 4 + 2 {JS}_{μ} (P, Q)$ .

[F2]

Density-defined Jensen–Shannon divergence: for $m = (p + q) / 2$ and $r = p / m$ , $s = q / m$ on $m > 0$ , ${JS}_{μ} (P, Q) = \frac{1}{2} \int m ϕ (r) d μ + \frac{1}{2} \int m ϕ (s) d μ$ , with $ϕ (0) = 0$ and $ϕ (t) = t \ln t$ .

Verification

Given: The two-point laws and counting measure in the Example.

1.1givenF2construct

Their densities are $p (a) = 1, p (b) = 0, q (a) = 0, q (b) = 1$ . Thus $m (a) = m (b) = 1 / 2$ , $(r (a), s (a)) = (2, 0)$ and $(r (b), s (b)) = (0, 2)$ .

2.1givenF1step 1.1algebra

By [F1], $D^{*} (a) = 1 / (1 + 0) = 1$ and $D^{*} (b) = 0 / (0 + 1) = 0$ .

2.2F2step 1.1algebra

Since $ϕ (0) = 0$ and $ϕ (2) = 2 \ln 2$ , the two integrals in [F2] each equal $\ln 2$ before their factor $1 / 2$ ; hence ${JS}_{μ} (P_{d a t a}, P_{G}) = \ln 2$ .

3.1F1step 2.1step 2.2algebra∎

By [F1] and step 2.2, $C (P_{d a t a}, P_{G}) = - \ln 4 + 2 \ln 2 = 0$ . The discriminator takes only the saturated endpoint values on the two supports, as claimed.

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

Ian J. Goodfellow et al., Generative Adversarial Nets, arXiv:1406.2661v1 (standard reference, not scraped)
Yingzhen Li, Lecture notes on generative adversarial networks (GANs), Deep Learning (Winter 2022, Imperial College London) (standard reference, not scraped)