Lax Lean Archive

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

A uniform RAM program for the rounded ellipsoid update

Lax263307.NativeRoundedStep · concepts/Lax263307/NativeRoundedStep.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

    One fixed finite RAM program reads a rational shape, an integer cut normal, a rational center, and the iteration index, and writes the rounded next shape and center. Both its instruction count and sufficient word length are polynomial in the dimension, iteration index, and coordinate bit bound. It works at every larger word length. The input has no length prefix.

    Concept map
    11 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 Lax263307.RoundedOracleSearch
    2import Lax808846.Ram
    3
    4/-!
    5---
    6title: A uniform RAM program for the rounded ellipsoid update
    7type: theorem
    8---
    9One fixed finite RAM program reads a rational shape, an integer cut normal,
    10a rational center, and the iteration index, and writes the rounded next
    11shape and center. Both its instruction count and sufficient word length
    12are polynomial in the dimension, iteration index, and coordinate bit bound.
    13It works at every larger word length. The input has no length prefix.
    14
    15# Formalization notes
    16
    17This statement concerns actual `Lax808846.Ram.RunsTo`. The proof compiles
    18the registered LP submission's complete rational ellipsoid update, adding
    19the input reader and canonical output writer. It is one subroutine of the
    20recursive QPTAS; it does not assert that the complete QPTAS program exists.
    21-/
    22
    23namespace Lax263307.NativeRoundedStep
    24
    25open Matrix Lax263307.RoundedOracleSearch Lax109476.RationalEncoding
    26
    27def height (q : ℚ) (h : ℕ) : Prop := q.num.natAbs ≤ 2 ^ h ∧ q.den ≤ 2 ^ h
    28
    29def encodeInput {n : ℕ} (k : ℕ) (state : State n) (a : Fin n → ℤ) : List ℕ :=
    30 [n, k] ++ (List.ofFn fun i => encodeVector (state.1 i)).flatten ++
    31 encodeVector (rationalNormal a) ++ encodeVector state.2
    32
    33def encodeOutput {n : ℕ} (state : State n) : List ℕ :=
    34 (List.ofFn fun i : Fin (n * n) => state.1 i.divNat i.modNat).flatMap encodeRational ++
    35 encodeVector state.2
    36
    37axiom exists_program : ∃ p : Lax808846.Ram.Program, ∃ c : ℕ, 0 < c ∧
    38 ∀ (n k h : ℕ), 2 ≤ n → 1 ≤ h →
    39 ∀ (state : State n) (a : Fin n → ℤ),
    40 (∀ i j, height (state.1 i j) h) →
    41 (∀ i, height (rationalNormal a i) h) → (∀ i, height (state.2 i) h) →
    42 0 < rationalNormal a ⬝ᵥ (state.1 *ᵥ rationalNormal a) →
    43 ∀ w : ℕ, c * (n + h + k + 1) ^ 12 ≤ w →
    44 ∃ t ≤ c * (n + h + k + 1) ^ 12, Lax808846.Ram.RunsTo w p
    45 (encodeInput k state a) (encodeOutput (update k state a)) t
    46
    47end Lax263307.NativeRoundedStep
    48
    Show Proof
    Formalization notes

    This statement concerns actual Lax808846.Ram.RunsToLax808846.Ram.RunsTo. The proof compiles the registered LP submission's complete rational ellipsoid update, adding the input reader and canonical output writer. It is one subroutine of the recursive QPTAS; it does not assert that the complete QPTAS program exists.

    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…