The volume estimate of Proposition 5.6

Paper: D-hepp — Prop 5.6 — the volume estimate (5.12)–(5.14)

This file connects the finite actual-cluster carriers to the scalar bookkeeping in VolumeIteration, then states the division-free forms of paper (5.13) and (5.14).

theorem Anderson4D.one_le_leafCount (t : PlaneTree) : 1 ≤ t.leafCount

Every plane tree has at least one paper leaf.

theorem Anderson4D.scaleN_branchDescendant_le {t : PlaneTree} (ht : t.isValid = true) (Nm : t.HeppMarking) {v u : t.VPos} (hu : u ∈ branchDescendants v) : scaleN Nm u ≤ scaleN Nm v

A branching descendant has no larger dyadic scale than its ancestor.

theorem Anderson4D.tildeScale_le_two_mul_leafCount_mul_scaleN {t : PlaneTree} (ht : t.isValid = true) (Nm : t.HeppMarking) (v : t.VPos) : tildeScale Nm v ≤ 2 * ↑t.leafCount * ↑(scaleN Nm v)

Crude local form of the paper's final O(r²) comparison: the accumulated scale below any vertex is at most 2r times its own dyadic scale.

The concrete one-child placement set

theorem Anderson4D.znorm_triangle (x y z : LatticePoint) : znorm (x - z) ≤ znorm (x - y) + znorm (y - z)

Triangle inequality for the lattice sup norm.

noncomputable def Anderson4D.actualLinkParent {t : PlaneTree} {M : ℕ} (N : t.BranchExponentData (4 * M)) (hN : N.IsValid) {v : t.VPos} (hv : v ∈ t.BranchNodes) (zv : ClusterEmbeddingAt v) (hzv : zv ∈ clusterRestrictions N hN v) (root : ClusterChild v) : ClusterChild v → ClusterChild v

The canonical shortest-path parent function extracted from an actual cluster restriction.

Equations

• Anderson4D.actualLinkParent N hN hv zv hzv root = Anderson4D.linkParent hv ⋯ root

noncomputable def Anderson4D.childAnchorCandidates {t : PlaneTree} {M : ℕ} (N : t.BranchExponentData (4 * M)) (hN : N.IsValid) {v : t.VPos} (p c : ClusterChild v) (ep : ClusterEmbeddingAt ↑p) (hep : ep ∈ clusterRestrictions N hN ↑p) : Finset LatticePoint

Possible values of a representative leaf of child c, after the restriction on its selected parent child p has been fixed.

Equations

• One or more equations did not get rendered due to their size.

theorem Anderson4D.card_childAnchorCandidates_le {t : PlaneTree} {M : ℕ} (N : t.BranchExponentData (4 * M)) (hN : N.IsValid) {v : t.VPos} (p c : ClusterChild v) (ep : ClusterEmbeddingAt ↑p) (hep : ep ∈ clusterRestrictions N hN ↑p) : ↑(childAnchorCandidates N hN p c ep hep).card ≤ ↑step5LatticeConstant * ↑(scaleN (N.toHeppMarking hN) v) ^ 4 * (1 + tildeScale (N.toHeppMarking hN) ↑p / ↑(scaleN (N.toHeppMarking hN) v)) * (1 + tildeScale (N.toHeppMarking hN) ↑c / ↑(scaleN (N.toHeppMarking hN) v)) ^ 4

Cardinality form of the one-child lattice estimate (5.23).

theorem Anderson4D.childAnchor_mem_candidates {t : PlaneTree} {M : ℕ} (N : t.BranchExponentData (4 * M)) (hN : N.IsValid) {v : t.VPos} (hv : v ∈ t.BranchNodes) (zv : ClusterEmbeddingAt v) (hzv : zv ∈ clusterRestrictions N hN v) (root c p : ClusterChild v) (hc : c ≠ root) (hp : actualLinkParent N hN hv zv hzv root c = p) (f : ClusterLeafAt ↑c) : zv ((clusterLeafInclusion ⋯) f) ∈ childAnchorCandidates N hN p c (restrictClusterEmbedding ⋯ zv) ⋯

The representative of every non-root child selected by the canonical link parent lies in its concrete (5.23) placement set.

One-child finite-fiber count

theorem Anderson4D.card_childRestriction_image_le {t : PlaneTree} {M : ℕ} (N : t.BranchExponentData (4 * M)) (hN : N.IsValid) {v : t.VPos} (hv : v ∈ t.BranchNodes) (root c p : ClusterChild v) (hc : c ≠ root) (S : Finset (ClusterEmbeddingAt v)) (hS : ∀ zv ∈ S, zv ∈ clusterRestrictions N hN v) (ep : ClusterEmbeddingAt ↑p) (hep : ep ∈ clusterRestrictions N hN ↑p) (hparent : ∀ (zv : ClusterEmbeddingAt v) (hzvS : zv ∈ S), actualLinkParent N hN hv zv ⋯ root c = p) (hfixed : ∀ zv ∈ S, restrictClusterEmbedding ⋯ zv = ep) (f : ClusterLeafAt ↑c) (A : ℝ) (hA : 0 ≤ A) (hchild : ∀ (x : LatticePoint), ↑(clusterJ0 N hN (↑c) f x) ≤ A) : ↑(Finset.image (fun (zv : ClusterEmbeddingAt v) => restrictClusterEmbedding ⋯ zv) S).card ≤ ↑step5LatticeConstant * ↑(scaleN (N.toHeppMarking hN) v) ^ 4 * (1 + tildeScale (N.toHeppMarking hN) ↑p / ↑(scaleN (N.toHeppMarking hN) v)) * (1 + tildeScale (N.toHeppMarking hN) ↑c / ↑(scaleN (N.toHeppMarking hN) v)) ^ 4 * A

Once a selected parent restriction is fixed, the possible restrictions on one non-root child are bounded by its (5.23) placement count times a uniform bound for the internally anchored child carrier.

Parent-before-child exposure order

def Anderson4D.IsSuffixExposure {α : Type u_1} [BEq α] [LawfulBEq α] (p : α → α) (root : α) : List α → Prop

In every suffix, its head is either the distinguished root or its selected parent has already disappeared from that suffix.

Equations

• Anderson4D.IsSuffixExposure p root [] = True
• Anderson4D.IsSuffixExposure p root (c :: cs) = ((c = root ∨ p c ∉ c :: cs) ∧ Anderson4D.IsSuffixExposure p root cs)

theorem Anderson4D.isSuffixExposure_of_index {α : Type u_1} [BEq α] [LawfulBEq α] (p : α → α) (root : α) (L : List α) (hnodup : L.Nodup) (h : ∀ c ∈ L, c ≠ root → p c ∉ L ∨ List.idxOf (p c) L < List.idxOf c L) : IsSuffixExposure p root L

