Calling conventions for matrix and graph algorithms

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

definition

Loading review…

Natural Language Statement

Definition

Concrete memory layouts and input/output contracts for thin matrix products, lopsided triangle counting and detection, Exact and Negative Triangle, 3SUM, min-plus products, and APSP. Solvers preserve the caller’s other memory and may be reused on successive inputs.

Concept map

6 concepts; 6 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/PaperStatements.lean / ThreeSumApsp/Programs/Tasks.lean / Spec/Sec3/Problems.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.ProcedureContracts
26	import Lax350013.ThreeSUM
27
28	/-!
29	---
30	title: Calling conventions for matrix and graph algorithms
31	type: definition
32	---
33	Concrete memory layouts and input/output contracts for thin matrix products, lopsided triangle counting and detection, Exact and Negative Triangle, 3SUM, min-plus products, and APSP. Solvers preserve the caller’s other memory and may be reused on successive inputs.
34	-/
35
36	namespace Lax350013.CallableProblems
37
38	open Finset
39	open Lax350013.StructuredPrograms
40	open Lax350013.ProcedureContracts
41
42	/-- Section 3.2: "An instance of Exact Triangle [...] consists of a complete tripartite graph on
43	vertex parts A, B, C of n vertices each, and an integer weight w(e) on every edge". The three
44	fields are the weights `w(a,b)`, `w(b,c)` and `w(a,c)`. The type `R` of the weights is `ℤ` in
45	Section 3; Section 5 also uses real weights. The bound on the weights is a separate predicate
46	(`WeightsBoundedBy`, `WeightsPolyBounded`). -/
47	structure TriangleInstance (R : Type) (n : ℕ) where
48	/-- `wAB a b` is the weight `w(a,b)` of the edge between `a ∈ A` and `b ∈ B`. -/
49	wAB : Fin n → Fin n → R
50	/-- `wBC b c` is the weight `w(b,c)` of the edge between `b ∈ B` and `c ∈ C`. -/
51	wBC : Fin n → Fin n → R
52	/-- `wAC a c` is the weight `w(a,c)` of the edge between `a ∈ A` and `c ∈ C`. -/
53	wAC : Fin n → Fin n → R
54
55	namespace TriangleInstance
56
57	/-- Section 3.2: "Let S(a,b,c) := w(a,b) + w(b,c) + w(a,c)." -/
58	def S {R : Type} [Add R] {n : ℕ} (T : TriangleInstance R n) (a b c : Fin n) : R :=
59	T.wAB a b + T.wBC b c + T.wAC a c
60
61	/-- Section 3.2: "A zero triangle is a triangle (a,b,c) ∈ A × B × C with S(a,b,c) = 0". -/
62	def IsZeroTriangle {R : Type} [Add R] [Zero R] {n : ℕ} (T : TriangleInstance R n) (a b c : Fin n) :
63	Prop :=
64	T.S a b c = 0
65
66	/-- Section 3.2: "the task is to decide whether one exists". -/
67	def HasZeroTriangle {R : Type} [Add R] [Zero R] {n : ℕ} (T : TriangleInstance R n) : Prop :=
68	∃ a b c : Fin n, T.IsZeroTriangle a b c
69
70	end TriangleInstance
71
72	/-- Negative Triangle, Section 1.2: "asks whether an edge-weighted graph has a triangle of
73	negative total weight". The instances here are those of Exact Triangle. -/
74	def TriangleInstance.HasNegativeTriangle {R : Type} [Add R] [Zero R] [LT R] {n : ℕ}
75	(T : TriangleInstance R n) : Prop :=
76	∃ a b c : Fin n, T.S a b c < 0
77
78	/-- Convolution-3SUM, Section 1.2: "do x₀, …, x_{n−1} satisfy x_i + x_j = x_{i+j} for some
79	i, j?" -/
80	def Convolution3SUM {R : Type} [Add R] {N : ℕ} (x : Fin N → R) : Prop :=
81	∃ (i j : Fin N) (h : i.val + j.val < N), x i + x j = x ⟨i.val + j.val, h⟩
82
83	/-- The vertex at which the walk that starts at `i` and then visits `rest` ends. -/
84	def walkEnd {n : ℕ} : Fin n → List (Fin n) → Fin n
85	\| i, [] => i
86	\| _, j :: rest => walkEnd j rest
87
88	/-- The total weight of the walk that starts at `i` and then visits `rest`; it is `⊤` if one of its
89	edges is missing, and the empty walk has weight 0. -/
90	def walkWeight {R : Type} [Add R] [Zero R] {n : ℕ} (w : Fin n → Fin n → WithTop R) :
91	Fin n → List (Fin n) → WithTop R
92	\| _, [] => 0
93	\| i, j :: rest => w i j + walkWeight w j rest
94
95	/-- Section 1 and Theorems 21 and 22: "no negative cycles". Stated for closed walks, which is the
96	same thing: a closed walk decomposes into cycles. -/
97	def NoNegativeCycle {R : Type} [Add R] [Zero R] [LE R] {n : ℕ} (w : Fin n → Fin n → WithTop R) :
98	Prop :=
99	∀ (i : Fin n) (rest : List (Fin n)), walkEnd i rest = i → 0 ≤ walkWeight w i rest
100
101	/-- APSP, Section 1: "compute the shortest-path distance between every pair of vertices". `d i
102	j` is the least weight of a walk from `i` to `j`, and `⊤` if `j` cannot be reached from `i`. -/
103	def IsDistanceMatrix {R : Type} [Add R] [Zero R] [Preorder R] {n : ℕ}
104	(w : Fin n → Fin n → WithTop R) (d : Fin n → Fin n → WithTop R) : Prop :=
105	∀ i j, IsLeast {x \| ∃ rest : List (Fin n), walkEnd i rest = j ∧ walkWeight w i rest = x} (d i j)
106
107	abbrev ThreeSum := @Lax350013.ThreeSUM.ThreeSum.yes
108
109	/-- The entry `(i, j)` of a matrix with `n` columns that is stored in the list `L`, row by row. -/
110	abbrev entry (n : ℕ) (L : List ℤ) (i j : ℕ) : ℤ := L.getD (i * n + j) 0
111
112	/-- The `N` numbers in a list. -/
113	def vecOf (N : ℕ) (x : List ℤ) : Fin N → ℤ := fun i => x.getD i 0
114
115	/-- The complete tripartite graph with `n` vertices per part whose three weight matrices are in
116	three lists, row by row: the weight of `(a, b)` at `a n + b` of the first, of `(b, c)` at `b n + c`
117	of the second, of `(a, c)` at `a n + c` of the third. -/
118	def triOf (n : ℕ) (AB BC AC : List ℤ) : TriangleInstance ℤ n where
119	wAB a b := AB.getD (a * n + b) 0
120	wBC b c := BC.getD (b * n + c) 0
121	wAC a c := AC.getD (a * n + c) 0
122
123	/-- The weight matrix of a directed graph on `n` vertices: the weight of the edge `(i, j)` is in
124	cell `i n + j` of `w` if cell `i n + j` of `adj` holds 1, and there is no edge otherwise. -/
125	def graphOf (n : ℕ) (adj w : List ℤ) : Fin n → Fin n → WithTop ℤ := fun i j =>
126	if adj.getD (i * n + j) 0 = 1 then ((w.getD (i * n + j) 0 : ℤ) : WithTop ℤ) else ⊤
127
128	/-- The smallest of `A[i,k] + B[k,j]` over `k < n`, by one pass, for `n ≥ 1`. -/
129	def minPlusEntry (n : ℕ) (A B : List ℤ) (i j : ℕ) : ℤ :=
130	(List.range (n - 1)).foldl
131	(fun acc k => min acc (entry n A i (k + 1) + entry n B (k + 1) j))
132	(entry n A i 0 + entry n B 0 j)
133
134	/-- The (min,+)-product of two `n × n` matrices, row by row. -/
135	def minPlusList (n : ℕ) (A B : List ℤ) : List ℤ :=
136	(List.range (n * n)).map fun q => minPlusEntry n A B (q / n) (q % n)
137
138	open Classical in
139	/-- The answer of a decision problem as a number: 1 for yes, 0 for no. -/
140	noncomputable def flag (p : Prop) : ℤ := if p then 1 else 0
141
142	/-- Three `n × n` matrices of weights in the memory. -/
143	structure TriInst : Type where
144	n : ℕ
145	U : ℕ
146	ab : ℕ
147	bc : ℕ
148	ac : ℕ
149	AB : List ℤ
150	BC : List ℤ
151	AC : List ℤ
152
153	/-- The three matrices lie below the free pointer, and their entries are bounded by `U`. -/
154	structure TriInst.Pre (x : TriInst) (μ : ℕ → ℤ) (fr : ℕ) : Prop where
155	n_pos : 1 ≤ x.n
156	U_pos : 1 ≤ x.U
157	lenAB : x.AB.length = x.n * x.n
158	lenBC : x.BC.length = x.n * x.n
159	lenAC : x.AC.length = x.n * x.n
160	segAB : Seg μ x.ab x.AB
161	segBC : Seg μ x.bc x.BC
162	segAC : Seg μ x.ac x.AC
163	leAB : AbsLe x.AB x.U
164	leBC : AbsLe x.BC x.U
165	leAC : AbsLe x.AC x.U
166	belowAB : x.ab + x.n * x.n ≤ fr
167	belowBC : x.bc + x.n * x.n ≤ fr
168	belowAC : x.ac + x.n * x.n ≤ fr
169
170	/-- Exact Triangle: et(n, U, ab, bc, ac, fr) returns 1 if there is a zero triangle and 0 if not.
171	-/
172	noncomputable def etTask : Task where
173	Inst := TriInst
174	size x := x.n
175	bound x := x.U
176	args x := [x.n, x.U, x.ab, x.bc, x.ac]
177	Pre := TriInst.Pre
178	Post x μ fr r μ' := r = flag (triOf x.n x.AB x.BC x.AC).HasZeroTriangle ∧ Kept μ μ' fr
179
180	/-- Negative Triangle: nt(n, U, ab, bc, ac, fr) returns 1 if there is a negative triangle and 0
181	if not. -/
182	noncomputable def ntTask : Task where
183	Inst := TriInst
184	size x := x.n
185	bound x := x.U
186	args x := [x.n, x.U, x.ab, x.bc, x.ac]
187	Pre := TriInst.Pre
188	Post x μ fr r μ' := r = flag (triOf x.n x.AB x.BC x.AC).HasNegativeTriangle ∧ Kept μ μ' fr
189
190	/-- A list of `N` numbers in the memory. -/
191	structure VecInst : Type where
192	N : ℕ
193	U : ℕ
194	a : ℕ
195	X : List ℤ
196
197	/-- The list lies below the free pointer, and its entries are bounded by `U`. -/
198	structure VecInst.Pre (x : VecInst) (μ : ℕ → ℤ) (fr : ℕ) : Prop where
199	N_pos : 1 ≤ x.N
200	U_pos : 1 ≤ x.U
201	len : x.X.length = x.N
202	seg : Seg μ x.a x.X
203	le : AbsLe x.X x.U
204	below : x.a + x.N ≤ fr
205
206	/-- Convolution-3SUM: c3(N, U, x, fr) returns 1 if `x_i + x_j = x_{i+j}` for some `i`, `j`, and
207	0 if not. -/
208	noncomputable def c3Task : Task where
209	Inst := VecInst
210	size x := x.N
211	bound x := x.U
212	args x := [x.N, x.U, x.a]
213	Pre := VecInst.Pre
214	Post x μ fr r μ' := r = flag (Convolution3SUM (vecOf x.N x.X)) ∧ Kept μ μ' fr
215
216	/-- 3SUM: s3(n, U, x, fr) returns 1 if three of the numbers, at different positions, sum to 0,
217	and 0 if not. -/
218	noncomputable def s3Task : Task where
219	Inst := VecInst
220	size x := x.N
221	bound x := x.U
222	args x := [x.N, x.U, x.a]
223	Pre := VecInst.Pre
224	Post x μ fr r μ' := r = flag (ThreeSum (vecOf x.N x.X)) ∧ Kept μ μ' fr
225
226	/-- Two `n × n` matrices in the memory, and the place for a third. -/
227	structure MatInst : Type where
228	n : ℕ
229	U : ℕ
230	a : ℕ
231	b : ℕ
232	c : ℕ
233	A : List ℤ
234	B : List ℤ
235
236	/-- The two matrices and the place for the product lie below the free pointer; the place for the
237	product does not meet the two matrices. -/
238	structure MatInst.Pre (x : MatInst) (μ : ℕ → ℤ) (fr : ℕ) : Prop where
239	n_pos : 1 ≤ x.n
240	U_pos : 1 ≤ x.U
241	lenA : x.A.length = x.n * x.n
242	lenB : x.B.length = x.n * x.n
243	segA : Seg μ x.a x.A
244	segB : Seg μ x.b x.B
245	leA : AbsLe x.A x.U
246	leB : AbsLe x.B x.U
247	belowA : x.a + x.n * x.n ≤ fr
248	belowB : x.b + x.n * x.n ≤ fr
249	belowC : x.c + x.n * x.n ≤ fr
250	apartA : Apart x.a (x.n * x.n) x.c (x.n * x.n)
251	apartB : Apart x.b (x.n * x.n) x.c (x.n * x.n)
252
253	/-- The (min,+)-product: mp(n, U, a, b, c, fr) writes the product of the matrices at `a` and `b`
254	to `c`. -/
255	def mpTask : Task where
256	Inst := MatInst
257	size x := x.n
258	bound x := x.U
259	args x := [x.n, x.U, x.a, x.b, x.c]
260	Pre := MatInst.Pre
261	Post x μ fr _ μ' := Seg μ' x.c (minPlusList x.n x.A x.B) ∧ KeptBut μ μ' fr x.c (x.n * x.n)
262
263	/-- A directed graph in the memory: adjacency matrix and weights, and the place for the `2n²` cells
264	of the answer. -/
265	structure GraphInst : Type where
266	n : ℕ
267	U : ℕ
268	adj : ℕ
269	w : ℕ
270	out : ℕ
271	ADJ : List ℤ
272	W : List ℤ
273
274	/-- The graph and the place for the answer lie below the free pointer; the graph has no negative
275	cycle. -/
276	structure GraphInst.Pre (x : GraphInst) (μ : ℕ → ℤ) (fr : ℕ) : Prop where
277	n_pos : 1 ≤ x.n
278	U_pos : 1 ≤ x.U
279	lenADJ : x.ADJ.length = x.n * x.n
280	lenW : x.W.length = x.n * x.n
281	segADJ : Seg μ x.adj x.ADJ
282	segW : Seg μ x.w x.W
283	zeroOne : ∀ e ∈ x.ADJ, e = 0 ∨ e = 1
284	leW : AbsLe x.W x.U
285	belowADJ : x.adj + x.n * x.n ≤ fr
286	belowW : x.w + x.n * x.n ≤ fr
287	belowOut : x.out + 2 * (x.n * x.n) ≤ fr
288	apartADJ : Apart x.adj (x.n * x.n) x.out (2 * (x.n * x.n))
289	apartW : Apart x.w (x.n * x.n) x.out (2 * (x.n * x.n))
290	noNegativeCycle : NoNegativeCycle (graphOf x.n x.ADJ x.W)
291
292	/-- APSP: ap(n, U, adj, w, out, fr) writes two cells for each pair `(i, j)`, at
293	`out + 2 (i n + j)`: 1 and the distance from `i` to `j` if `j` can be reached from `i`, and 0 in the
294	first cell if not. -/
295	def apTask : Task where
296	Inst := GraphInst
297	size x := x.n
298	bound x := x.U
299	args x := [x.n, x.U, x.adj, x.w, x.out]
300	Pre := GraphInst.Pre
301	Post x μ fr _ μ' :=
302	(∃ dist : Fin x.n → Fin x.n → WithTop ℤ, IsDistanceMatrix (graphOf x.n x.ADJ x.W) dist ∧
303	∀ i j : Fin x.n,
304	(dist i j = ⊤ → μ' (x.out + 2 * (i.val * x.n + j.val)) = 0) ∧
305	∀ z : ℤ, dist i j = (z : WithTop ℤ) →
306	μ' (x.out + 2 * (i.val * x.n + j.val)) = 1 ∧
307	μ' (x.out + 2 * (i.val * x.n + j.val) + 1) = z) ∧
308	KeptBut μ μ' fr x.out (2 * (x.n * x.n))
309
310	/-- Matrices `X` (`N × D`) and `Y` (`D × N`), row by row, `w` wanted positions (rows in `WI`,
311	columns in `WJ`), and the place for `w` answers. -/
312	structure ThinInst : Type where
313	/-- The number of rows of `X` and of columns of `Y`. -/
314	N : ℕ
315	/-- The number of columns of `X` and of rows of `Y`. -/
316	D : ℕ
317	/-- The number of wanted positions. -/
318	w : ℕ
319	/-- The bound on the absolute values of the entries. -/
320	U : ℕ
321	/-- The address of `X`. -/
322	x : ℕ
323	/-- The address of `Y`. -/
324	y : ℕ
325	/-- The address of `WI`. -/
326	wi : ℕ
327	/-- The address of `WJ`. -/
328	wj : ℕ
329	/-- The address of the answers. -/
330	out : ℕ
331	/-- The first matrix, row by row. -/
332	X : List ℤ
333	/-- The second matrix, row by row. -/
334	Y : List ℤ
335	/-- The rows of the wanted positions. -/
336	WI : List ℕ
337	/-- The columns of the wanted positions. -/
338	WJ : List ℕ
339
340	/-- Everything lies below the free pointer, the entries are bounded by `U`, the positions are
341	distinct positions of an `N × N` matrix, and the place for the answers meets none of the inputs. -/
342	structure ThinInst.Pre (x : ThinInst) (μ : ℕ → ℤ) (fr : ℕ) : Prop where
343	N_pos : 1 ≤ x.N
344	D_pos : 1 ≤ x.D
345	U_pos : 1 ≤ x.U
346	lenX : x.X.length = x.N * x.D
347	lenY : x.Y.length = x.D * x.N
348	lenWI : x.WI.length = x.w
349	lenWJ : x.WJ.length = x.w
350	segX : Seg μ x.x x.X
351	segY : Seg μ x.y x.Y
352	segWI : SegN μ x.wi x.WI
353	segWJ : SegN μ x.wj x.WJ
354	leX : AbsLe x.X x.U
355	leY : AbsLe x.Y x.U
356	ltWI : ∀ i ∈ x.WI, i < x.N
357	ltWJ : ∀ j ∈ x.WJ, j < x.N
358	nodup : (x.WI.zip x.WJ).Nodup
359	belowX : x.x + x.N * x.D ≤ fr
360	belowY : x.y + x.D * x.N ≤ fr
361	belowWI : x.wi + x.w ≤ fr
362	belowWJ : x.wj + x.w ≤ fr
363	belowOut : x.out + x.w ≤ fr
364	apartX : Apart x.out x.w x.x (x.N * x.D)
365	apartY : Apart x.out x.w x.y (x.D * x.N)
366	apartWI : Apart x.out x.w x.wi x.w
367	apartWJ : Apart x.out x.w x.wj x.w
368
369	/-- The entries of both matrices are 0 or 1. -/
370	def ThinInst.ZeroOne (x : ThinInst) : Prop := (∀ v ∈ x.X, v = 0 ∨ v = 1) ∧ ∀ v ∈ x.Y, v = 0 ∨ v = 1
371
372	/-- The entry `(XY)[I, J]`. -/
373	def thinEntry (N D : ℕ) (X Y : List ℤ) (I J : ℕ) : ℤ :=
374	((List.range D).map fun k => X.getD (I * D + k) 0 * Y.getD (k * N + J) 0).sum
375
376	/-- The wanted entries, in the order of the positions. -/
377	def thinOut (N D : ℕ) (X Y : List ℤ) (WI WJ : List ℕ) : List ℤ :=
378	(WI.zip WJ).map fun q => thinEntry N D X Y q.1 q.2
379
380	/-- The wanted entries of a thin matrix product (Theorem 5, Corollary 26):
381	`thin(N, D, w, U, x, y, wi, wj, out, fr)`. -/
382	def thinTask : TaskN where
383	Inst := ThinInst
384	pars x := [x.N, x.D, x.w, x.U]
385	args x := [x.N, x.D, x.w, x.U, x.x, x.y, x.wi, x.wj, x.out]
386	Pre := ThinInst.Pre
387	Post x μ fr _ μ' := Seg μ' x.out (thinOut x.N x.D x.X x.Y x.WI x.WJ) ∧ KeptBut μ μ' fr x.out x.w
388
389	/-- #Lop-AE-SparseTri (Definition 14), the graph given by its two biadjacency matrices: the same
390	call with `U = 1` on matrices of zeros and ones; the answers are the numbers of common
391	neighbours. -/
392	def lopCountTask : TaskN where
393	Inst := ThinInst
394	pars x := [x.N, x.D, x.w]
395	args x := [x.N, x.D, x.w, x.U, x.x, x.y, x.wi, x.wj, x.out]
396	Pre x μ fr := x.Pre μ fr ∧ x.ZeroOne ∧ x.U = 1
397	Post x μ fr _ μ' := Seg μ' x.out (thinOut x.N x.D x.X x.Y x.WI x.WJ) ∧ KeptBut μ μ' fr x.out x.w
398
399	/-- Lop-AE-SparseTri (Definition 13): the answer is 1 if the pair has a common neighbour and 0
400	if not. -/
401	def lopDetectTask : TaskN where
402	Inst := ThinInst
403	pars x := [x.N, x.D, x.w]
404	args x := [x.N, x.D, x.w, x.U, x.x, x.y, x.wi, x.wj, x.out]
405	Pre x μ fr := x.Pre μ fr ∧ x.ZeroOne ∧ x.U = 1
406	Post x μ fr _ μ' :=
407	Seg μ' x.out ((thinOut x.N x.D x.X x.Y x.WI x.WJ).map fun v => if v = 0 then 0 else 1) ∧
408	KeptBut μ μ' fr x.out x.w
409
410	/-- "The thin matrix product is solved in time `T N D w' u`", where `w'` is an upper bound on the
411	number `w` of wanted positions and `u` one on the bound `U`. -/
412	def ThinSolvedIn (T : ℕ → ℕ → ℕ → ℝ → ℝ) : Prop :=
413	∃ (P : Program) (p : ℕ) (Tn : List ℕ → ℕ) (need : List ℕ → Need), PolyNeedN need ∧
414	SolvesN thinTask P p Tn need ∧
415	∀ (N D w w' U : ℕ) (u : ℝ), 1 ≤ N → 1 ≤ D → 1 ≤ U → w ≤ w' → (U : ℝ) ≤ u →
416	(Tn [N, D, w, U] : ℝ) ≤ T N D w' u
417
418	/-- "The task (one of the two lopsided triangle problems) is solved in time `T n D w'`", where `w'`
419	is an upper bound on the number `w` of query pairs. -/
420	def LopSolvedIn (task : TaskN) (T : ℕ → ℕ → ℕ → ℝ) : Prop :=
421	∃ (P : Program) (p : ℕ) (Tn : List ℕ → ℕ) (need : List ℕ → Need), PolyNeedN need ∧
422	SolvesN task P p Tn need ∧
423	∀ (n D w w' : ℕ), 1 ≤ n → 1 ≤ D → w ≤ w' → (Tn [n, D, w] : ℝ) ≤ T n D w'
424
425	end Lax350013.CallableProblems
426

Builds on

Used by

Lax350013.CallableAlgorithms

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

Calling conventions for matrix and graph algorithms

Flags

Flag this concept

Natural Language Statement

Definition

Lean source view on GitHub

Discussion

Settings

Your comments