Modular splitting of Exact Triangle into finite lopsided queries

Pieces of the third part and chunks of A–B residue classes define lopsided graphs with a middle vertex (c, label). The three input matrices retain their original orientations. All bounds below use 16 ≤ D ≤ n and 1 ≤ g; the sharper degree bound also uses g ≤ sqrt D. No native program, fast solver or charged instruction bound is asserted.

Main definitions

• piece, residueClass, chunkOf: vertex blocks and residue query chunks.
• lopInstance, instanceIndices, totalChunks: lopsided graphs and their finite indices.

Main results

• existsUnique_mem_piece, card_piece_le: unique piece coverage and size.
• totalChunks_le, card_instanceIndices_le: chunk and instance bounds.
• card_middle_lopInstance, hasCommonNeighbor_lopInstance_iff: size and modular correctness.
• ncard_nbr_lopInstance_le: degree bound.

References

The reduction is part of [AlmanWilliams2026, Section 3]. Direct adaptation of Instances.lean, with only required definitions from PaperStatements.lean, Chunks.lean and Parameters.lean, at anthropics/formal-math@16a5ce41304fcdaea4e0be7c132e1c361dc26da5. Quoted docstring fragments reproduce comments in the pinned formal source; other prose describes the local Lean API.

def Cslib.Algorithms.ExactTriangle.queryCap (n D : ℕ) : ℕ

The largest number of query pairs that is "at most n²/√D" (Corollary 15 and Theorem 17; Theorem 5 has "at most N²/√D"): ⌊n²/√D⌋.

theorem Cslib.Algorithms.ExactTriangle.queryCap_eq_floor (n D : ℕ) : queryCap n D = ⌊↑n ^ 2 / √↑D⌋₊

The integer capacity is exactly the real-valued floor used in the reduction.

def Cslib.Algorithms.ExactTriangle.sOf (D : ℕ) : ℕ

Proof of Theorem 17: "let s := ⌊√D⌋".

def Cslib.Algorithms.ExactTriangle.pieceSize (D g : ℕ) : ℕ

Proof of Theorem 17: the bound "⌈s/g⌉" on the number of vertices of a piece.

theorem Cslib.Algorithms.ExactTriangle.pieceSize_eq_ceil (D g : ℕ) : pieceSize D g = ⌈↑(sOf D) / ↑g⌉₊

The integer block size equals the real ceiling, also at the zero-divisor convention.

def Cslib.Algorithms.ExactTriangle.piece (n D g k : ℕ) : Finset (Fin n)

Proof of Theorem 17: "split C into pieces C₁, …, C_h of at most ⌈s/g⌉ vertices each". The paper does not say how; we take blocks of ⌈s/g⌉ consecutive vertices. piece n D g k is the paper's C_{k+1}.

def Cslib.Algorithms.ExactTriangle.numPieces (n D g : ℕ) : ℕ

Proof of Theorem 17: the number h of pieces, ⌈n / ⌈s/g⌉⌉ for the blocks of piece (meaningful when ⌈s/g⌉ ≥ 1).

theorem Cslib.Algorithms.ExactTriangle.numPieces_eq_ceil (n D g : ℕ) : numPieces n D g = ⌈↑n / ↑(pieceSize D g)⌉₊

The number of blocks is the ceiling of the real quotient by the block size.

@[reducible, inline]

abbrev Cslib.Algorithms.ExactTriangle.InstanceIndex (p : ℕ) : Type

The index of an instance built by the reduction of Theorem 17: a residue ϱ ∈ ℤ_p, the number j of a chunk of W_ϱ, and the number k of a piece of C.

def Cslib.Algorithms.ExactTriangle.residueClass {n : ℕ} (wAB : Fin n → Fin n → ℤ) (p : ℕ) (ϱ : Fin p) : Finset (Fin n × Fin n)

Proof of Theorem 17: "For ϱ ∈ ℤ_p let W_ϱ be the set of edges (a,b) ∈ A × B with w(a,b) ≡ ϱ (mod p)".

def Cslib.Algorithms.ExactTriangle.chunkOf {n : ℕ} (wAB : Fin n → Fin n → ℤ) (D p : ℕ) (ϱ : Fin p) (j : ℕ) : Finset (Fin n × Fin n)

Proof of Theorem 17: "and cut it into chunks of at most n²/√D query pairs". The j-th chunk of W_ϱ.

