Finite lopsided triangle queries as matrix products

Two outer parts have n vertices each; the finite middle part embeds into Fin D. The matrices count common neighbors at every outer pair. Only pairs in W are graph edges, so only those counts are triangle counts. Answers outside W are unconstrained.

This mathematical interface gives no native program, preprocessing cost, sparsity bound, fast solver or subquadratic running time.

Main definitions

• LopsidedGraph: two adjacency relations, a finite middle part and queried outer edges.
• LopsidedGraph.matX, LopsidedGraph.matY: padded biadjacency matrices.
• LopsidedGraph.signedBitInstance: four sign choices for each pair of binary digits.

Main results

• LopsidedGraph.matX_mul_matY_apply: entries count common middle neighbors.
• LopsidedGraph.matX_mul_matY_apply_ne_zero_iff: nonzero entries detect common neighbors.
• LopsidedGraph.mul_apply_eq_commonNeighborCount_ofMatrices: the converse for zero/one matrices.
• LopsidedGraph.mul_apply_eq_sum_signedBitInstance_counts: signed products from 4 * β² counts.

References

The lopsided matrix interface is used in [AlmanWilliams2026, Section 3]. Adapted from Anthropic's MatrixLanguage.lean and the lopsided definitions in PaperStatements.lean. The adaptation uses Set.EqOn, pointwise signed parts, and direct finite cardinalities.

structure Cslib.Algorithms.ExactTriangle.LopsidedGraph (n : ℕ) : Type 1

An unweighted tripartite graph whose outer parts each have n vertices.

• M : Type

  The middle vertices.

• fintypeM : Fintype self.M

  The middle part is finite.

• adjA : Fin n → self.M → Prop

  Edges from the first outer part to the middle.

• adjB : self.M → Fin n → Prop

  Edges from the middle to the second outer part.

• W : Finset (Fin n × Fin n)

  Queried outer edges.

def Cslib.Algorithms.ExactTriangle.LopsidedGraph.HasCommonNeighbor {n : ℕ} (I : LopsidedGraph n) (a b : Fin n) : Prop

On a pair in W, a common middle neighbor closes a triangle. For a pair outside W, this predicate does not assert an outer edge.

noncomputable def Cslib.Algorithms.ExactTriangle.LopsidedGraph.commonNeighborCount {n : ℕ} (I : LopsidedGraph n) (a b : Fin n) : ℕ

Number of common middle neighbors. At pairs in W this is the triangle count.

def Cslib.Algorithms.ExactTriangle.LopsidedGraph.ofMatrices {n D : ℕ} (X : Matrix (Fin n) (Fin D) ℤ) (Y : Matrix (Fin D) (Fin n) ℤ) (W : Finset (Fin n × Fin n)) : LopsidedGraph n

Two thin matrices describe adjacency where their entries equal one. The theorem mul_apply_eq_commonNeighborCount_ofMatrices requires zero/one entries.

theorem Cslib.Algorithms.ExactTriangle.LopsidedGraph.commonNeighborCount_ofMatrices {n D : ℕ} (X : Matrix (Fin n) (Fin D) ℤ) (Y : Matrix (Fin D) (Fin n) ℤ) (W : Finset (Fin n × Fin n)) (a b : Fin n) : (ofMatrices X Y W).commonNeighborCount a b = {v : Fin D | X a v = 1 ∧ Y v b = 1}.card

The count for a matrix-defined graph uses the ordinary finite middle indices.

noncomputable def Cslib.Algorithms.ExactTriangle.LopsidedGraph.matX {n D : ℕ} (I : LopsidedGraph n) (e : I.M ↪ Fin D) : Matrix (Fin n) (Fin D) ℤ

The first biadjacency matrix, with zero columns outside the injection range.

noncomputable def Cslib.Algorithms.ExactTriangle.LopsidedGraph.matY {n D : ℕ} (I : LopsidedGraph n) (e : I.M ↪ Fin D) : Matrix (Fin D) (Fin n) ℤ

