Lax Lean Archive

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

Exact polynomial-time linear programming on a word RAM

Lax109476.PolynomialTimeSolver · concepts/Lax109476/PolynomialTimeSolver.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

    There is one polynomial-time word-RAM algorithm that solves every rational linear program exactly. It returns either an optimal primal point and matching dual multipliers, an infeasibility certificate, or a feasible point and an improving recession direction certifying 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: Exact polynomial-time linear programming on a word RAM
    6type: theorem
    7---
    8There is one polynomial-time word-RAM algorithm that solves every rational
    9linear program exactly. It returns either an optimal primal point and matching
    10dual multipliers, an infeasibility certificate, or a feasible point and an
    11improving recession direction certifying unboundedness.
    12
    13# Formalization notes
    14
    15This is the classical polynomial-time solvability theorem for rational
    16linear programming, with the outcomes stated through exact certificates.
    17The computation predicate is `Lax759944.RamPolytime.RamPolytime`, using the
    18registered word RAM and the input's binary size. The returned word must
    19equal the encoding of the same certificate whose conditions are checked.
    20No fixed dimension, bounded coefficient magnitude, or feasibility promise
    21is imposed. Empty dimensions are included.
    22
    23The existence of a polynomial-time solver is the algorithmic obligation;
    24ellipsoid-method internals are not separate claims in this submission.
    25-/
    26
    27namespace Lax109476.PolynomialTimeSolver
    28
    29open Lax109476.LinearProgram Lax109476.RationalCertificates Lax109476.RationalEncoding
    30open Lax759944.RamPolytime
    31
    32/-- One uniform polynomial-time RAM produces exact certificates for every LP. -/
    33axiom exists_exact_polynomial_time_solver :
    34 ∃ solve : List ℕ → List ℕ, RamPolytime solve ∧
    35 ∀ (m n : ℕ) (P : Program ℚ m n), ∃ certificate : Certificate m n,
    36 solve (encodeProgram P) = encodeCertificate certificate ∧
    37 IsValidCertificate P certificate
    38
    39end Lax109476.PolynomialTimeSolver
    40
    Show Proof
    Formalization notes

    This is the classical polynomial-time solvability theorem for rational linear programming, with the outcomes stated through exact certificates. The computation predicate is Lax759944.RamPolytime.RamPolytimeLax759944.RamPolytime.RamPolytime, using the registered word RAM and the input's binary size. The returned word must equal the encoding of the same certificate whose conditions are checked. No fixed dimension, bounded coefficient magnitude, or feasibility promise is imposed. Empty dimensions are included.

    The existence of a polynomial-time solver is the algorithmic obligation; ellipsoid-method internals are not separate claims in this submission.

    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…