Uniform polynomial time on the word RAM
Lax350013.PolynomialTime · concepts/Lax350013/PolynomialTime.lean · lax-350013
No public endorsements yet.
Loading review…
Sign in with ORCIDNatural Language Statement
Definition
For each fixed input-magnitude exponent , one program, one word-size coefficient and one time bound work for every input size and every admissible word size. The input integers have absolute value at most and the words have at least bits. The verdict and the output cells must both be correct. Rational exponents are expressed using integer powers.
Concept map
Lean source view on GitHub
| 1 | /- |
| 2 | Copyright (c) 2026 Anthropic, PBC. All rights reserved. |
| 3 | Released under Apache 2.0 license as described in the file LICENSE. |
| 4 | SPDX-License-Identifier: Apache-2.0 |
| 5 | -/ |
| 6 | /- |
| 7 | Modified for the independent Lax packaging by Édouard Bonnet, 2026. |
| 8 | Derived from 3sum-apsp/EndStatement.lean / PaperStatements.lean at upstream commit e1a4e6508154ea59f030480661590a9fe3018011. |
| 9 | Changes: Lax module/namespace layout, separated concepts and proofs, archive |
| 10 | annotations, and compatibility with the archive Lean/mathlib environment. |
| 11 | See NOTICE and README.md in the submission root for provenance and scope. |
| 12 | -/ |
| 13 | |
| 14 | import Lax350013.WordRAM |
| 15 | |
| 16 | /-! |
| 17 | --- |
| 18 | title: Uniform polynomial time on the word RAM |
| 19 | type: definition |
| 20 | --- |
| 21 | For each fixed input-magnitude exponent , one program, one word-size coefficient and one time bound work for every input size and every admissible word size. The input integers have absolute value at most and the words have at least bits. The verdict and the output cells must both be correct. Rational exponents are expressed using integer powers. |
| 22 | -/ |
| 23 | |
| 24 | namespace Lax350013.PolynomialTime |
| 25 | |
| 26 | open Lax350013.WordRAM |
| 27 | |
| 28 | /-- `T(n) = O(n^r)`, both sides raised to the power `r.den`: core Lean has no fractional powers. For `r = 1.9992 = |
| 29 | 2499/1250` it says `T(n)^1250 ≤ K n^2499`. -/ |
| 30 | def BigO (T : Nat → Nat) (r : Rat) : Prop := |
| 31 | ∃ K : Nat, ∀ n ≥ 2, T n ^ r.den ≤ K * n ^ r.num.toNat |
| 32 | |
| 33 | /-- `yes`: when to accept (always, if not given). `output`: a condition on the cells after the input, read as signed. -/ |
| 34 | structure Problem where |
| 35 | Instance : Nat → Type |
| 36 | input {n : Nat} : Instance n → List Int |
| 37 | yes {n : Nat} : Instance n → Prop := fun _ => True |
| 38 | output {n : Nat} : Instance n → (Nat → Int) → Prop := fun _ _ => True |
| 39 | |
| 40 | /-- One run: with `n` in cell 0 and the input after it, `P` halts within `t` steps with the right verdict and output. -/ |
| 41 | def Problem.SolvedBy (Q : Problem) {n : Nat} (x : Q.Instance n) (P : List Instr) (W t : Nat) : Prop := |
| 42 | ∃ verdict m, exec P t 0 (loadWords W ((n : Int) :: Q.input x)) = some (verdict, m) ∧ |
| 43 | (verdict = true ↔ Q.yes x) ∧ Q.output x fun a => (m (1 + (Q.input x).length + a : Nat)).toInt |
| 44 | |
| 45 | /-- Theorem 2: «a word RAM with O(log n)-bit words», «all numbers in the input are integers of absolute value |
| 46 | n^O(1)»: for every `κ`, one `P`, `b`, `T` for all instances, correct at every `W ≥ b(⌊log₂ n⌋ + 1)`. -/ |
| 47 | def Problem.SolvedInTime (Q : Problem) (r : Rat) : Prop := |
| 48 | ∀ κ : Nat, ∃ (P : List Instr) (b : Nat) (T : Nat → Nat), BigO T r ∧ |
| 49 | ∀ (n : Nat) (x : Q.Instance n), (∀ a ∈ Q.input x, a.natAbs ≤ n ^ κ) → ∀ W ≥ b * (Nat.log2 n + 1), |
| 50 | Q.SolvedBy x P W (T n) |
| 51 | |
| 52 | def rowByRow {n : Nat} (w : Fin n → Fin n → Int) : List Int := |
| 53 | (List.ofFn fun u => List.ofFn fun v => w u v).flatten |
| 54 | |
| 55 | end Lax350013.PolynomialTime |
| 56 |
Discussion
Ask a question or add context. Endorsements and structured flags are kept in the review panel above.
0 comments