Lax Lean Archive

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

Polynomial-time certified optimization

Lax109476.CertifiedOptimization · concepts/Lax109476/CertifiedOptimization.lean · lax-109476

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

    Theorem

    One polynomial-time word-RAM algorithm returns an exact certificate of the correct real outcome for every rational linear program: optimality, infeasibility, or unboundedness.

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

    Each proof establishes this claim relative to its assumptions.

    Lean source view on GitHub

    1import Lax109476.RationalEncoding
    2
    3/-!
    4---
    5title: Polynomial-time certified optimization
    6type: theorem
    7---
    8One polynomial-time word-RAM algorithm returns an exact certificate of the
    9correct real outcome for every rational linear program: optimality,
    10infeasibility, or unboundedness.
    11
    12# Formalization notes
    13
    14This combines the exact solver specification with certificate soundness.
    15The output equals the encoding of a certificate that both passes the exact
    16rational conditions and establishes the corresponding claim over real
    17variables. The two guarantees refer to the same certificate.
    18-/
    19
    20namespace Lax109476.CertifiedOptimization
    21
    22open Lax109476.LinearProgram Lax109476.RationalCertificates Lax109476.RationalEncoding
    23open Lax759944.RamPolytime
    24
    25/-- A uniform polynomial-time RAM returns valid certificates of the real outcome. -/
    26axiom exists_certified_polynomial_time_solver :
    27 ∃ solve : List ℕ → List ℕ, RamPolytime solve ∧
    28 ∀ (m n : ℕ) (P : Program ℚ m n), ∃ certificate : Certificate m n,
    29 solve (encodeProgram P) = encodeCertificate certificate ∧
    30 IsValidCertificate P certificate ∧ IsCorrectOutcome P certificate
    31
    32end Lax109476.CertifiedOptimization
    33
    Show Proof
    Formalization notes

    This combines the exact solver specification with certificate soundness. The output equals the encoding of a certificate that both passes the exact rational conditions and establishes the corresponding claim over real variables. The two guarantees refer to the same certificate.

    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…