Integer triangle sums and magnitude bounds

Main definitions

• weightSum: the sum of the three supplied integer edge weights.
• WeightsBoundedBy: a shared real bound on their absolute values.

Main results

• abs_weightSum_le: a triangle's magnitude is at most three times the edge bound.

References

Adapted from the weight sum and bound definitions in Anthropic's PaperStatements.lean and the triangle inequality in its Hashing.lean. The existing HasZeroTriangle remains the decision predicate.

def Cslib.Algorithms.ExactTriangle.weightSum {n : ℕ} (wAB wBC wAC : Fin n → Fin n → ℤ) (a b c : Fin n) : ℤ

Sum of the A–B, B–C and A–C weights at a triangle.

def Cslib.Algorithms.ExactTriangle.WeightsBoundedBy {n : ℕ} (wAB wBC wAC : Fin n → Fin n → ℤ) (U : ℝ) : Prop

Every supplied edge weight has absolute value at most U.

theorem Cslib.Algorithms.ExactTriangle.abs_weightSum_le {n : ℕ} (wAB wBC wAC : Fin n → Fin n → ℤ) {U : ℝ} (h : WeightsBoundedBy wAB wBC wAC U) (a b c : Fin n) : ↑|weightSum wAB wBC wAC a b c| ≤ 3 * U

The three edge bounds imply a threefold bound on every triangle sum.