A strict parent-index decrease implies the recursive suffix exposure property, even after earlier vertices have been removed.

theorem Anderson4D.isSuffixExposure_actualLinkParent {t : PlaneTree} {M : ℕ} (N : t.BranchExponentData (4 * M)) (hN : N.IsValid) {v : t.VPos} (hv : v ∈ t.BranchNodes) (zv : ClusterEmbeddingAt v) (hzv : zv ∈ clusterRestrictions N hN v) (root : ClusterChild v) : IsSuffixExposure (actualLinkParent N hN hv zv hzv root) root (childrenByLinkDistance (N.toHeppMarking hN) (clusterExtension N hN v zv hzv) v root)

The distance-sorted child list of the canonical extension is a valid suffix exposure order for its selected parent function.

Multiplying the exposed child fibers

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

Every cluster of an actual restriction has a leaf.

noncomputable def Anderson4D.childExposureWeight {t : PlaneTree} (Nm : t.HeppMarking) {v : t.VPos} (root : ClusterChild v) (p : ClusterChild v → ClusterChild v) (W : ClusterChild v → ℝ) (c : ClusterChild v) : ℝ

Per-child factor revealed in the parent-before-child exposure.

Equations

• One or more equations did not get rendered due to their size.

theorem Anderson4D.childExposureWeight_nonneg {t : PlaneTree} (Nm : t.HeppMarking) {v : t.VPos} (root : ClusterChild v) (p : ClusterChild v → ClusterChild v) (W : ClusterChild v → ℝ) (hW : ∀ (c : ClusterChild v), 0 ≤ W c) (c : ClusterChild v) : 0 ≤ childExposureWeight Nm root p W c

theorem Anderson4D.card_clusterFiber_le_exposureProduct {t : PlaneTree} {M : ℕ} (N : t.BranchExponentData (4 * M)) (hN : N.IsValid) {v : t.VPos} (hv : v ∈ t.BranchNodes) (root : ClusterChild v) (froot : ClusterLeafAt ↑root) (x : LatticePoint) (p : ClusterChild v → ClusterChild v) (W : ClusterChild v → ℝ) (hW0 : ∀ (c : ClusterChild v), 0 ≤ W c) (hW : ∀ (c : ClusterChild v) (f : ClusterLeafAt ↑c) (y : LatticePoint), ↑(clusterJ0 N hN (↑c) f y) ≤ W c) (L : List (ClusterChild v)) (F : Finset (ClusterEmbeddingAt v)) (hF : ∀ zv ∈ F, zv ∈ clusterRestrictions N hN v) (hp : ∀ (zv : ClusterEmbeddingAt v) (hzvF : zv ∈ F), actualLinkParent N hN hv zv ⋯ root = p) (hanchor : ∀ zv ∈ F, restrictClusterEmbedding ⋯ zv froot = x) (hfixed : ∀ d ∉ L, ∀ zv ∈ F, ∀ zv' ∈ F, restrictClusterEmbedding ⋯ zv = restrictClusterEmbedding ⋯ zv') (hexposure : IsSuffixExposure p root L) : ↑F.card ≤ (List.map (childExposureWeight (N.toHeppMarking hN) root p W) L).prod

Fiberwise multiplication along a parent-before-child exposure list.

Two anchored leaves in one parent fiber

noncomputable def Anderson4D.pairChildExposureWeight {t : PlaneTree} (Nm : t.HeppMarking) {v : t.VPos} (root₀ root₁ : ClusterChild v) (p : ClusterChild v → ClusterChild v) (W : ClusterChild v → ℝ) (P : ℝ) (c : ClusterChild v) : ℝ

Child weight for the two-anchor exposure.

If both anchors lie in the root child, its recursive weight is replaced by the two-anchor weight P. If they lie in distinct children, the second anchored child pays the usual one-anchor placement weight times the saved factor N_v⁻⁴.

Equations

• One or more equations did not get rendered due to their size.

theorem Anderson4D.pairChildExposureWeight_nonneg {t : PlaneTree} (Nm : t.HeppMarking) {v : t.VPos} (root₀ root₁ : ClusterChild v) (p : ClusterChild v → ClusterChild v) (W : ClusterChild v → ℝ) (hW0 : ∀ (c : ClusterChild v), 0 ≤ W c) (P : ℝ) (hP0 : 0 ≤ P) (c : ClusterChild v) : 0 ≤ pairChildExposureWeight Nm root₀ root₁ p W P c

theorem Anderson4D.childWeight_le_exposureWeight_mul_lcaScaleGain {t : PlaneTree} (Nm : t.HeppMarking) {v : t.VPos} (root c : ClusterChild v) (hc : c ≠ root) (p : ClusterChild v → ClusterChild v) (W : ClusterChild v → ℝ) (hW0 : 0 ≤ W c) : W c ≤ childExposureWeight Nm root p W c * lcaScaleGain Nm v

Fixing an anchor in a non-root child is no more expensive than the ordinary placement weight with the N_v⁻⁴ gain inserted.

theorem Anderson4D.card_clusterPairFiber_le_exposureProduct {t : PlaneTree} {M : ℕ} (N : t.BranchExponentData (4 * M)) (hN : N.IsValid) {v : t.VPos} (hv : v ∈ t.BranchNodes) (root₀ root₁ : ClusterChild v) (froot₀ : ClusterLeafAt ↑root₀) (froot₁ : ClusterLeafAt ↑root₁) (x₀ x₁ : LatticePoint) (p : ClusterChild v → ClusterChild v) (W : ClusterChild v → ℝ) (hW0 : ∀ (c : ClusterChild v), 0 ≤ W c) (hW : ∀ (c : ClusterChild v) (f : ClusterLeafAt ↑c) (y : LatticePoint), ↑(clusterJ0 N hN (↑c) f y) ≤ W c) (P : ℝ) (hP0 : 0 ≤ P) (hP : ∀ (hsame : root₀ = root₁), ↑(clusterJ01 N hN (↑root₀) froot₀ (⋯ ▸ froot₁) x₀ x₁) ≤ P) (L : List (ClusterChild v)) (F : Finset (ClusterEmbeddingAt v)) (hF : ∀ zv ∈ F, zv ∈ clusterRestrictions N hN v) (hp : ∀ (zv : ClusterEmbeddingAt v) (hzvF : zv ∈ F), actualLinkParent N hN hv zv ⋯ root₀ = p) (hanchor₀ : ∀ zv ∈ F, restrictClusterEmbedding ⋯ zv froot₀ = x₀) (hanchor₁ : ∀ zv ∈ F, restrictClusterEmbedding ⋯ zv froot₁ = x₁) (hfixed : ∀ d ∉ L, ∀ zv ∈ F, ∀ zv' ∈ F, restrictClusterEmbedding ⋯ zv = restrictClusterEmbedding ⋯ zv') (hexposure : IsSuffixExposure p root₀ L) : ↑F.card ≤ (List.map (pairChildExposureWeight (N.toHeppMarking hN) root₀ root₁ p W P) L).prod

