Lax Lean Archive

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

A bounded rounded ellipsoid search with answer-or-cut replies

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

    An oracle returns an answer, a certified rejection, or a nonzero integer central-cut normal. The search stores a rational matrix and center, advances them once per cut, and stops after an explicit finite iteration budget. When rejection is impossible and every cut preserves a fixed dyadic cube around a scaled unit-cube point, the search must return an answer.

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

    This concept declares 4 statements. Each proof establishes one of them relative to its assumptions.

    1 center_encoding_bound proven

    2 search_complete proven

    3 search_sound proven

    4 shape_encoding_bound proven

    Lean source view on GitHub

    1import Lax263307.BufferedEllipsoid
    2import Lax109476.RationalEncoding
    3import Mathlib.Data.Rat.Floor
    4import Mathlib.Data.Nat.Sqrt
    5import Mathlib.Data.Nat.Size
    6
    7/-!
    8---
    9title: A bounded rounded ellipsoid search with answer-or-cut replies
    10type: theorem
    11---
    12An oracle returns an answer, a certified rejection, or a nonzero integer
    13central-cut normal. The search stores a rational matrix and center, advances
    14them once per cut, and stops after an explicit finite iteration budget.
    15When rejection is impossible and every cut preserves a fixed dyadic cube
    16around a scaled unit-cube point, the search must return an answer.
    17
    18# Formalization notes
    19
    20The computable rational update is the registered LP ellipsoid update,
    21written explicitly so that definitions and statement types do not import
    22a proof package. The proof identifies its trajectory with the registered
    23sequence and applies that sequence's determinant and containment theorems.
    24This is a functional search; its oracle and RAM refinements are separate
    25implementation obligations.
    26-/
    27
    28namespace Lax263307.RoundedOracleSearch
    29
    30open Matrix
    31
    32abbrev State (n : ℕ) := Matrix (Fin n) (Fin n) ℚ × (Fin n → ℚ)
    33
    34inductive Reply (n : ℕ) (Result : Type)
    35 | found (answer : Result)
    36 | reject
    37 | cut (normal : Fin n → ℤ)
    38
    39def rationalNormal {n : ℕ} (a : Fin n → ℤ) : Fin n → ℚ := fun i => a i
    40
    41def roundDown (q : ℚ) (D : ℕ) : ℚ := (Int.floor (q * D) : ℚ) / D
    42
    43def sqrtUpper (q : ℚ) (D : ℕ) : ℚ :=
    44 ((Nat.sqrt (Nat.ceil (q * (D : ℚ) ^ 2)) + 1 : ℕ) : ℚ) / D
    45
    46def cutShape {n : ℕ} (A : Matrix (Fin n) (Fin n) ℚ) (a : Fin n → ℚ) :
    47 Matrix (Fin n) (Fin n) ℚ :=
    48 ((n : ℚ) ^ 2 / ((n : ℚ) ^ 2 - 1)) •
    49 (A - (2 / (((n : ℚ) + 1) * (a ⬝ᵥ (A *ᵥ a)))) •
    50 Matrix.vecMulVec (A *ᵥ a) (A *ᵥ a))
    51
    52def grid (n k : ℕ) : ℕ := 2 ^ ((2 * k + 2) + (2 * n + 4) + n + 3)
    53
    54def cached {n : ℕ} (state : State n) : State n :=
    55 let rows : Vector (Vector ℚ n) n := Vector.ofFn (fun i => Vector.ofFn (state.1 i))
    56 let center : Vector ℚ n := Vector.ofFn state.2
    57 ((fun i j => (rows.get i).get j), fun i => center.get i)
    58
    59def update {n : ℕ} (k : ℕ) (state : State n) (a : Fin n → ℤ) : State n :=
    60 let a := rationalNormal a
    61 let D := grid n k
    62 let η : ℚ := 1 / (2 : ℚ) ^ (2 * n + 4)
    63 let shape := ((1 + η) ^ 2) •
    64 ((Matrix.of fun i j => roundDown (cutShape state.1 a i j) D) + ((n : ℚ) / D) • 1)
    65 let center := fun i => roundDown
    66 (state.2 i - (1 / (((n : ℚ) + 1) * sqrtUpper (a ⬝ᵥ (state.1 *ᵥ a)) D)) *
    67 (state.1 *ᵥ a) i) D
    68 cached (shape, center)
    69
    70def fallback {n : ℕ} : Fin n → ℤ := fun i => if i.val = 0 then 1 else 0
    71
    72def selectedNormal {n : ℕ} {Result : Type} : Reply n Result → Fin n → ℤ
    73 | .cut a => a
    74 | _ => fallback
    75
    76def trajectory {n : ℕ} {Result : Type} (oracle : ℕ → (Fin n → ℚ) → Reply n Result) :
    77 ℕ → State n
    78 | 0 => (1, 0)
    79 | k + 1 =>
    80 let old := trajectory oracle k
    81 update k old (selectedNormal (oracle k old.2))
    82
    83def normalSchedule {n : ℕ} {Result : Type}
    84 (oracle : ℕ → (Fin n → ℚ) → Reply n Result) (k : ℕ) : Fin n → ℤ :=
    85 selectedNormal (oracle k (trajectory oracle k).2)
    86
    87def scan {n : ℕ} {Result : Type} (oracle : ℕ → (Fin n → ℚ) → Reply n Result) :
    88 ℕ → ℕ → State n → Option Result
    89 | _, 0, _ => none
    90 | k, count + 1, state =>
    91 match oracle k state.2 with
    92 | .found answer => some answer
    93 | .reject => none
    94 | .cut a => scan oracle (k + 1) count (update k state a)
    95
    96def steps (n B : ℕ) : ℕ := 4 * (n + 1) * (B * n + 1)
    97
    98def search {n : ℕ} {Result : Type} (oracle : ℕ → (Fin n → ℚ) → Reply n Result)
    99 (B : ℕ) : Option Result := scan oracle 0 (steps n B) (1, 0)
    100
    101axiom search_sound {n : ℕ} {Result : Type}
    102 (oracle : ℕ → (Fin n → ℚ) → Reply n Result) (B : ℕ) (Good : Result → Prop)
    103 (answers : ∀ k center answer, oracle k center = .found answer → Good answer) :
    104 ∀ answer, search oracle B = some answer → Good answer
    105
    106axiom search_complete {n : ℕ} {Result : Type} (dimension : 2 ≤ n)
    107 (oracle : ℕ → (Fin n → ℚ) → Reply n Result) (B : ℕ) (precision : 2 ≤ B)
    108 (nonzero : ∀ k center a, oracle k center = .cut a → ∃ i, a i ≠ 0)
    109 (no_reject : ∀ k center, oracle k center ≠ .reject)
    110 (z : Fin n → ℝ) (cube : ∀ i, 0 ≤ z i ∧ z i ≤ 1)
    111 (retains : ∀ k center a, oracle k center = .cut a →
    112 ∀ e : Fin n → ℝ, (∀ i, |e i| ≤ ((2 : ℝ) ^ B)⁻¹) →
    113 (fun i => (a i : ℝ)) ⬝ᵥ
    114 (Lax263307.BufferedEllipsoid.scale z + e - (fun i => (center i : ℝ))) ≤ 0) :
    115 ∃ answer, search oracle B = some answer
    116
    117axiom center_encoding_bound {n : ℕ} {Result : Type} (dimension : 2 ≤ n)
    118 (oracle : ℕ → (Fin n → ℚ) → Reply n Result)
    119 (nonzero : ∀ k center a, oracle k center = .cut a → ∃ i, a i ≠ 0) (k : ℕ) (i : Fin n) :
    120 Lax759944.BinaryWordEncoding.bitSize
    121 (Lax109476.RationalEncoding.encodeRational ((trajectory oracle k).2 i)) ≤ 60 + 6 * k + 14 * n
    122
    123axiom shape_encoding_bound {n : ℕ} {Result : Type} (dimension : 2 ≤ n)
    124 (oracle : ℕ → (Fin n → ℚ) → Reply n Result)
    125 (nonzero : ∀ k center a, oracle k center = .cut a → ∃ i, a i ≠ 0)
    126 (k : ℕ) (i j : Fin n) :
    127 Lax759944.BinaryWordEncoding.bitSize
    128 (Lax109476.RationalEncoding.encodeRational ((trajectory oracle k).1 i j)) ≤ 60 + 6 * k + 14 * n
    129
    130end Lax263307.RoundedOracleSearch
    131
    Show ProofShow ProofShow ProofShow Proof
    Formalization notes

    The computable rational update is the registered LP ellipsoid update, written explicitly so that definitions and statement types do not import a proof package. The proof identifies its trajectory with the registered sequence and applies that sequence's determinant and containment theorems. This is a functional search; its oracle and RAM refinements are separate implementation obligations.

    Builds on
    Used by
    From Mathlib

    Discussion

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

    Loading discussion…