Finite witness recovery from modular lopsided answers

Correct finite answers are ordinary Set.EqOn premises on the actual lopsided graphs. The recovery scans each accepted piece until it finds an exact zero. Distinct failed scans contain distinct modular false positives. No solver, native program or time oracle is assumed.

Main definitions

• scanPiece, runScans: finite witness search and number of scans.
• AnswersCorrect, IsScanOrder: correctness on queried pairs and a duplicate-free scan order.

Main results

• recovery_correct: sound and complete recovery with at most falsePositiveCount + 1 scans.
• card_failedScans_le: false-positive accounting.
• falsePositiveCount_add_one_mul_pieceSize_le: bound on the number of vertices scanned.

References

Adapted from Witnesses.lean and the minimal scan definitions in PaperStatements.lean at anthropics/formal-math@16a5ce41304fcdaea4e0be7c132e1c361dc26da5. Context: [AlmanWilliams2026, Section 3]. Quoted docstring fragments reproduce comments in the pinned formal source; other prose describes the local Lean API.

def Cslib.Algorithms.ExactTriangle.IsSearchAnswer {n : ℕ} (wAB wBC wAC : Fin n → Fin n → ℤ) (r : Option (Fin n × Fin n × Fin n)) : Prop

A finite search result returns a zero triangle, or certifies that no zero triangle exists. This specifies mathematical correctness only.

def Cslib.Algorithms.ExactTriangle.scanPiece {n : ℕ} (wAB wBC wAC : Fin n → Fin n → ℤ) (D g k : ℕ) (a b : Fin n) : Option (Fin n)

Proof of Theorem 17: "scan the piece C_k of its instance for a c with S(a,b,c) = 0". The vertices of the piece are tried in increasing order; the result is the first c found, or none if the scan fails.

def Cslib.Algorithms.ExactTriangle.acceptedPairs {n : ℕ} (wAB wBC wAC : Fin n → Fin n → ℤ) (D g p : ℕ) (ans : InstanceIndex p → Fin n × Fin n → Bool) : Finset (InstanceIndex p × Fin n × Fin n)

Proof of Theorem 17: "For every query pair that the oracle accepts". ans ι is the oracle's answer to the instance with index ι. The result is the set of all (instance, query pair of that instance) that the oracle accepts; each of them calls for one scan.

def Cslib.Algorithms.ExactTriangle.runScans {n : ℕ} (wAB wBC wAC : Fin n → Fin n → ℤ) (D g : ℕ) {p : ℕ} : List (InstanceIndex p × Fin n × Fin n) → Option (Fin n × Fin n × Fin n) × ℕ

Proof of Theorem 17: the scans, one after the other, over a list of accepted pairs: "We stop as soon as a zero triangle is found." The result is the triangle found (or none) together with the number of scans that were carried out.

def Cslib.Algorithms.ExactTriangle.IsScanOrder {n : ℕ} (wAB wBC wAC : Fin n → Fin n → ℤ) (D g p : ℕ) (ans : InstanceIndex p → Fin n × Fin n → Bool) (L : List (InstanceIndex p × Fin n × Fin n)) : Prop

Proof of Theorem 17: "For every query pair that the oracle accepts, scan [...]". The paper does not say in which order. L is an order of the scans: a list in which every accepted pair occurs exactly once.

Scans and accepted pairs

theorem Cslib.Algorithms.ExactTriangle.scanPiece_eq_some {n D g : ℕ} {wAB wBC wAC : Fin n → Fin n → ℤ} {k : ℕ} {a b c : Fin n} (h : scanPiece wAB wBC wAC D g k a b = some c) : c ∈ piece n D g k ∧ weightSum wAB wBC wAC a b c = 0

Proof of Theorem 17, "scan the piece C_k of its instance for a c with S(a,b,c) = 0": a c that a scan returns lies in the piece and has S(a,b,c) = 0.

theorem Cslib.Algorithms.ExactTriangle.scanPiece_eq_none_iff {n D g : ℕ} {wAB wBC wAC : Fin n → Fin n → ℤ} {k : ℕ} {a b : Fin n} : scanPiece wAB wBC wAC D g k a b = none ↔ ∀ c ∈ piece n D g k, weightSum wAB wBC wAC a b c ≠ 0

