Keyboard shortcuts

Press ← or → to navigate between chapters

Press ? to show this help

Press Esc to hide this help

Finite colored hair-tree shapes

Abstract

Finite colored hair-tree shapes

Definition 1.1 (Ordinary colored binary trees).

Lean statement: D5/S3/Combinatorics/Graph/Jacobi/HairTreeShape.HairTree

Formalization. D5/S3/Combinatorics/Graph/Jacobi/HairTreeShape.HairTree (✓ std3).

Source. Repository-derived.

Commentary.

HairTree C is a finite full binary tree with a color in C at each leaf. HairContext C is an explicit one-hole context, and fill inserts a tree into that context. The structural decomposition into a leaf or a context containing a pair of sibling leaves is used inside actual flag embeddings; it is an auxiliary shape calculation, not a separate mathematical endpoint.

References