Host-append decomposition for planar multi-tree insertion

The planar 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 proof introduces hostBucketSum, a Multiset aggregator analogous to forestPairSum but splitting guests by a 2-bucket partition between two arbitrary host forests (rather than between a head tree and its tail). The bridge hostBucketSum_eq_insertionForest is proved by induction on host_A.

This is the planar-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.

§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 RootedTree.Planar.Pathed.hostBucketSum {α : Type u_1} (host_A host_B : List (Planar α)) : List (Planar α) → List (Planar α) → List (Planar α) → Multiset (List (Planar α))

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 RootedTree.Planar.Pathed.hostBucketSum_nil_remaining {α : Type u_1} (host_A host_B pre_A pre_B : List (Planar α)) : hostBucketSum host_A host_B pre_A pre_B [] = Multiset.map (fun (p : List (Planar α) × List (Planar α)) => p.1 ++ p.2) (insertionForest host_A pre_A ×ˢ insertionForest host_B pre_B)

theorem RootedTree.Planar.Pathed.hostBucketSum_cons_remaining {α : Type u_1} (host_A host_B pre_A pre_B : List (Planar α)) (x : Planar α) (rest : List (Planar α)) : hostBucketSum host_A host_B pre_A pre_B (x :: rest) = (↑[true, false]).bind fun (b : Bool) => if b = true then hostBucketSum host_A host_B (pre_A ++ [x]) pre_B rest else hostBucketSum host_A host_B pre_A (pre_B ++ [x]) rest

