Gamma-two transport under subtree restriction

Restriction preserves the child, simple-leaf, and compound-leaf terms in γ² exactly. This is the branch-power input for the restricted Proposition 5.10 call in the collapse induction.

theorem Anderson4D.map_simpleChildren_restrict {t : PlaneTree} (r : t.VPos) (compound : Finset t.VPos) (v : (t.subtreeAt ↑r).VPos) : Finset.map (subtreeVertexEmbedding r) (childrenOf v ∩ simpleLeaves (t.subtreeAt ↑r) (restrictCompound r compound)) = childrenOf (PlaneTree.subtreeVertex r v) ∩ simpleLeaves t compound

Simple leaf children map exactly under restriction of the compound set.

theorem Anderson4D.map_compoundChildren_restrict {t : PlaneTree} (r : t.VPos) (compound : Finset t.VPos) (v : (t.subtreeAt ↑r).VPos) : Finset.map (subtreeVertexEmbedding r) (childrenOf v ∩ compoundLeaves (t.subtreeAt ↑r) (restrictCompound r compound)) = childrenOf (PlaneTree.subtreeVertex r v) ∩ compoundLeaves t compound

Compound leaf children map exactly under restriction.

@[simp]

theorem Anderson4D.gamma2_restrictMultiplicities {t : PlaneTree} (mu : t.Multiplicities) (compound : Finset t.VPos) (r : t.VPos) (v : (t.subtreeAt ↑r).VPos) : gamma2 (restrictMultiplicities mu r) (restrictCompound r compound) v = gamma2 mu compound (PlaneTree.subtreeVertex r v)

γ² is unchanged at every branch of the restricted subtree.