def Cslib.Algorithms.ExactTriangle.lopInstance {n : ℕ} (wAB wBC wAC : Fin n → Fin n → ℤ) (D g p : ℕ) : InstanceIndex p → LopsidedGraph n

Proof of Theorem 17: "For each chunk 𝒬 ⊆ W_ϱ and each piece C_k form the instance of Lop-AE-SparseTri(n, D) with query pairs W := 𝒬 and middle part C_k × ℤ_p [...], whose middle vertices are pairs (vertex, label) [...], with a ∼ (c, σ) ⟺ σ ≡ w(a,c) + ϱ, (c, σ) ∼ b ⟺ σ ≡ −w(b,c) (mod p)."

def Cslib.Algorithms.ExactTriangle.instanceIndices {n : ℕ} (wAB : Fin n → Fin n → ℤ) (D g p : ℕ) : Finset (InstanceIndex p)

Proof of Theorem 17: "For each chunk 𝒬 ⊆ W_ϱ and each piece C_k" there is an instance; these are the indices of all the instances. This set depends only on the Exact Triangle instance and on D, g, p, not on any answer of the oracle.

def Cslib.Algorithms.ExactTriangle.totalChunks {n : ℕ} (wAB : Fin n → Fin n → ℤ) (D p : ℕ) : ℕ

Total number of query chunks, summed over residues.

theorem Cslib.Algorithms.ExactTriangle.one_le_queryCap {n D : ℕ} (hD : 1 ≤ D) (hDn : D ≤ n) : 1 ≤ queryCap n D

The bound ⌊n²/√D⌋ on the size of a chunk is at least 1, because √D ≤ n ≤ n².

The pieces

theorem Cslib.Algorithms.ExactTriangle.sOf_le_sqrt (D : ℕ) : ↑(sOf D) ≤ √↑D

s = ⌊√D⌋ ≤ √D.

theorem Cslib.Algorithms.ExactTriangle.sqrt_lt_sOf_add_one (D : ℕ) : √↑D < ↑(sOf D) + 1

√D < s + 1.

theorem Cslib.Algorithms.ExactTriangle.pieceSize_pos {D g : ℕ} (hD : 16 ≤ D) (hg1 : 1 ≤ g) : 0 < pieceSize D g

The bound ⌈s/g⌉ on the size of a piece is at least 1.

theorem Cslib.Algorithms.ExactTriangle.pieceSize_le_sOf {D g : ℕ} (hg1 : 1 ≤ g) : pieceSize D g ≤ sOf D

⌈s/g⌉ ≤ s because g ≥ 1.

theorem Cslib.Algorithms.ExactTriangle.mem_piece {n D g k : ℕ} (c : Fin n) : c ∈ piece n D g k ↔ ↑c / pieceSize D g = k

A vertex lies in the piece number k exactly if its number divided by ⌈s/g⌉ is k.

theorem Cslib.Algorithms.ExactTriangle.existsUnique_mem_piece {n D g : ℕ} (hD : 16 ≤ D) (hg1 : 1 ≤ g) (c : Fin n) : ∃! k : ℕ, k < numPieces n D g ∧ c ∈ piece n D g k

Proof of Theorem 17: "split C into pieces C₁, …, C_h of at most ⌈s/g⌉ vertices each": every vertex of C lies in exactly one of the h pieces.

theorem Cslib.Algorithms.ExactTriangle.card_piece_le {D g : ℕ} (hD : 16 ≤ D) (hg1 : 1 ≤ g) (n k : ℕ) : (piece n D g k).card ≤ pieceSize D g

Proof of Theorem 17, "pieces [...] of at most ⌈s/g⌉ vertices each": |C_k| ≤ ⌈s/g⌉, because the numbers of the vertices of the piece number k lie in [k ⌈s/g⌉, (k + 1) ⌈s/g⌉).

theorem Cslib.Algorithms.ExactTriangle.numPieces_le {n D g : ℕ} (hD : 16 ≤ D) (hg1 : 1 ≤ g) : numPieces n D g ≤ ⌈↑n * ↑g / ↑(sOf D)⌉₊

Proof of Theorem 17: "so that h ≤ ⌈ng/s⌉".

Residues

def Cslib.Algorithms.ExactTriangle.resFin {p : ℕ} (hp : p ≠ 0) (x : ℤ) : Fin p

