Anchored admissible embeddings

Paper Proposition 5.6, Step 2 reduces counts of realized sets containing one or two prescribed lattice points to admissible embeddings with specified leaves anchored at those points. This file records the exact finite counting statements before the geometric estimates of the subsequent steps.

Filtering by a property of the realized image

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

Realized sets satisfying a predicate on their underlying point set.

Equations

• Anderson4D.realizedSetsSatisfying N hN P = Finset.filter P (Anderson4D.realizedSets N hN)

@[simp]

theorem Anderson4D.mem_realizedSetsSatisfying {t : PlaneTree} {M : ℕ} {N : t.BranchExponentData (4 * M)} {hN : N.IsValid} {P : Finset (Fin 4 → ℤ) → Prop} {Z : Finset (Fin 4 → ℤ)} : Z ∈ realizedSetsSatisfying N hN P ↔ Z ∈ realizedSets N hN ∧ P Z

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

Admissible embeddings whose unindexed image satisfies P.

Equations

• Anderson4D.admissibleLeafEmbeddingsSatisfying N hN P = {z ∈ Anderson4D.admissibleLeafEmbeddings N hN | P (Anderson4D.leafEmbeddingImage z)}

@[simp]

theorem Anderson4D.mem_admissibleLeafEmbeddingsSatisfying {t : PlaneTree} {M : ℕ} {N : t.BranchExponentData (4 * M)} {hN : N.IsValid} {P : Finset (Fin 4 → ℤ) → Prop} {z : LeafEmbedding t} : z ∈ admissibleLeafEmbeddingsSatisfying N hN P ↔ z ∈ admissibleLeafEmbeddings N hN ∧ P (leafEmbeddingImage z)

noncomputable def Anderson4D.markedOrbitEmbeddingSatisfying {t : PlaneTree} {M : ℕ} (N : t.BranchExponentData (4 * M)) (hN : N.IsValid) (P : Finset (Fin 4 → ℤ) → Prop) : ↥(t.AutHeppMarked (N.toHeppMarking hN)) × ↥(realizedSetsSatisfying N hN P) → ↥(admissibleLeafEmbeddingsSatisfying N hN P)

Restrict markedOrbitEmbedding to realized sets satisfying P.

Equations

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

theorem Anderson4D.markedOrbitEmbeddingSatisfying_injective {t : PlaneTree} {M : ℕ} (N : t.BranchExponentData (4 * M)) (hN : N.IsValid) (P : Finset (Fin 4 → ℤ) → Prop) : Function.Injective (markedOrbitEmbeddingSatisfying N hN P)

The restricted orbit map remains injective.

theorem Anderson4D.card_autHeppMarked_mul_card_realizedSetsSatisfying_le {t : PlaneTree} {M : ℕ} (N : t.BranchExponentData (4 * M)) (hN : N.IsValid) (P : Finset (Fin 4 → ℤ) → Prop) : Fintype.card ↥(t.AutHeppMarked (N.toHeppMarking hN)) * (realizedSetsSatisfying N hN P).card ≤ (admissibleLeafEmbeddingsSatisfying N hN P).card

General restricted form of the free-orbit count.

One-point and two-point image conditions

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

Realized sets containing a prescribed lattice point.

Equations

• Anderson4D.realizedSetsContaining N hN z₀ = Anderson4D.realizedSetsSatisfying N hN fun (Z : Finset (Fin 4 → ℤ)) => z₀ ∈ Z

@[simp]

theorem Anderson4D.mem_realizedSetsContaining {t : PlaneTree} {M : ℕ} {N : t.BranchExponentData (4 * M)} {hN : N.IsValid} {z₀ : Fin 4 → ℤ} {Z : Finset (Fin 4 → ℤ)} : Z ∈ realizedSetsContaining N hN z₀ ↔ Z ∈ realizedSets N hN ∧ z₀ ∈ Z

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

Realized sets containing both prescribed points.

Equations

• Anderson4D.realizedSetsContainingPair N hN z₀ z₁ = Anderson4D.realizedSetsSatisfying N hN fun (Z : Finset (Fin 4 → ℤ)) => z₀ ∈ Z ∧ z₁ ∈ Z

