Host-append decomposition for RoseTree-level multi-tree insertion

The RoseTree-level substrate for Nonplanar.insertionMultiset_add_host: multi-graft into a concatenated host list host_A ++ host_B decomposes as a sum over boolean assignments of guests to either host_A or host_B, with each side recursively multi-grafted independently.

Architecture

The substrate is kBucketSum (§0): a polymorphic k-way bucketed enumeration that assigns each guest to one of idx buckets, then applies a leaf function to the final assignment. Its key identity kBucketSum_assignment_rewrite collapses the per-guest recursion into a single bind over all bucket assignments.

hostBucketSum (§1) is the 2-bucket (Bool-indexed) instance splitting guests between two arbitrary host forests, with a parallel cartesian-product leaf; hostBucketSum_assignment_rewrite is derived from the general identity via hostBucketSum_eq_kBucketSum. The bridge hostBucketSum_eq_insertionForest is proved by induction on host_A.

This is the RoseTree-level companion to the Nonplanar.insertionMultiset_add_host combinatorial identity used in GrossmanLarsonAssoc.lean's Oudom-Guin Prop 2.7.iii proof.

Status

[UPSTREAM] candidate. Sorry-free.

§0: kBucketSum — k-way bucketed enumeration substrate

Polymorphic substrate generalising the bucket-aggregator patterns used in RoseTree-level 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 consumes the final assignment. hostBucketSum (§1, 2 buckets) and hostTripleSum (§3, 3 buckets) are instances.

def RoseTree.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.

Equations

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

@[simp]

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

@[simp]

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

theorem RoseTree.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

theorem RoseTree.Pathed.bucketSlice_bool_true {ι : Type v} (Ts : List ι) (assn : List Bool) : bucketSlice Ts assn true = List.filterMap (fun (p : ι × Bool) => if p.2 = true then some p.1 else none) (Ts.zip assn)

The Bool-true bucket slice keeps the items whose bit is set.

theorem RoseTree.Pathed.bucketSlice_bool_false {ι : Type v} (Ts : List ι) (assn : List Bool) : bucketSlice Ts assn false = List.filterMap (fun (p : ι × Bool) => if p.2 = true then none else some p.1) (Ts.zip assn)

The Bool-false bucket slice keeps the items whose bit is unset.

def RoseTree.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

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

theorem RoseTree.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 RoseTree.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

theorem RoseTree.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.

§1: hostBucketSum aggregator

Splits a list of guest trees into two buckets — those destined for host_A and those destined for host_B — by accumulating boolean choices for each remaining guest. At the leaf, the cartesian product of each side's insertionForest is concatenated.

def RoseTree.Pathed.hostBucketSum {α : Type u_1} (host_A host_B : List (RoseTree α)) : List (RoseTree α) → List (RoseTree α) → List (RoseTree α) → Multiset (List (RoseTree α))

Two-host aggregator: at the leaf (no remaining guests), produce the cartesian product of insertionForest host_A pre_A and insertionForest host_B pre_B, joined by list concatenation. At a cons, bind over [true, false] and extend either bucket.

Equations

• One or more equations did not get rendered due to their size.

theorem RoseTree.Pathed.hostBucketSum_nil_remaining {α : Type u_1} (host_A host_B pre_A pre_B : List (RoseTree α)) : hostBucketSum host_A host_B pre_A pre_B [] = Multiset.map (fun (p : List (RoseTree α) × List (RoseTree α)) => p.1 ++ p.2) (insertionForest host_A pre_A ×ˢ insertionForest host_B pre_B)

