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

Cauchy averages admit no deterministic weak centering

Statement refuted

Assume countable choice and dependent choice. For IID real variables with density f(x)=1/[π(1+x2)] on R, there is no deterministic real sequence (μn) for which Sn/n−μn→0 in probability, where Sn=∑k=1nXk. Thus IID alone cannot guarantee a weak law even with varying deterministic centering.

Facts & Assumptions

[F1]

Exact tail criterion for a truncated-centered IID weak law: For IID real random variables (Xn)n≥1 and Sn=∑k=1nXk, there exist deterministic real constants (μn) with Sn/n−μn→0 in probability if and only if nP(∣X1∣>n)⟶0. When this condition holds, μn=E[X11{∣X1∣≤n}] works. Neither existence of an untruncated mean nor convergence of (μn) is asserted.

[F2]

Countably many independent copies of a prescribed law exist: Assume countable choice and dependent choice. Every probability measure ν on (S,Σ) is the common law of a countable independent family of S-valued random elements.

[F3]

Law or distribution of a random element: Let X:(Ω,F,P)→(S,Σ) be a random element. Its law or distribution is the set function PX:Σ→[0,+∞],PX(B):=P(X−1(B)). Thus the law of X records the probability of each measurable target set by pulling it back to an event in the original probability space.

[F4]

Probability laws correspond to distribution functions: Assume the Axiom of Countable Choice. 1. Let X be a real random variable, let PX be its law, and let FX(x)=P(X≤x). Then FX is nondecreasing and right-continuous, satisfies lim⁡x→−∞FX(x)=0,lim⁡x→+∞FX(x)=1, and obeys PX((a,b])=FX(b)−FX(a)(a<b). 2. Conversely, if F:R→R is nondecreasing and right-continuous with lim⁡x→−∞F(x)=0,lim⁡x→+∞F(x)=1, then there is a unique Borel probability measure μ on R such that μ((a,b])=F(b)−F(a)(a<b), equivalently F(x)=μ((−∞,x])(x∈R).

Counterexample

Given: The construction and assumptions above.

1.1F3F2givenalgebraF4

The nonnegative density has total integral [arctan⁡x/π]−∞∞=1 and F(x)=1/2+arctan⁡(x)/π is nondecreasing and continuous with limits zero and one. The distribution-function correspondence therefore supplies its Borel probability law; the fundamental theorem of calculus identifies its density as f. Under countable choice and dependent choice, construct IID copies with that law. Symmetry of the density gives P(∣X1∣>n)=(2/π)∫n∞(1+x2)−1 dx.

2.1F1step 1.1algebra∎

For x≥n≥1, x−2/(1+n−2)≤(1+x2)−1≤x−2. Integrating and multiplying by n gives 2/[π(1+n−2)]≤nP(∣X1∣>n)≤2/π. Thus this tail quantity tends to 2/π, not zero. Necessity in the truncated-centering criterion rules out every deterministic centering sequence.

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

26 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