Lopsided all-edges triangle detection and counting

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

definition

Loading review…

Natural Language Statement

Definition

An unweighted tripartite graph has two parts of size $N$ , a middle part of size at most $D$ , and a specified set of query edges between the large parts. The tasks are to detect or count the triangles containing each query edge. The input uses two Boolean biadjacency matrices; zero padding represents a smaller middle part.

Concept map

5 concepts; 1 descendant 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.ThinMatrices
26
27	/-!
28	---
29	title: Lopsided all-edges triangle detection and counting
30	type: definition
31	---
32	An unweighted tripartite graph has two parts of size $N$ , a middle part of size at most $D$ , and a specified set of query edges between the large parts. The tasks are to detect or count the triangles containing each query edge. The input uses two Boolean biadjacency matrices; zero padding represents a smaller middle part.
33	-/
34
35	namespace Lax350013.LopsidedTriangles
36
37	open Finset
38	open Lax350013.WordRAM
39	open Lax350013.RAMResources
40	open Lax350013.ThinMatrices
41
42	/-- Definition 13, the input: "an unweighted undirected tripartite graph with two parts
43	A and B of n vertices each and a middle part M [...], with arbitrary edges in M × A and M × B. Let
44	W ⊆ A × B be the set of edges between A and B." The bound "of at most D vertices" on the middle
45	part is `LopInstance.MiddleAtMost`. -/
46	structure LopInstance (n : ℕ) where
47	/-- The middle part `M`. -/
48	M : Type
49	/-- The middle part is finite. -/
50	[fintypeM : Fintype M]
51	/-- `adjA a v`: the vertex `a ∈ A` and the middle vertex `v ∈ M` are adjacent. -/
52	adjA : Fin n → M → Prop
53	/-- `adjB v b`: the middle vertex `v ∈ M` and the vertex `b ∈ B` are adjacent. -/
54	adjB : M → Fin n → Prop
55	/-- The set `W ⊆ A × B` of edges between `A` and `B`; Section 3.1 calls its elements the query
56	pairs. -/
57	W : Finset (Fin n × Fin n)
58
59	attribute [instance] LopInstance.fintypeM
60
61	/-- Definition 13: "a middle part M of at most D vertices". An instance of Lop-AE-SparseTri(n, D),
62	and of #Lop-AE-SparseTri(n, D), is an `I : LopInstance n` with `I.MiddleAtMost D`. -/
63	def LopInstance.MiddleAtMost {n : ℕ} (I : LopInstance n) (D : ℕ) : Prop :=
64	Fintype.card I.M ≤ D
65
66	/-- Definitions 13 and 14: the common neighbors of `a` and `b` in `M`. -/
67	def LopInstance.commonNeighbors {n : ℕ} (I : LopInstance n) (a b : Fin n) : Set I.M :=
68	{v \| I.adjA a v ∧ I.adjB v b}
69
70	/-- Definition 13: the pair `(a, b)` "lies in a triangle with some vertex of M, that is, [...] a and
71	b have a common neighbor in M". -/
72	def LopInstance.InTriangle {n : ℕ} (I : LopInstance n) (a b : Fin n) : Prop :=
73	∃ v : I.M, I.adjA a v ∧ I.adjB v b
74
75	/-- Definition 14: "the number of triangles it lies in, that is, the number of common
76	neighbors of a and b in M". -/
77	noncomputable def LopInstance.numTriangles {n : ℕ} (I : LopInstance n) (a b : Fin n) : ℕ :=
78	(I.commonNeighbors a b).ncard
79
80	/-- Definition 13, the task: "Decide, for every edge (a, b) ∈ W, whether it lies in a triangle
81	with some vertex of M". `ans` is a correct answer to the instance `I` of Lop-AE-SparseTri; its
82	values outside `W` are not constrained. -/
83	def LopInstance.IsDetectionAnswer {n : ℕ} (I : LopInstance n) (ans : Fin n × Fin n → Bool) : Prop :=
84	∀ q ∈ I.W, (ans q = true ↔ I.InTriangle q.1 q.2)
85
86	/-- Footnote 8, Section 3.1: "An instance of #Lop-AE-SparseTri(n,D) asks for the wanted entries of a
87	thin matrix product of two 0/1 matrices." This is the instance that two matrices and a set `W` of
88	positions describe: the middle part is the set of the `D` column indices of `X`, and adjacency means
89	that the entry is 1. -/
90	def LopInstance.ofMatrices {n D : ℕ} (X : Matrix (Fin n) (Fin D) ℤ) (Y : Matrix (Fin D) (Fin n) ℤ)
91	(W : Finset (Fin n × Fin n)) : LopInstance n where
92	M := Fin D
93	adjA a v := X a v = 1
94	adjB v b := Y v b = 1
95	W := W
96
97	abbrev ThinInstance := Lax350013.ThinMatrices.ThinInstance
98
99	/-- The entries of both matrices are 0 or 1: the two biadjacency matrices of an instance of
100	Lop-AE-SparseTri(N, D) (Section 3.1). -/
101	def ThinInstance.ZeroOne (x : ThinInstance) : Prop :=
102	(∀ i j, x.X i j = 0 ∨ x.X i j = 1) ∧ (∀ i j, x.Y i j = 0 ∨ x.Y i j = 1)
103
104	/-- The instance of the lopsided triangle problems that two 0/1 matrices and a list of query pairs
105	describe.
106
107	NOTE. Definition 13 has "a middle part M of at most D vertices"; here the middle part has exactly
108	`D` vertices, the columns of `X`. A smaller middle part is written with zero columns of `X` and
109	zero rows of `Y`: vertices without edges, which lie in no triangle. -/
110	def ThinInstance.lop (x : ThinInstance) : LopInstance x.N :=
111	LopInstance.ofMatrices x.X x.Y x.W.toFinset
112
113	/-- #Lop-AE-SparseTri (Definition 14), with the graph given by its two biadjacency matrices: the
114	`i`-th output cell holds the number of triangles through the `i`-th query pair. -/
115	def lopCount : Problem where
116	Inst := ThinInstance
117	params x := [x.N, x.D]
118	input x := x.input []
119	IsAnswer x verdict out :=
120	verdict = true ∧ ∀ (i : ℕ) (h : i < x.W.length),
121	out i = (x.lop.numTriangles x.W[i].1 x.W[i].2 : ℤ)
122
123	/-- Lop-AE-SparseTri (Definition 13): the `i`-th output cell holds 1 if the `i`-th query pair
124	lies in a triangle, and 0 if not. -/
125	def lopDetect : Problem where
126	Inst := ThinInstance
127	params x := [x.N, x.D]
128	input x := x.input []
129	IsAnswer x verdict out :=
130	verdict = true ∧ ∀ (i : ℕ) (h : i < x.W.length),
131	(x.lop.InTriangle x.W[i].1 x.W[i].2 → out i = 1) ∧
132	(¬ x.lop.InTriangle x.W[i].1 x.W[i].2 → out i = 0)
133
134	end Lax350013.LopsidedTriangles
135

Builds on

Lax350013.ThinMatrices

Used by

Lax350013.LopsidedTriangleAlgorithms

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

Lopsided all-edges triangle detection and counting

Flags

Flag this concept

Natural Language Statement

Definition

Lean source view on GitHub

Discussion

Settings

Your comments