Alphabeta Math
CounterexampleConstruction: AI-adaptedVerification: AI-adaptedPipeline-generatedjudge pass (gpt-5.6-terra)audited 2026-09-13
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.

Infinite variance can defeat square-root-n CLT scaling

Statement refuted

Assume AC. There are iid real variables with density c(x)=1/[π(1+x2)] and infinite second moment such that n−1/2∑k=1nXk has no weak limit. In particular square-root-n scaling need not produce a normal limit when finite variance is dropped.

Facts & Assumptions

[F2]

Compact continuous Riemann integrals agree with Lebesgue integrals under countable choice. A bounded Riemann integrable function on a closed bounded interval is Lebesgue measurable and has the same integral.

[F3]

The real exponential differentiates to itself. The exponential function is smooth and (exp⁡)′=exp⁡.

[F4]

Trigonometric derivatives justify real-component exponential antiderivatives. The derivatives of sine and cosine are cosine and minus sine.

[F6]

Increasing nonnegative integer truncations converge in integral. Monotone convergence for the integral.

[F7]

Integrable density majorants allow complex truncation limits. Dominated convergence.

[F8]

A nonnegative measurable density defines a measure. The indefinite integral of a nonnegative measurable function is a measure.

[F9]

For nonnegative measurable f and g, integration against the density measure f dμ satisfies ∫g d(f dμ)=∫gf dμ. Integrating against a density agrees with integrating the product.

[F11]

Arctangent takes its values strictly between -pi/2 and pi/2. The principal inverse tangent arctan⁡:R→(−π/2,π/2).

[F12]

An integrable transform gives a continuous probability density by inversion under AC. Density inversion from an integrable characteristic function.

[F14]

Independent copies of a given law exist under DC and countable choice. Countably many independent copies of a prescribed law exist.

[F15]

AC supplies dependent and countable choice. AC supplies countable selections and prescribed serial paths.

[F16]

Independent sums and scalar scaling give product transforms. Characteristic functions under affine maps and independent sums.

[F17]

Weak convergence would force convergence of every characteristic-function value. Levy continuity theorem forward direction.

[F18]

Every characteristic function is continuous at zero and equals one there. Basic properties of characteristic functions.

[F20]

Continuous functions on compact intervals are Riemann integrable. A continuous function on [a,b] is Riemann integrable, by Heine-Cantor and Riemann's criterion.

[F21]

Real integrals are defined by positive and negative parts, and complex integrals by real and imaginary parts. Integrable real and complex functions, and their integrals.

Counterexample

Given: Assume AC. There are iid real variables with density c(x)=1/[π(1+x2)] and infinite second moment such that n−1/2∑k=1nXk has no weak limit. In particular square-root-n scaling need not produce a normal limit when finite variance is dropped.

1.1F1F2F3F4F5F6F7F8F9F19F20F21

First construct the symmetric Laplace density l(x)=e−∣x∣/2. On [0,R] the primitive of e−x is −e−x, so [F1]–[F3], [F5] and [F20] give integral 1−e−R; the other half interval gives the same value by the primitive ex. The bridge [F2] and MCT [F6] yield ∫l=1. The elementary exponential series bound eR≥1+R makes e−R→0. Thus [F8] defines a probability with density l. For every bounded measurable complex h=u+iv, apply [F9] to u+,u−,v+,v−; these four functions are bounded by ∣h∣, so their products with l have finite integral. The real/imaginary definition [F21] then gives ∫h d(l dλ)=∫hl dλ. In particular the characteristic function of the constructed law is its density integral. For real t, componentwise differentiation using [F3]–[F5] gives the primitive e(−1+it)x/(−1+it) on the positive half-line and e(1+it)x/(1+it) on the negative half-line. Their nonzero denominators have modulus at least one. Taking integer R limits with DCT majorant e−∣x∣ and [F19] gives φl(t)=12((1−it)−1+(1+it)−1)=1/(1+t2).

2.1step 1.1F1F2F6F8F10F11F12F13F20

By [F10]–[F11], ∫−RR(1+t2)−1 dt=arctan⁡R−arctan⁡(−R)<π. The integrands are continuous, so the bridge and MCT make φl Lebesgue integrable. [F12] supplies the continuous density f(y)=(2π)−1∫e−ity/(1+t2) dt for the Laplace law. It equals l everywhere: both are continuous and have the same integral on every interval, whereas any nonzero value of f-l would, by continuity, have one strict sign bounded away from zero on a nonempty interval, contradicting that integral equality and [F13]. At y=0 this identity gives ∫(1+t2)−1 dt=π. Therefore [F8] makes c a probability density. At y=-u the same identity, multiplied by two, gives ∫eiuxc(x) dx=e−∣u∣. No contour integral is used.

3.1step 2.1F9F13F14F15F16

For R>=1, ∫1Rx2c(x) dx≥(R−1)/(2π) because x2/(1+x2)≥1/2 for x>=1. Nonnegative integral monotonicity and [F13] give this lower bound, tending to infinity; [F9] identifies the second moment as infinite. By [F14]–[F15], AC realizes iid copies of the c law. By [F16], their normalized-sum characteristic function is (e−∣t∣/n)n=e−n∣t∣. It tends to zero for t different from zero and stays one at zero.

4.1step 3.1F17F18∎

If those row laws had any weak limit probability, [F17] would make its characteristic function equal to the pointwise limit just calculated. That function is discontinuous at zero, contradicting [F18]. Thus there is no weak probability limit, and in particular no normal limit. AC was used through the Lebesgue bridge, density inversion and independent-copy construction; the direct moment lower bound and discontinuity argument make no additional selections.

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

137 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