Automorphism cardinality for rooted nonplanar trees

The cardinality of the automorphism group of a rooted nonplanar tree (or a forest of such trees), used as the symmetry-weight in the Connes-Kreimer / Grossman-Larson pairing (Linglib/Core/Algebra/RootedTree/GrossmanLarsonPairing.lean).

RoseTree-level formula

For a node with children-multiset M = {c₁ × k₁, c₂ × k₂, …} (distinct trees cᵢ with multiplicities kᵢ):

|Aut(node a M)| = ∏ᵢ kᵢ! · |Aut(cᵢ)|^kᵢ

A leaf has |Aut(leaf)| = 1.

The factorial factor kᵢ! accounts for permutations of identical children; the power |Aut(cᵢ)|^kᵢ accounts for independent choice of auts within each copy.

Forest-level formula

For a forest (multiset of trees) F = {T₁ × m₁, T₂ × m₂, …}:

|Aut(F)| = ∏ⱼ mⱼ! · |Aut(Tⱼ)|^mⱼ

Same formula structure as the tree-level case, applied to the top-level multiset of constituent trees.

Implementation status

[UPSTREAM] candidate. Eventual mathlib home would be Mathlib.Combinatorics.RootedTree.Aut. Sorry-free.

Nonplanar.autCard descends from treeAutCard on the RoseTree α representative, defined by structural recursion over the children list ((cs.map treeAutCard).prod aggregates the children product; no aux twin — RoseTree's nested-List recursion is handled by the equation compiler and its @[induction_eliminator]). PermStep-invariance is established via the standard swap/recurse case split, and the lift to Nonplanar uses Nonplanar.lift. autCard_node bridges to the forestAutCard-as-Finset-product form via Finset.prod_multiset_map_count (turning the all-children prod into a ∏ distinct, c ^ count-form) + Finset.prod_mul_distrib.

forestAutCard is defined in terms of autCard.

RoseTree-representative substrate

treeAutCard computes |Aut(mk t)| on a planar RoseTree representative t; PermEquiv-invariance (below) lets it descend to Nonplanar.autCard through the quotient.

noncomputable def RootedTree.Nonplanar.multinomialFactor {α : Type u_1} (M : Multiset (Nonplanar α)) : ℕ

Symmetry-factor at one node: ∏_{distinct c ∈ M} (M.count c)!. Uses Classical.decEq for Multiset.toFinset and Multiset.count.

Equations

• RootedTree.Nonplanar.multinomialFactor M = ∏ t ∈ M.toFinset, (Multiset.count t M).factorial

@[irreducible]

noncomputable def RootedTree.Nonplanar.treeAutCard {α : Type u_1} : RoseTree α → ℕ

The automorphism count |Aut(mk t)| of the nonplanar tree represented by a planar RoseTree t. Substrate for Nonplanar.autCard (which lifts it through the PermEquiv quotient). At a node, the product of the children's counts times multinomialFactor on the multiset of nonplanar-mk children (counting symmetric rearrangements).

Equations

• RootedTree.Nonplanar.treeAutCard (RoseTree.node value cs) = (List.map RootedTree.Nonplanar.treeAutCard cs).prod * RootedTree.Nonplanar.multinomialFactor ↑(List.map RootedTree.Nonplanar.mk cs)

theorem RootedTree.Nonplanar.treeAutCard_node {α : Type u_1} (a : α) (cs : List (RoseTree α)) : treeAutCard (RoseTree.node a cs) = (List.map treeAutCard cs).prod * multinomialFactor ↑(List.map mk cs)

treeAutCard is PermEquiv-invariant

theorem RootedTree.Nonplanar.treeAutCard_permEquiv {α : Type u_1} {t s : RoseTree α} (h : t.PermEquiv s) : treeAutCard t = treeAutCard s

treeAutCard is invariant under PermEquiv. By induction on EqvGen.

Positivity of treeAutCard

theorem RootedTree.Nonplanar.treeAutCard_pos {α : Type u_1} (t : RoseTree α) : 0 < treeAutCard t

treeAutCard is positive: at a node, multinomialFactor is positive (factorials) and the children product is positive by the IH.

Nonplanar automorphism count via lift

noncomputable def RootedTree.Nonplanar.autCard {α : Type u_1} : Nonplanar α → ℕ

The cardinality |Aut(t)| of the automorphism group of a rooted nonplanar tree t.

Recursive structure: for t = node a M with children-multiset M, autCard t = ∏ distinct c ∈ M, (M.count c)! * (autCard c)^(M.count c) (see autCard_node). A leaf has autCard = 1 (autCard_leaf).

Defined by lifting treeAutCard through the PermEquiv quotient.

Equations

• RootedTree.Nonplanar.autCard = RootedTree.Nonplanar.lift RootedTree.Nonplanar.treeAutCard ⋯

@[simp]

theorem RootedTree.Nonplanar.autCard_mk {α : Type u_1} (t : RoseTree α) : (mk t).autCard = treeAutCard t

@[simp]

theorem RootedTree.Nonplanar.autCard_leaf {α : Type u_1} (a : α) : (leaf a).autCard = 1

A leaf has trivial aut group.

theorem RootedTree.Nonplanar.autCard_pos {α : Type u_1} (t : Nonplanar α) : 0 < t.autCard

The automorphism group of any tree is non-trivial (contains identity). Stated as positivity of the cardinality. Descends from treeAutCard_pos via the quotient.

noncomputable def RootedTree.Nonplanar.forestAutCard {α : Type u_1} (F : Multiset (Nonplanar α)) : ℕ

The cardinality |Aut(F)| of the automorphism group of a forest F (multiset of nonplanar trees), defined as the product over distinct trees T ∈ F:

forestAutCard F = ∏_{distinct T ∈ F} (F.count T)! · (autCard T)^(F.count T)

Uses Classical.decEq for the multiset operations (the function is noncomputable regardless).

Stays in Nonplanar namespace (rather than Forest) because Forest = Multiset is just a stylistic alias used at the ConnesKreimer algebra layer; here we work directly with Multiset (Nonplanar α) to keep the combinatorics layer free of algebra-layer abbreviations.

Equations

• RootedTree.Nonplanar.forestAutCard F = ∏ t ∈ F.toFinset, (Multiset.count t F).factorial * t.autCard ^ Multiset.count t F

@[simp]

theorem RootedTree.Nonplanar.forestAutCard_zero {α : Type u_1} : forestAutCard 0 = 1

The empty forest has trivial aut group.

theorem RootedTree.Nonplanar.forestAutCard_pos {α : Type u_1} (F : Multiset (Nonplanar α)) : 0 < forestAutCard F

The aut group of any forest is non-trivial (contains identity). Each factor (F.count t)! * autCard t ^ F.count t is positive (factorial always positive; autCard_pos gives the tree factor).

@[simp]

theorem RootedTree.Nonplanar.autCard_node {α : Type u_1} (a : α) (F : Multiset (Nonplanar α)) : (node a F).autCard = forestAutCard F

autCard on the smart node constructor: the recursive definition. Proof: induct on F to get a list rep lst; treeAutCard on the tree node splits into a children-product factor (which lifts to (lst.map autCard).prod via prod_out_treeAutCard) and a multinomialFactor factor (which lifts to multinomialFactor F via ofList_map_mk_qout). Combine via Finset.prod_multiset_map_count (to express (F.map autCard).prod as a Finset prod over F.toFinset) and Finset.prod_mul_distrib (to recombine the two legs into forestAutCard F).

Multinomial split identity

The automorphism count of a disjoint union F + G factors through any fixed split: |Aut(F+G)| = N · |Aut F| · |Aut G| where N counts the occurrences of the ordered pair (F, G) among the two-sided sub-multiset splits of F + G (Multiset.antidiagonal). Per distinct tree t, this is (m₁ + m₂)! = C(m₁ + m₂, m₁) · m₁! · m₂! with mᵢ the multiplicities in F, G — Nat.add_choose_mul_factorial_mul_factorial aggregated over (F + G).toFinset. The adjoint role: this is exactly what makes the symmetry-weighted pairing turn CK multiplication into the sub-multiset split coproduct (GrossmanLarsonPairing.pairing_of'_mul).

Computationally validated (scratch/validate_duality.lean, V2 battery, exhaustive over forests of weight ≤ 3 plus duplicate-tree traps).

theorem RootedTree.Nonplanar.forestAutCard_add {α : Type u_1} (F G : Multiset (Nonplanar α)) : Multiset.count (F, G) (F + G).antidiagonal * (forestAutCard F * forestAutCard G) = forestAutCard (F + G)

Multinomial split identity for forestAutCard: count (F,G) (antidiagonal (F+G)) · |Aut F| · |Aut G| = |Aut (F+G)|.