Lax Lean Archive

While this submission is a draft, it cannot be used by other submissions.

Randomized computations as NP certificates

Lax253009.RandomizedContainments · concepts/Lax253009/RandomizedContainments.lean · lax-253009

proven

Loading review…

Community review

Flags

Each flag is tied to a public ORCID identity and explains why this concept may be incorrect.

No flags have been submitted.

    Community review

    Flag this concept

    State precisely what appears incorrect. This explanation will be public under your ORCID name.

    No source line selected.

    Natural Language Statement

    Lemma

    A successful random tape is a polynomial-length NP certificate for an RP algorithm. A deterministic verifier simulates every coin-selected tape transition and checks the resulting answer. The simulation includes a polynomial running-time bound in the registered machine models.

    Replacing a zero-error algorithm's failure answer by rejection also gives an RP algorithm. Consequently both RP and ZPP are contained in the registered NP class.

    Concept map
    7 concepts
    100%
    Proven claimDefinitionThis conceptRelated conceptA → B: B builds on A
    Evidence

    This concept declares 2 statements. Each proof establishes one of them relative to its assumptions.

    1 RP_subset_NP proven

    2 ZPP_subset_NP proven

    Lean source view on GitHub

    1import Lax434930.NondeterministicPolynomialTime
    2import Lax666725.OneSidedError
    3import Lax666725.ZeroError
    4
    5/-!
    6---
    7title: Randomized computations as NP certificates
    8type: lemma
    9---
    10A successful random tape is a polynomial-length NP certificate for an RP
    11algorithm. A deterministic verifier simulates every coin-selected tape
    12transition and checks the resulting answer. The simulation includes a
    13polynomial running-time bound in the registered machine models.
    14
    15Replacing a zero-error algorithm's failure answer by rejection also gives
    16an RP algorithm. Consequently both RP and ZPP are contained in the
    17registered NP class.
    18-/
    19
    20namespace Lax253009.RandomizedContainments
    21
    22axiom RP_subset_NP :
    23 Lax666725.OneSidedError.RP ⊆ Lax434930.NondeterministicPolynomialTime.NP
    24
    25axiom ZPP_subset_NP :
    26 Lax666725.ZeroError.ZPP ⊆ Lax434930.NondeterministicPolynomialTime.NP
    27
    28end Lax253009.RandomizedContainments
    29
    Show ProofShow Proof
    Builds on
    Used by

    none

    From Mathlib

    none

    Discussion

    Ask a question or add context. Endorsements and structured flags are kept in the review panel above.

    Loading discussion…