The residue of the integer x modulo p, as an element of Fin p.

theorem Cslib.Algorithms.ExactTriangle.resFin_modEq {p : ℕ} (hp : p ≠ 0) (x : ℤ) : ↑↑(resFin hp x) ≡ x [ZMOD ↑p]

The residue of x is congruent to x.

The arithmetic behind the two counts

theorem Cslib.Algorithms.ExactTriangle.le_sOf_and_sqrt_le {n D : ℕ} (hD : 16 ≤ D) (hDn : D ≤ n) : 3 * √↑D / 4 ≤ ↑(sOf D) ∧ √↑D ≤ 2 * ↑n / 3

Proof of Theorem 17: the two facts used for the count of the instances, "s ≥ √D − 1 ≥ 3√D/4 because D ≥ 16, and √D ≤ √n ≤ 2n/3 because D ≤ n and we may assume n ≥ 3".

The sets W_ϱ

theorem Cslib.Algorithms.ExactTriangle.mem_residueClass {n p : ℕ} (wAB : Fin n → Fin n → ℤ) (hp : p ≠ 0) (ϱ : Fin p) (q : Fin n × Fin n) : q ∈ residueClass wAB p ϱ ↔ ϱ = resFin hp (wAB q.1 q.2)

A pair lies in W_ϱ exactly if ϱ is the residue of its weight.

theorem Cslib.Algorithms.ExactTriangle.existsUnique_mem_residueClass {n p : ℕ} (wAB : Fin n → Fin n → ℤ) (hp : p ≠ 0) (q : Fin n × Fin n) : ∃! ϱ : Fin p, q ∈ residueClass wAB p ϱ

Proof of Theorem 17, the sets W_ϱ for ϱ ∈ ℤ_p: every pair (a,b) ∈ A × B lies in exactly one of them.

The chunks

theorem Cslib.Algorithms.ExactTriangle.card_chunkOf_le {n D p : ℕ} (wAB : Fin n → Fin n → ℤ) (hD : 1 ≤ D) (hDn : D ≤ n) (ϱ : Fin p) (j : ℕ) : ↑(chunkOf wAB D p ϱ j).card ≤ ↑n ^ 2 / √↑D

Proof of Theorem 17: "cut it into chunks of at most n²/√D query pairs". (The chunks of W_ϱ cover it: biUnion_chunk.)

theorem Cslib.Algorithms.ExactTriangle.totalChunks_le {n D p : ℕ} (wAB : Fin n → Fin n → ℤ) (hD : 16 ≤ D) (hDn : D ≤ n) (hp : p ∈ D.sqrtPrimeWindow) : ↑(totalChunks wAB D p) ≤ ↑p + √↑D ∧ ↑p + √↑D ≤ 2 * √↑D

Proof of Theorem 17: "There are at most p + √D ≤ 2√D chunks in all."

NOTE. A chunk holds a whole number of pairs, at most ⌊n²/√D⌋, so the count is at most p + (n² − p)/⌊n²/√D⌋, and the second term can exceed √D slightly. The printed bound is still true, because the count is an integer, D is an integer and D ≤ n (sq_lt_mul_queryCap_add).

The instances

theorem Cslib.Algorithms.ExactTriangle.card_middle_lopInstance {n D g p : ℕ} (wAB wBC wAC : Fin n → Fin n → ℤ) (hD : 16 ≤ D) (hg1 : 1 ≤ g) (hp : p ∈ D.sqrtPrimeWindow) (ι : InstanceIndex p) : Fintype.card (lopInstance wAB wBC wAC D g p ι).M ≤ D

Proof of Theorem 17: "middle part C_k × ℤ_p, of size at most sp ≤ D". So each instance is an instance of Lop-AE-SparseTri(n, D).

theorem Cslib.Algorithms.ExactTriangle.mem_lopInstance_W {n D g p : ℕ} {wAB wBC wAC : Fin n → Fin n → ℤ} {ι : InstanceIndex p} {q : Fin n × Fin n} (hq : q ∈ (lopInstance wAB wBC wAC D g p ι).W) : q ∈ residueClass wAB p ι.1 ∧ Matrix.rankIn (residueClass wAB p ι.1) q / queryCap n D = ι.2.1

A query pair of the instance with index (ϱ, j, k) lies in W_ϱ, and j is the number of its chunk.

