kBucketSum: k-way bucketed enumeration

Polymorphic substrate generalising the family of bucket-aggregator patterns used in planar multi-graft proofs (Foissy 2021, Marcolli-Chomsky-Berwick 2025, Oudom-Guin 2004).

For each item in remaining, a choice from idx selects a bucket; items accumulate into the per-bucket lists pres. At empty remaining, the leaf function leaf : (τ → List ι) → Multiset ω consumes the final bucket assignment and produces the output.

This unifies the previously hand-rolled hostBucketSum (2 buckets, parallel cartesian leaf), hostTripleSum (3 buckets, parallel triple bind leaf), and assocBucketSum (2 buckets, iterated bind leaf), and provides a one-liner pattern for future variants like the 5-bucket aggregator needed for the deep case of assocBucketSum's bridge.

Status

[UPSTREAM] candidate. Sorry-free.

§1: bucketSlice — items routed to a single bucket

def RootedTree.Planar.Pathed.bucketSlice {τ : Type u} {ι : Type v} [DecidableEq τ] (Ts : List ι) (assn : List τ) (t : τ) : List ι

The slice of items from Ts whose assignment in assn equals t. Pairs Ts with assn, then collects items whose paired assignment matches the target bucket label.

Equations

• RootedTree.Planar.Pathed.bucketSlice Ts assn t = List.filterMap (fun (p : ι × τ) => if p.2 = t then some p.1 else none) (Ts.zip assn)

@[simp]

theorem RootedTree.Planar.Pathed.bucketSlice_nil_left {τ : Type u} {ι : Type v} [DecidableEq τ] (assn : List τ) (t : τ) : bucketSlice [] assn t = []

@[simp]

theorem RootedTree.Planar.Pathed.bucketSlice_nil_right {τ : Type u} {ι : Type v} [DecidableEq τ] (Ts : List ι) (t : τ) : bucketSlice Ts [] t = []

theorem RootedTree.Planar.Pathed.bucketSlice_cons_cons {τ : Type u} {ι : Type v} [DecidableEq τ] (x : ι) (Ts : List ι) (s : τ) (assn : List τ) (t : τ) : bucketSlice (x :: Ts) (s :: assn) t = (if s = t then [x] else []) ++ bucketSlice Ts assn t

§2: kBucketSum — definition and basic equation lemmas

def RootedTree.Planar.Pathed.kBucketSum {τ : Type u} {ι : Type v} {ω : Type w} [DecidableEq τ] (idx : List τ) (leaf : (τ → List ι) → Multiset ω) (pres : τ → List ι) : List ι → Multiset ω

k-way bucketed enumeration. For each item in remaining, bind over idx to choose a bucket; the accumulator pres t for that bucket grows by one item. At empty remaining, apply leaf.

Equations

• RootedTree.Planar.Pathed.kBucketSum idx leaf pres [] = leaf pres
• RootedTree.Planar.Pathed.kBucketSum idx leaf pres (x_1 :: rest) = (↑idx).bind fun (t : τ) => RootedTree.Planar.Pathed.kBucketSum idx leaf (Function.update pres t (pres t ++ [x_1])) rest

theorem RootedTree.Planar.Pathed.kBucketSum_nil_remaining {τ : Type u} {ι : Type v} {ω : Type w} [DecidableEq τ] (idx : List τ) (leaf : (τ → List ι) → Multiset ω) (pres : τ → List ι) : kBucketSum idx leaf pres [] = leaf pres

theorem RootedTree.Planar.Pathed.kBucketSum_cons_remaining {τ : Type u} {ι : Type v} {ω : Type w} [DecidableEq τ] (idx : List τ) (leaf : (τ → List ι) → Multiset ω) (pres : τ → List ι) (x : ι) (rest : List ι) : kBucketSum idx leaf pres (x :: rest) = (↑idx).bind fun (t : τ) => kBucketSum idx leaf (Function.update pres t (pres t ++ [x])) rest

§3: assignment rewrite

theorem RootedTree.Planar.Pathed.kBucketSum_assignment_rewrite {τ : Type u} {ι : Type v} {ω : Type w} [DecidableEq τ] (idx : List τ) (leaf : (τ → List ι) → Multiset ω) (pres : τ → List ι) (Ts : List ι) : kBucketSum idx leaf pres Ts = (↑(listChoices idx Ts.length)).bind fun (assn : List τ) => leaf fun (t : τ) => pres t ++ bucketSlice Ts assn t

Key identity: kBucketSum over remaining items Ts equals a single bind over all length-Ts.length assignments (drawn from idx) of the leaf applied to the accumulators augmented by the per-bucket slice of Ts. Generalises hostBucketSum_assignment_rewrite and assocBucketSum_assignment_rewrite.