ExampleConstruction: AI-generatedVerification: AI-generatedPipeline-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.

Heavy tails and a location shift in split R-hat

Example

The standard Cauchy law has density $f (x) = 1 / (π (1 + x^{2}))$ by Standard Cauchy probability law. Its second moment is infinite, so the population variance used to interpret an unranked variance diagnostic does not exist. Separately, take two finite chains of length eight:

$x_{1} = (- 1, - 1, 1, 1, - 1, - 1, 1, 1), x_{2} = (1, 1, 3, 3, 1, 1, 3, 3) .$

The raw split statistic and the rank-normalized split statistic on these location-shifted arrays are both $\sqrt{7 / 4}$ ; the folded component is $\sqrt{3 / 4}$ . This finite calculation illustrates location sensitivity. It is distinct from the paper's replicated Cauchy simulations, which are empirical evidence rather than a theorem.

Facts & Assumptions

Given: The standard Cauchy law Standard Cauchy probability law, the two finite arrays above, and the split and rank-normalized folded split procedures.

[A1]

The Axiom of Choice assumed by the standard-normal rank-score interface. The Axiom of Choice

[A2]

Countable Choice is used by the construction of the standard Cauchy probability law. The Axiom of Countable Choice ( ${A C}_{ω}$ )

[F1]

Variance is defined for square-integrable random variables. Moments, variance, and covariance on a probability space

[F2]

Split $\hat{R}$ uses ${\hat{V}}^{+} = (N - 1) W / N + B / N$ and returns $\sqrt{{\hat{V}}^{+} / W}$ when $W > 0$ . Split R-hat from multiple chains

[F3]

The improved procedure takes the maximum of rank-normalized split $\hat{R}$ and rank-normalized folded split $\hat{R}$ . Rank-normalized folded split R-hat

[F7]

Every probability in $(0, 1)$ has a unique finite standard-normal score, and complementary probabilities have opposite scores. The standard normal CDF has unique symmetric quantiles

[F8]

The standard Cauchy law is the measure $f d λ$ , with $f (x) = 1 / (π (1 + x^{2}))$ . For nonnegative measurable $g$ , $\int g d (f d λ) = \int g f d λ$ . Standard Cauchy probability law Integrating against a density agrees with integrating the product

[F9]

The nonnegative integral is monotone, positively homogeneous, and agrees with the simple integral on simple functions; in particular, $\int c 1_{A} d λ = c λ (A)$ for $c \geq 0$ and measurable $A$ . Monotonicity and nonnegative homogeneity of the nonnegative integral The nonnegative integral agrees with the simple integral on simple functions

[F10]

Under Countable Choice, the interval $[1, R]$ has Lebesgue measure $R - 1$ for every finite $R \geq 1$ . A box in $R^{n}$ with parameters $a_{i} \leq b_{i}$ is Lebesgue measurable of measure $\prod_{i < n} (b_{i} - a_{i})$ , whichever of its faces are included

[F11]

$π > 0$ , and the polynomial $x^{2}$ and the function $h (x) = x^{2} / (π (1 + x^{2}))$ are continuous, hence Lebesgue measurable under Countable Choice: the denominator never vanishes, algebra preserves continuity, continuous functions are Borel measurable, and Borel sets are Lebesgue measurable. Pi as twice the smallest positive zero of cosine Sums, scalar multiples, products, absolute values, maxima, minima and quotients with nonvanishing denominator of continuous functions are continuous, as are constants, the identity and every polynomial function Continuous functions on Euclidean spaces are Borel measurable Assuming countable choice, every Borel subset of $R^{n}$ is Lebesgue measurable

Verification

Given: The density and arrays in the Example.

1.1A2givenF1F8F9F10F11algebra

Put $h (x) : = x^{2} f (x) = x^{2} / (π (1 + x^{2}))$ , which is nonnegative and measurable by [F11]. For every finite $R > 1$ and $x \in [1, R]$ , $x^{2} / (1 + x^{2}) \geq 1 / 2$ , so $(2 π)^{- 1} 1_{[1, R]} (x) \leq h (x)$ . By [F9] and [F10], $\int_{R} h d λ \geq \int_{R} (2 π)^{- 1} 1_{[1, R]} d λ = \frac{R - 1}{2 π} .$ These lower bounds are unbounded as $R \to \infty$ , so $\int h d λ = + \infty$ . Applying [F8] to the nonnegative measurable function $x \mapsto x^{2}$ gives $\int_{R} x^{2} d μ_{C} = \int_{R} x^{2} f d λ = \int_{R} h d λ = + \infty .$ Thus the Cauchy target is not square-integrable, and its population variance is not defined under [F1].

1.2givenF2algebra

Splitting the arrays gives four length-four chains, two with values $(- 1, - 1, 1, 1)$ and two with $(1, 1, 3, 3)$ . Each has sample variance $4 / 3$ ; their means are $0, 0, 2, 2$ , with grand mean $1$ . Hence $W = 4 / 3$ and $B = (4 / 3) (1 + 1 + 1 + 1) = 16 / 3$ .

1.3A1F2F3F7algebra

In the pooled sample, $- 1, 1, 3$ have multiplicities $4, 8, 4$ and average ranks $2.5, 8.5, 14.5$ . Their Blom probabilities are $17 / 130, 1 / 2, 113 / 130$ . By [F7], the corresponding scores are $- a, 0, a$ for $a = Φ^{- 1} (113 / 130) > 0$ . The four split-chain means are $- a / 2, - a / 2, a / 2, a / 2$ , each variance is $a^{2} / 3$ , and the scale factors cancel in [F2]; the rank-normalized split statistic is again $\sqrt{7 / 4}$ .

2.1step 1.2F2algebra

Therefore ${\hat{V}}^{+} = (3 / 4) (4 / 3) + (1 / 4) (16 / 3) = 7 / 3$ , and the raw split statistic is $\sqrt{(7 / 3) / (4 / 3)} = \sqrt{7 / 4}$ .

2.2A1step 1.2F2F3F7algebra

The pooled median is $1$ , so the raw folds have values $0$ and $2$ , each occurring eight times. Their average ranks are $4.5$ and $12.5$ , with Blom probabilities $33 / 130$ and $97 / 130$ . By [F7], their scores are $- b$ and $b$ , where $b = Φ^{- 1} (97 / 130) > 0$ . Thus every folded score is $b$ times its raw fold minus $b$ . A positive scaling and common translation multiply $W$ and $B$ by $b^{2}$ and leave ${\hat{V}}^{+} / W$ unchanged. The raw folded split chains are $(2, 2, 0, 0)$ and $(0, 0, 2, 2)$ ; each has mean $1$ and sample variance $4 / 3$ , so $B = 0$ and the rank-normalized folded statistic is $\sqrt{3 / 4}$ .

3.1step 1.1step 1.3step 2.1step 2.2F3algebra∎

The maximum in [F3] is $\sqrt{7 / 4}$ . The calculation detects this finite location shift, while step 1.1 shows why variance-based population reasoning is unavailable for the Cauchy target.

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

92 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

Aki Vehtari et al., Rank-normalization, folding, and localization, §§1.2 and 4.1–4.2 (standard reference, not scraped)
Art B. Owen, Monte Carlo Theory, Methods and Examples, Chapter 11, §11.11 (standard reference, not scraped)