Cancellation of a finite bad subfamily in a torsion-free additive group

Proved

ProofsInTheBook.Chapter30.total_sum_eq_good_sum_of_bad_sign_reversing

by xiangyazi24 · Sep 12, 2026 · Mathlib c5ea003 (Lean v4.30.0)

combinatoricsconditional-identitydeterminantsfinite-sumslean4proofs-from-the-book

Let A be a finite type with decidable equality, and let R be an additive commutative group whose addition is torsion-free. Let $\mathrm{bad}:A\to\mathrm{Prop}$ be decidable. Suppose a bijection $\tau_B:B\simeq B$ is supplied on $B=\{x\in A:\mathrm{bad}(x)\}$ , together with $w:A\to R$ satisfying $w(\tau_B(x))=-w(x)$ for every $x\in B$ . Then

\sum_{x\in A}w(x)=\sum_{\substack{x\in A\\\neg\mathrm{bad}(x)}}w(x).

The bad-subfamily bijection and sign-reversal identity are hypotheses; the bijection need not be an involution.

Preamble

import Mathlib
import Definitions.Def_ProofsInTheBook_Chapter30
open ProofsInTheBook.Chapter30
open Matrix BigOperators

Formal statement

theorem ProofsInTheBook.Chapter30.total_sum_eq_good_sum_of_bad_sign_reversing {α R : Type*} [Fintype α]
    [DecidableEq α] [AddCommGroup R] [IsAddTorsionFree R]
    (bad : α → Prop) [DecidablePred bad] (τbad : {x : α // bad x} ≃ {x : α // bad x})
    (w : α → R) (hw : ∀ x : {x : α // bad x}, w (τbad x).1 = -w x.1) :
    (∑ x : α, w x) = ∑ x ∈ (Finset.univ.filter fun x : α => ¬ bad x), w x := by sorry

Source

Exact repository declaration: https://github.com/xiangyazi24/proof_in_the_book/blob/88d88d141768cded75e782c525ef1bf04b8fe220/ProofsInTheBook/Chapter30.lean#L96. PathCountSystem hypotheses: https://github.com/xiangyazi24/proof_in_the_book/blob/88d88d141768cded75e782c525ef1bf04b8fe220/ProofsInTheBook/Chapter30.lean#L435. Explicit scope limitation: https://github.com/xiangyazi24/proof_in_the_book/blob/88d88d141768cded75e782c525ef1bf04b8fe220/ProofsInTheBook/Chapter30.lean#L578. Repository topic: “Lattice paths and determinants.” No edition-specific chapter mapping or geometric application is asserted.

View graph