Finite realization sets for a fixed marked Hepp tree

For a fixed plane tree and finite restricted branch data, Proposition 5.6 counts realized sets of lattice points. The outer carrier in this file is therefore the image of the admissible-embedding finset under z ↦ Finset.univ.image z. In particular, embeddings with the same image are deliberately deduplicated.

Only the elementary image-cardinality inequality is recorded here. It is not the sharp embedding estimate (5.13), whose proof requires the geometric and automorphism arguments of Proposition 5.6.

@[reducible, inline]

abbrev Anderson4D.LeafEmbedding (t : PlaneTree) : Type

A lattice embedding indexed by the leaves of t.

Equations

• Anderson4D.LeafEmbedding t = (↥t.Leaves → Fin 4 → ℤ)

def Anderson4D.leafEmbeddingImage {t : PlaneTree} (z : LeafEmbedding t) : Finset (Fin 4 → ℤ)

The set of lattice points underlying a leaf embedding. This forgets the leaf indices and all multiplicities.

Equations

• Anderson4D.leafEmbeddingImage z = Finset.image z Finset.univ

noncomputable def Anderson4D.boundedLeafEmbeddings (t : PlaneTree) (M : ℕ) : Finset (LeafEmbedding t)

All leaf-indexed embeddings into the lattice box [-M,M]⁴.

Equations

• Anderson4D.boundedLeafEmbeddings t M = Fintype.piFinset fun (x : ↥t.Leaves) => Fintype.piFinset fun (x : Fin 4) => Finset.Icc (-↑M) ↑M

@[simp]

theorem Anderson4D.mem_boundedLeafEmbeddings {t : PlaneTree} {M : ℕ} {z : LeafEmbedding t} : z ∈ boundedLeafEmbeddings t M ↔ ∀ (l : ↥t.Leaves) (i : Fin 4), |z l i| ≤ ↑M

theorem Anderson4D.card_boundedLeafEmbeddings (t : PlaneTree) (M : ℕ) : (boundedLeafEmbeddings t M).card = (2 * M + 1) ^ (4 * t.Leaves.card)

Cardinality of the explicit ambient embedding box.

noncomputable def Anderson4D.admissibleLeafEmbeddings {t : PlaneTree} {M : ℕ} (N : t.BranchExponentData (4 * M)) (hN : N.IsValid) : Finset (LeafEmbedding t)

The explicit finite carrier of admissible embeddings for fixed restricted branch data. The proof hN only packages N as a HeppMarking; it is not enumerated and contributes no count.

Equations

• Anderson4D.admissibleLeafEmbeddings N hN = {z ∈ Anderson4D.boundedLeafEmbeddings t M | Anderson4D.IsAdmissible (N.toHeppMarking hN) M z}

@[simp]

theorem Anderson4D.mem_admissibleLeafEmbeddings {t : PlaneTree} {M : ℕ} {N : t.BranchExponentData (4 * M)} {hN : N.IsValid} {z : LeafEmbedding t} : z ∈ admissibleLeafEmbeddings N hN ↔ IsAdmissible (N.toHeppMarking hN) M z

noncomputable def Anderson4D.realizedSets {t : PlaneTree} {M : ℕ} (N : t.BranchExponentData (4 * M)) (hN : N.IsValid) : Finset (Finset (Fin 4 → ℤ))

Realized sets for a fixed tree and restricted branch datum. Finset.image is essential: two admissible leaf embeddings with the same range represent one realized set.

Equations

• Anderson4D.realizedSets N hN = Finset.image Anderson4D.leafEmbeddingImage (Anderson4D.admissibleLeafEmbeddings N hN)

theorem Anderson4D.mem_realizedSets_iff {t : PlaneTree} {M : ℕ} {N : t.BranchExponentData (4 * M)} {hN : N.IsValid} {Z : Finset (Fin 4 → ℤ)} : Z ∈ realizedSets N hN ↔ ∃ (z : LeafEmbedding t), IsAdmissible (N.toHeppMarking hN) M z ∧ Finset.image z Finset.univ = Z

Membership is exactly existence of an admissible embedding with the specified image.

theorem Anderson4D.mem_realizedSets_iff_realizes {t : PlaneTree} {M : ℕ} {N : t.BranchExponentData (4 * M)} {hN : N.IsValid} {Z : Finset (Fin 4 → ℤ)} : Z ∈ realizedSets N hN ↔ Realizes (N.toHeppMarking hN) M Z

The preceding membership theorem in the existing Realizes vocabulary.

theorem Anderson4D.card_realizedSets_le_card_admissibleLeafEmbeddings {t : PlaneTree} {M : ℕ} (N : t.BranchExponentData (4 * M)) (hN : N.IsValid) : (realizedSets N hN).card ≤ (admissibleLeafEmbeddings N hN).card

Deduplication can only decrease cardinality. This deliberately does not claim the sharp formula or bound (5.13).

theorem Anderson4D.card_realizedSets_le_box {t : PlaneTree} {M : ℕ} (N : t.BranchExponentData (4 * M)) (hN : N.IsValid) : (realizedSets N hN).card ≤ (2 * M + 1) ^ (4 * t.Leaves.card)

A coarse ambient-box consequence of the image bound.

Index invariance of the image construction

def Anderson4D.reindexLeafEmbedding {t t' : PlaneTree} (e : ↥t.Leaves ≃ ↥t'.Leaves) (z : LeafEmbedding t) : LeafEmbedding t'

Reindex a leaf embedding along an arbitrary equivalence of leaf carriers. This is the basic operation later used for tree automorphisms.

Equations

• Anderson4D.reindexLeafEmbedding e z l = z (e.symm l)

theorem Anderson4D.leafEmbeddingImage_reindex {t t' : PlaneTree} (e : ↥t.Leaves ≃ ↥t'.Leaves) (z : LeafEmbedding t) : leafEmbeddingImage (reindexLeafEmbedding e z) = leafEmbeddingImage z

Reindexing leaves does not change the realized set of lattice points.

theorem Anderson4D.reindexLeafEmbedding_mem_bounded_iff {t t' : PlaneTree} {M : ℕ} (e : ↥t.Leaves ≃ ↥t'.Leaves) (z : LeafEmbedding t) : reindexLeafEmbedding e z ∈ boundedLeafEmbeddings t' M ↔ z ∈ boundedLeafEmbeddings t M

The explicit box enumeration is invariant under leaf reindexing.

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

The finite carriers are independent of the particular proof that the restricted branch data is valid.

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

Proof irrelevance also holds after passing from embeddings to sets.

Interface to full finite realization data

noncomputable def Anderson4D.realizedSetsOfData {t : PlaneTree} {M m : ℕ} (d : t.RealizationData M m) (hd : d.IsValid) : Finset (Finset (Fin 4 → ℤ))

Realized sets attached to a valid RealizationData pair. Only its branch component is used; the leaf multiplicity component remains part of the separate denominator data.

Equations

• Anderson4D.realizedSetsOfData d hd = Anderson4D.realizedSets d.1 ⋯

theorem Anderson4D.mem_realizedSetsOfData_iff {t : PlaneTree} {M m : ℕ} {d : t.RealizationData M m} {hd : d.IsValid} {Z : Finset (Fin 4 → ℤ)} : Z ∈ realizedSetsOfData d hd ↔ Realizes (d.toHeppMarking hd) M Z