Alphabeta Math
TheoremStatement: Literature-sourcedProof: AI-adaptedjudge 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.

Levin--Schnorr characterization of Martin-Löf randomness

Statement

X2ω is Martin-Löf random iff some constant c satisfies K(Xn)nc for every n.

Facts & Assumptions

Given: X2ω and fixed optimal prefix complexity.

Proof

1.1

For k0, let Vk={[σ]:K(σ)<σk}. The sequence is uniformly effectively open: dovetail the fixed prefix machine and enumerate σ at level k when a description shorter than σk appears. Choose one shortest program pσ for each such σ. These programs are distinct and belong to a prefix-free domain, so Kraft inequality and effective prefix-code allocation gives μ(Vk)σ2σ2kσ2pσ2k. Thus (Vk) is a Martin-Löf test. If the deficiencies nK(Xn) are unbounded, then XVk for every k, so X is not random.

givenconstruct
1.2

Conversely, suppose X fails a Martin-Löf test (Uj). For each k, turn the enumeration of U2k+2 into a computable disjoint cylinder cover: when a cylinder arrives, enumerate a finite prefix-free partition of the part not covered at earlier stages. For every resulting cylinder [σ], issue the request (σ,σk). Its length is nonnegative because one such cylinder already has measure at most μ(U2k+2)22k2, and the total request weight is k2kμ(U2k+2)k2k21. The effective allocation clause of Kraft inequality and effective prefix-code allocation therefore gives a prefix-free machine M with KM(σ)σk for every request. Prefix optimality Invariance theorem for prefix complexity supplies a constant d with K(σ)σk+d. Since XU2k+2, for every k one of the covering strings σX gives deficiency at least kd. Hence the prefix deficiencies of X are unbounded.

givenconstruct
2.1

Step 1.1 says bounded deficiency is necessary for randomness, while step 1.2 says nonrandomness forces unbounded deficiency. Taking contrapositives under Martin-Löf tests and random sequences proves the equivalence.

step 1.1step 1.2

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

6 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