Lax Lean Archive

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

Real feasibility of rational linear programs has a rational witness

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

    A finite linear system with rational coefficients has a nonnegative real feasible point if and only if it has a nonnegative rational feasible point. The direction requiring a rational witness follows from elimination over the rationals and the soundness of rational infeasibility certificates over the reals.

    Concept map
    6 concepts; 1 descendant hidden
    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.RationalCertificates
    2import Lax109476.FarkasSoundness
    3
    4/-!
    5---
    6title: Real feasibility of rational linear programs has a rational witness
    7type: theorem
    8---
    9A finite linear system with rational coefficients has a nonnegative real
    10feasible point if and only if it has a nonnegative rational feasible point.
    11The direction requiring a rational witness follows from elimination over
    12the rationals and the soundness of rational infeasibility certificates over
    13the reals.
    14
    15# Formalization notes
    16
    17The statement imposes no full-dimension or interior-point condition. It
    18does not bound the size of the rational point or the time needed to find it.
    19-/
    20
    21namespace Lax109476.RationalFeasibility
    22
    23open Lax109476.LinearProgram Lax109476.RationalCertificates
    24
    25/-- Real feasibility of rational coefficient data has an exact rational witness. -/
    26axiom exists_rational_feasible_point :
    27 ∀ (m n : ℕ) (P : Program ℚ m n), IsFeasible (toReal P) →
    28 ∃ x : Fin n → ℚ, PrimalFeasible P x
    29
    30end Lax109476.RationalFeasibility
    31
    Show Proof
    Formalization notes

    The statement imposes no full-dimension or interior-point condition. It does not bound the size of the rational point or the time needed to find it.

    Builds on
    Used by
    From Mathlib

    none

    Discussion

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

    Loading discussion…