Lax Lean Archive

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

Rational LP certificates for distance projection

Lax263307.RationalProjection · concepts/Lax263307/RationalProjection.lean · lax-263307

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

    Every valid exact certificate for the infinity-distance LP gives one of three outcomes: the original relaxation is infeasible; a rational point is feasible and within the prescribed coordinate error; or a rational normal separates every feasible point with a gap exceeding that error. The separating normal has sum of absolute coefficients at most one.

    Concept map
    7 concepts; 4 descendants hidden
    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 certificate_outcome proven

    2 classify_correct proven

    Lean source view on GitHub

    1import Lax263307.DistanceProjection
    2import Lax109476.CertificateSoundness
    3
    4/-!
    5---
    6title: Rational LP certificates for distance projection
    7type: theorem
    8---
    9Every valid exact certificate for the infinity-distance LP gives one of
    10three outcomes: the original relaxation is infeasible; a rational point
    11is feasible and within the prescribed coordinate error; or a rational
    12normal separates every feasible point with a gap exceeding that error.
    13The separating normal has sum of absolute coefficients at most one.
    14
    15# Formalization notes
    16
    17The objective of the projection LP is bounded, so an unbounded
    18certificate is impossible. Optimal primal and dual witnesses cast exactly
    19to real variables. This theorem checks the actual registered certificate
    20type; the dense matrix construction and solver RAM invocation still need
    21implementation.
    22-/
    23
    24namespace Lax263307.RationalProjection
    25
    26open Lax109476.LinearProgram Lax109476.RationalCertificates
    27open Lax263307.DistanceProjection
    28
    29inductive Outcome (n : ℕ)
    30 | near (point : Fin n → ℚ)
    31 | far (normal : Fin n → ℚ) (bound : ℚ)
    32 | reject
    33
    34/-- Inspect the actual certificate and compare its distance by exact arithmetic. -/
    35def classify {m n : ℕ} (P : Program ℚ m n) (ρ : ℚ) :
    36 Certificate (m + (n + n)) (n + 1) → Outcome n
    37 | .optimal z dual =>
    38 if distance z ≤ ρ then .near (point z)
    39 else .far (normal dual) (dualValue P (oldMultipliers dual))
    40 | .infeasible _ => .reject
    41 | .unbounded _ _ => .reject
    42
    43def Correct {m n : ℕ} (P : Program ℚ m n) (center : Fin n → ℚ) (ρ : ℚ) :
    44 Outcome n → Prop
    45 | .near y => PrimalFeasible (toReal P) (realVector y) ∧
    46 ∀ j, |(y j : ℝ) - (center j : ℝ)| ≤ (ρ : ℝ)
    47 | .far a α => (∑ j, |(a j : ℝ)|) ≤ 1 ∧
    48 (∀ y, PrimalFeasible (toReal P) y → (∑ j, (a j : ℝ) * y j) ≤ (α : ℝ)) ∧
    49 (ρ : ℝ) < (∑ j, (a j : ℝ) * (center j : ℝ)) - (α : ℝ)
    50 | .reject => ¬ IsFeasible (toReal P)
    51
    52axiom classify_correct {m n : ℕ} (P : Program ℚ m n) (center : Fin n → ℚ) (ρ : ℚ)
    53 (certificate : Certificate (m + (n + n)) (n + 1))
    54 (valid : IsValidCertificate (distanceProgram P center) certificate) :
    55 Correct P center ρ (classify P ρ certificate)
    56
    57axiom certificate_outcome {m n : ℕ} (P : Program ℚ m n) (center : Fin n → ℚ)
    58 (certificate : Certificate (m + (n + n)) (n + 1))
    59 (valid : IsValidCertificate (distanceProgram P center) certificate) (ρ : ℝ) :
    60 (¬ IsFeasible (toReal P)) ∨
    61 (∃ y : Fin n → ℚ, PrimalFeasible (toReal P) (realVector y) ∧
    62 ∀ j, |(y j : ℝ) - (center j : ℝ)| ≤ ρ) ∨
    63 (∃ a : Fin n → ℚ, ∃ α : ℚ,
    64 (∑ j, |(a j : ℝ)|) ≤ 1 ∧
    65 (∀ y, PrimalFeasible (toReal P) y → (∑ j, (a j : ℝ) * y j) ≤ (α : ℝ)) ∧
    66 ρ < (∑ j, (a j : ℝ) * (center j : ℝ)) - (α : ℝ))
    67
    68end Lax263307.RationalProjection
    69
    Show ProofShow Proof
    Formalization notes

    The objective of the projection LP is bounded, so an unbounded certificate is impossible. Optimal primal and dual witnesses cast exactly to real variables. This theorem checks the actual registered certificate type; the dense matrix construction and solver RAM invocation still need implementation.

    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…