Free marked-automorphism orbits of admissible embeddings

This file formalizes the finite counting statement in paper §5.3, Step 2, equation (5.18). For fixed restricted branch data N, its marked-tree automorphism group reindexes admissible leaf embeddings without changing their underlying lattice-point set. Since admissible embeddings are injective and a rooted-tree automorphism is determined by its action on leaves, this action is free.

Choosing one admissible embedding above each realized set therefore gives an injection

AutHeppMarked(t,N) × realizedSets(N) ↪ admissibleLeafEmbeddings(N),

which yields the desired division-free cardinality inequality.

Elementary extensionality and faithfulness on leaves

theorem Anderson4D.aut_eq_of_autLeavesEquiv_eq {t : PlaneTree} {g h : t.Aut} (hleaf : autLeavesEquiv g = autLeavesEquiv h) : g = h

The action of Aut t on the leaves is faithful.

theorem Anderson4D.smulLeafEmbedding_left_injective {t : PlaneTree} (z : LeafEmbedding t) (hz : Function.Injective z) : Function.Injective fun (g : t.Aut) => smulLeafEmbedding g z

For an injective leaf embedding, reindexing by distinct tree automorphisms gives distinct embeddings.

The fixed-marking action on admissible embeddings

theorem Anderson4D.smul_toHeppMarking_eq_of_mem_autHeppMarked {t : PlaneTree} {M : ℕ} (N : t.BranchExponentData (4 * M)) (hN : N.IsValid) (g : ↥(t.AutHeppMarked (N.toHeppMarking hN))) : smulHeppMarking (↑g) (N.toHeppMarking hN) = N.toHeppMarking hN

For canonical restricted branch data, membership in the marked-tree stabilizer fixes the bundled marking literally, not merely on branch vertices. The canonical zero extension is important here.

theorem Anderson4D.IsAdmissible.map_autHeppMarked {t : PlaneTree} {M : ℕ} {N : t.BranchExponentData (4 * M)} {hN : N.IsValid} {z : LeafEmbedding t} (hz : IsAdmissible (N.toHeppMarking hN) M z) (g : ↥(t.AutHeppMarked (N.toHeppMarking hN))) : IsAdmissible (N.toHeppMarking hN) M (smulLeafEmbedding (↑g) z)

The marked-tree stabilizer preserves admissibility for the fixed restricted marking.

@[simp]

theorem Anderson4D.leafEmbeddingImage_smulLeafEmbedding {t : PlaneTree} (g : t.Aut) (z : LeafEmbedding t) : leafEmbeddingImage (smulLeafEmbedding g z) = leafEmbeddingImage z

Reindexing by a tree automorphism preserves the unindexed lattice-point set of an embedding.

theorem Anderson4D.autHeppMarked_toHeppMarking_proof_irrel {t : PlaneTree} {M : ℕ} (N : t.BranchExponentData (4 * M)) (hN hN' : N.IsValid) : t.AutHeppMarked (N.toHeppMarking hN) = t.AutHeppMarked (N.toHeppMarking hN')

The stabilizer itself is independent of the proof term witnessing validity of the restricted marking.

One representative above each realized set

noncomputable def Anderson4D.realizedSetRepresentative {t : PlaneTree} {M : ℕ} (N : t.BranchExponentData (4 * M)) (hN : N.IsValid) (Z : ↥(realizedSets N hN)) : LeafEmbedding t

A noncanonical admissible embedding whose image is the given realized set.

Equations

• Anderson4D.realizedSetRepresentative N hN Z = Classical.choose ⋯

theorem Anderson4D.realizedSetRepresentative_mem {t : PlaneTree} {M : ℕ} (N : t.BranchExponentData (4 * M)) (hN : N.IsValid) (Z : ↥(realizedSets N hN)) : realizedSetRepresentative N hN Z ∈ admissibleLeafEmbeddings N hN

theorem Anderson4D.realizedSetRepresentative_image {t : PlaneTree} {M : ℕ} (N : t.BranchExponentData (4 * M)) (hN : N.IsValid) (Z : ↥(realizedSets N hN)) : leafEmbeddingImage (realizedSetRepresentative N hN Z) = ↑Z

noncomputable def Anderson4D.realizedSetRepresentativeEmbedding {t : PlaneTree} {M : ℕ} (N : t.BranchExponentData (4 * M)) (hN : N.IsValid) (Z : ↥(realizedSets N hN)) : ↥(admissibleLeafEmbeddings N hN)

The representative packaged in the finite admissible-embedding carrier.

Equations

• Anderson4D.realizedSetRepresentativeEmbedding N hN Z = ⟨Anderson4D.realizedSetRepresentative N hN Z, ⋯⟩

The product injection and finite count

noncomputable def Anderson4D.markedOrbitEmbedding {t : PlaneTree} {M : ℕ} (N : t.BranchExponentData (4 * M)) (hN : N.IsValid) : ↥(t.AutHeppMarked (N.toHeppMarking hN)) × ↥(realizedSets N hN) → ↥(admissibleLeafEmbeddings N hN)

Act on one chosen representative over each realized set.

Equations

• Anderson4D.markedOrbitEmbedding N hN p = ⟨Anderson4D.smulLeafEmbedding ↑p.1 ↑(Anderson4D.realizedSetRepresentativeEmbedding N hN p.2), ⋯⟩

theorem Anderson4D.markedOrbitEmbedding_image {t : PlaneTree} {M : ℕ} (N : t.BranchExponentData (4 * M)) (hN : N.IsValid) (p : ↥(t.AutHeppMarked (N.toHeppMarking hN)) × ↥(realizedSets N hN)) : leafEmbeddingImage ↑(markedOrbitEmbedding N hN p) = ↑p.2

theorem Anderson4D.markedOrbitEmbedding_injective {t : PlaneTree} {M : ℕ} (N : t.BranchExponentData (4 * M)) (hN : N.IsValid) : Function.Injective (markedOrbitEmbedding N hN)

Freeness on each representative and disjointness of distinct image fibers make the product map injective.

theorem Anderson4D.card_autHeppMarked_mul_card_realizedSets_le {t : PlaneTree} {M : ℕ} (N : t.BranchExponentData (4 * M)) (hN : N.IsValid) : Fintype.card ↥(t.AutHeppMarked (N.toHeppMarking hN)) * (realizedSets N hN).card ≤ (admissibleLeafEmbeddings N hN).card

Paper (5.18), finite division-free form.

theorem Anderson4D.card_autHeppMarked_mul_card_realizedSets_le_proof_irrel {t : PlaneTree} {M : ℕ} (N : t.BranchExponentData (4 * M)) (hGroup hSets : N.IsValid) : Fintype.card ↥(t.AutHeppMarked (N.toHeppMarking hGroup)) * (realizedSets N hSets).card ≤ (admissibleLeafEmbeddings N hSets).card

Proof-irrelevant form of (5.18): the validity proof used to name the stabilizer may differ from the proof used to enumerate the two finite carriers.