ExampleConstruction: AI-generatedVerification: AI-generatedPipeline-generatedprecheck pass

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.

Eight-bit Box–Muller has a finite radial cutoff

Example

For $b = 8$ , a midpoint uniform is at least $1 / 512 = 2^{- 9}$ . The exact real-arithmetic Box–Muller reference transform therefore has radius at most $\sqrt{18 \log 2}$ . Its radial target law assigns probability $1 / 512$ beyond that radius, while the finite midpoint grid attains the cutoff at $K = 0$ but never exceeds it.

Facts & Assumptions

Given: Two independent 8-bit midpoint uniforms and the exact Box–Muller map used as a mathematical reference.

[F1]

A $b$ -bit midpoint has the form $(K + 1 / 2) 2^{- b}$ with integer $0 \leq K < 2^{b}$ . Its smallest value, at $K = 0$ , is $2^{- b - 1}$ ; this is finite arithmetic, independent of any countable-bit-stream realization.

[F2]

Under the ideal Box–Muller transform, $P (R > r) = e^{- r^{2} / 2}$ . Box–Muller has a product Gaussian density and Rayleigh second moment

[F3]

The natural logarithm is increasing on positive reals. Order, continuity, range, and the product, quotient, and reciprocal laws for the natural logarithm

[F4]

A square root is nonnegative and squares to its argument; squaring is order-preserving on nonnegatives. Square roots exist: a unique $\sqrt{a} \geq 0$ with $(\sqrt{a})^{2} = a$ ; the positives are ${x^{2} : x \neq 0}$ , Squaring is monotone on the nonnegatives

[F5]

For $x > 0$ , $\exp (\log x) = x$ . The natural logarithm as the inverse of the exponential function

[A1]

The exact Box–Muller change-of-variables supplier assumes Countable Choice. The Axiom of Countable Choice ( ${A C}_{ω}$ )

Verification

1.1givenF1algebra

For $b = 8$ , $2^{b} = 256$ and the smallest midpoint is $(0 + 1 / 2) / 256 = 1 / 512 = 2^{- 9}$ by [F1].

2.1F1F2F3F4F5A1step 1.1algebra∎

For $0 < u \leq v \leq 1$ , [F3] gives $0 \leq - 2 \log v \leq - 2 \log u$ . Their nonnegative square roots satisfy $\sqrt{- 2 \log v} \leq \sqrt{- 2 \log u}$ by [F4]; thus $r (u) = \sqrt{- 2 \log u}$ is nonincreasing, and the largest radius occurs at $u = 2^{- 9}$ and equals $\sqrt{18 \log 2}$ . The logarithm laws [F3] give $\log (2^{- 9}) = - 9 \log 2$ . By [F2] and [F5], the ideal radial tail beyond the cutoff is $e^{- 18 \log 2 / 2} = e^{\log (2^{- 9})} = 2^{- 9} = 1 / 512$ , while no finite midpoint input has a larger radius.

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

39 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

Luc Devroye, Non-Uniform Random Variate Generation, Chapter V §4.4 (standard reference, not scraped)
E. M. Raz, Lecture Notes in Probability, Chapter 5, Exercise 5.2 (standard reference, not scraped)