A scan fails exactly if the piece has no c with S(a,b,c) = 0.

@[reducible, inline]

abbrev Cslib.Algorithms.ExactTriangle.scanOf {n p : ℕ} (wAB wBC wAC : Fin n → Fin n → ℤ) (D g : ℕ) (x : InstanceIndex p × Fin n × Fin n) : Option (Fin n)

The scan that belongs to x = ((ϱ, j, k), (a, b)), a query pair (a, b) of the instance with index (ϱ, j, k): the piece C_k is scanned for the pair (a, b).

def Cslib.Algorithms.ExactTriangle.AnswersCorrect {n : ℕ} (wAB wBC wAC : Fin n → Fin n → ℤ) (D g p : ℕ) (ans : InstanceIndex p → Fin n × Fin n → Bool) : Prop

The hypothesis on the oracle: ans ι is a correct answer to the instance with index ι, for every instance of the reduction.

def Cslib.Algorithms.ExactTriangle.failedScans {n : ℕ} (wAB wBC wAC : Fin n → Fin n → ℤ) (D g p : ℕ) (ans : InstanceIndex p → Fin n × Fin n → Bool) : Finset (InstanceIndex p × Fin n × Fin n)

Proof of Theorem 17: a "failed scan, of a piece C_k for a pair (a,b)": the oracle accepted the pair in the instance, and the piece contains no c with S(a,b,c) = 0.

theorem Cslib.Algorithms.ExactTriangle.mem_acceptedPairs {n D g p : ℕ} {wAB wBC wAC : Fin n → Fin n → ℤ} {ans : InstanceIndex p → Fin n × Fin n → Bool} {ι : InstanceIndex p} {q : Fin n × Fin n} : (ι, q) ∈ acceptedPairs wAB wBC wAC D g p ans ↔ ι ∈ instanceIndices wAB D g p ∧ q ∈ (lopInstance wAB wBC wAC D g p ι).W ∧ ans ι q = true

The accepted pairs: an index of an instance, a query pair of that instance, and the answer "yes".

The sentences of the paragraph "Witnesses"

theorem Cslib.Algorithms.ExactTriangle.exists_mem_acceptedPairs {n D g p : ℕ} {wAB wBC wAC : Fin n → Fin n → ℤ} {ans : InstanceIndex p → Fin n × Fin n → Bool} (hD : 16 ≤ D) (hDn : D ≤ n) (hg1 : 1 ≤ g) (hp : p ≠ 0) (hans : AnswersCorrect wAB wBC wAC D g p ans) {a b c : Fin n} (h0 : weightSum wAB wBC wAC a b c = 0) : ∃ (ϱ : Fin p) (j : ℕ) (k : ℕ), ((ϱ, j, k), a, b) ∈ acceptedPairs wAB wBC wAC D g p ans ∧ c ∈ piece n D g k

Proof of Theorem 17: "A zero triangle is always found, since its c lies in some piece and makes the oracle accept its pair."

theorem Cslib.Algorithms.ExactTriangle.exists_isFalsePositive_of_mem_failedScans {n D g p : ℕ} {wAB wBC wAC : Fin n → Fin n → ℤ} {ans : InstanceIndex p → Fin n × Fin n → Bool} (hp : p ≠ 0) (hans : AnswersCorrect wAB wBC wAC D g p ans) {ϱ : Fin p} {j k : ℕ} {a b : Fin n} (hx : ((ϱ, j, k), a, b) ∈ failedScans wAB wBC wAC D g p ans) : ∃ c ∈ piece n D g k, IsFalsePositive wAB wBC wAC p (a, b, c)

Proof of Theorem 17: "A failed scan, of a piece C_k for a pair (a,b), contains a c ∈ C_k with S(a,b,c) ≡ 0 (mod p) but S(a,b,c) ≠ 0, that is, a false positive (a,b,c) of p".