@[simp]

theorem Anderson4D.mem_realizedSetsContainingPair {t : PlaneTree} {M : ℕ} {N : t.BranchExponentData (4 * M)} {hN : N.IsValid} {z₀ z₁ : Fin 4 → ℤ} {Z : Finset (Fin 4 → ℤ)} : Z ∈ realizedSetsContainingPair N hN z₀ z₁ ↔ Z ∈ realizedSets N hN ∧ z₀ ∈ Z ∧ z₁ ∈ Z

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

Admissible embeddings whose image contains a prescribed point.

Equations

• Anderson4D.admissibleLeafEmbeddingsContaining N hN z₀ = Anderson4D.admissibleLeafEmbeddingsSatisfying N hN fun (Z : Finset (Fin 4 → ℤ)) => z₀ ∈ Z

@[simp]

theorem Anderson4D.mem_admissibleLeafEmbeddingsContaining {t : PlaneTree} {M : ℕ} {N : t.BranchExponentData (4 * M)} {hN : N.IsValid} {z₀ : Fin 4 → ℤ} {z : LeafEmbedding t} : z ∈ admissibleLeafEmbeddingsContaining N hN z₀ ↔ z ∈ admissibleLeafEmbeddings N hN ∧ z₀ ∈ leafEmbeddingImage z

noncomputable def Anderson4D.admissibleLeafEmbeddingsContainingPair {t : PlaneTree} {M : ℕ} (N : t.BranchExponentData (4 * M)) (hN : N.IsValid) (z₀ z₁ : Fin 4 → ℤ) : Finset (LeafEmbedding t)

Admissible embeddings whose image contains both prescribed points.

Equations

• Anderson4D.admissibleLeafEmbeddingsContainingPair N hN z₀ z₁ = Anderson4D.admissibleLeafEmbeddingsSatisfying N hN fun (Z : Finset (Fin 4 → ℤ)) => z₀ ∈ Z ∧ z₁ ∈ Z

@[simp]

theorem Anderson4D.mem_admissibleLeafEmbeddingsContainingPair {t : PlaneTree} {M : ℕ} {N : t.BranchExponentData (4 * M)} {hN : N.IsValid} {z₀ z₁ : Fin 4 → ℤ} {z : LeafEmbedding t} : z ∈ admissibleLeafEmbeddingsContainingPair N hN z₀ z₁ ↔ z ∈ admissibleLeafEmbeddings N hN ∧ z₀ ∈ leafEmbeddingImage z ∧ z₁ ∈ leafEmbeddingImage z

noncomputable def Anderson4D.markedOrbitEmbeddingContaining {t : PlaneTree} {M : ℕ} (N : t.BranchExponentData (4 * M)) (hN : N.IsValid) (z₀ : Fin 4 → ℤ) : ↥(t.AutHeppMarked (N.toHeppMarking hN)) × ↥(realizedSetsContaining N hN z₀) → ↥(admissibleLeafEmbeddingsContaining N hN z₀)

One-point restricted orbit map.

Equations

• Anderson4D.markedOrbitEmbeddingContaining N hN z₀ = Anderson4D.markedOrbitEmbeddingSatisfying N hN fun (Z : Finset (Fin 4 → ℤ)) => z₀ ∈ Z

noncomputable def Anderson4D.markedOrbitEmbeddingContainingPair {t : PlaneTree} {M : ℕ} (N : t.BranchExponentData (4 * M)) (hN : N.IsValid) (z₀ z₁ : Fin 4 → ℤ) : ↥(t.AutHeppMarked (N.toHeppMarking hN)) × ↥(realizedSetsContainingPair N hN z₀ z₁) → ↥(admissibleLeafEmbeddingsContainingPair N hN z₀ z₁)

Two-point restricted orbit map.

Equations

• Anderson4D.markedOrbitEmbeddingContainingPair N hN z₀ z₁ = Anderson4D.markedOrbitEmbeddingSatisfying N hN fun (Z : Finset (Fin 4 → ℤ)) => z₀ ∈ Z ∧ z₁ ∈ Z

