Lax Lean Archive

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

Binary-size encoding of rational linear programs

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

definition

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

    Definition

    An LP input word begins with its number of inequalities mm and variables nn, followed by the matrix in row order, the vector bb, and the vector cc. A rational is encoded by its numerator sign, numerator magnitude, and positive denominator, in reduced form. Solution words begin with an outcome tag and contain the corresponding rational certificate coordinates.

    Concept map
    8 concepts; 3 descendants hidden
    100%
    Proven claimDefinitionThis conceptRelated conceptA → B: B builds on A

    Lean source view on GitHub

    1import Lax109476.RationalCertificates
    2import Lax759944.RamPolytime
    3
    4/-!
    5---
    6title: Binary-size encoding of rational linear programs
    7type: definition
    8---
    9An LP input word begins with its number of inequalities mm and variables
    10nn, followed by the matrix in row order, the vector bb, and the vector cc.
    11A rational is encoded by its numerator sign, numerator magnitude, and
    12positive denominator, in reduced form. Solution words begin with an outcome
    13tag and contain the corresponding rational certificate coordinates.
    14
    15# Formalization notes
    16
    17The input sign is zero for nonnegative numerators and one for negative
    18numerators. Output tags zero, one, and two mean optimal, infeasible, and
    19unbounded. Dimensions are supplied by the input, so witness vectors have
    20fixed known lengths. Each rational keeps its exact denominator.
    21
    22The imported `RamPolytime` predicate uses binary word-list size, a single
    23uniform program, polynomial bounds on sufficient word length and executed
    24instructions, and correctness at every sufficiently large word length on
    25Lax808846's registered RAM. Its specified physical tape is length-prefixed.
    26Malformed logical inputs have no prescribed output, but the solver function
    27is total. No new machine model or abstract running-time annotation is introduced.
    28-/
    29
    30namespace Lax109476.RationalEncoding
    31
    32open Lax109476.LinearProgram Lax109476.RationalCertificates
    33
    34/-- Encode a reduced rational by sign, magnitude, and denominator. -/
    35def encodeRational (q : ℚ) : List ℕ :=
    36 [if q.num < 0 then 1 else 0, q.num.natAbs, q.den]
    37
    38/-- Encode all coordinates of a rational vector in index order. -/
    39def encodeVector {n : ℕ} (x : Fin n → ℚ) : List ℕ :=
    40 (List.ofFn x).flatMap encodeRational
    41
    42/-- Encode dimensions, row-major coefficients, row bounds, and objective. -/
    43def encodeProgram {m n : ℕ} (P : Program ℚ m n) : List ℕ :=
    44 [m, n] ++ (List.ofFn fun i => List.ofFn (P.A i)).flatten.flatMap encodeRational ++
    45 encodeVector P.b ++ encodeVector P.c
    46
    47/-- Encode the outcome tag and all rational certificate coordinates. -/
    48def encodeCertificate {m n : ℕ} : Certificate m n → List ℕ
    49 | .optimal x y => [0] ++ encodeVector x ++ encodeVector y
    50 | .infeasible y => [1] ++ encodeVector y
    51 | .unbounded x d => [2] ++ encodeVector x ++ encodeVector d
    52
    53end Lax109476.RationalEncoding
    54
    Formalization notes

    The input sign is zero for nonnegative numerators and one for negative numerators. Output tags zero, one, and two mean optimal, infeasible, and unbounded. Dimensions are supplied by the input, so witness vectors have fixed known lengths. Each rational keeps its exact denominator.

    The imported RamPolytimeRamPolytime predicate uses binary word-list size, a single uniform program, polynomial bounds on sufficient word length and executed instructions, and correctness at every sufficiently large word length on Lax808846's registered RAM. Its specified physical tape is length-prefixed. Malformed logical inputs have no prescribed output, but the solver function is total. No new machine model or abstract running-time annotation is introduced.

    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…