Alphabeta Math
TheoremStatement: Literature-sourcedProof: AI-generatedprecheck passaudited 2026-09-02
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.

Polynomial-time many-one reductions transfer P-, NP-, and coNP-membership

Statement

Let A,B⊆{0,1}∗ and suppose that A≤pB.

  1. If B∈P, then A∈P.
  2. If B∈NP, then A∈NP.
  3. If B∈coNP, then A∈coNP.

Facts & Assumptions

Given: Binary languages A,B⊆{0,1}∗ and a fixed total polynomial-time map f witnessing A≤pB.

[L1]

A polynomial-time many-one reduction is a total polynomial-time membership-preserving map, by Polynomial-time many-one reductions.

[L2]

Composites of polynomial-time many-one reductions are again polynomial-time many-one reductions, by Polynomial-time many-one reductions compose.

[L3]

P is the class of polynomial-time decidable languages, by The class P.

[L4]

NP is the class of languages with polynomial-time verifiers and polynomially bounded certificates, by The class NP via polynomial-time verifiers and Polynomial-time verifiers with polynomially bounded certificates.

[L5]

coNP consists of complements of NP-languages, by The class coNP.

Proof

technique · direct
1.1L1L3givenconstruct

Assume B∈P, and let DB be a polynomial-time decider for B from [L3]. On input x, compute the fixed map f(x) and then run DB on that output. By [L1], the answer is correct because x∈A iff f(x)∈B, and the whole procedure is polynomial-time because both stages are. Thus A∈P.

1.2L1L4givenconstruct

Assume B∈NP. By [L4], choose a verifier relation RB and polynomial certificate bound p for B. Using the fixed reduction map f, define a verifier for A by declaring that (x,u) is accepted exactly when (f(x),u)∈RB. The output length ∣f(x)∣ is polynomial in ∣x∣, so the bound p(∣f(x)∣) is still polynomial in ∣x∣. Correctness follows from x∈A  ⟺  f(x)∈B  ⟺  ∃u with ∣u∣≤p(∣f(x)∣) and (f(x),u)∈RB. Therefore A∈NP.

2.1L1L2L5step 1.2given

Assume B∈coNP. Then Bc∈NP by [L5]. The fixed reduction map f also witnesses Ac≤pBc, because x∈Ac  ⟺  x∉A  ⟺  f(x)∉B  ⟺  f(x)∈Bc. Applying step 1.2 to the reduction Ac≤pBc gives Ac∈NP, and then [L5] yields A∈coNP. The composition principle [L2] guarantees that chaining such transfers remains inside the same reduction class.

3.1step 1.1step 1.2step 2.1∎

Steps 1.1, 1.2, and 2.1 prove the three transfer clauses.

Depends on

Used by

Dependency tree · two levels

8 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