The second biadjacency matrix, with zero rows outside the injection range.

theorem Cslib.Algorithms.ExactTriangle.LopsidedGraph.matX_eq_zero_or_one {n D : ℕ} (I : LopsidedGraph n) (e : I.M ↪ Fin D) (a : Fin n) (j : Fin D) : I.matX e a j = 0 ∨ I.matX e a j = 1

Every first biadjacency entry is zero or one.

theorem Cslib.Algorithms.ExactTriangle.LopsidedGraph.matY_eq_zero_or_one {n D : ℕ} (I : LopsidedGraph n) (e : I.M ↪ Fin D) (j : Fin D) (b : Fin n) : I.matY e j b = 0 ∨ I.matY e j b = 1

Every second biadjacency entry is zero or one.

theorem Cslib.Algorithms.ExactTriangle.LopsidedGraph.nonempty_embedding {n D : ℕ} (I : LopsidedGraph n) (h : Fintype.card I.M ≤ D) : Nonempty (I.M ↪ Fin D)

A middle part of cardinality at most D admits the required numbering.

theorem Cslib.Algorithms.ExactTriangle.LopsidedGraph.matX_apply_emb {n D : ℕ} (I : LopsidedGraph n) (e : I.M ↪ Fin D) (a : Fin n) (v : I.M) : I.matX e a (e v) = if I.adjA a v then 1 else 0

At a middle vertex, the first matrix records its adjacency.

theorem Cslib.Algorithms.ExactTriangle.LopsidedGraph.matY_apply_emb {n D : ℕ} (I : LopsidedGraph n) (e : I.M ↪ Fin D) (v : I.M) (b : Fin n) : I.matY e (e v) b = if I.adjB v b then 1 else 0

At a middle vertex, the second matrix records its adjacency.

theorem Cslib.Algorithms.ExactTriangle.LopsidedGraph.matX_apply_of_notMem_range {n D : ℕ} (I : LopsidedGraph n) (e : I.M ↪ Fin D) (a : Fin n) {j : Fin D} (hj : j ∉ Set.range ⇑e) : I.matX e a j = 0

An unused column is zero.

theorem Cslib.Algorithms.ExactTriangle.LopsidedGraph.matY_apply_of_notMem_range {n D : ℕ} (I : LopsidedGraph n) (e : I.M ↪ Fin D) {j : Fin D} (hj : j ∉ Set.range ⇑e) (b : Fin n) : I.matY e j b = 0

An unused row is zero.

theorem Cslib.Algorithms.ExactTriangle.LopsidedGraph.commonNeighborCount_ne_zero_iff {n : ℕ} (I : LopsidedGraph n) (a b : Fin n) : I.commonNeighborCount a b ≠ 0 ↔ I.HasCommonNeighbor a b

A pair has a common neighbor if and only if its count is nonzero.

theorem Cslib.Algorithms.ExactTriangle.LopsidedGraph.matX_mul_matY_apply {n D : ℕ} (I : LopsidedGraph n) (e : I.M ↪ Fin D) (a b : Fin n) : (I.matX e * I.matY e) a b = ↑(I.commonNeighborCount a b)

Every product entry counts common middle neighbors, independently of the numbering.

theorem Cslib.Algorithms.ExactTriangle.LopsidedGraph.matX_mul_matY_apply_ne_zero_iff {n D : ℕ} (I : LopsidedGraph n) (e : I.M ↪ Fin D) (a b : Fin n) : (I.matX e * I.matY e) a b ≠ 0 ↔ I.HasCommonNeighbor a b

A nonzero product entry detects a common middle neighbor.

theorem Cslib.Algorithms.ExactTriangle.LopsidedGraph.counting_eqOn_iff {n D : ℕ} (I : LopsidedGraph n) (e : I.M ↪ Fin D) (ans : Fin n × Fin n → ℕ) : Set.EqOn ans (fun (q : Fin n × Fin n) => I.commonNeighborCount q.1 q.2) ↑I.W ↔ Set.EqOn (fun (q : Fin n × Fin n) => ↑(ans q)) (fun (q : Fin n × Fin n) => (I.matX e * I.matY e) q.1 q.2) ↑I.W