Fiberwise exposure with two fixed anchored leaves. This is the carrier-level Step 6 refinement: in the split-child case the second fixed anchor removes one lattice placement.

One branch: summing the canonical parent-function fibers

noncomputable def Anderson4D.anchorRootChild {t : PlaneTree} {v : t.VPos} (hv : v ∈ t.BranchNodes) (f : ClusterLeafAt v) : ClusterChild v

The immediate child containing an anchored cluster leaf.

Equations

• Anderson4D.anchorRootChild hv f = Classical.choose ⋯

theorem Anderson4D.anchorRootChild_contains {t : PlaneTree} {v : t.VPos} (hv : v ∈ t.BranchNodes) (f : ClusterLeafAt v) : ↑f ∈ leavesUnder ↑(anchorRootChild hv f)

def Anderson4D.anchorLeafInRootChild {t : PlaneTree} {v : t.VPos} (hv : v ∈ t.BranchNodes) (f : ClusterLeafAt v) : ClusterLeafAt ↑(anchorRootChild hv f)

The anchored leaf, viewed inside its immediate root child.

Equations

• Anderson4D.anchorLeafInRootChild hv f = ⟨↑f, ⋯⟩

theorem Anderson4D.cast_clusterLeafAt_val {t : PlaneTree} {v : t.VPos} {c d : ClusterChild v} (h : c = d) (f : ClusterLeafAt ↑d) : ↑(⋯ ▸ f) = ↑f

Transporting a cluster leaf across equality of its cluster child does not change the underlying global leaf.

noncomputable def Anderson4D.anchoredParentCode {t : PlaneTree} {M : ℕ} (N : t.BranchExponentData (4 * M)) (hN : N.IsValid) {v : t.VPos} (hv : v ∈ t.BranchNodes) (f : ClusterLeafAt v) (x : LatticePoint) (zv : ClusterEmbeddingAt v) : ClusterChild v → ClusterChild v

Total parent-code function used to partition an anchored carrier. Away from that carrier it takes the harmless identity fallback.

Equations

• One or more equations did not get rendered due to their size.

theorem Anderson4D.anchoredParentCode_eq {t : PlaneTree} {M : ℕ} (N : t.BranchExponentData (4 * M)) (hN : N.IsValid) {v : t.VPos} (hv : v ∈ t.BranchNodes) (f : ClusterLeafAt v) (x : LatticePoint) {zv : ClusterEmbeddingAt v} (hzv : zv ∈ anchoredClusterRestrictions N hN v f x) : anchoredParentCode N hN hv f x zv = actualLinkParent N hN hv zv ⋯ (anchorRootChild hv f)

theorem Anderson4D.prod_childExposureWeight_eq {t : PlaneTree} (Nm : t.HeppMarking) {v : t.VPos} (root : ClusterChild v) (p : ClusterChild v → ClusterChild v) (hpRoot : p root = root) (W : ClusterChild v → ℝ) : ∏ c : ClusterChild v, childExposureWeight Nm root p W c = (∏ c : ClusterChild v, W c) * fullParentWeight root (fun (c : ClusterChild v) => 1 + tildeScale Nm ↑c / ↑(scaleN Nm v)) (fun (c : ClusterChild v) => ↑step5LatticeConstant * ↑(scaleN Nm v) ^ 4 * (1 + tildeScale Nm ↑c / ↑(scaleN Nm v)) ^ 4) p

Product of the exposed child factors, separated into the recursive child counts and the fullParentWeight consumed by Step 5.

theorem Anderson4D.card_anchoredParentFiber_le {t : PlaneTree} {M : ℕ} (N : t.BranchExponentData (4 * M)) (hN : N.IsValid) {v : t.VPos} (hv : v ∈ t.BranchNodes) (f : ClusterLeafAt v) (x : LatticePoint) (W : ClusterChild v → ℝ) (hW0 : ∀ (c : ClusterChild v), 0 ≤ W c) (hW : ∀ (c : ClusterChild v) (fc : ClusterLeafAt ↑c) (y : LatticePoint), ↑(clusterJ0 N hN (↑c) fc y) ≤ W c) (p : ClusterChild v → ClusterChild v) : have A := anchoredClusterRestrictions N hN v f x; have F := {zv ∈ A | anchoredParentCode N hN hv f x zv = p}; ↑F.card ≤ (∏ c : ClusterChild v, W c) * fullParentWeight (anchorRootChild hv f) (fun (c : ClusterChild v) => 1 + tildeScale (N.toHeppMarking hN) ↑c / ↑(scaleN (N.toHeppMarking hN) v)) (fun (c : ClusterChild v) => ↑step5LatticeConstant * ↑(scaleN (N.toHeppMarking hN) v) ^ 4 * (1 + tildeScale (N.toHeppMarking hN) ↑c / ↑(scaleN (N.toHeppMarking hN) v)) ^ 4) p

Bound one fiber of the canonical parent code by its full parent weight.

theorem Anderson4D.prod_pairChildExposureWeight_eq_same {t : PlaneTree} (Nm : t.HeppMarking) {v : t.VPos} (root₀ root₁ : ClusterChild v) (hsame : root₀ = root₁) (p : ClusterChild v → ClusterChild v) (hpRoot : p root₀ = root₀) (W : ClusterChild v → ℝ) (P : ℝ) : ∏ c : ClusterChild v, pairChildExposureWeight Nm root₀ root₁ p W P c = (∏ c : ClusterChild v, if c = root₀ then P else W c) * fullParentWeight root₀ (fun (c : ClusterChild v) => 1 + tildeScale Nm ↑c / ↑(scaleN Nm v)) (fun (c : ClusterChild v) => ↑step5LatticeConstant * ↑(scaleN Nm v) ^ 4 * (1 + tildeScale Nm ↑c / ↑(scaleN Nm v)) ^ 4) p

Product identity when both fixed leaves lie in the same child.

