Weighted Weisner cancellation in a finite lattice

Proved

FiniteLattice.weighted_weisner_cancellation

by Yuxuan Xu · Sep 22, 2026 · Mathlib 0df444a (Lean v4.33.1)

combinatoricslattice-theorymobius-inversion

Let $L$ be a finite lattice, let $d,a,b\in L$ with $a\le b$ , and let $w:L\to\mathbb Q$ . Suppose that for every $x$ in the interval $[a,b]$ , the weighted prefix sum

\sum_{d\le c\le x} w(c)=0.

Then the weighted join fibre at $b$ vanishes:

\sum_{\substack{d\le c\le b\\c\vee a=b}}w(c)=0.

No relation between $d$ and $a$ is assumed. This is a complete finite-lattice statement, not a conditional reduction.

Preamble

import Mathlib
open Finset
attribute [local instance] Classical.propDecidable

Formal statement

namespace FiniteLattice

theorem weighted_weisner_cancellation {L : Type*} [Lattice L] [Fintype L] [DecidableEq L]
    (d a b : L) (w : L → ℚ) (hab : a ≤ b)
    (hzero : ∀ x : L, a ≤ x → x ≤ b →
      (∑ c ∈ (Finset.univ : Finset L).filter (fun c => d ≤ c ∧ c ≤ x), w c) = 0) :
    (∑ c ∈ (Finset.univ : Finset L).filter
      (fun c => d ≤ c ∧ c ≤ b ∧ c ⊔ a = b), w c) = 0 := by
  sorry

end FiniteLattice

Source

A proved weighted prefix-cancellation form whose mechanism is the order-dual of Weisner's theorem. It is our weighted generalization, not a verbatim formula in the source. See Richard P. Stanley, Enumerative Combinatorics, Volume 1, author manuscript, Corollary 3.9.3 (p. 313), applied in the order dual: https://math.mit.edu/~rstan/ec/ec1.pdf.

View graph