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).

Tree-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.

Nonplanar.autCard is currently sorry — implementation requires mutual recursion through the children-multiset structure (with a DecidableEq (Nonplanar α) from Classical), descended from a planar implementation. Fully writing it out is ~80-150 LOC of mutual recursion + invariance-under-PlanarStep proofs, deferred until the GL pairing scaffold consumes it.

forestAutCard IS defined in terms of autCard (no extra sorry beyond what flows from autCard's sorry).

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)

A leaf has autCard = 1. TODO: implementation.

Equations

• RootedTree.Nonplanar.autCard = sorry

@[simp]

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

A leaf has trivial aut group.

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.