theorem Anderson4D.prod_pairChildExposureWeight_eq_split {t : PlaneTree} (Nm : t.HeppMarking) {v : t.VPos} (root₀ root₁ : ClusterChild v) (hsplit : root₀ ≠ root₁) (p : ClusterChild v → ClusterChild v) (hpRoot : p root₀ = root₀) (W : ClusterChild v → ℝ) (P : ℝ) : ∏ c : ClusterChild v, pairChildExposureWeight Nm root₀ root₁ p W P c = (∏ c : ClusterChild v, W c) * fullParentWeight root₀ (fun (c : ClusterChild v) => 1 + tildeScale Nm ↑c / ↑(scaleN Nm v)) (fun (c : ClusterChild v) => ↑step5LatticeConstant * ↑(scaleN Nm v) ^ 4 * (1 + tildeScale Nm ↑c / ↑(scaleN Nm v)) ^ 4) p * lcaScaleGain Nm v

Product identity when the fixed leaves first split at the current branch. Exactly one factor N_v⁻⁴ survives.

noncomputable def Anderson4D.pairParentVolumeWeight {t : PlaneTree} (Nm : t.HeppMarking) {v : t.VPos} (root₀ root₁ : ClusterChild v) (p : ClusterChild v → ClusterChild v) (W : ClusterChild v → ℝ) (P : ℝ) : ℝ

Finalized parent-code weight. Unlike the raw exposure product, this vanishes on functions that do not fix the distinguished root child.

Equations

• One or more equations did not get rendered due to their size.

theorem Anderson4D.card_doublyAnchoredParentFiber_le {t : PlaneTree} {M : ℕ} (N : t.BranchExponentData (4 * M)) (hN : N.IsValid) {v : t.VPos} (hv : v ∈ t.BranchNodes) (f₀ f₁ : ClusterLeafAt v) (x₀ x₁ : LatticePoint) (W : ClusterChild v → ℝ) (hW0 : ∀ (c : ClusterChild v), 0 ≤ W c) (hW : ∀ (c : ClusterChild v) (fc : ClusterLeafAt ↑c) (y : LatticePoint), ↑(clusterJ0 N hN (↑c) fc y) ≤ W c) (P : ℝ) (hP0 : 0 ≤ P) (hP : ∀ (hsame : anchorRootChild hv f₀ = anchorRootChild hv f₁), ↑(clusterJ01 N hN (↑(anchorRootChild hv f₀)) (anchorLeafInRootChild hv f₀) (⋯ ▸ anchorLeafInRootChild hv f₁) x₀ x₁) ≤ P) (p : ClusterChild v → ClusterChild v) : have A := doublyAnchoredClusterRestrictions N hN v f₀ f₁ x₀ x₁; have F := {zv ∈ A | anchoredParentCode N hN hv f₀ x₀ zv = p}; ↑F.card ≤ ∏ c : ClusterChild v, pairChildExposureWeight (N.toHeppMarking hN) (anchorRootChild hv f₀) (anchorRootChild hv f₁) p W P c

Bound one two-anchor parent-code fiber by its exposed child product.

theorem Anderson4D.card_doublyAnchoredParentFiber_full_le {t : PlaneTree} {M : ℕ} (N : t.BranchExponentData (4 * M)) (hN : N.IsValid) {v : t.VPos} (hv : v ∈ t.BranchNodes) (f₀ f₁ : ClusterLeafAt v) (x₀ x₁ : LatticePoint) (W : ClusterChild v → ℝ) (hW0 : ∀ (c : ClusterChild v), 0 ≤ W c) (hW : ∀ (c : ClusterChild v) (fc : ClusterLeafAt ↑c) (y : LatticePoint), ↑(clusterJ0 N hN (↑c) fc y) ≤ W c) (P : ℝ) (hP0 : 0 ≤ P) (hP : ∀ (hsame : anchorRootChild hv f₀ = anchorRootChild hv f₁), ↑(clusterJ01 N hN (↑(anchorRootChild hv f₀)) (anchorLeafInRootChild hv f₀) (⋯ ▸ anchorLeafInRootChild hv f₁) x₀ x₁) ≤ P) (p : ClusterChild v → ClusterChild v) : have A := doublyAnchoredClusterRestrictions N hN v f₀ f₁ x₀ x₁; have F := {zv ∈ A | anchoredParentCode N hN hv f₀ x₀ zv = p}; ↑F.card ≤ pairParentVolumeWeight (N.toHeppMarking hN) (anchorRootChild hv f₀) (anchorRootChild hv f₁) p W P

Finalized two-anchor fiber bound, including the root-fixing factor of fullParentWeight. This wrapper is needed for empty fibers indexed by arbitrary parent functions.

theorem Anderson4D.clusterJ01_branch_parent_sum_le {t : PlaneTree} {M : ℕ} (N : t.BranchExponentData (4 * M)) (hN : N.IsValid) {v : t.VPos} (hv : v ∈ t.BranchNodes) (f₀ f₁ : ClusterLeafAt v) (x₀ x₁ : LatticePoint) (W : ClusterChild v → ℝ) (hW0 : ∀ (c : ClusterChild v), 0 ≤ W c) (hW : ∀ (c : ClusterChild v) (fc : ClusterLeafAt ↑c) (y : LatticePoint), ↑(clusterJ0 N hN (↑c) fc y) ≤ W c) (P : ℝ) (hP0 : 0 ≤ P) (hP : ∀ (hsame : anchorRootChild hv f₀ = anchorRootChild hv f₁), ↑(clusterJ01 N hN (↑(anchorRootChild hv f₀)) (anchorLeafInRootChild hv f₀) (⋯ ▸ anchorLeafInRootChild hv f₁) x₀ x₁) ≤ P) : ↑(clusterJ01 N hN v f₀ f₁ x₀ x₁) ≤ ∑ p : ClusterChild v → ClusterChild v, pairParentVolumeWeight (N.toHeppMarking hN) (anchorRootChild hv f₀) (anchorRootChild hv f₁) p W P

Two-anchor carrier estimate before evaluating the parent-function sum.

theorem Anderson4D.clusterJ01_branch_le_same {t : PlaneTree} {M : ℕ} (N : t.BranchExponentData (4 * M)) (hN : N.IsValid) {v : t.VPos} (hv : v ∈ t.BranchNodes) (f₀ f₁ : ClusterLeafAt v) (x₀ x₁ : LatticePoint) (hsame : anchorRootChild hv f₀ = anchorRootChild hv f₁) (W : ClusterChild v → ℝ) (hW0 : ∀ (c : ClusterChild v), 0 ≤ W c) (hW : ∀ (c : ClusterChild v) (fc : ClusterLeafAt ↑c) (y : LatticePoint), ↑(clusterJ0 N hN (↑c) fc y) ≤ W c) (P : ℝ) (hP0 : 0 ≤ P) (hP : ↑(clusterJ01 N hN (↑(anchorRootChild hv f₀)) (anchorLeafInRootChild hv f₀) (⋯ ▸ anchorLeafInRootChild hv f₁) x₀ x₁) ≤ P) : ↑(clusterJ01 N hN v f₀ f₁ x₀ x₁) ≤ (∏ c : ClusterChild v, if c = anchorRootChild hv f₀ then P else W c) * ↑(t.childCount ↑v).factorial * ↑step5VolumeConstant ^ (t.childCount ↑v - 1) * ↑(scaleN (N.toHeppMarking hN) v) ^ (4 * (t.childCount ↑v - 1)) * Real.exp (6 * ∑ c : ClusterChild v, tildeScale (N.toHeppMarking hN) ↑c / ↑(scaleN (N.toHeppMarking hN) v))

