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

Finite-DMC hypothesis-testing meta-converse

Statement

Let a finite-DMC code have M≥1 messages and average error ϵ. For any output probability vector QYn, let PMYn(m,yn)=M−1Wn(yn∣xmn) be the true joint law and let Q~MYn(m,yn)=M−1QYn(yn). With the type-II testing function βϵ of Finite type-II testing function with explicit orientation, which constrains rejection under its first argument, one has βϵ(PMYn,Q~MYn)≤1M.

Facts & Assumptions

Given: A deterministic length-n code with M messages, average error ϵ, and any output probability vector QYn.

[F1]

Finite type-II testing function with explicit orientation: βϵ(P,Q) is the infimum of EQ(1−ϕ) over tests 0≤ϕ≤1 with EPϕ≤ϵ; the first law is the null and the second is the alternative.

[F2]

Fixed-length codes for a finite DMC and Average and maximal error of a fixed-length code: the decoder is a deterministic map d:Yn→[M], and the average error is the uniform-message error probability.

[F3]

Finite discrete memoryless channels and The DMC product laws are stochastic kernels: Wn(⋅∣xmn) is a probability vector for every codeword.

Proof

1.1F1F2F3givenalgebra

Define ϕ(m,yn)=1{d(yn)≠m}. Under the true law PMYn, EPϕ=ϵ, so ϕ is feasible in [F1]. Under Q~, its type-II error is EQ~(1−ϕ)=1M∑m=1M∑ynQYn(yn)1{d(yn)=m}=1M, since for each output exactly one message is decoded. No likelihood ratio is used, so zeros in QYn cause no support problem.

2.1F1step 1.1algebra∎

The infimum over all feasible tests in [F1] is at most the value of the particular test in step 1.1. This gives the claimed bound for every auxiliary output law, including singular ones.

Depends on

Used by

Dependency tree · two levels

16 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