theorem RootedTree.Planar.Pathed.hostBucketSum_assignment_rewrite {α : Type u_1} (host_A host_B pre_A pre_B Ts : List (Planar α)) : 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 : Planar α × Bool) => if p.2 = true then some p.1 else none) (Ts.zip α_1)) (pre_B ++ List.filterMap (fun (p : Planar α × 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. Mirrors forestPairSum_assignment_rewrite in Insertion.lean.

theorem RootedTree.Planar.Pathed.hostBucketSum_eq_kBucketSum {α : Type u_1} (host_A host_B pre_A pre_B Ts : List (Planar α)) : hostBucketSum host_A host_B pre_A pre_B Ts = kBucketSum [true, false] (fun (pres' : Bool → List (Planar α)) => Multiset.map (fun (p : List (Planar α) × List (Planar α)) => 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.

§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 planar 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").

@[implicit_reducible]

instance RootedTree.Planar.Pathed.instDecidableEqTripleIdx : DecidableEq RootedTree.Planar.Pathed.TripleIdx✝

Equations

• RootedTree.Planar.Pathed.instDecidableEqTripleIdx x✝ y✝ = if h : RootedTree.Planar.Pathed.TripleIdx.ctorIdx✝ x✝ = RootedTree.Planar.Pathed.TripleIdx.ctorIdx✝ y✝ then isTrue ⋯ else isFalse ⋯

theorem RootedTree.Planar.Pathed.insertionForest_cons_assignment {α : Type u_1} (T : Planar α) (F X : List (Planar α)) : insertionForest (T :: F) X = (↑(listChoices [true, false] X.length)).bind fun (α_1 : List Bool) => (insertion T (List.filterMap (fun (p : Planar α × Bool) => if p.2 = true then some p.1 else none) (X.zip α_1))).bind fun (T' : Planar α) => Multiset.map (fun (F' : List (Planar α)) => T' :: F') (insertionForest F (List.filterMap (fun (p : Planar α × 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 RootedTree.Planar.Pathed.listChoices_succ_append_bind {γ : Type u_2} (n : ℕ) (g : List Bool → Multiset γ) : (↑(listChoices [true, false] (n + 1))).bind g = (↑(listChoices [true, false] n)).bind fun (a : List Bool) => g (a ++ [true]) + g (a ++ [false])

Lemma X (listChoices append-decomposition): enumerating length-(n+1) bit vectors and applying g equals enumerating length-n bit vectors and summing g (α ++ [true]) + g (α ++ [false]). Multiset-level, NOT list-level.

theorem RootedTree.Planar.Pathed.listChoices_append_bind {γ : Type u_2} (m n : ℕ) (g : List Bool → Multiset γ) : (↑(listChoices [true, false] (m + n))).bind g = (↑(listChoices [true, false] m)).bind fun (a : List Bool) => (↑(listChoices [true, false] n)).bind fun (b : List Bool) => g (a ++ b)

Length-additive splitting: a bind over length-(m+n) bit vectors equals a nested bind: outer over length-m, inner over length-n, with the leaf function applied to the concatenation.

Companion to listChoices_succ_append_bind (which splits off a single bit from the end). Original consumer was the A3.3 basis-level proof in InsertionAssoc.lean (deleted 2026-05-16); kept as a general utility.

Proof: induction on n. Base n = 0 reduces via List.append_nil; step n + 1 peels off one bit via listChoices_succ_append_bind on both sides and rebinds via List.append_assoc.

theorem RootedTree.Planar.Pathed.listChoices_split_bind {β : Type u_2} {γ : Type u_3} (xs : List β) (m n : ℕ) (g : List β → Multiset γ) : (↑(listChoices xs (m + n))).bind g = (↑(listChoices xs m)).bind fun (a : List β) => (↑(listChoices xs n)).bind fun (b : List β) => g (a ++ b)

Polymorphic length-additive splitting: a bind over length-(m+n) enumerations equals a nested bind, outer over length-m and inner over length-n, with the leaf function applied to the concatenation.

Generalizes listChoices_append_bind (the Bool case) to arbitrary xs : List β. The proof inducts on m, peeling one element off the front via listChoices_succ (rather than the back, as in the Bool version which uses listChoices_succ_append_bind).

Used by RHS_eq_canonical_msform to split a length-(pre_T_B.length + T_orig-count) choice into a pre_T_B.length prefix (choice_T) and a T_orig-count suffix (choice_T_orig).

theorem RootedTree.Planar.Pathed.listChoices_split_map {β : Type u_2} {γ : Type u_3} (xs : List β) (m n : ℕ) (g : List β → γ) : Multiset.map g ↑(listChoices xs (m + n)) = (↑(listChoices xs m)).bind fun (a : List β) => Multiset.map (fun (b : List β) => g (a ++ b)) ↑(listChoices xs n)

.map-variant of listChoices_split_bind. When the consumer is .map g instead of .bind g, the same length-additive splitting holds, with the inner .bind becoming a .map. Derived from listChoices_split_bind by rewriting the outer .map as .bind over a singleton multiset and converting back.

theorem RootedTree.Planar.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 RootedTree.Planar.Pathed.listChoices_succ_cons_bind {γ : Type u_2} (n : ℕ) (g : List Bool → Multiset γ) : (↑(listChoices [true, false] (n + 1))).bind g = (↑(listChoices [true, false] n)).bind fun (α : List Bool) => g (true :: α) + g (false :: α)

Cons-prepending analog of listChoices_succ_append_bind. The bit for the cons-front guest goes at the FRONT of α rather than the back.

theorem RootedTree.Planar.Pathed.hostBucketSum_eq_insertionForest {α : Type u_1} (host_A host_B guests : List (Planar α)) : 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 RootedTree.Planar.Pathed.insertionForest_perm_host_msform {α : Type u_1} {host host' : List (Planar α)} (h : host.Perm host') (gs : List (Planar α)) : Multiset.map (fun (L : List (Planar α)) => ↑(List.map Nonplanar.mk L)) (insertionForest host gs) = Multiset.map (fun (L : List (Planar α)) => ↑(List.map 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 RootedTree.Planar.Pathed.filterMap_t_add_filterMap_f_eq_self {β : Type u_2} (l : List β) (assn : List Bool) (hlen : assn.length = l.length) : ↑(List.filterMap (fun (p : β × Bool) => if p.2 = true then some p.1 else none) (l.zip assn)) + ↑(List.filterMap (fun (p : β × Bool) => if p.2 = true then none else some p.1) (l.zip assn)) = ↑l

The complementary filter_t / filter_f operations on a bit-vector over a list l partition l (as multisets) when their lengths match: ↑(filter_t l assn) + ↑(filter_f l assn) = ↑l.

theorem RootedTree.Planar.Pathed.filterMap_f_eq_sub {β : Type u_2} [DecidableEq β] (l : List β) (assn : List Bool) (hlen : assn.length = l.length) : ↑(List.filterMap (fun (p : β × Bool) => if p.2 = true then none else some p.1) (l.zip assn)) = ↑l - ↑(List.filterMap (fun (p : β × Bool) => if p.2 = true then some p.1 else none) (l.zip assn))

Corollary: ↑(filter_f l assn) = ↑l - ↑(filter_t l assn), given matching length.

theorem RootedTree.Planar.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 RootedTree.Planar.Pathed.listChoices_bridge_powerset {β : Type u_2} [DecidableEq β] (l : List β) : Multiset.map (fun (assn : List Bool) => ↑(List.filterMap (fun (p : β × Bool) => if p.2 = true then some p.1 else none) (l.zip assn))) ↑(listChoices [true, false] l.length) = (↑l).powerset

Bit-vector ↔ powerset bridge (paired form, first-component map only): enumerating bit-vectors and mapping to ↑(filter_t) gives the powerset of ↑l. (No second component yet — see paired version below.)

theorem RootedTree.Planar.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 planar representatives or order. This combines guest-Perm invariance + guest-PlanarEquiv invariance into a single lemma matching the level used by Nonplanar.insertionMultiset.

theorem RootedTree.Planar.Pathed.insertionForest_planarEquiv_guests {α : Type u_1} (F : List (Planar α)) {Ts Ts' : List (Planar α)} (h : List.Forall₂ PlanarEquiv Ts Ts') : Multiset.map (List.map Nonplanar.mk) (insertionForest F Ts) = Multiset.map (List.map Nonplanar.mk) (insertionForest F Ts')

Forest version of guest-PlanarEquiv invariance: Forall₂ PlanarEquiv on guests preserves (insertionForest F Ts).map (List.map mk). Mirrors insertionForest_planarEquiv_host (Insertion.lean §6) but for the guest list.

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

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