theorem Cslib.Algorithms.ExactTriangle.weightSum_modEq_zero_iff {n : ℕ} (wAB wBC wAC : Fin n → Fin n → ℤ) {p ϱ : ℤ} {a b : Fin n} (hϱ : wAB a b ≡ ϱ [ZMOD p]) (c : Fin n) : weightSum wAB wBC wAC a b c ≡ 0 [ZMOD p] ↔ wAC a c + ϱ ≡ -wBC b c [ZMOD p]

Proof of Theorem 17: "Within the chunk, the condition S(a,b,c) ≡ 0 (mod p) has become the equality w(a,c) + ϱ ≡ −w(b,c) of a label of (a,c) and a label of (b,c)".

theorem Cslib.Algorithms.ExactTriangle.hasCommonNeighbor_lopInstance_iff {n D g p : ℕ} (wAB wBC wAC : Fin n → Fin n → ℤ) (hp : p ≠ 0) {ι : InstanceIndex p} {q : Fin n × Fin n} (hq : q ∈ (lopInstance wAB wBC wAC D g p ι).W) : (lopInstance wAB wBC wAC D g p ι).HasCommonNeighbor q.1 q.2 ↔ ∃ c ∈ piece n D g ι.2.2, weightSum wAB wBC wAC q.1 q.2 c ≡ 0 [ZMOD ↑p]

Proof of Theorem 17: "a query pair (a,b) ∈ 𝒬 has a common neighbor if and only if some c ∈ C_k has S(a,b,c) ≡ 0 (mod p)".

theorem Cslib.Algorithms.ExactTriangle.mem_instanceIndices {n D g p : ℕ} (wAB : Fin n → Fin n → ℤ) (ι : InstanceIndex p) : ι ∈ instanceIndices wAB D g p ↔ ι.2.1 < Matrix.numChunks (residueClass wAB p ι.1) (queryCap n D) ∧ ι.2.2 < numPieces n D g

Proof of Theorem 17, "For each chunk 𝒬 ⊆ W_ϱ and each piece C_k": (ϱ, j, k) is the index of an instance exactly if j is the number of a chunk of W_ϱ and k the number of a piece.

theorem Cslib.Algorithms.ExactTriangle.card_instanceIndices {n : ℕ} (wAB : Fin n → Fin n → ℤ) (D g p : ℕ) : (instanceIndices wAB D g p).card = totalChunks wAB D p * numPieces n D g

There are as many instances as chunks times pieces.

theorem Cslib.Algorithms.ExactTriangle.card_instanceIndices_le {n D g p : ℕ} (wAB : Fin n → Fin n → ℤ) (hD : 16 ≤ D) (hDn : D ≤ n) (hg1 : 1 ≤ g) (hp : p ∈ D.sqrtPrimeWindow) : ↑(instanceIndices wAB D g p).card ≤ 4 * ↑n * ↑g

Proof of Theorem 17: "There are at most 2√D h ≤ 2√D(ng/s + 1) ≤ 4ng instances".

The neighborhoods in an instance

theorem Cslib.Algorithms.ExactTriangle.ncard_nbr_lopInstance_le {n D g p : ℕ} (wAB wBC wAC : Fin n → Fin n → ℤ) (hD : 16 ≤ D) (hg1 : 1 ≤ g) (hp : p ≠ 0) (ι : InstanceIndex p) : (∀ (a : Fin n), {v : (lopInstance wAB wBC wAC D g p ι).M | (lopInstance wAB wBC wAC D g p ι).adjA a v}.ncard ≤ pieceSize D g) ∧ ∀ (b : Fin n), {v : (lopInstance wAB wBC wAC D g p ι).M | (lopInstance wAB wBC wAC D g p ι).adjB v b}.ncard ≤ pieceSize D g

Section 3.1, "The reductions below [...] produce at most n²/√D query pairs and sets of at most √D elements", and Remark 20, "every vertex of A has O(√D/g) neighbors in the middle part": in an instance of the reduction, a vertex of A or of B has exactly one neighbor (c, σ) for every c ∈ C_k, hence at most ⌈s/g⌉ neighbors. (And ⌈s/g⌉ ≤ s ≤ √D; for g ≤ √D also ⌈s/g⌉ ≤ 2√D/g, pieceSize_le_two_mul_sqrt_div.)