Lax Lean Archive

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

Time bounds, persistent queries and phased inputs

Lax350013.RAMResources · concepts/Lax350013/RAMResources.lean · lax-350013

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

    The word-RAM resource conventions for problems with several size parameters, real exponents, logarithmic factors, persistent data structures and inputs revealed in phases. Programs are fixed before the instance. Queries retain the memory left by earlier queries; a phase cannot inspect the input of a later phase.

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

    Lean source view on GitHub

    1/-
    2Copyright (c) 2026 Anthropic, PBC. All rights reserved.
    3Released under Apache 2.0 license as described in the file LICENSE.
    4SPDX-License-Identifier: Apache-2.0
    5-/
    6/-
    7Modified for the independent Lax packaging by Édouard Bonnet, 2026.
    8Derived from 3sum-apsp/EndStatement.lean / PaperStatements.lean at upstream commit e1a4e6508154ea59f030480661590a9fe3018011.
    9Changes: Lax module/namespace layout, separated concepts and proofs, archive
    10annotations, and compatibility with the archive Lean/mathlib environment.
    11See NOTICE and README.md in the submission root for provenance and scope.
    12-/
    13
    14import Mathlib.Algebra.MvPolynomial.Basic
    15import Mathlib.Analysis.SpecialFunctions.Log.Base
    16import Mathlib.Analysis.SpecialFunctions.Log.Basic
    17import Mathlib.Analysis.SpecialFunctions.Pow.Real
    18import Mathlib.Combinatorics.SimpleGraph.Basic
    19import Mathlib.Data.Finset.Sort
    20import Mathlib.LinearAlgebra.Matrix.Notation
    21import Mathlib.MeasureTheory.Integral.Bochner.Basic
    22import Mathlib.NumberTheory.PrimeCounting
    23import Mathlib.Probability.Independence.Basic
    24import Mathlib.Tactic.DeriveFintype
    25import Lax350013.PolynomialTime
    26
    27/-!
    28---
    29title: Time bounds, persistent queries and phased inputs
    30type: definition
    31---
    32The word-RAM resource conventions for problems with several size parameters, real exponents, logarithmic factors, persistent data structures and inputs revealed in phases. Programs are fixed before the instance. Queries retain the memory left by earlier queries; a phase cannot inspect the input of a later phase.
    33-/
    34
    35namespace Lax350013.RAMResources
    36
    37open Finset
    38open Lax350013.WordRAM
    39
    40/-- The word size `W` is admissible against the slope `b` for an input with the parameters `params`
    41(its sizes): `W` is at least `b · (⌊log₂ p₁⌋ + ⌊log₂ p₂⌋ + … + 1)`. If every parameter is at most a
    42fixed power of the size `n`, the smallest admissible word size is a constant times `log n`: "O(log
    43n)-bit words". A statement fixes only the slope `b`, together with the program, and the program has
    44to work, within the same bound on the number of steps, at every admissible word size. -/
    45def Admissible (b : Nat) (params : List Nat) (W : Nat) : Prop :=
    46 b * ((params.map Nat.log2).sum + 1) ≤ W
    47
    48/-- The output of a function problem: the cells right after the input, read as signed words.
    49`output c len i` is the number in the `i`-th cell of the memory `c` after an input of `len`
    50cells. -/
    51def output {W : Nat} (c : Int → BitVec W) (len : Nat) (i : Nat) : Int :=
    52 (c ((len : Int) + (i : Int))).toInt
    53
    54/-- A computational problem on the word RAM. -/
    55structure Problem where
    56 /-- The instances. -/
    57 Inst : Type
    58 /-- The parameters of an instance on which the word size depends: its sizes. -/
    59 params : Inst → List ℕ
    60 /-- The input: the numbers written into the cells 0, 1, 2, … -/
    61 input : Inst → List ℤ
    62 /-- `IsAnswer x verdict out`: the verdict, and the numbers `out 0, out 1, …` in the cells right
    63 after the input, are a correct answer to the instance `x`. -/
    64 IsAnswer : Inst → Bool → (ℕ → ℤ) → Prop
    65
    66/-- **Solving a problem within a time bound.** The program `P` with slope `b` solves the problem on
    67the instances in `dom` within time `T`: on every such instance `x` and at every admissible word size
    68`bits`, the run from the first instruction on the starting memory (input in the cells 0, 1, 2, …,
    69zeros elsewhere) gives a verdict after at most `T x` steps, and the verdict and the output are a
    70correct answer. -/
    71def Solves (prob : Problem) (P : List Instr) (b : ℕ) (dom : prob.Inst → Prop) (T : prob.Inst → ℝ) :
    72 Prop :=
    73 ∀ x : prob.Inst, dom x → ∀ bits : ℕ, Admissible b (prob.params x) bits →
    74 ∃ (t : ℕ) (verdict : Bool) (c : ℤ → BitVec bits), (t : ℝ) ≤ T x ∧
    75 exec P t 0 (loadWords bits (prob.input x)) = some (verdict, c) ∧
    76 prob.IsAnswer x verdict (output c (prob.input x).length)
    77
    78/-- The program `P` with slope `b` solves the problem `Q` within `T(n)` steps when all numbers are
    79integers of absolute value at most `n^κ`. This is what `Lax350013.PolynomialTime.Problem.SolvedInTime` asks of
    80the runs of `P`, for a real bound `T`: on every such instance, of any size `n`, and at every word
    81size of at least `b (⌊log₂ n⌋ + 1)` bits, `P` halts within `T(n)` steps with the right verdict and
    82output (`Lax350013.PolynomialTime.Problem.SolvedBy`).
    83
    84NOTE. As in `Lax350013.PolynomialTime.Problem.SolvedInTime`, the bound speaks of every number of the input
    85list. Where the input contains an adjacency matrix, its entries 1 count too; `n^κ` is at least 1 as
    86soon as there is a vertex. -/
    87def SolvesWithin (Q : Lax350013.PolynomialTime.Problem) (κ : ℕ) (P : List Instr) (b : ℕ) (T : ℕ → ℝ) : Prop :=
    88 ∀ (n : ℕ) (x : Q.Instance n), (∀ a ∈ Q.input x, a.natAbs ≤ n ^ κ) → ∀ W ≥ b * (Nat.log2 n + 1),
    89 ∃ t : ℕ, (t : ℝ) ≤ T n ∧ Q.SolvedBy x P W t
    90
    91/-- The problem `Q`, a value of `Lax350013.PolynomialTime.Problem`, is solved by a deterministic algorithm in
    92`O(n^a (log n)^e)` time when all numbers are integers of absolute value at most `n^κ`: there are a
    93program, a slope and a constant `C` such that the program solves `Q` within `C (n^a (log n)^e + 1)`
    94steps. (For `a ≥ 0` the `+ 1` matters only at `n ≤ 1`, where `n^a (log n)^e` may be 0.) -/
    95def SolvedInTimeAt (Q : Lax350013.PolynomialTime.Problem) (κ : ℕ) (a : ℝ) (e : ℕ) : Prop :=
    96 ∃ (P : List Instr) (b : ℕ) (C : ℝ),
    97 SolvesWithin Q κ P b fun n => C * ((n : ℝ) ^ a * Real.log n ^ e + 1)
    98
    99/-- The same for every constant `κ`: "all numbers in the input are integers of absolute value
    100n^{O(1)}" (Theorem 2). The program, the slope and the constant may depend on `κ`.
    101
    102NOTE. `κ` is the paper's ν. Where the paper has ν ≥ 1 (Theorem 19, Corollary 39), `κ = 0` is
    103included here. -/
    104def SolvedInTime (Q : Lax350013.PolynomialTime.Problem) (a : ℝ) (e : ℕ) : Prop :=
    105 ∀ κ : ℕ, SolvedInTimeAt Q κ a e
    106
    107/-- The same in `O(n^a (log n)^{O(1)})` time, which Theorem 22 writes Õ(n^a).
    108
    109NOTE. The exponent of the logarithm may depend on `κ` too: this is the weaker reading of the
    110Õ of Theorem 22. -/
    111def SolvedInPolylogTime (Q : Lax350013.PolynomialTime.Problem) (a : ℝ) : Prop :=
    112 ∀ κ : ℕ, ∃ e : ℕ, SolvedInTimeAt Q κ a e
    113
    114/-- The problem `Q` is solved by a deterministic algorithm in `n^{a+o(1)}` time when all numbers are
    115integers of absolute value at most `n^κ`, for every constant `κ`: as `SolvedInTime`, with the bound
    116`C (n^{a+o(n)} + 1)` for a function `o` that tends to 0. The program, the slope, the constant and
    117the function may depend on `κ`. (The constant is needed at `n ≤ 1`, where `n^{a+o(n)}` is 0 or 1;
    118the `+ 1` keeps the form of `SolvedInTimeAt`. For `a < 0` the bound means `O(1)`.) -/
    119def SolvedInLittleOTime (Q : Lax350013.PolynomialTime.Problem) (a : ℝ) : Prop :=
    120 ∀ κ : ℕ, ∃ (P : List Instr) (b : ℕ) (C : ℝ) (o : ℕ → ℝ), Filter.Tendsto o Filter.atTop (nhds 0) ∧
    121 SolvesWithin Q κ P b fun n => C * ((n : ℝ) ^ (a + o n) + 1)
    122
    123/-- The memory on which a query starts: the memory `c`, left behind by the preprocessing or by the
    124previous query, with the row `I` and the column `J` written into the two query cells `qI` and
    125`qJ`. -/
    126def withQuery {bits : ℕ} (c : ℤ → BitVec bits) (qI qJ : ℤ) (I J : ℕ) : ℤ → BitVec bits :=
    127 fun a => if a = qI then BitVec.ofInt bits I else if a = qJ then BitVec.ofInt bits J else c a
    128
    129/-- The query program `Q` serves the queries of the list one after the other, starting from the
    130memory `c`: each run starts at the first instruction, accepts within `tq` steps and leaves the right
    131entry in the cell `qOut`; the next query starts from the memory that this run leaves. -/
    132def Serves {bits : ℕ} (Q : List Instr) (qI qJ qOut : ℤ) (tq : ℕ) (entry : ℕ → ℕ → ℤ) :
    133 (ℤ → BitVec bits) → List (ℕ × ℕ) → Prop
    134 | _, [] => True
    135 | c, q :: rest =>
    136 ∃ c' : ℤ → BitVec bits, exec Q tq 0 (withQuery c qI qJ q.1 q.2) = some (true, c') ∧
    137 (c' qOut).toInt = entry q.1 q.2 ∧ Serves Q qI qJ qOut tq entry c' rest
    138
    139/-- The memory on which a phase starts: the memory `c` with the list `ws` written into the cells
    140`off, off + 1, …`. -/
    141def withInput {bits : ℕ} (c : ℤ → BitVec bits) (off : ℕ) (ws : List ℤ) : ℤ → BitVec bits :=
    142 fun a =>
    143 if (off : ℤ) ≤ a ∧ a < (off : ℤ) + (ws.length : ℤ) then
    144 BitVec.ofInt bits (ws.getD (a - (off : ℤ)).toNat 0)
    145 else c a
    146
    147/-- The phases of the list, each given by its program, its input and a number of steps, run one
    148after the other from the memory `c`: every phase starts at its first instruction and accepts within
    149its number of steps, the inputs are written one after the other from the cell `off` on, and the last
    150memory, with the address of the first cell after the last input, satisfies `good`.
    151-/
    152def RunsPhases {bits : ℕ} (good : (ℤ → BitVec bits) → ℕ → Prop) :
    153 (ℤ → BitVec bits) → ℕ → List (List Instr × List ℤ × ℕ) → Prop
    154 | c, off, [] => good c off
    155 | c, off, (P, ws, s) :: rest =>
    156 ∃ c' : ℤ → BitVec bits, exec P s 0 (withInput c off ws) = some (true, c') ∧
    157 RunsPhases good c' (off + ws.length) rest
    158
    159/-- A number `s` of steps is `O(n^a)` with the constant `C`: `s ≤ C (n^a + 1)`. For `n ≥ 1` and
    160`a ≥ 0` the `+ 1` only changes the constant; for `a < 0` the bound means `O(1)`. -/
    161def Within (s : ℕ) (C : ℝ) (n : ℕ) (a : ℝ) : Prop := (s : ℝ) ≤ C * ((n : ℝ) ^ a + 1)
    162
    163end Lax350013.RAMResources
    164
    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…