Volume iteration for Proposition 5.6

This file isolates the scalar bookkeeping in paper §5.3, Steps 5--6. step5_parent_volume_bound combines the lattice-ball estimate (5.23) with the parent-function replacement for the weighted Cayley calculation in (5.24)--(5.25). volume_iteration_bound then combines its iterated form with the geometric ancestor sum (5.27) and the ordering estimate (5.21), and produces the explicit version of (5.28).

The geometric construction which injects admissible embeddings into the parent-function sum is deliberately outside this file. Its output is the single hiterate hypothesis of volume_iteration_bound; this keeps the analytic bookkeeping independent of the concrete cluster-cover carrier.

Finite products with one distinguished root

The one-branch parent-function estimate, (5.23)--(5.25)

def Anderson4D.step5VolumeConstant : ℕ

Explicit absolute constant in the parent-function implementation of paper (5.25). The factor 3888 is the four-dimensional lattice-ball constant from (5.23), and 16 absorbs q^(q-1) into q! for q ≥ 2.

Equations

• Anderson4D.step5VolumeConstant = 16 * Anderson4D.step5LatticeConstant

theorem Anderson4D.step5_parent_volume_bound {α : Type u_1} [Fintype α] [DecidableEq α] (root : α) (w : α → ℝ) (hw : ∀ (i : α), 0 ≤ w i) (hq : 2 ≤ Fintype.card α) (Nroot : ℝ) : ∑ p : α → α, fullParentWeight root (fun (i : α) => 1 + w i) (fun (i : α) => ↑step5LatticeConstant * Nroot ^ 4 * (1 + w i) ^ 4) p ≤ ↑(Fintype.card α).factorial * ↑step5VolumeConstant ^ (Fintype.card α - 1) * Nroot ^ (4 * (Fintype.card α - 1)) * Real.exp (6 * ∑ i : α, w i)

Paper (5.23)--(5.25), parent-function form.

At a branch with q ≥ 2 children, w i = tildeN_i / N_root. For every non-root child, step5LatticeConstant * N_root^4 is the four-dimensional ball count from (5.23), (1 + w (p i)) is the chosen parent-cluster factor, and (1 + w i)^4 is the child-radius factor. Summing over the enlarged space of all rooted parent functions gives the right side of (5.25), with a fully explicit absolute constant.

Iteration over the Hepp tree, (5.27)--(5.29)

noncomputable def Anderson4D.branchScaleProduct {t : PlaneTree} (Nm : t.HeppMarking) : ℝ

Scale monomial occurring in (5.26)--(5.29).

Equations

• Anderson4D.branchScaleProduct Nm = ∏ v ∈ t.BranchNodes, ↑(Anderson4D.scaleN Nm v) ^ (4 * (t.childCount ↑v - 1))

noncomputable def Anderson4D.ancestorRatioCost {t : PlaneTree} (Nm : t.HeppMarking) : ℝ

Reordered exponent cost from (5.27). Expanding every tildeN and swapping the two finite sums turns the paper's double sum into this form.

Equations

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

theorem Anderson4D.ancestorRatioCost_nonneg {t : PlaneTree} (Nm : t.HeppMarking) : 0 ≤ ancestorRatioCost Nm

theorem Anderson4D.ancestorRatioCost_le_two_mul_leafCount {t : PlaneTree} (ht : t.isValid = true) (Nm : t.HeppMarking) : ancestorRatioCost Nm ≤ 2 * ↑t.leafCount

Paper (5.27), exposed under the name consumed by the iteration.

theorem Anderson4D.branchScaleProduct_nonneg {t : PlaneTree} (Nm : t.HeppMarking) : 0 ≤ branchScaleProduct Nm

theorem Anderson4D.volume_iteration_bound {t : PlaneTree} (ht : t.isValid = true) (Nm : t.HeppMarking) (J : ℝ) (hiterate : J ≤ (↑step5VolumeConstant ^ (t.leafCount - 1) * ∏ v ∈ t.BranchNodes, ↑(t.childCount ↑v).factorial) * branchScaleProduct Nm * Real.exp (6 * ancestorRatioCost Nm)) : J ≤ ↑step5VolumeConstant ^ (t.leafCount - 1) * 256 ^ t.leafCount * Real.exp (12 * ↑t.leafCount) * ↑t.autCard * branchScaleProduct Nm

Paper (5.23), (5.25), (5.27), and (5.28), combined.

hiterate is exactly (5.26), obtained by recursively applying step5_parent_volume_bound; its constant is therefore the explicit step5VolumeConstant. The conclusion discharges both remaining global costs: (5.27) contributes exp (12 r), and (5.21) contributes 256^r times the order-forgetting automorphism cardinality.

theorem Anderson4D.volume_iteration_bound_with_gain {t : PlaneTree} (ht : t.isValid = true) (Nm : t.HeppMarking) (J gain : ℝ) (hgain : 0 ≤ gain) (hiterate : J ≤ (↑step5VolumeConstant ^ (t.leafCount - 1) * ∏ v ∈ t.BranchNodes, ↑(t.childCount ↑v).factorial) * branchScaleProduct Nm * Real.exp (6 * ancestorRatioCost Nm) * gain) : J ≤ ↑step5VolumeConstant ^ (t.leafCount - 1) * 256 ^ t.leafCount * Real.exp (12 * ↑t.leafCount) * ↑t.autCard * branchScaleProduct Nm * gain

Gain-preserving version of volume_iteration_bound. Taking gain = N_(f₀ ∨ f₁)⁻⁴ is precisely the Step 6 estimate (5.29): at the lowest common ancestor one lattice-placement factor is replaced by 1, and all later scalar bookkeeping leaves that gain untouched.

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

The concrete nonnegative gain used in paper (5.29).

Equations

• Anderson4D.lcaScaleGain Nm v = (↑(Anderson4D.scaleN Nm v) ^ 4)⁻¹

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

theorem Anderson4D.volume_iteration_pair_bound {t : PlaneTree} (ht : t.isValid = true) (Nm : t.HeppMarking) (v : t.VPos) (J01 : ℝ) (hiterate : J01 ≤ (↑step5VolumeConstant ^ (t.leafCount - 1) * ∏ u ∈ t.BranchNodes, ↑(t.childCount ↑u).factorial) * branchScaleProduct Nm * Real.exp (6 * ancestorRatioCost Nm) * lcaScaleGain Nm v) : J01 ≤ ↑step5VolumeConstant ^ (t.leafCount - 1) * 256 ^ t.leafCount * Real.exp (12 * ↑t.leafCount) * ↑t.autCard * branchScaleProduct Nm * lcaScaleGain Nm v

Paper (5.29) with the lowest-common-ancestor vertex supplied explicitly. The geometric caller instantiates v with f₀ ∨ f₁.