Evaluated branch recursion when both anchors remain in the same immediate child.

theorem Anderson4D.clusterJ01_branch_le_split {t : PlaneTree} {M : ℕ} (N : t.BranchExponentData (4 * M)) (hN : N.IsValid) {v : t.VPos} (hv : v ∈ t.BranchNodes) (f₀ f₁ : ClusterLeafAt v) (x₀ x₁ : LatticePoint) (hsplit : anchorRootChild hv f₀ ≠ anchorRootChild hv f₁) (W : ClusterChild v → ℝ) (hW0 : ∀ (c : ClusterChild v), 0 ≤ W c) (hW : ∀ (c : ClusterChild v) (fc : ClusterLeafAt ↑c) (y : LatticePoint), ↑(clusterJ0 N hN (↑c) fc y) ≤ W c) : ↑(clusterJ01 N hN v f₀ f₁ x₀ x₁) ≤ (∏ c : ClusterChild v, W c) * ↑(t.childCount ↑v).factorial * ↑step5VolumeConstant ^ (t.childCount ↑v - 1) * ↑(scaleN (N.toHeppMarking hN) v) ^ (4 * (t.childCount ↑v - 1)) * Real.exp (6 * ∑ c : ClusterChild v, tildeScale (N.toHeppMarking hN) ↑c / ↑(scaleN (N.toHeppMarking hN) v)) * lcaScaleGain (N.toHeppMarking hN) v

Evaluated branch recursion at the first child split.

theorem Anderson4D.clusterJ0_branch_parent_sum_le {t : PlaneTree} {M : ℕ} (N : t.BranchExponentData (4 * M)) (hN : N.IsValid) {v : t.VPos} (hv : v ∈ t.BranchNodes) (f : ClusterLeafAt v) (x : LatticePoint) (W : ClusterChild v → ℝ) (hW0 : ∀ (c : ClusterChild v), 0 ≤ W c) (hW : ∀ (c : ClusterChild v) (fc : ClusterLeafAt ↑c) (y : LatticePoint), ↑(clusterJ0 N hN (↑c) fc y) ≤ W c) : ↑(clusterJ0 N hN v f x) ≤ (∏ c : ClusterChild v, W c) * ∑ p : ClusterChild v → ClusterChild v, fullParentWeight (anchorRootChild hv f) (fun (c : ClusterChild v) => 1 + tildeScale (N.toHeppMarking hN) ↑c / ↑(scaleN (N.toHeppMarking hN) v)) (fun (c : ClusterChild v) => ↑step5LatticeConstant * ↑(scaleN (N.toHeppMarking hN) v) ^ 4 * (1 + tildeScale (N.toHeppMarking hN) ↑c / ↑(scaleN (N.toHeppMarking hN) v)) ^ 4) p

One-branch actual-carrier estimate before evaluating the sum over full parent functions.

theorem Anderson4D.clusterJ0_branch_le {t : PlaneTree} {M : ℕ} (N : t.BranchExponentData (4 * M)) (hN : N.IsValid) {v : t.VPos} (hv : v ∈ t.BranchNodes) (f : ClusterLeafAt v) (x : LatticePoint) (W : ClusterChild v → ℝ) (hW0 : ∀ (c : ClusterChild v), 0 ≤ W c) (hW : ∀ (c : ClusterChild v) (fc : ClusterLeafAt ↑c) (y : LatticePoint), ↑(clusterJ0 N hN (↑c) fc y) ≤ W c) : ↑(clusterJ0 N hN v f x) ≤ (∏ c : ClusterChild v, W c) * ↑(t.childCount ↑v).factorial * ↑step5VolumeConstant ^ (t.childCount ↑v - 1) * ↑(scaleN (N.toHeppMarking hN) v) ^ (4 * (t.childCount ↑v - 1)) * Real.exp (6 * ∑ c : ClusterChild v, tildeScale (N.toHeppMarking hN) ↑c / ↑(scaleN (N.toHeppMarking hN) v))

Evaluated one-branch recursion, the actual-carrier form of paper (5.25).

Iteration over branch descendants

noncomputable def Anderson4D.localRatioCost {t : PlaneTree} (Nm : t.HeppMarking) (v : t.VPos) : ℝ

The local exponential cost paid at one branching vertex.

Equations

• Anderson4D.localRatioCost Nm v = ∑ c : Anderson4D.ClusterChild v, Anderson4D.tildeScale Nm ↑c / ↑(Anderson4D.scaleN Nm v)

noncomputable def Anderson4D.branchVolumeFactor {t : PlaneTree} (Nm : t.HeppMarking) (v : t.VPos) : ℝ

Complete local factor contributed by one branch in (5.26).

Equations

• One or more equations did not get rendered due to their size.

noncomputable def Anderson4D.localIterationWeight {t : PlaneTree} (Nm : t.HeppMarking) (v : t.VPos) : ℝ

Product of all local branch factors below v.

Equations

• Anderson4D.localIterationWeight Nm v = ∏ u ∈ Anderson4D.branchDescendants v, Anderson4D.branchVolumeFactor Nm u

theorem Anderson4D.localRatioCost_nonneg {t : PlaneTree} (Nm : t.HeppMarking) (v : t.VPos) : 0 ≤ localRatioCost Nm v

theorem Anderson4D.one_le_branchVolumeFactor {t : PlaneTree} (Nm : t.HeppMarking) {v : t.VPos} (hv : v ∈ t.BranchNodes) : 1 ≤ branchVolumeFactor Nm v

