Finite restrictions of admissible embeddings to Hepp-tree clusters

This file supplies the carrier-level interface needed by paper §5.3, Steps 5--6. The geometric lemmas work on leavesUnder v, whereas the finite counting carrier in AnchoredEmbeddings consists of full leaf embeddings. We bridge the two without introducing a new admissibility notion: a cluster restriction is, by definition, the restriction of an actual globally admissible embedding.

@[reducible, inline]

abbrev Anderson4D.ClusterEmbeddingAt {t : PlaneTree} (v : t.VPos) : Type

An embedding of the leaves below a fixed vertex.

Equations

• Anderson4D.ClusterEmbeddingAt v = (Anderson4D.ClusterLeafAt v → Fin 4 → ℤ)

def Anderson4D.restrictLeafEmbedding {t : PlaneTree} (z : LeafEmbedding t) (v : t.VPos) : ClusterEmbeddingAt v

Restrict a full leaf embedding to the leaves below v.

Equations

• Anderson4D.restrictLeafEmbedding z v l = z ↑l

theorem Anderson4D.leaf_under_parent_of_under_child {t : PlaneTree} {v c : t.VPos} (hc : c ∈ childrenOf v) {l : ↥t.Leaves} (hl : l ∈ leavesUnder c) : l ∈ leavesUnder v

A leaf below a child is canonically a leaf below its parent.

def Anderson4D.clusterLeafInclusion {t : PlaneTree} {v c : t.VPos} (hc : c ∈ childrenOf v) : ClusterLeafAt c ↪ ClusterLeafAt v

Inclusion of a child-cluster leaf carrier into the parent cluster.

Equations