theorem Anderson4D.markedOrbitEmbeddingContaining_injective {t : PlaneTree} {M : ℕ} (N : t.BranchExponentData (4 * M)) (hN : N.IsValid) (z₀ : Fin 4 → ℤ) : Function.Injective (markedOrbitEmbeddingContaining N hN z₀)

The one-point restricted orbit map is injective.

theorem Anderson4D.markedOrbitEmbeddingContainingPair_injective {t : PlaneTree} {M : ℕ} (N : t.BranchExponentData (4 * M)) (hN : N.IsValid) (z₀ z₁ : Fin 4 → ℤ) : Function.Injective (markedOrbitEmbeddingContainingPair N hN z₀ z₁)

The two-point restricted orbit map is injective.

theorem Anderson4D.card_autHeppMarked_mul_card_realizedSetsContaining_le {t : PlaneTree} {M : ℕ} (N : t.BranchExponentData (4 * M)) (hN : N.IsValid) (z₀ : Fin 4 → ℤ) : Fintype.card ↥(t.AutHeppMarked (N.toHeppMarking hN)) * (realizedSetsContaining N hN z₀).card ≤ (admissibleLeafEmbeddingsContaining N hN z₀).card

Free-orbit count restricted to realized sets containing z₀.

theorem Anderson4D.card_autHeppMarked_mul_card_realizedSetsContainingPair_le {t : PlaneTree} {M : ℕ} (N : t.BranchExponentData (4 * M)) (hN : N.IsValid) (z₀ z₁ : Fin 4 → ℤ) : Fintype.card ↥(t.AutHeppMarked (N.toHeppMarking hN)) * (realizedSetsContainingPair N hN z₀ z₁).card ≤ (admissibleLeafEmbeddingsContainingPair N hN z₀ z₁).card

Free-orbit count restricted to realized sets containing both points.

Fixed-leaf anchored carriers

noncomputable def Anderson4D.anchoredLeafEmbeddings {t : PlaneTree} {M : ℕ} (N : t.BranchExponentData (4 * M)) (hN : N.IsValid) (f₀ : ↥t.Leaves) (z₀ : Fin 4 → ℤ) : Finset (LeafEmbedding t)

Admissible embeddings sending the specified leaf to z₀.

Equations

• Anderson4D.anchoredLeafEmbeddings N hN f₀ z₀ = {z ∈ Anderson4D.admissibleLeafEmbeddings N hN | z f₀ = z₀}

@[simp]

theorem Anderson4D.mem_anchoredLeafEmbeddings {t : PlaneTree} {M : ℕ} {N : t.BranchExponentData (4 * M)} {hN : N.IsValid} {f₀ : ↥t.Leaves} {z₀ : Fin 4 → ℤ} {z : LeafEmbedding t} : z ∈ anchoredLeafEmbeddings N hN f₀ z₀ ↔ z ∈ admissibleLeafEmbeddings N hN ∧ z f₀ = z₀

noncomputable def Anderson4D.J0 {t : PlaneTree} {M : ℕ} (N : t.BranchExponentData (4 * M)) (hN : N.IsValid) (f₀ : ↥t.Leaves) (z₀ : Fin 4 → ℤ) : ℕ

Paper's one-anchor count for a fixed leaf.

Equations

• Anderson4D.J0 N hN f₀ z₀ = (Anderson4D.anchoredLeafEmbeddings N hN f₀ z₀).card

noncomputable def Anderson4D.doublyAnchoredLeafEmbeddings {t : PlaneTree} {M : ℕ} (N : t.BranchExponentData (4 * M)) (hN : N.IsValid) (f₀ f₁ : ↥t.Leaves) (z₀ z₁ : Fin 4 → ℤ) : Finset (LeafEmbedding t)

Admissible embeddings sending two specified leaves to z₀,z₁.

Equations

• Anderson4D.doublyAnchoredLeafEmbeddings N hN f₀ f₁ z₀ z₁ = {z ∈ Anderson4D.admissibleLeafEmbeddings N hN | z f₀ = z₀ ∧ z f₁ = z₁}

