Ordering bound for Hepp trees

This file formalizes paper §5.3, Step 3, equation (5.21), on the real Anderson4D.PlaneTree carrier. Local permutations of the children at every vertex are encoded by a target plane tree together with an isomorphism from the original unordered tree. For each fixed target the isomorphism set is a torsor for Aut(t), while the possible valid targets are bounded by TreeCountReal.card_validTreesExactly_le.

Local ordering choices

The tree/list mutual definitions are structural. This is important here: using a nested Fin cs.length → ... recursive definition would elaborate by well-founded recursion and would not reduce while building the finite instances.

def Anderson4D.PlaneTree.LocalOrdering : PlaneTree → Type

A permutation at a root together with local choices in its child forest.

Equations

• (Anderson4D.PlaneTree.node cs).LocalOrdering = (Equiv.Perm (Fin cs.length) × Anderson4D.PlaneTree.LocalOrderingList cs)

def Anderson4D.PlaneTree.LocalOrderingList : List PlaneTree → Type

Local ordering choices for a forest, as a structural dependent product.

Equations

• Anderson4D.PlaneTree.LocalOrderingList [] = PUnit.{1}
• Anderson4D.PlaneTree.LocalOrderingList (c :: cs) = (c.LocalOrdering × Anderson4D.PlaneTree.LocalOrderingList cs)

@[reducible]

noncomputable def Anderson4D.PlaneTree.localOrderingFintypeDef (t : PlaneTree) : Fintype t.LocalOrdering

Equations

• (Anderson4D.PlaneTree.node cs).localOrderingFintypeDef = id inferInstance

@[reducible]

noncomputable def Anderson4D.PlaneTree.localOrderingListFintypeDef (cs : List PlaneTree) : Fintype (LocalOrderingList cs)

Equations

• Anderson4D.PlaneTree.localOrderingListFintypeDef [] = id inferInstance
• Anderson4D.PlaneTree.localOrderingListFintypeDef (c :: cs) = id inferInstance

@[implicit_reducible]

noncomputable instance Anderson4D.PlaneTree.localOrderingFintype (t : PlaneTree) : Fintype t.LocalOrdering

Equations

• t.localOrderingFintype = t.localOrderingFintypeDef

@[implicit_reducible]

noncomputable instance Anderson4D.PlaneTree.localOrderingListFintype (cs : List PlaneTree) : Fintype (LocalOrderingList cs)

Equations

• Anderson4D.PlaneTree.localOrderingListFintype cs = Anderson4D.PlaneTree.localOrderingListFintypeDef cs

def Anderson4D.PlaneTree.localOrderingListToPi {cs : List PlaneTree} : LocalOrderingList cs → (i : Fin cs.length) → (cs.get i).LocalOrdering

View structural forest choices as a dependent function over child indices.

Equations

• Anderson4D.PlaneTree.localOrderingListToPi x_2 = fun (i : Fin [].length) => i.elim0
• Anderson4D.PlaneTree.localOrderingListToPi (o, os) = fun (i : Fin (tail.length + 1)) => Fin.cases o (fun (i : Fin tail.length) => Anderson4D.PlaneTree.localOrderingListToPi os i) i

def Anderson4D.PlaneTree.localOrderingListOfPi {cs : List PlaneTree} : ((i : Fin cs.length) → (cs.get i).LocalOrdering) → LocalOrderingList cs

Build structural forest choices from a dependent function over indices.

Equations

• Anderson4D.PlaneTree.localOrderingListOfPi x_2 = PUnit.unit
• Anderson4D.PlaneTree.localOrderingListOfPi f = (f 0, Anderson4D.PlaneTree.localOrderingListOfPi fun (i : Fin tail.length) => f i.succ)

theorem Anderson4D.PlaneTree.localOrderingListOfPi_toPi {cs : List PlaneTree} (os : LocalOrderingList cs) : localOrderingListOfPi (localOrderingListToPi os) = os

def Anderson4D.PlaneTree.orderingFactor : PlaneTree → ℕ

The recursive product of all child-count factorials.

Equations

• (Anderson4D.PlaneTree.node cs).orderingFactor = cs.length.factorial * Anderson4D.PlaneTree.orderingFactorList cs

def Anderson4D.PlaneTree.orderingFactorList : List PlaneTree → ℕ

Forest companion of orderingFactor.

Equations

• Anderson4D.PlaneTree.orderingFactorList [] = 1
• Anderson4D.PlaneTree.orderingFactorList (c :: cs) = c.orderingFactor * Anderson4D.PlaneTree.orderingFactorList cs

theorem Anderson4D.PlaneTree.card_localOrdering (t : PlaneTree) : Fintype.card t.LocalOrdering = t.orderingFactor

The local-ordering type has the expected product-factorial cardinality.