• Anderson4D.clusterLeafInclusion hc = { toFun := fun (l : Anderson4D.ClusterLeafAt c) => ⟨↑l, ⋯⟩, inj' := ⋯ }

def Anderson4D.restrictClusterEmbedding {t : PlaneTree} {v c : t.VPos} (hc : c ∈ childrenOf v) (z : ClusterEmbeddingAt v) : ClusterEmbeddingAt c

Restrict a parent-cluster embedding to one immediate child.

Equations

• Anderson4D.restrictClusterEmbedding hc z l = z ((Anderson4D.clusterLeafInclusion hc) l)

@[simp]

theorem Anderson4D.restrictClusterEmbedding_restrictLeafEmbedding {t : PlaneTree} (z : LeafEmbedding t) {v c : t.VPos} (hc : c ∈ childrenOf v) : restrictClusterEmbedding hc (restrictLeafEmbedding z v) = restrictLeafEmbedding z c

noncomputable def Anderson4D.clusterRestrictions {t : PlaneTree} {M : ℕ} (N : t.BranchExponentData (4 * M)) (hN : N.IsValid) (v : t.VPos) : Finset (ClusterEmbeddingAt v)

The finite carrier of restrictions of actual admissible embeddings.

Equations

• Anderson4D.clusterRestrictions N hN v = Finset.image (fun (z : Anderson4D.LeafEmbedding t) => Anderson4D.restrictLeafEmbedding z v) (Anderson4D.admissibleLeafEmbeddings N hN)

@[simp]

theorem Anderson4D.mem_clusterRestrictions {t : PlaneTree} {M : ℕ} {N : t.BranchExponentData (4 * M)} {hN : N.IsValid} {v : t.VPos} {zv : ClusterEmbeddingAt v} : zv ∈ clusterRestrictions N hN v ↔ ∃ z ∈ admissibleLeafEmbeddings N hN, restrictLeafEmbedding z v = zv

noncomputable def Anderson4D.anchoredClusterRestrictions {t : PlaneTree} {M : ℕ} (N : t.BranchExponentData (4 * M)) (hN : N.IsValid) (v : t.VPos) (f : ClusterLeafAt v) (x : Fin 4 → ℤ) : Finset (ClusterEmbeddingAt v)

Actual cluster restrictions with one specified cluster leaf anchored.

Equations

• Anderson4D.anchoredClusterRestrictions N hN v f x = {zv ∈ Anderson4D.clusterRestrictions N hN v | zv f = x}

@[simp]

theorem Anderson4D.mem_anchoredClusterRestrictions {t : PlaneTree} {M : ℕ} {N : t.BranchExponentData (4 * M)} {hN : N.IsValid} {v : t.VPos} {f : ClusterLeafAt v} {x : Fin 4 → ℤ} {zv : ClusterEmbeddingAt v} : zv ∈ anchoredClusterRestrictions N hN v f x ↔ zv ∈ clusterRestrictions N hN v ∧ zv f = x

noncomputable def Anderson4D.clusterJ0 {t : PlaneTree} {M : ℕ} (N : t.BranchExponentData (4 * M)) (hN : N.IsValid) (v : t.VPos) (f : ClusterLeafAt v) (x : Fin 4 → ℤ) : ℕ

Cardinality of the one-anchor actual cluster carrier.

Equations

• Anderson4D.clusterJ0 N hN v f x = (Anderson4D.anchoredClusterRestrictions N hN v f x).card

noncomputable def Anderson4D.doublyAnchoredClusterRestrictions {t : PlaneTree} {M : ℕ} (N : t.BranchExponentData (4 * M)) (hN : N.IsValid) (v : t.VPos) (f₀ f₁ : ClusterLeafAt v) (x₀ x₁ : Fin 4 → ℤ) : Finset (ClusterEmbeddingAt v)

Actual cluster restrictions with two specified cluster leaves anchored.

Equations

• Anderson4D.doublyAnchoredClusterRestrictions N hN v f₀ f₁ x₀ x₁ = {zv ∈ Anderson4D.clusterRestrictions N hN v | zv f₀ = x₀ ∧ zv f₁ = x₁}

@[simp]

theorem Anderson4D.mem_doublyAnchoredClusterRestrictions {t : PlaneTree} {M : ℕ} {N : t.BranchExponentData (4 * M)} {hN : N.IsValid} {v : t.VPos} {f₀ f₁ : ClusterLeafAt v} {x₀ x₁ : Fin 4 → ℤ} {zv : ClusterEmbeddingAt v} : zv ∈ doublyAnchoredClusterRestrictions N hN v f₀ f₁ x₀ x₁ ↔ zv ∈ clusterRestrictions N hN v ∧ zv f₀ = x₀ ∧ zv f₁ = x₁

noncomputable def Anderson4D.clusterJ01 {t : PlaneTree} {M : ℕ} (N : t.BranchExponentData (4 * M)) (hN : N.IsValid) (v : t.VPos) (f₀ f₁ : ClusterLeafAt v) (x₀ x₁ : Fin 4 → ℤ) : ℕ

Cardinality of the two-anchor actual cluster carrier.

Equations

• Anderson4D.clusterJ01 N hN v f₀ f₁ x₀ x₁ = (Anderson4D.doublyAnchoredClusterRestrictions N hN v f₀ f₁ x₀ x₁).card

theorem Anderson4D.restrictClusterEmbedding_mem {t : PlaneTree} {M : ℕ} {N : t.BranchExponentData (4 * M)} {hN : N.IsValid} {v c : t.VPos} (hc : c ∈ childrenOf v) {zv : ClusterEmbeddingAt v} (hzv : zv ∈ clusterRestrictions N hN v) : restrictClusterEmbedding hc zv ∈ clusterRestrictions N hN c

Restriction preserves membership in the actual carrier.

Canonical extension and cover witnesses

noncomputable def Anderson4D.clusterExtension {t : PlaneTree} {M : ℕ} (N : t.BranchExponentData (4 * M)) (hN : N.IsValid) (v : t.VPos) (zv : ClusterEmbeddingAt v) (hzv : zv ∈ clusterRestrictions N hN v) : LeafEmbedding t

Choose one globally admissible extension of an actual cluster restriction.

Equations

• Anderson4D.clusterExtension N hN v zv hzv = Classical.choose ⋯

theorem Anderson4D.clusterExtension_mem {t : PlaneTree} {M : ℕ} (N : t.BranchExponentData (4 * M)) (hN : N.IsValid) (v : t.VPos) (zv : ClusterEmbeddingAt v) (hzv : zv ∈ clusterRestrictions N hN v) : clusterExtension N hN v zv hzv ∈ admissibleLeafEmbeddings N hN

theorem Anderson4D.clusterExtension_admissible {t : PlaneTree} {M : ℕ} (N : t.BranchExponentData (4 * M)) (hN : N.IsValid) (v : t.VPos) (zv : ClusterEmbeddingAt v) (hzv : zv ∈ clusterRestrictions N hN v) : IsAdmissible (N.toHeppMarking hN) M (clusterExtension N hN v zv hzv)

theorem Anderson4D.clusterExtension_restrict {t : PlaneTree} {M : ℕ} (N : t.BranchExponentData (4 * M)) (hN : N.IsValid) (v : t.VPos) (zv : ClusterEmbeddingAt v) (hzv : zv ∈ clusterRestrictions N hN v) : restrictLeafEmbedding (clusterExtension N hN v zv hzv) v = zv

@[simp]

theorem Anderson4D.clusterExtension_value {t : PlaneTree} {M : ℕ} (N : t.BranchExponentData (4 * M)) (hN : N.IsValid) (v : t.VPos) (zv : ClusterEmbeddingAt v) (hzv : zv ∈ clusterRestrictions N hN v) (l : ClusterLeafAt v) : clusterExtension N hN v zv hzv ↑l = zv l

noncomputable def Anderson4D.actualClusterCover {t : PlaneTree} {M : ℕ} (N : t.BranchExponentData (4 * M)) (hN : N.IsValid) (v : t.VPos) (zv : ClusterEmbeddingAt v) (hzv : zv ∈ clusterRestrictions N hN v) (R : ℝ) (hR : 0 < R) : Finset (Fin 4 → ℤ)

A canonical Step-4(b) cover of an actual cluster restriction.

Equations

• Anderson4D.actualClusterCover N hN v zv hzv R hR = Classical.choose ⋯

theorem Anderson4D.actualClusterCover_spec {t : PlaneTree} {M : ℕ} (N : t.BranchExponentData (4 * M)) (hN : N.IsValid) (v : t.VPos) (zv : ClusterEmbeddingAt v) (hzv : zv ∈ clusterRestrictions N hN v) (R : ℝ) (hR : 0 < R) : have Q := actualClusterCover N hN v zv hzv R hR; Q ⊆ Finset.image (clusterExtension N hN v zv hzv) (leavesUnder v) ∧ (∀ l ∈ leavesUnder v, ∃ q ∈ Q, znorm (clusterExtension N hN v zv hzv l - q) ≤ R) ∧ ↑Q.card ≤ 3 * (1 + tildeScale (N.toHeppMarking hN) v / R)

Child partition of a non-leaf cluster

def Anderson4D.clusterChildAt {t : PlaneTree} (v : t.VPos) (i : Fin (t.childCount ↑v)) : t.VPos

Child number i of v, represented as a vertex position.

Equations

• Anderson4D.clusterChildAt v i = ⟨↑v ++ [↑i], ⋯⟩

@[simp]

theorem Anderson4D.clusterChildAt_mem_childrenOf {t : PlaneTree} (v : t.VPos) (i : Fin (t.childCount ↑v)) : clusterChildAt v i ∈ childrenOf v

theorem Anderson4D.exists_child_containing_clusterLeaf {t : PlaneTree} {v : t.VPos} (hv : 0 < t.childCount ↑v) (l : ClusterLeafAt v) : ∃ (c : ClusterChild v), ↑l ∈ leavesUnder ↑c

Every leaf below a non-leaf vertex belongs to one immediate child.

theorem Anderson4D.child_eq_of_common_clusterLeaf {t : PlaneTree} {v : t.VPos} {c d : ClusterChild v} {l : ↥t.Leaves} (hlc : l ∈ leavesUnder ↑c) (hld : l ∈ leavesUnder ↑d) : c = d

Two immediate children containing the same leaf are equal.

def Anderson4D.restrictEmbeddingToChildren {t : PlaneTree} {v : t.VPos} (z : ClusterEmbeddingAt v) (c : ClusterChild v) : ClusterEmbeddingAt ↑c

The tuple of all immediate-child restrictions.

Equations

• Anderson4D.restrictEmbeddingToChildren z c = Anderson4D.restrictClusterEmbedding ⋯ z

theorem Anderson4D.restrictEmbeddingToChildren_injective {t : PlaneTree} {v : t.VPos} (hv : 0 < t.childCount ↑v) : Function.Injective restrictEmbeddingToChildren

A parent embedding is determined by all of its child restrictions.

Root carrier and the paper's J₀

def Anderson4D.rootClusterLeaf {t : PlaneTree} (f : ↥t.Leaves) : ClusterLeafAt t.rootV

Regard a full-tree leaf as a leaf of the root cluster.

Equations

• Anderson4D.rootClusterLeaf f = ⟨f, ⋯⟩

theorem Anderson4D.restrictLeafEmbedding_root_injective (t : PlaneTree) : Function.Injective fun (z : LeafEmbedding t) => restrictLeafEmbedding z t.rootV

Restriction to the root is injective on all leaf embeddings.

theorem Anderson4D.anchoredClusterRestrictions_root_eq_image {t : PlaneTree} {M : ℕ} (N : t.BranchExponentData (4 * M)) (hN : N.IsValid) (f : ↥t.Leaves) (x : Fin 4 → ℤ) : anchoredClusterRestrictions N hN t.rootV (rootClusterLeaf f) x = Finset.image (fun (z : LeafEmbedding t) => restrictLeafEmbedding z t.rootV) (anchoredLeafEmbeddings N hN f x)

The anchored root-restriction carrier is exactly the image of the paper's full-tree anchored carrier.

theorem Anderson4D.clusterJ0_root_eq_J0 {t : PlaneTree} {M : ℕ} (N : t.BranchExponentData (4 * M)) (hN : N.IsValid) (f : ↥t.Leaves) (x : Fin 4 → ℤ) : clusterJ0 N hN t.rootV (rootClusterLeaf f) x = J0 N hN f x

At the root, the actual cluster count is literally the paper's J₀.

theorem Anderson4D.doublyAnchoredClusterRestrictions_root_eq_image {t : PlaneTree} {M : ℕ} (N : t.BranchExponentData (4 * M)) (hN : N.IsValid) (f₀ f₁ : ↥t.Leaves) (x₀ x₁ : Fin 4 → ℤ) : doublyAnchoredClusterRestrictions N hN t.rootV (rootClusterLeaf f₀) (rootClusterLeaf f₁) x₀ x₁ = Finset.image (fun (z : LeafEmbedding t) => restrictLeafEmbedding z t.rootV) (doublyAnchoredLeafEmbeddings N hN f₀ f₁ x₀ x₁)

The two-anchor root carrier is the image of the paper's full-tree two-anchor carrier.

theorem Anderson4D.clusterJ01_root_eq_J01 {t : PlaneTree} {M : ℕ} (N : t.BranchExponentData (4 * M)) (hN : N.IsValid) (f₀ f₁ : ↥t.Leaves) (x₀ x₁ : Fin 4 → ℤ) : clusterJ01 N hN t.rootV (rootClusterLeaf f₀) (rootClusterLeaf f₁) x₀ x₁ = J01 N hN f₀ f₁ x₀ x₁

At the root, the actual two-anchor cluster count is the paper's J₀₁.

A reusable finite exposure bound

noncomputable def Anderson4D.HasExposureBounds {α : Type u_1} {ι : Type u_2} {κ : Type u_3} [DecidableEq α] [DecidableEq κ] (coord : ι → α → κ) (B : ι → ℝ) : Finset α → List ι → Prop

Recursive certificate for revealing one coordinate at a time.

At a head coordinate its image has size at most B i; in each resulting fiber the tail coordinates satisfy the same certificate. Once no coordinates remain, at most one object is allowed.

Equations

• One or more equations did not get rendered due to their size.
• Anderson4D.HasExposureBounds coord B x✝ [] = (x✝.card ≤ 1)

theorem Anderson4D.card_le_prod_of_hasExposureBounds {α : Type u_1} {ι : Type u_2} {κ : Type u_3} [DecidableEq α] [DecidableEq κ] (coord : ι → α → κ) (B : ι → ℝ) (S : Finset α) (L : List ι) (hB : ∀ i ∈ L, 0 ≤ B i) (h : HasExposureBounds coord B S L) : ↑S.card ≤ (List.map B L).prod

Multiplication of the successive image bounds in an exposure certificate. This is the finite fiber-counting step used to multiply the one-child estimate (5.23) through a parent-before-child list.

def Anderson4D.childRestrictionCoordinate {t : PlaneTree} {v : t.VPos} (c : ClusterChild v) (z : ClusterEmbeddingAt v) : (c : ClusterChild v) ×' ClusterEmbeddingAt ↑c

A common sigma codomain for exposing child restrictions.

Equations

• Anderson4D.childRestrictionCoordinate c z = ⟨c, Anderson4D.restrictClusterEmbedding ⋯ z⟩