@[simp]

theorem Anderson4D.mem_doublyAnchoredLeafEmbeddings {t : PlaneTree} {M : ℕ} {N : t.BranchExponentData (4 * M)} {hN : N.IsValid} {f₀ f₁ : ↥t.Leaves} {z₀ z₁ : Fin 4 → ℤ} {z : LeafEmbedding t} : z ∈ doublyAnchoredLeafEmbeddings N hN f₀ f₁ z₀ z₁ ↔ z ∈ admissibleLeafEmbeddings N hN ∧ z f₀ = z₀ ∧ z f₁ = z₁

noncomputable def Anderson4D.J01 {t : PlaneTree} {M : ℕ} (N : t.BranchExponentData (4 * M)) (hN : N.IsValid) (f₀ f₁ : ↥t.Leaves) (z₀ z₁ : Fin 4 → ℤ) : ℕ

Paper's two-anchor count for a fixed ordered pair of leaves.

Equations

• Anderson4D.J01 N hN f₀ f₁ z₀ z₁ = (Anderson4D.doublyAnchoredLeafEmbeddings N hN f₀ f₁ z₀ z₁).card

Exact leafwise covers and their cardinality bounds

theorem Anderson4D.admissibleLeafEmbeddingsContaining_eq_biUnion_anchored {t : PlaneTree} {M : ℕ} (N : t.BranchExponentData (4 * M)) (hN : N.IsValid) (z₀ : Fin 4 → ℤ) : admissibleLeafEmbeddingsContaining N hN z₀ = Finset.univ.biUnion fun (f₀ : ↥t.Leaves) => anchoredLeafEmbeddings N hN f₀ z₀

An admissible embedding contains z₀ exactly when at least one leaf is anchored at z₀.

theorem Anderson4D.card_admissibleLeafEmbeddingsContaining_le_sum_J0 {t : PlaneTree} {M : ℕ} (N : t.BranchExponentData (4 * M)) (hN : N.IsValid) (z₀ : Fin 4 → ℤ) : (admissibleLeafEmbeddingsContaining N hN z₀).card ≤ ∑ f₀ : ↥t.Leaves, J0 N hN f₀ z₀

Union bound over the possible leaf carrying z₀.

theorem Anderson4D.card_autHeppMarked_mul_card_realizedSetsContaining_le_sum_J0 {t : PlaneTree} {M : ℕ} (N : t.BranchExponentData (4 * M)) (hN : N.IsValid) (z₀ : Fin 4 → ℤ) : Fintype.card ↥(t.AutHeppMarked (N.toHeppMarking hN)) * (realizedSetsContaining N hN z₀).card ≤ ∑ f₀ : ↥t.Leaves, J0 N hN f₀ z₀

The full one-anchor Step 2 reduction, retaining the exact sum over the choice of anchored leaf.

theorem Anderson4D.admissibleLeafEmbeddingsContainingPair_eq_biUnion_anchored {t : PlaneTree} {M : ℕ} (N : t.BranchExponentData (4 * M)) (hN : N.IsValid) (z₀ z₁ : Fin 4 → ℤ) : admissibleLeafEmbeddingsContainingPair N hN z₀ z₁ = Finset.univ.biUnion fun (f : ↥t.Leaves × ↥t.Leaves) => doublyAnchoredLeafEmbeddings N hN f.1 f.2 z₀ z₁

An admissible embedding contains both points exactly when an ordered leaf pair is anchored at them.

theorem Anderson4D.card_admissibleLeafEmbeddingsContainingPair_le_sum_J01 {t : PlaneTree} {M : ℕ} (N : t.BranchExponentData (4 * M)) (hN : N.IsValid) (z₀ z₁ : Fin 4 → ℤ) : (admissibleLeafEmbeddingsContainingPair N hN z₀ z₁).card ≤ ∑ f : ↥t.Leaves × ↥t.Leaves, J01 N hN f.1 f.2 z₀ z₁

Union bound over ordered pairs of leaves carrying z₀,z₁.

