card_bind_le_sum
The inequality asserts that the cardinality of the biUnion of sets f(z) over a finite set s is at most the sum of the individual cardinalities of f(z). Researchers bounding neighbor expansion in discrete causal graphs cite it when deriving linear growth controls from a bounded-degree step relation. The proof is a direct one-line wrapper around the Mathlib lemma Finset.card_biUnion_le.
claim$|s.biUnion f| ≤ ∑_{z ∈ s} |f(z)|$ for any finite set $s$ and map $f$ sending each element of $s$ to a finite set.
background
The ConeBound module supplies minimal local definitions to avoid heavy imports while providing ball growth bounds under a bounded-degree step relation. It equips the causality setting with cardinality tools for unions of neighbor sets in a graph-like structure. The lemma supplies the basic subadditivity fact needed before degree bounds are applied.
proof idea
The proof is a one-line wrapper that applies Finset.card_biUnion_le.
why it matters in Recognition Science
It is invoked inside card_bind_neighbors_le to obtain the linear bound (s.biUnion neighbors).card ≤ d * s.card, which controls cone expansion in the causality module. This step supports discrete light-cone estimates consistent with the Recognition framework's eight-tick octave and three-dimensional spatial structure. No open scaffolding questions are closed by this declaration.
scope and limits
- Does not claim equality between union cardinality and the sum.
- Does not require the image sets f(z) to be pairwise disjoint.
- Does not extend to infinite index sets.
- Does not encode any metric or ordering on the type α.
Lean usage
have h1 := card_bind_le_sum s (fun z => B.neighbors z)formal statement (Lean)
75theorem card_bind_le_sum (s : Finset α) (f : α → Finset α) :
76 (s.biUnion f).card ≤ Finset.sum s (fun z => (f z).card) :=
proof body
One-line wrapper that applies Finset.card_biUnion_le.
77 Finset.card_biUnion_le