Thin matrix products and persistent entry queries

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

definition

Loading review…

Natural Language Statement

Definition

Two integer matrices have dimensions $N\times D$ and $D\times N$ , and entries bounded in absolute value by $U$ . Wanted output positions are a list without repetitions. The data-structure specification bounds preprocessing time and the extent of retained memory, then requires correctness for every finite sequence of entry queries.

Concept map

4 concepts; 7 descendants hidden

100%

Proven claimDefinitionThis conceptRelated conceptA → B: B builds on A

Lean source view on GitHub

Show types on hover

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 Mathlib.Algebra.MvPolynomial.Basic
15	import Mathlib.Analysis.SpecialFunctions.Log.Base
16	import Mathlib.Analysis.SpecialFunctions.Log.Basic
17	import Mathlib.Analysis.SpecialFunctions.Pow.Real
18	import Mathlib.Combinatorics.SimpleGraph.Basic
19	import Mathlib.Data.Finset.Sort
20	import Mathlib.LinearAlgebra.Matrix.Notation
21	import Mathlib.MeasureTheory.Integral.Bochner.Basic
22	import Mathlib.NumberTheory.PrimeCounting
23	import Mathlib.Probability.Independence.Basic
24	import Mathlib.Tactic.DeriveFintype
25	import Lax350013.RAMResources
26
27	/-!
28	---
29	title: Thin matrix products and persistent entry queries
30	type: definition
31	---
32	Two integer matrices have dimensions $N\times D$ and $D\times N$ , and entries bounded in absolute value by $U$ . Wanted output positions are a list without repetitions. The data-structure specification bounds preprocessing time and the extent of retained memory, then requires correctness for every finite sequence of entry queries.
33	-/
34
35	namespace Lax350013.ThinMatrices
36
37	open Finset
38	open Lax350013.WordRAM
39	open Lax350013.RAMResources
40
41	/-- A matrix written row by row. -/
42	def rowMajor {n m : ℕ} (A : Fin n → Fin m → ℤ) : List ℤ :=
43	(List.finRange n).flatMap fun i => (List.finRange m).map fun j => A i j
44
45	/-- A Boolean as a number. -/
46	def bit (p : Bool) : ℤ := if p then 1 else 0
47
48	/-- Two matrices `X ∈ ℤ^{N×D}` and `Y ∈ ℤ^{D×N}` with entries of absolute value at most `U`. -/
49	structure ThinPair where
50	/-- The long side. -/
51	N : ℕ
52	/-- The short side. -/
53	D : ℕ
54	/-- The bound on the absolute values of the entries. -/
55	U : ℕ
56	/-- The first matrix. -/
57	X : Matrix (Fin N) (Fin D) ℤ
58	/-- The second matrix. -/
59	Y : Matrix (Fin D) (Fin N) ℤ
60	/-- The entries of `X` are bounded. -/
61	boundX : ∀ i j, \|X i j\| ≤ (U : ℤ)
62	/-- The entries of `Y` are bounded. -/
63	boundY : ∀ i j, \|Y i j\| ≤ (U : ℤ)
64
65	/-- Theorem 5: two such matrices and "a set W of [...] positions of an N × N matrix".
66
67	NOTE. The paper does not say how a set is given. Here it is a list without repetitions, in any
68	order. -/
69	structure ThinInstance extends ThinPair where
70	/-- The wanted positions. -/
71	W : List (Fin N × Fin N)
72	/-- No position is listed twice. -/
73	nodup : W.Nodup
74
75	/-- The input of the matrix problems: `N`, `D`, `\|W\|`, then further parameters `extra` (none, except
76	in Theorem 30), then `X`, then `Y`, then the rows `I` of the wanted positions, then their columns
77	`J`. -/
78	def ThinInstance.input (x : ThinInstance) (extra : List ℤ) : List ℤ :=
79	[(x.N : ℤ), (x.D : ℤ), (x.W.length : ℤ)] ++ extra ++ rowMajor x.X ++ rowMajor x.Y ++
80	x.W.map (fun q => (q.1.val : ℤ)) ++ x.W.map (fun q => (q.2.val : ℤ))
81
82	/-- The wanted entries of a thin matrix product (Theorem 5): accept, and leave `(XY)[I,J]` for
83	the `i`-th wanted position `(I,J)` in the `i`-th output cell. -/
84	def thinProduct (extra : List ℤ) : Problem where
85	Inst := ThinInstance
86	params x := [x.N, x.D]
87	input x := x.input extra
88	IsAnswer x verdict out :=
89	verdict = true ∧ ∀ (i : ℕ) (h : i < x.W.length), out i = (x.X * x.Y) x.W[i].1 x.W[i].2
90
91	/-- The input of the preprocessing: `N`, `D`, further parameters `extra` (none, except in
92	Theorem 30), then `X`, then `Y`. The list `extra` is fixed before the instance. -/
93	def ThinPair.input (x : ThinPair) (extra : List ℤ) : List ℤ :=
94	[(x.N : ℤ), (x.D : ℤ)] ++ extra ++ rowMajor x.X ++ rowMajor x.Y
95
96	/-- A data structure for the entries of a thin matrix product (Theorem 30, Corollary 26): "After
97	preprocessing X and Y [...], the data structure answers a query for any single entry of XY, not
98	known in advance" (Section 4).
99
100	`P` is the preprocessing program, `Q` the query program, `qI`, `qJ`, `qOut` the three cells through
101	which queries are put and answered; all of them, and the slope `b`, are fixed before the instance.
102	On every instance in `dom` and at every admissible word size:
103
104	* time: the preprocessing accepts within `Tp x` steps;
105	* space: it leaves unchanged every cell `a` with `a < -Sp x` or `a > len + Sp x`, where the input
106	occupies the cells 0 to `len - 1` (so the cells of the input are not counted);
107	* queries: then every sequence of queries `(I, J)` with `I, J < N` is served, each query within
108	`Tq x` steps. A query starts on the memory left behind; nothing is reset for it.
109
110	NOTE. The paper says "time and space" and does not define space. Here space is the extent of the
111	memory in which the preprocessing leaves the data structure, not the number of cells written, which
112	is at most the time anyway; a structure that is scattered over a large range of addresses does not
113	count as small. Cells that the preprocessing restores, and cells that the queries write, are not
114	constrained. -/
115	def IsDataStructure (P Q : List Instr) (qI qJ qOut : ℤ) (b : ℕ) (extra : List ℤ)
116	(dom : ThinPair → Prop) (Tp Sp Tq : ThinPair → ℝ) : Prop :=
117	∀ x : ThinPair, dom x → ∀ bits : ℕ, Admissible b [x.N, x.D] bits →
118	∃ (tp tq : ℕ) (c : ℤ → BitVec bits), (tp : ℝ) ≤ Tp x ∧ (tq : ℝ) ≤ Tq x ∧
119	exec P tp 0 (loadWords bits (x.input extra)) = some (true, c) ∧
120	(∀ a : ℤ, ((a : ℝ) < -Sp x ∨ ((x.input extra).length : ℝ) + Sp x < (a : ℝ)) →
121	c a = loadWords bits (x.input extra) a) ∧
122	∀ queries : List (ℕ × ℕ), (∀ q ∈ queries, q.1 < x.N ∧ q.2 < x.N) →
123	Serves Q qI qJ qOut tq
124	(fun I J => if h : I < x.N ∧ J < x.N then (x.X * x.Y) ⟨I, h.1⟩ ⟨J, h.2⟩ else 0) c queries
125
126	end Lax350013.ThinMatrices
127

Builds on

Lax350013.RAMResources

Used by

From Mathlib

Discussion

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

Loading discussion…

Lax Lean Archive

Thin matrix products and persistent entry queries

Flags

Flag this concept

Natural Language Statement

Definition

Lean source view on GitHub

Discussion

Settings

Your comments