theorem Anderson4D.card_autHeppMarked_mul_card_realizedSetsContainingPair_le_sum_J01 {t : PlaneTree} {M : ℕ} (N : t.BranchExponentData (4 * M)) (hN : N.IsValid) (z₀ z₁ : Fin 4 → ℤ) : Fintype.card ↥(t.AutHeppMarked (N.toHeppMarking hN)) * (realizedSetsContainingPair N hN z₀ z₁).card ≤ ∑ f : ↥t.Leaves × ↥t.Leaves, J01 N hN f.1 f.2 z₀ z₁

The full two-anchor Step 2 reduction with the exact ordered-pair sum.

Distinct anchors for distinct prescribed points

def Anderson4D.distinctLeafPairs (t : PlaneTree) : Finset (↥t.Leaves × ↥t.Leaves)

Ordered pairs of distinct leaves.

Equations

• Anderson4D.distinctLeafPairs t = {f : ↥t.Leaves × ↥t.Leaves | f.1 ≠ f.2}

@[simp]

theorem Anderson4D.mem_distinctLeafPairs {t : PlaneTree} {f : ↥t.Leaves × ↥t.Leaves} : f ∈ distinctLeafPairs t ↔ f.1 ≠ f.2

theorem Anderson4D.doublyAnchoredLeafEmbeddings_same_leaf_eq_empty {t : PlaneTree} {M : ℕ} (N : t.BranchExponentData (4 * M)) (hN : N.IsValid) (f : ↥t.Leaves) (z₀ z₁ : Fin 4 → ℤ) (hne : z₀ ≠ z₁) : doublyAnchoredLeafEmbeddings N hN f f z₀ z₁ = ∅

A single leaf cannot be anchored at two distinct lattice points.

theorem Anderson4D.J01_same_leaf_eq_zero {t : PlaneTree} {M : ℕ} (N : t.BranchExponentData (4 * M)) (hN : N.IsValid) (f : ↥t.Leaves) (z₀ z₁ : Fin 4 → ℤ) (hne : z₀ ≠ z₁) : J01 N hN f f z₀ z₁ = 0

theorem Anderson4D.admissibleLeafEmbeddingsContainingPair_eq_biUnion_distinctAnchored {t : PlaneTree} {M : ℕ} (N : t.BranchExponentData (4 * M)) (hN : N.IsValid) (z₀ z₁ : Fin 4 → ℤ) (hne : z₀ ≠ z₁) : admissibleLeafEmbeddingsContainingPair N hN z₀ z₁ = (distinctLeafPairs t).biUnion fun (f : ↥t.Leaves × ↥t.Leaves) => doublyAnchoredLeafEmbeddings N hN f.1 f.2 z₀ z₁

If z₀ ≠ z₁, the two-point image carrier is already covered by anchoring ordered pairs of distinct leaves.

theorem Anderson4D.card_admissibleLeafEmbeddingsContainingPair_le_sum_J01_distinct {t : PlaneTree} {M : ℕ} (N : t.BranchExponentData (4 * M)) (hN : N.IsValid) (z₀ z₁ : Fin 4 → ℤ) (hne : z₀ ≠ z₁) : (admissibleLeafEmbeddingsContainingPair N hN z₀ z₁).card ≤ ∑ f ∈ distinctLeafPairs t, J01 N hN f.1 f.2 z₀ z₁

Distinct-point version of the ordered leaf-pair union bound.

theorem Anderson4D.card_autHeppMarked_mul_card_realizedSetsContainingPair_le_sum_J01_distinct {t : PlaneTree} {M : ℕ} (N : t.BranchExponentData (4 * M)) (hN : N.IsValid) (z₀ z₁ : Fin 4 → ℤ) (hne : z₀ ≠ z₁) : Fintype.card ↥(t.AutHeppMarked (N.toHeppMarking hN)) * (realizedSetsContainingPair N hN z₀ z₁).card ≤ ∑ f ∈ distinctLeafPairs t, J01 N hN f.1 f.2 z₀ z₁

Full two-anchor Step 2 reduction with diagonal leaf pairs removed when the prescribed points are distinct.