theorem Anderson4D.branchDescendants_disjoint_of_children_ne {t : PlaneTree} {v c c' : t.VPos} (hc : c ∈ childrenOf v) (hc' : c' ∈ childrenOf v) (hne : c ≠ c') : Disjoint (branchDescendants c) (branchDescendants c')

Branch-descendant sets below distinct immediate children are disjoint.

theorem Anderson4D.biUnion_branchDescendants_subset_erase {t : PlaneTree} {v : t.VPos} : (childrenOf v).biUnion branchDescendants ⊆ (branchDescendants v).erase v

All child branch descendants are strict branch descendants of the parent.

theorem Anderson4D.prod_localIterationWeight_children_le {t : PlaneTree} (Nm : t.HeppMarking) (v : t.VPos) : ∏ c : ClusterChild v, localIterationWeight Nm ↑c ≤ ∏ u ∈ (branchDescendants v).erase v, branchVolumeFactor Nm u

Products of descendant weights over the immediate children fit inside the strict-descendant product of the parent.

theorem Anderson4D.branchVolumeFactor_mul_children_le_localIterationWeight {t : PlaneTree} (Nm : t.HeppMarking) {v : t.VPos} (hv : v ∈ t.BranchNodes) : branchVolumeFactor Nm v * ∏ c : ClusterChild v, localIterationWeight Nm ↑c ≤ localIterationWeight Nm v

Multiplying the current branch factor with all child subtree weights is bounded by the full descendant product at the current vertex.

Leaf base case and well-founded cluster iteration

theorem Anderson4D.childCount_pos_of_strict_prefix {t : PlaneTree} {v w : t.VPos} (hpre : ↑v <+: ↑w) (hne : v ≠ w) : 0 < t.childCount ↑v

A strict valid descendant forces a positive child count at its ancestor.

theorem Anderson4D.branchDescendants_eq_empty_of_leaf {t : PlaneTree} {v : t.VPos} (hv : v ∈ t.Leaves) : branchDescendants v = ∅

A leaf vertex has no branching descendants.

theorem Anderson4D.clusterLeafAt_eq_of_leaf {t : PlaneTree} {v : t.VPos} (hv : v ∈ t.Leaves) (a b : ClusterLeafAt v) : a = b

The cluster leaf carrier below a leaf vertex is a subsingleton.

theorem Anderson4D.clusterJ0_le_one_of_leaf {t : PlaneTree} {M : ℕ} (N : t.BranchExponentData (4 * M)) (hN : N.IsValid) {v : t.VPos} (hv : v ∈ t.Leaves) (f : ClusterLeafAt v) (x : LatticePoint) : clusterJ0 N hN v f x ≤ 1

An anchored actual restriction at a leaf has at most one element.

theorem Anderson4D.leaf_or_branch_of_valid {t : PlaneTree} (ht : t.isValid = true) (v : t.VPos) : v ∈ t.Leaves ∨ v ∈ t.BranchNodes

Every vertex of a valid Hepp tree is either a leaf or a branch.

theorem Anderson4D.localIterationWeight_nonneg {t : PlaneTree} (Nm : t.HeppMarking) (v : t.VPos) : 0 ≤ localIterationWeight Nm v

The local descendant product is nonnegative.

theorem Anderson4D.clusterJ0_le_localIterationWeight {t : PlaneTree} (ht : t.isValid = true) {M : ℕ} (N : t.BranchExponentData (4 * M)) (hN : N.IsValid) (v : t.VPos) (f : ClusterLeafAt v) (x : LatticePoint) : ↑(clusterJ0 N hN v f x) ≤ localIterationWeight (N.toHeppMarking hN) v

Actual-carrier iteration over every cluster below a valid tree.

Well-founded two-anchor iteration

theorem Anderson4D.lcaV_eq_of_under_distinct_children {t : PlaneTree} {v c c' : t.VPos} (hc : c ∈ childrenOf v) (hc' : c' ∈ childrenOf v) (hne : c ≠ c') {l l' : ↥t.Leaves} (hl : l ∈ leavesUnder c) (hl' : l' ∈ leavesUnder c') : lcaV ↑l ↑l' = v

Leaves below distinct immediate children have the parent as their lowest common ancestor.

theorem Anderson4D.lcaV_eq_of_anchorRootChild_ne {t : PlaneTree} {v : t.VPos} (hv : v ∈ t.BranchNodes) (f₀ f₁ : ClusterLeafAt v) (hne : anchorRootChild hv f₀ ≠ anchorRootChild hv f₁) : lcaV ↑↑f₀ ↑↑f₁ = v

theorem Anderson4D.prod_replace_mul_eq_prod_mul {α : Type u_1} [Fintype α] [DecidableEq α] (W : α → ℝ) (root : α) (gain : ℝ) : (∏ c : α, if c = root then W c * gain else W c) = (∏ c : α, W c) * gain

Replacing one factor by itself times gain multiplies the whole finite product by exactly gain.

theorem Anderson4D.clusterJ01_le_localIterationWeight_mul_lcaScaleGain {t : PlaneTree} (ht : t.isValid = true) {M : ℕ} (N : t.BranchExponentData (4 * M)) (hN : N.IsValid) (v : t.VPos) (f₀ f₁ : ClusterLeafAt v) (x₀ x₁ : LatticePoint) (hne : f₀ ≠ f₁) : ↑(clusterJ01 N hN v f₀ f₁ x₀ x₁) ≤ localIterationWeight (N.toHeppMarking hN) v * lcaScaleGain (N.toHeppMarking hN) (lcaV ↑↑f₀ ↑↑f₁)

Actual-carrier Step 6 iteration. The scale gain is created exactly at the first branch where the two distinct leaves split and is preserved through every ancestor above it.

Reindexing the accumulated local ratio cost

theorem Anderson4D.sum_tildeScale_children_le_strictDescendants {t : PlaneTree} (Nm : t.HeppMarking) (v : t.VPos) : ∑ c : ClusterChild v, tildeScale Nm ↑c ≤ ∑ u ∈ (branchDescendants v).erase v, ↑(t.childCount ↑u) * ↑(scaleN Nm u)

Sum of child accumulated scales is bounded by the strict branch descendants of the parent.

noncomputable def Anderson4D.strictDescendantRatioCost {t : PlaneTree} (Nm : t.HeppMarking) (v : t.VPos) : ℝ

The same strict-descendant ratio cost, indexed with the ancestor vertex on the outside.

Equations

• Anderson4D.strictDescendantRatioCost Nm v = ∑ u ∈ t.BranchNodes with v ∈ Anderson4D.strictBranchAncestors u, ↑(t.childCount ↑u) * (↑(Anderson4D.scaleN Nm u) / ↑(Anderson4D.scaleN Nm v))

theorem Anderson4D.erase_branchDescendants_eq_filter_strictAncestors {t : PlaneTree} {v : t.VPos} (hv : v ∈ t.BranchNodes) : (branchDescendants v).erase v = {u ∈ t.BranchNodes | v ∈ strictBranchAncestors u}

theorem Anderson4D.localRatioCost_le_strictDescendantRatioCost {t : PlaneTree} (Nm : t.HeppMarking) {v : t.VPos} (hv : v ∈ t.BranchNodes) : localRatioCost Nm v ≤ strictDescendantRatioCost Nm v

The Step-5 child ratio at one branch is bounded by the cost of all its strict branching descendants.

theorem Anderson4D.sum_strictDescendantRatioCost_eq_ancestorRatioCost {t : PlaneTree} (Nm : t.HeppMarking) : ∑ v ∈ t.BranchNodes, strictDescendantRatioCost Nm v = ancestorRatioCost Nm

Reversing the order of the strict ancestor/descendant sum gives exactly the scalar cost used by VolumeIteration.

theorem Anderson4D.sum_localRatioCost_le_ancestorRatioCost {t : PlaneTree} (Nm : t.HeppMarking) : ∑ v ∈ t.BranchNodes, localRatioCost Nm v ≤ ancestorRatioCost Nm

The total local Step-5 exponential cost is at most ancestorRatioCost.

Closing the one-anchor iteration

@[simp]

theorem Anderson4D.branchDescendants_root_eq (t : PlaneTree) : branchDescendants t.rootV = t.BranchNodes

Every branch is a branch descendant of the root.

theorem Anderson4D.localIterationWeight_root_le_hiterate {t : PlaneTree} (ht : t.isValid = true) (Nm : t.HeppMarking) : localIterationWeight Nm t.rootV ≤ (↑step5VolumeConstant ^ (t.leafCount - 1) * ∏ v ∈ t.BranchNodes, ↑(t.childCount ↑v).factorial) * branchScaleProduct Nm * Real.exp (6 * ancestorRatioCost Nm)

The actual descendant product at the root is bounded by the exact hiterate expression consumed by volume_iteration_bound.

theorem Anderson4D.J0_le_iterated_volume {t : PlaneTree} (ht : t.isValid = true) {M : ℕ} (N : t.BranchExponentData (4 * M)) (hN : N.IsValid) (f : ↥t.Leaves) (x : LatticePoint) : ↑(J0 N hN f x) ≤ ↑step5VolumeConstant ^ (t.leafCount - 1) * 256 ^ t.leafCount * Real.exp (12 * ↑t.leafCount) * ↑t.autCard * branchScaleProduct (N.toHeppMarking hN)

A fixed anchored leaf satisfies the fully iterated Step-5 bound.

theorem Anderson4D.rootClusterLeaf_injective {t : PlaneTree} : Function.Injective rootClusterLeaf

The embedding of a full-tree leaf into the root cluster is injective.

theorem Anderson4D.J01_le_iterated_volume_with_gain {t : PlaneTree} (ht : t.isValid = true) {M : ℕ} (N : t.BranchExponentData (4 * M)) (hN : N.IsValid) (f₀ f₁ : ↥t.Leaves) (hne : f₀ ≠ f₁) (x₀ x₁ : LatticePoint) : ↑(J01 N hN f₀ f₁ x₀ x₁) ≤ ↑step5VolumeConstant ^ (t.leafCount - 1) * 256 ^ t.leafCount * Real.exp (12 * ↑t.leafCount) * ↑t.autCard * branchScaleProduct (N.toHeppMarking hN) * lcaScaleGain (N.toHeppMarking hN) (lcaV ↑f₀ ↑f₁)

A fixed ordered pair of distinct anchored leaves satisfies the fully iterated Step-6 bound with its exact LCA scale gain.

noncomputable def Anderson4D.latticeBracketInvFourth (x₀ x₁ : LatticePoint) : ℝ

The lattice bracket appearing in paper (5.14), written with the same sup norm used by admissibility.

Equations

• Anderson4D.latticeBracketInvFourth x₀ x₁ = ((1 + Anderson4D.znorm (x₀ - x₁) ^ 2) ^ 2)⁻¹

theorem Anderson4D.latticeBracketInvFourth_nonneg (x₀ x₁ : LatticePoint) : 0 ≤ latticeBracketInvFourth x₀ x₁

theorem Anderson4D.lcaScaleGain_le_leafCountFactor_mul_bracket {t : PlaneTree} (ht : t.isValid = true) (Nm : t.HeppMarking) (a : t.VPos) (x₀ x₁ : LatticePoint) (hdist : znorm (x₀ - x₁) ≤ tildeScale Nm a) : lcaScaleGain Nm a ≤ (1 + 2 * ↑t.leafCount) ^ 4 * latticeBracketInvFourth x₀ x₁

Convert the LCA scale gain into the spatial bracket. The only geometric input is the Step-4 cluster-diameter estimate at the LCA.

theorem Anderson4D.J01_le_iterated_volume_bracket {t : PlaneTree} (ht : t.isValid = true) {M : ℕ} (N : t.BranchExponentData (4 * M)) (hN : N.IsValid) (f₀ f₁ : ↥t.Leaves) (hne : f₀ ≠ f₁) (x₀ x₁ : LatticePoint) : ↑(J01 N hN f₀ f₁ x₀ x₁) ≤ ↑step5VolumeConstant ^ (t.leafCount - 1) * 256 ^ t.leafCount * Real.exp (12 * ↑t.leafCount) * ↑t.autCard * branchScaleProduct (N.toHeppMarking hN) * (1 + 2 * ↑t.leafCount) ^ 4 * latticeBracketInvFourth x₀ x₁

Fixed-leaf form of (5.14), after converting the LCA gain to the spatial bracket.

theorem Anderson4D.volume_estimate_one_anchor_raw {t : PlaneTree} (ht : t.isValid = true) {M : ℕ} (N : t.BranchExponentData (4 * M)) (hN : N.IsValid) (x : LatticePoint) : ↑(Fintype.card ↥(t.AutHeppMarked (N.toHeppMarking hN)) * (realizedSetsContaining N hN x).card) ≤ ↑t.leafCount * (↑step5VolumeConstant ^ (t.leafCount - 1) * 256 ^ t.leafCount * Real.exp (12 * ↑t.leafCount) * ↑t.autCard * branchScaleProduct (N.toHeppMarking hN))

Division-free one-point volume bound before absorbing the harmless choice of anchored leaf into the universal exponential constant.

theorem Anderson4D.volume_estimate_two_anchor_raw {t : PlaneTree} (ht : t.isValid = true) {M : ℕ} (N : t.BranchExponentData (4 * M)) (hN : N.IsValid) (x₀ x₁ : LatticePoint) (hne : x₀ ≠ x₁) : ↑(Fintype.card ↥(t.AutHeppMarked (N.toHeppMarking hN)) * (realizedSetsContainingPair N hN x₀ x₁).card) ≤ ↑t.leafCount ^ 2 * (↑step5VolumeConstant ^ (t.leafCount - 1) * 256 ^ t.leafCount * Real.exp (12 * ↑t.leafCount) * ↑t.autCard * branchScaleProduct (N.toHeppMarking hN) * (1 + 2 * ↑t.leafCount) ^ 4 * latticeBracketInvFourth x₀ x₁)

Division-free two-point estimate before absorbing the ordered leaf-pair choice and the polynomial LCA-to-distance loss into a universal exponential constant.

noncomputable def Anderson4D.volumeEstimateConstant : ℝ

A single explicit universal constant for both exponential losses in the one-anchor estimate.

Equations

• Anderson4D.volumeEstimateConstant = 2 * ↑Anderson4D.step5VolumeConstant * 256 * Real.exp 12

theorem Anderson4D.leafCount_mul_iterationScalar_le (r : ℕ) (hr : 1 ≤ r) : ↑r * (↑step5VolumeConstant ^ (r - 1) * 256 ^ r * Real.exp (12 * ↑r)) ≤ volumeEstimateConstant ^ r

Elementary absorption of the anchored-leaf choice and all Step-5 scalar constants into volumeEstimateConstant ^ r.

noncomputable def Anderson4D.volumeEstimateFinalConstant : ℝ

A common universal constant large enough for both (5.13) and (5.14).

Equations

• Anderson4D.volumeEstimateFinalConstant = 5184 * ↑Anderson4D.step5VolumeConstant * 256 * Real.exp 12

theorem Anderson4D.leafCountSq_mul_pairIterationScalar_le (r : ℕ) (hr : 1 ≤ r) : ↑r ^ 2 * (↑step5VolumeConstant ^ (r - 1) * 256 ^ r * Real.exp (12 * ↑r) * (1 + 2 * ↑r) ^ 4) ≤ volumeEstimateFinalConstant ^ r

Absorb the ordered leaf-pair count and the polynomial (1 + 2r)^4 loss into a universal exponential constant.

theorem Anderson4D.volume_estimate_one_anchor {t : PlaneTree} (ht : t.isValid = true) {M : ℕ} (N : t.BranchExponentData (4 * M)) (hN : N.IsValid) (x : LatticePoint) : ↑(Fintype.card ↥(t.AutHeppMarked (N.toHeppMarking hN)) * (realizedSetsContaining N hN x).card) ≤ volumeEstimateConstant ^ t.leafCount * ↑t.autCard * branchScaleProduct (N.toHeppMarking hN)

Paper (5.13), division-free form. Multiplying by the marked-tree automorphism cardinality avoids field division while retaining exactly the paper's automorphism ratio.

theorem Anderson4D.volume_estimate_one_anchor_final {t : PlaneTree} (ht : t.isValid = true) {M : ℕ} (N : t.BranchExponentData (4 * M)) (hN : N.IsValid) (x : LatticePoint) : ↑(Fintype.card ↥(t.AutHeppMarked (N.toHeppMarking hN)) * (realizedSetsContaining N hN x).card) ≤ volumeEstimateFinalConstant ^ t.leafCount * ↑t.autCard * branchScaleProduct (N.toHeppMarking hN)

The one-anchor estimate with the common constant used by the complete Proposition 5.6 interface.

theorem Anderson4D.volume_estimate_two_anchor_of_ne {t : PlaneTree} (ht : t.isValid = true) {M : ℕ} (N : t.BranchExponentData (4 * M)) (hN : N.IsValid) (x₀ x₁ : LatticePoint) (hne : x₀ ≠ x₁) : ↑(Fintype.card ↥(t.AutHeppMarked (N.toHeppMarking hN)) * (realizedSetsContainingPair N hN x₀ x₁).card) ≤ volumeEstimateFinalConstant ^ t.leafCount * ↑t.autCard * branchScaleProduct (N.toHeppMarking hN) * latticeBracketInvFourth x₀ x₁

Paper (5.14), division-free form, for distinct prescribed points. The LCA scale gain has been converted to the spatial fourth-order bracket, and all ordered-leaf choices are absorbed into the common universal constant.

@[simp]

theorem Anderson4D.realizedSetsContainingPair_self {t : PlaneTree} {M : ℕ} (N : t.BranchExponentData (4 * M)) (hN : N.IsValid) (x : LatticePoint) : realizedSetsContainingPair N hN x x = realizedSetsContaining N hN x

Requiring the same prescribed point twice gives exactly the one-anchor realized-set carrier. This is the diagonal case singled out in paper Proposition 5.6, Step 2.

@[simp]

theorem Anderson4D.latticeBracketInvFourth_self (x : LatticePoint) : latticeBracketInvFourth x x = 1

theorem Anderson4D.volume_estimate_two_anchor {t : PlaneTree} (ht : t.isValid = true) {M : ℕ} (N : t.BranchExponentData (4 * M)) (hN : N.IsValid) (x₀ x₁ : LatticePoint) : ↑(Fintype.card ↥(t.AutHeppMarked (N.toHeppMarking hN)) * (realizedSetsContainingPair N hN x₀ x₁).card) ≤ volumeEstimateFinalConstant ^ t.leafCount * ↑t.autCard * branchScaleProduct (N.toHeppMarking hN) * latticeBracketInvFourth x₀ x₁

Paper (5.14), division-free form. This paper-facing version covers all prescribed points. On the diagonal it is exactly (5.13), since the bracket equals one; off the diagonal it is the LCA-gain estimate above.

theorem Anderson4D.volume_estimate {t : PlaneTree} (ht : t.isValid = true) {M : ℕ} (N : t.BranchExponentData (4 * M)) (hN : N.IsValid) : (∀ {m : ℕ} (mu : t.Multiplicities) (y : Fin m → LatticePoint), RealizesTuple t (N.toHeppMarking hN) mu M y → Fintype.card t.Aut ≤ treeSymDenom t M m y * Fintype.card ↥(t.AutHeppMarked (N.toHeppMarking hN))) ∧ (∀ (x : LatticePoint), ↑(Fintype.card ↥(t.AutHeppMarked (N.toHeppMarking hN)) * (realizedSetsContaining N hN x).card) ≤ volumeEstimateFinalConstant ^ t.leafCount * ↑t.autCard * branchScaleProduct (N.toHeppMarking hN)) ∧ ∀ (x₀ x₁ : LatticePoint), ↑(Fintype.card ↥(t.AutHeppMarked (N.toHeppMarking hN)) * (realizedSetsContainingPair N hN x₀ x₁).card) ≤ volumeEstimateFinalConstant ^ t.leafCount * ↑t.autCard * branchScaleProduct (N.toHeppMarking hN) * latticeBracketInvFourth x₀ x₁

Proposition 5.6 (P-5.6), complete frozen interface.

The three conjuncts are respectively the division-free forms of (5.12), (5.13), and (5.14), all using the order-forgetting tree automorphism group.