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

P/poly equals polynomial time with polynomial advice

Statement

P/poly is exactly the class of languages decided in polynomial time with polynomial-length advice.

Facts & Assumptions

Given: the circuit-family and advised-machine conventions of the claim.

[L1]

A P/poly language has a polynomial-size circuit Cn at each input length n, by Circuit families and P/poly.

[L2]

Advice may depend on the input length and need not be computable, but has polynomial length, by Polynomial advice for a deterministic machine.

[L3]

Every polynomial-time language has polynomial-size circuits, by Every polynomial-time language has polynomial-size circuits.

Proof

technique · direct
1.1L1L2given

Suppose (Cn) has size at most p(n). Encode Cn as a topologically ordered gate list: each of its at most p(n) records contains a constant-size gate tag and at most two indices of O(log⁡(n+p(n))) bits. This is polynomial advice. A fixed evaluator scans the list in topological order and computes Cn(x) in polynomial time, so [L2] gives an advised decider.

1.2L2L3givenconstruct

Conversely, let M(x,an) run in polynomial time with ∣an∣≤p(n). Use a fixed self-delimiting encoding ⟨x,a⟩ whose length depends only on ∣x∣ and ∣a∣, and let B={⟨x,a⟩:M(x,a)=1}. This is a language in P, so [L3] supplies polynomial-size circuits for B. For a fixed n, put mn=∣an∣ and take the circuit for the common encoding length of ⟨x,an⟩ with ∣x∣=n. Hardwire the delimiter bits and all bits of an, leaving only the n bits of x free. Because mn≤p(n), the resulting n-input circuit has polynomial size and agrees with the original computation M(x,an); no change to the advice string or its length is made.

2.1step 1.1step 1.2∎

Step 1.1 proves the circuit-to-advice inclusion and step 1.2 proves the advice-to-circuit inclusion, including the advice-length and simulation-size bounds.

Depends on

Used by

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