Alphabeta Math
ExampleConstruction: AI-adaptedVerification: AI-adaptedPipeline-generatedaudited 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.

A Lindeberg array with no identically distributed row

Example

Assume AC. For 1≤k≤n, take independent Bernoulli variables Bn,k with pn,k=k/(2n+2) and put Xn,k=Bn,k−pn,k. The centered laws are distinct within each row of length at least two, yet the array satisfies Lindeberg and sn−1∑kXn,k⇒N(0,1).

Facts & Assumptions

[F1]

Under DC and countable choice the specified countable family of probability spaces has a product probability. Assuming countable and dependent choice, countable products of arbitrary probability spaces.

[F2]

The product coordinates are independent and have the specified laws. Coordinate random elements of a countable product are independent.

[F3]

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

[F5]

Under AC the Lindeberg condition gives a standard-normal limit. Lindeberg-Feller central limit theorem: sufficiency.

Verification

Given: Assume AC. For 1≤k≤n, take independent Bernoulli variables Bn,k with pn,k=k/(2n+2) and put Xn,k=Bn,k−pn,k. The centered laws are distinct within each row of length at least two, yet the array satisfies Lindeberg and sn−1∑kXn,k⇒N(0,1).

1.1F1F2F3F4

Each 0<pn,k<1/2 defines a two-point probability. Index the pairs by n(n−1)/2+k and use [F1]–[F3] to construct all coordinates independently. By [F4], the centered entry has mean zero and variance pn,k(1−pn,k). Its values are −pn,k and 1−pn,k, both of absolute value less than one. Distinct p have distinct negative support points with positive mass, hence distinct centered laws. Normalizing every entry in a fixed row by the same positive s_n also preserves this distinction.

2.1step 1.1F5∎

Since 1−pn,k>1/2, sn2≥12∑k=1nk/(2n+2)=n/8. Here ∑k=1nk=n(n+1)/2, obtained by pairing k with n+1-k and adding the n equal pair sums. Thus s_n is positive and tends to infinity. For any fixed epsilon>0, eventually εsn>1, so every event ∣Xn,k∣>εsn is empty. The Lindeberg sum is then exactly zero. All second moments are finite, so [F5] gives the claimed limit. AC is used only through the stated product construction and CLT suppliers; no cross-row independence is needed by the theorem.

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

40 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