theorem RoseTree.Pathed.hostBucketSum_eq_kBucketSum {α : Type u_1} (host_A host_B pre_A pre_B Ts : List (RoseTree α)) : hostBucketSum host_A host_B pre_A pre_B Ts = kBucketSum [true, false] (fun (pres' : Bool → List (RoseTree α)) => Multiset.map (fun (p : List (RoseTree α) × List (RoseTree α)) => p.1 ++ p.2) (insertionForest host_A (pres' true) ×ˢ insertionForest host_B (pres' false))) (fun (b : Bool) => if b = true then pre_A else pre_B) Ts

hostBucketSum as a kBucketSum instance: 2 buckets indexed by Bool, parallel cartesian-product leaf.

theorem RoseTree.Pathed.hostBucketSum_assignment_rewrite {α : Type u_1} (host_A host_B pre_A pre_B Ts : List (RoseTree α)) : hostBucketSum host_A host_B pre_A pre_B Ts = (↑(listChoices [true, false] Ts.length)).bind fun (α_1 : List Bool) => hostBucketSum host_A host_B (pre_A ++ List.filterMap (fun (p : RoseTree α × Bool) => if p.2 = true then some p.1 else none) (Ts.zip α_1)) (pre_B ++ List.filterMap (fun (p : RoseTree α × Bool) => if p.2 = true then none else some p.1) (Ts.zip α_1)) []

Assignment rewrite: hostBucketSum accumulating into pre_A/pre_B over remaining guests Ts equals the sum over [true, false]- assignments of Ts of hostBucketSum on empty remaining with the accumulators augmented by the partition. Specialises the general kBucketSum_assignment_rewrite to the 2-bucket Bool instance.

§2: Base case — hostBucketSum [] host_B [] [] guests = insertionForest host_B guests

When host_A = [], only the "all-false" boolean assignment can produce a non-zero insertionForest [] _ ≠ 0, since insertionForest [] _ = 0 whenever the second argument is non-empty. The all-false path gives ({[]} ×ˢ insertionForest host_B guests).map (++), which collapses to insertionForest host_B guests.

§3: 3-bucket aggregator and the full bridge

The headline RoseTree-level identity. Combined with the Nonplanar lift below (via Quotient.out + host-Perm invariance lifted through Nonplanar.mk), this yields the substrate for Nonplanar.insertionMultiset_add_host.

The proof goes by induction on host_A. The base case (host_A = []) is hostBucketSum_nil_A (above). The inductive case host_A = T :: F_A proceeds via a 3-bucket aggregator hostTripleSum that explicitly partitions guests into three buckets {T-bucket, F_A-bucket, host_B-bucket}. We then prove:

• hostBucketSum_eq_hostTripleSum: LHS (the 2-step hostBucketSum) equals the 3-bucket sum (reorganizing "A-vs-B then T-vs-F_A within A").
• insertionForest_cons_append_eq_hostTripleSum: RHS (the insertionForest over T :: (F_A ++ host_B)) equals the 3-bucket sum (using the outer IH on F_A to convert insertionForest (F_A ++ host_B) Y into hostBucketSum F_A host_B, reorganizing "T-vs-rest then F_A-vs-host_B within rest").

theorem RoseTree.Pathed.insertionForest_cons_assignment {α : Type u_1} (T : RoseTree α) (F X : List (RoseTree α)) : insertionForest (T :: F) X = (↑(listChoices [true, false] X.length)).bind fun (α_1 : List Bool) => (insertion T (List.filterMap (fun (p : RoseTree α × Bool) => if p.2 = true then some p.1 else none) (X.zip α_1))).bind fun (T' : RoseTree α) => Multiset.map (fun (F' : List (RoseTree α)) => T' :: F') (insertionForest F (List.filterMap (fun (p : RoseTree α × Bool) => if p.2 = true then none else some p.1) (X.zip α_1)))

Uniform decomposition of insertionForest (T :: F) X over [true, false]-assignments of X's elements to the T-bucket or F-bucket. Works for empty X via singleton bind.

theorem RoseTree.Pathed.mem_listChoices_length {β : Type u_2} (xs : List β) (n : ℕ) (α : List β) : α ∈ listChoices xs n → α.length = n

Length lemma: every element of listChoices xs n has length exactly n. Used in the cons case of hostBucketSum_eq_hostTripleSum_aux to invoke List.zip_append.

§4: Connecting hostTripleSum with insertion T ∘ hostBucketSum F_A host_B

Lemma A reduces hostBucketSum (T :: F_A) host_B [] [] guests to hostTripleSum T F_A host_B [] [] [] guests. To complete the bridge, we need hostTripleSum T F_A host_B [] [] [] guests = insertionForest (T :: (F_A ++ host_B)) guests.

Approach: generalize to hostTripleSum_T_split:

hostTripleSum T F_A host_B pre_T pre_FA pre_B remaining =
  bind α over remaining.length:
    (insertion T (pre_T ++ filter_true remaining α)).bind T' =>
      (hostBucketSum F_A host_B pre_FA pre_B (filter_false remaining α)).map (T' :: ·)

Then for pre_T = pre_FA = pre_B = [], combine with the IH hostBucketSum F_A host_B = insertionForest (F_A ++ host_B) to close the bridge.

Requires listChoices_succ_cons_bind (the cons-prepending analog of listChoices_succ_append_bind).

theorem RoseTree.Pathed.hostBucketSum_eq_insertionForest {α : Type u_1} (host_A host_B guests : List (RoseTree α)) : hostBucketSum host_A host_B [] [] guests = insertionForest (host_A ++ host_B) guests

§5: Host-Perm invariance at the multiset-of-multiset level

insertionForest is invariant under permutation of host trees, but only at the level where output lists are wrapped via Multiset.ofList ∘ List.map mk (i.e., the level used by Nonplanar.insertionMultiset). The list structure of inner outputs (which is host-position-correlated) is discarded by this outer wrapper, allowing host trees to be permuted without changing the multiset-of-multiset image.

The key combinatorial lemma is the swap symmetry of two adjacent host trees, which we prove via hostTripleSum's 3-bucket structure: when the F_A bucket is a singleton [T₂], swapping the T-bucket with the F_A-bucket gives a configuration symmetric in (T₁, T₂) at the multiset level.

theorem RoseTree.Pathed.insertionForest_perm_host_msform {α : Type u_1} {host host' : List (RoseTree α)} (h : host.Perm host') (gs : List (RoseTree α)) : Multiset.map (fun (L : List (RoseTree α)) => ↑(List.map RootedTree.Nonplanar.mk L)) (insertionForest host gs) = Multiset.map (fun (L : List (RoseTree α)) => ↑(List.map RootedTree.Nonplanar.mk L)) (insertionForest host' gs)

Host-Perm invariance at the multiset-of-multiset level: when host trees are permuted, the (insertionForest host gs).map (Multiset.ofList ∘ List.map mk) is unchanged.

This is the key invariance used by Nonplanar.insertionMultiset_add_host (and similar Nonplanar-side lifts) to bridge (A + B).toList.map Q.out with A.toList.map Q.out ++ B.toList.map Q.out.

§6: Bit-vector ↔ powerset bridge

For a list l : List β, bit-vectors of length |l| enumerate sublists of l (the elements where the bit is true). At the multiset level, the collection of (filter_t, filter_f) pairs over all bit-vectors equals the collection of (s, ↑l - s) over s ∈ (↑l).powerset. Used by Nonplanar.insertionMultiset_add_host to bridge the hostBucketSum_assignment_rewrite form (bind over bit-vectors) with the C.powerset.bind form on the RHS.

theorem RoseTree.Pathed.mem_listChoices_bool_length (n : ℕ) (assn : List Bool) : assn ∈ listChoices [true, false] n → assn.length = n

Length lemma: every element of listChoices [b₁, b₂] n has length exactly n. A re-export of the existing mem_listChoices_length for [true, false].

theorem RoseTree.Pathed.listChoices_bridge_powerset_paired {β : Type u_2} [DecidableEq β] (l : List β) : Multiset.map (fun (assn : List Bool) => have s_t := ↑(List.filterMap (fun (p : β × Bool) => if p.2 = true then some p.1 else none) (l.zip assn)); have s_f := ↑(List.filterMap (fun (p : β × Bool) => if p.2 = true then none else some p.1) (l.zip assn)); (s_t, s_f)) ↑(listChoices [true, false] l.length) = Multiset.map (fun (s : Multiset β) => (s, ↑l - s)) (↑l).powerset

Bit-vector ↔ powerset bridge (paired form): enumerating bit-vectors and pairing (filter_t, filter_f) gives the powerset paired with complement (s, ↑l - s). Derived from the single-component version + filterMap_f_eq_sub.

§7: Guest-multiset invariance at the msform level

(insertionForest host gs).map msform depends only on the multiset image of gs.map mk, not on the RoseTree representatives or order. This combines guest-Perm invariance + guest-PermEquiv invariance into a single lemma matching the level used by Nonplanar.insertionMultiset.

theorem RoseTree.Pathed.insertionForest_msform_invariance_guests {α : Type u_1} (host : List (RoseTree α)) {gs1 gs2 : List (RoseTree α)} (h : (List.map RootedTree.Nonplanar.mk gs1).Perm (List.map RootedTree.Nonplanar.mk gs2)) : Multiset.map (fun (L : List (RoseTree α)) => ↑(List.map RootedTree.Nonplanar.mk L)) (insertionForest host gs1) = Multiset.map (fun (L : List (RoseTree α)) => ↑(List.map RootedTree.Nonplanar.mk L)) (insertionForest host gs2)

Combined guest invariance at the multiset-of-multiset level.