On queried outer edges, correct natural counts are exactly the integer product entries. Ordinary Set.EqOn leaves all unqueried entries unconstrained.

theorem Cslib.Algorithms.ExactTriangle.LopsidedGraph.detection_iff_of_counting {n : ℕ} (I : LopsidedGraph n) (ans : Fin n × Fin n → ℕ) (h : Set.EqOn ans (fun (q : Fin n × Fin n) => I.commonNeighborCount q.1 q.2) ↑I.W) (q : Fin n × Fin n) : q ∈ I.W → (ans q ≠ 0 ↔ I.HasCommonNeighbor q.1 q.2)

Counts on queried edges provide their detection answers.

theorem Cslib.Algorithms.ExactTriangle.LopsidedGraph.mul_apply_eq_commonNeighborCount_ofMatrices {n D : ℕ} (X : Matrix (Fin n) (Fin D) ℤ) (Y : Matrix (Fin D) (Fin n) ℤ) (W : Finset (Fin n × Fin n)) (hX : ∀ (a : Fin n) (j : Fin D), X a j = 0 ∨ X a j = 1) (hY : ∀ (j : Fin D) (b : Fin n), Y j b = 0 ∨ Y j b = 1) (a b : Fin n) : (X * Y) a b = ↑((ofMatrices X Y W).commonNeighborCount a b)

For zero/one matrices, each product entry is the count in the graph they describe.

def Cslib.Algorithms.ExactTriangle.LopsidedGraph.signedBitInstance {n D : ℕ} (X : Matrix (Fin n) (Fin D) ℤ) (Y : Matrix (Fin D) (Fin n) ℤ) (W : Finset (Fin n × Fin n)) (negativeX negativeY : Bool) (i j : ℕ) : LopsidedGraph n

One of four sign choices for a pair of binary digits; true selects the negative part. Every instance has exactly D middle vertices and the original queried edges W.

def Cslib.Algorithms.ExactTriangle.LopsidedGraph.signedBitInstances {n D : ℕ} (X : Matrix (Fin n) (Fin D) ℤ) (Y : Matrix (Fin D) (Fin n) ℤ) (W : Finset (Fin n × Fin n)) (β : ℕ) : Bool × Bool × Fin β × Fin β → LopsidedGraph n

The finite family of sign/digit instances for a magnitude width β. Different slots may describe the same graph.

theorem Cslib.Algorithms.ExactTriangle.LopsidedGraph.card_signedBit_indices (β : ℕ) : Fintype.card (Bool × Bool × Fin β × Fin β) = 4 * β ^ 2

The indexed family has 4 * β² slots, allowing repeated or zero instances.

theorem Cslib.Algorithms.ExactTriangle.LopsidedGraph.mul_apply_eq_sum_signedBitInstance_counts {n D : ℕ} (X : Matrix (Fin n) (Fin D) ℤ) (Y : Matrix (Fin D) (Fin n) ℤ) (W : Finset (Fin n × Fin n)) (β : ℕ) (hX : ∀ (a : Fin n) (j : Fin D), |X a j| < 2 ^ β) (hY : ∀ (j : Fin D) (b : Fin n), |Y j b| < 2 ^ β) (a b : Fin n) : (X * Y) a b = ∑ i ∈ Finset.range β, ∑ j ∈ Finset.range β, 2 ^ (i + j) * (↑((signedBitInstance X Y W false false i j).commonNeighborCount a b) - ↑((signedBitInstance X Y W false true i j).commonNeighborCount a b) - ↑((signedBitInstance X Y W true false i j).commonNeighborCount a b) + ↑((signedBitInstance X Y W true true i j).commonNeighborCount a b))

Signed bounded product entries are weighted sums of four count instances per digit pair, with signs +, −, −, +. Only counts at the same queried edge are needed. The absolute bounds are strict; β = 0 therefore permits only zero entries.