theorem Cslib.Algorithms.ExactTriangle.eq_of_mem_acceptedPairs {n D g p : ℕ} {wAB wBC wAC : Fin n → Fin n → ℤ} {ans : InstanceIndex p → Fin n × Fin n → Bool} {ϱ ϱ' : Fin p} {j j' k k' : ℕ} {q : Fin n × Fin n} (hx : ((ϱ, j, k), q) ∈ acceptedPairs wAB wBC wAC D g p ans) (hy : ((ϱ', j', k'), q) ∈ acceptedPairs wAB wBC wAC D g p ans) {c : Fin n} (hc : c ∈ piece n D g k) (hc' : c ∈ piece n D g k') : (ϱ, j, k) = (ϱ', j', k')

Proof of Theorem 17: "distinct scans contain distinct false positives": a triple (a,b,c) belongs to the scan of at most one accepted pair.

theorem Cslib.Algorithms.ExactTriangle.card_le_falsePositiveCount_of_distinct_scans {n p : ℕ} (wAB wBC wAC : Fin n → Fin n → ℤ) {σ : Type u_1} (s : Finset σ) (contains : σ → Fin n × Fin n × Fin n → Prop) (hfalse : ∀ x ∈ s, ∃ (t : Fin n × Fin n × Fin n), contains x t ∧ IsFalsePositive wAB wBC wAC p t) (hdistinct : ∀ (t : Fin n × Fin n × Fin n), ∀ x ∈ s, ∀ y ∈ s, contains x t → contains y t → x = y) : s.card ≤ falsePositiveCount wAB wBC wAC p

Proof of Theorem 17: "distinct scans contain distinct false positives, so there are at most F(p) failed scans", for any finite family s of scans and any notion "the scan x contains the triple t". This applies to the accepted-pair scans in card_failedScans_le.

theorem Cslib.Algorithms.ExactTriangle.card_failedScans_le {n D g p : ℕ} {wAB wBC wAC : Fin n → Fin n → ℤ} {ans : InstanceIndex p → Fin n × Fin n → Bool} (hp : p ≠ 0) (hans : AnswersCorrect wAB wBC wAC D g p ans) : (failedScans wAB wBC wAC D g p ans).card ≤ falsePositiveCount wAB wBC wAC p

Proof of Theorem 17: "so there are at most F(p) failed scans".

theorem Cslib.Algorithms.ExactTriangle.pieceSize_le_two_mul_sqrt_div {D g : ℕ} (hg1 : 1 ≤ g) (hg : ↑g ≤ √↑D) : ↑(pieceSize D g) ≤ 2 * √↑D / ↑g

Proof of Theorem 17: the length of a scan, the O(√D/g) in "the scans cost O((F(p) + 1)√D/g)": a piece has at most ⌈s/g⌉ ≤ 2√D/g vertices.

theorem Cslib.Algorithms.ExactTriangle.falsePositiveCount_add_one_mul_pieceSize_le {n D g p : ℕ} {κ : ℝ} (wAB wBC wAC : Fin n → Fin n → ℤ) (hD : 16 ≤ D) (hDn : D ≤ n) (hg1 : 1 ≤ g) (hg : ↑g ≤ √↑D) (hκ : 1 ≤ κ) (hT : WeightsBoundedBy wAB wBC wAC (↑n ^ κ)) (hp : IsSelectedPrime wAB wBC wAC D p) : (↑(falsePositiveCount wAB wBC wAC p) + 1) * ↑(pieceSize D g) ≤ (2 * falsePositiveConst + 2) * (κ * ↑n ^ 3 * Real.log ↑n / ↑g)

For 16 ≤ D ≤ n, 1 ≤ g ≤ sqrt D, κ ≥ 1 and edge weights bounded by n^κ, bound (falsePositiveCount + 1) * pieceSize at any selected prime by (2 * falsePositiveConst + 2) * κ * n^3 * log n / g. This arithmetic estimate counts candidate vertices rather than native instructions.

The output of the reduction

theorem Cslib.Algorithms.ExactTriangle.recovery_correct {n D g p : ℕ} (hD : 16 ≤ D) (hDn : D ≤ n) (hg1 : 1 ≤ g) (wAB wBC wAC : Fin n → Fin n → ℤ) (hp : IsSelectedPrime wAB wBC wAC D p) {ans : InstanceIndex p → Fin n × Fin n → Bool} (hans : AnswersCorrect wAB wBC wAC D g p ans) {L : List (InstanceIndex p × Fin n × Fin n)} (hL : IsScanOrder wAB wBC wAC D g p ans L) : IsSearchAnswer wAB wBC wAC (runScans wAB wBC wAC D g L).1 ∧ (runScans wAB wBC wAC D g L).2 ≤ falsePositiveCount wAB wBC wAC p + 1

Theorem 17, correctness. Given any correct answers of an oracle for Lop-AE-SparseTri to the instances of the reduction, and whatever the order L of the scans, the reduction's output is correct: it is a zero triangle if one exists, and none otherwise. It carries out at most F(p) + 1 scans ("We stop as soon as a zero triangle is found").

theorem Cslib.Algorithms.ExactTriangle.exists_isScanOrder {n : ℕ} (wAB wBC wAC : Fin n → Fin n → ℤ) (D g p : ℕ) (ans : InstanceIndex p → Fin n × Fin n → Bool) : ∃ (L : List (InstanceIndex p × Fin n × Fin n)), IsScanOrder wAB wBC wAC D g p ans L

Every finite set of accepted queries admits a duplicate-free scan order.

theorem Cslib.Algorithms.ExactTriangle.exists_answersCorrect {n : ℕ} (wAB wBC wAC : Fin n → Fin n → ℤ) (D g p : ℕ) : ∃ (ans : InstanceIndex p → Fin n × Fin n → Bool), AnswersCorrect wAB wBC wAC D g p ans

Correct finite answer tables exist. This is a finite specification, with no solver or complexity claim. Values outside the queried edges remain unconstrained.

theorem Cslib.Algorithms.ExactTriangle.answersCorrect_of_counting {n : ℕ} (wAB wBC wAC : Fin n → Fin n → ℤ) (D g p : ℕ) (counts : InstanceIndex p → Fin n × Fin n → ℕ) (hcounts : ∀ ι ∈ instanceIndices wAB D g p, Set.EqOn (counts ι) (fun (q : Fin n × Fin n) => (lopInstance wAB wBC wAC D g p ι).commonNeighborCount q.1 q.2) ↑(lopInstance wAB wBC wAC D g p ι).W) : AnswersCorrect wAB wBC wAC D g p fun (ι : InstanceIndex p) (q : Fin n × Fin n) => decide (counts ι q ≠ 0)

Correct finite common-neighbor counts supply the Boolean answers used by recovery. This connects directly to the lopsided matrix/counting interface.

theorem Cslib.Algorithms.ExactTriangle.recovery_vertexBound {n D g p : ℕ} {κ : ℝ} (hD : 16 ≤ D) (hDn : D ≤ n) (hg1 : 1 ≤ g) (hg : ↑g ≤ √↑D) (hκ : 1 ≤ κ) (wAB wBC wAC : Fin n → Fin n → ℤ) (hw : WeightsBoundedBy wAB wBC wAC (↑n ^ κ)) (hp : IsSelectedPrime wAB wBC wAC D p) {ans : InstanceIndex p → Fin n × Fin n → Bool} (hans : AnswersCorrect wAB wBC wAC D g p ans) {L : List (InstanceIndex p × Fin n × Fin n)} (hL : IsScanOrder wAB wBC wAC D g p ans L) : IsSearchAnswer wAB wBC wAC (runScans wAB wBC wAC D g L).1 ∧ ↑(runScans wAB wBC wAC D g L).2 * ↑(pieceSize D g) ≤ (2 * falsePositiveConst + 2) * (κ * ↑n ^ 3 * Real.log ↑n / ↑g)

The recovery scan examines at most the uniform false-positive bound times the piece size. This counts candidate vertices only; it is not a charged native running-time theorem.

theorem Cslib.Algorithms.ExactTriangle.recovery_eq_none_iff {n D g p : ℕ} (hD : 16 ≤ D) (hDn : D ≤ n) (hg1 : 1 ≤ g) (wAB wBC wAC : Fin n → Fin n → ℤ) (hp : IsSelectedPrime wAB wBC wAC D p) {ans : InstanceIndex p → Fin n × Fin n → Bool} (hans : AnswersCorrect wAB wBC wAC D g p ans) {L : List (InstanceIndex p × Fin n × Fin n)} (hL : IsScanOrder wAB wBC wAC D g p ans L) : (runScans wAB wBC wAC D g L).1 = none ↔ ¬HasZeroTriangle wAB wBC wAC

Finite reduction equivalence: scanning all accepted queries returns none exactly when the original three matrices have no zero triangle. Any duplicate-free scan order works.