theorem Anderson4D.PlaneTree.card_localOrderingList (cs : List PlaneTree) : Fintype.card (LocalOrderingList cs) = orderingFactorList cs

Realizing an ordering as a target plane tree plus an isomorphism

@[irreducible]

noncomputable def Anderson4D.PlaneTree.realizeLocalOrdering (t : PlaneTree) : t.LocalOrdering → (s : PlaneTree) × t.Iso s

Realize all local ordering choices as a plane presentation of the same unordered rooted tree, retaining the induced isomorphism.

Equations

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

@[irreducible]

noncomputable def Anderson4D.PlaneTree.decodeLocalOrdering (t : PlaneTree) : (s : PlaneTree) × t.Iso s → t.LocalOrdering

Split a target isomorphism back into local ordering choices.

Equations

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

theorem Anderson4D.PlaneTree.decode_realizeLocalOrdering (t : PlaneTree) (o : t.LocalOrdering) : t.decodeLocalOrdering (t.realizeLocalOrdering o) = o

Decoding the target and isomorphism produced by an ordering recovers the ordering. Consequently realizeLocalOrdering is injective.

theorem Anderson4D.PlaneTree.realizeLocalOrdering_injective (t : PlaneTree) : Function.Injective t.realizeLocalOrdering

Isomorphism invariants needed to restrict the target

theorem Anderson4D.PlaneTree.leafCount_eq_of_iso (s t : PlaneTree) : ∀ (a : s.Iso t), s.leafCount = t.leafCount

An unordered-tree isomorphism preserves the number of leaves.

theorem Anderson4D.PlaneTree.isValid_of_iso (s t : PlaneTree) : ∀ (a : s.Iso t), s.isValid = true → t.isValid = true

An unordered-tree isomorphism sends a valid Hepp tree to a valid Hepp tree.

Counting the ordering choices by their valid targets

@[reducible, inline]

abbrev Anderson4D.PlaneTree.OrderedIsoTarget (t : PlaneTree) : Type

A valid plane presentation with the same leaf count as t, together with an unordered-tree isomorphism from t.

Equations

• t.OrderedIsoTarget = ((s : ↥(Anderson4D.PlaneTree.validTreesExactly t.leafCount)) × t.Iso ↑s)

@[implicit_reducible]

noncomputable instance Anderson4D.PlaneTree.orderedIsoTargetFintype (t : PlaneTree) : Fintype t.OrderedIsoTarget

Equations

• t.orderedIsoTargetFintype = Fintype.ofFinite t.OrderedIsoTarget

noncomputable def Anderson4D.PlaneTree.realizeValidLocalOrdering (t : PlaneTree) (ht : t.isValid = true) : t.LocalOrdering → t.OrderedIsoTarget

Restrict the realized ordering to the finite set of valid targets.

Equations

• t.realizeValidLocalOrdering ht o = ⟨⟨(t.realizeLocalOrdering o).fst, ⋯⟩, (t.realizeLocalOrdering o).snd⟩

theorem Anderson4D.PlaneTree.realizeValidLocalOrdering_injective (t : PlaneTree) (ht : t.isValid = true) : Function.Injective (t.realizeValidLocalOrdering ht)

theorem Anderson4D.PlaneTree.card_orderedIsoTarget_le (t : PlaneTree) : Fintype.card t.OrderedIsoTarget ≤ (validTreesExactly t.leafCount).card * t.autCard

Every valid target contributes at most |Aut(t)| isomorphisms.

theorem Anderson4D.PlaneTree.orderingFactor_le (t : PlaneTree) (ht : t.isValid = true) : t.orderingFactor ≤ 4 ^ (4 * t.leafCount) * t.autCard

Paper (5.21), first in its recursive product-factorial form.

Identification with the branching-vertex product

theorem Anderson4D.PlaneTree.orderingFactorList_eq_map (cs : List PlaneTree) : orderingFactorList cs = (List.map orderingFactor cs).prod

theorem Anderson4D.PlaneTree.prod_childCount_factorial_eq_orderingFactor (t : PlaneTree) : ∏ v : t.VPos, (t.childCount ↑v).factorial = t.orderingFactor

The recursive ordering factor is the product of the factorial of the child count over all vertices.

theorem Anderson4D.PlaneTree.prod_branchNodes_factorial_eq_orderingFactor (t : PlaneTree) : ∏ v ∈ t.BranchNodes, (t.childCount ↑v).factorial = t.orderingFactor

Vertices outside BranchNodes have zero or one child, hence contribute factorial one.

theorem Anderson4D.PlaneTree.prod_branchNodes_factorial_le (t : PlaneTree) (ht : t.isValid = true) : ∏ v ∈ t.BranchNodes, (t.childCount ↑v).factorial ≤ 4 ^ (4 * t.leafCount) * t.autCard

Paper §5.3 Step 3, equation (5.21), on the real PlaneTree carrier.