Master decomposition of the lattice chain sum over marked Hepp trees (node R-decomp)

Paper (5.6)–(5.11) of arXiv:2607.10105, packaging the counting sum (5.5) into tree-indexed pieces, in the paperSum normalization.

• rdec_boundedTuples, latticeChainSum — the (5.5)-type sum over n-tuples of lattice points in the box [-M, M]⁴.
• RealizesTuple, realizedTuples — the realization class of a marked Hepp tree (t, Nm, mu) (Def 5.4, multiplicity form): tuples y = z ∘ w for an admissible embedding z and an assignment word w with letter multiplicities mu.m (validWords).
• card_realizedTuples_le — trivial volume bound (sharp (5.6)–(5.7) form is node P-5.6).
• rdec_exists_realizing_marked_tree — the general multi-scale Lemma 5.5 (single-linkage dyadic merging), proved by recursion on cluster partitions.
• exists_realizing_tree — every bounded tuple with all values repeated (m_ℓ ≥ 2 of Def 5.1 forces repetition) lies in some realization class with at most n leaves.
• rdec_treeEnum, latticeChainSum_le_treeSum — the (5.10)-shaped weak bridge: the repeated-tuple part of the chain sum is dominated by the sum over valid trees with at most n leaves of their realized-tuple sums.

The bounded-tuple sum (5.5)

noncomputable def Anderson4D.rdec_boundedTuples (M n : ℕ) : Finset (Fin n → Fin 4 → ℤ)

Tuples of n lattice points with every coordinate in [-M, M].

Equations

• Anderson4D.rdec_boundedTuples M n = Fintype.piFinset fun (x : Fin n) => Fintype.piFinset fun (x : Fin 4) => Finset.Icc (-↑M) ↑M

@[simp]

theorem Anderson4D.rdec_mem_boundedTuples {M n : ℕ} {y : Fin n → Fin 4 → ℤ} : y ∈ rdec_boundedTuples M n ↔ ∀ (j : Fin n) (i : Fin 4), |y j i| ≤ ↑M

noncomputable def Anderson4D.latticeChainSum (M n : ℕ) (F : (Fin n → Fin 4 → ℤ) → ℝ) : ℝ

The lattice chain sum (5.5): a statistic F summed over all bounded tuples.

Equations

• Anderson4D.latticeChainSum M n F = ∑ y ∈ Anderson4D.rdec_boundedTuples M n, F y

theorem Anderson4D.rdec_card_boundedTuples (M n : ℕ) : (rdec_boundedTuples M n).card = (2 * M + 1) ^ (4 * n)

The box volume count: there are (2M+1)^{4n} bounded tuples.

noncomputable def Anderson4D.rdec_repeatedTuples (M n : ℕ) : Finset (Fin n → Fin 4 → ℤ)

Bounded tuples in which every value occurs at least twice. Def 5.1's leaf multiplicities m_ℓ ≥ 2 mean realization classes only contain such tuples (in the paper these are the tuples surviving the expectation of the mean-zero chain).

Equations

• Anderson4D.rdec_repeatedTuples M n = {y ∈ Anderson4D.rdec_boundedTuples M n | ∀ (j : Fin n), 2 ≤ {k : Fin n | y k = y j}.card}

@[simp]

theorem Anderson4D.rdec_mem_repeatedTuples {M n : ℕ} {y : Fin n → Fin 4 → ℤ} : y ∈ rdec_repeatedTuples M n ↔ y ∈ rdec_boundedTuples M n ∧ ∀ (j : Fin n), 2 ≤ {k : Fin n | y k = y j}.card

Realization classes (Def 5.4, multiplicity form)

def Anderson4D.RealizesTuple (t : PlaneTree) (Nm : t.HeppMarking) (mu : t.Multiplicities) (M : ℕ) {n : ℕ} (y : Fin n → Fin 4 → ℤ) : Prop

The tuple y is realized by the marked tree (t, Nm, mu): some admissible embedding z of the leaves and some assignment word w : Fin n → Leaves t whose letter multiplicities are mu.m (membership in validWords, the word structure of §5.5) write y as y j = z (w j). Since every leaf multiplicity is ≥ 2 ≥ 1, every leaf is hit by w, so the value multiset of y is exactly ⋃_ℓ {mu.m ℓ copies of z ℓ} (Def 5.4, multiplicity version).

Equations

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

noncomputable def Anderson4D.realizedTuples (t : PlaneTree) (Nm : t.HeppMarking) (mu : t.Multiplicities) (M n : ℕ) : Finset (Fin n → Fin 4 → ℤ)

The realization class of (t, Nm, mu) inside the bounded tuples.

Equations

• Anderson4D.realizedTuples t Nm mu M n = {y ∈ Anderson4D.rdec_boundedTuples M n | Anderson4D.RealizesTuple t Nm mu M y}

theorem Anderson4D.mem_realizedTuples {t : PlaneTree} {Nm : t.HeppMarking} {mu : t.Multiplicities} {M n : ℕ} {y : Fin n → Fin 4 → ℤ} : y ∈ realizedTuples t Nm mu M n ↔ y ∈ rdec_boundedTuples M n ∧ RealizesTuple t Nm mu M y

theorem Anderson4D.card_realizedTuples_le (t : PlaneTree) (Nm : t.HeppMarking) (mu : t.Multiplicities) (M n : ℕ) : (realizedTuples t Nm mu M n).card ≤ (2 * M + 1) ^ (4 * n)

Trivial volume-facing bound: a realization class has at most (2M+1)^{4n} tuples. The sharp (5.6)–(5.7) denominator form is deferred to node P-5.6.

Metric helpers

theorem Anderson4D.rdec_one_le_znorm {x y : Fin 4 → ℤ} (h : x ≠ y) : 1 ≤ znorm (x - y)

Distinct integer vectors are at sup-distance at least 1.

theorem Anderson4D.rdec_znorm_le_pow {M : ℕ} {x y : Fin 4 → ℤ} (hx : ∀ (i : Fin 4), |x i| ≤ ↑M) (hy : ∀ (i : Fin 4), |y i| ≤ ↑M) : znorm (x - y) ≤ 2 ^ (M + 1)

Points of the box [-M, M]⁴ are at sup-distance at most 2^{M+1}.

Realizability with bounded branch exponents (the Lemma 5.5 invariant)

def Anderson4D.rdec_RealizableBelow (M : ℕ) (C : Finset (Fin 4 → ℤ)) (N : ℕ) : Prop

C is realized by some valid marked Hepp tree with C.card leaves whose branch exponents are all < N (the recursion invariant of Lemma 5.5).

Equations

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

theorem Anderson4D.rdec_RealizableBelow.mono {M : ℕ} {C : Finset (Fin 4 → ℤ)} {N N' : ℕ} (h : rdec_RealizableBelow M C N) (hN : N ≤ N') : rdec_RealizableBelow M C N'

theorem Anderson4D.rdec_realizableBelow_singleton (M N : ℕ) (x : Fin 4 → ℤ) (hx : ∀ (i : Fin 4), |x i| ≤ ↑M) : rdec_RealizableBelow M {x} N

Singletons are realizable below every exponent bound, by the bare leaf.

Vertex transport into a node (assembly plumbing)

theorem Anderson4D.rdec_childCount_cons {cs : List PlaneTree} {i : ℕ} {p : PlaneTree.Pos} (h : i < cs.length) : (PlaneTree.node cs).childCount (i :: p) = cs[i].childCount p

theorem Anderson4D.rdec_childCount_childV {cs : List PlaneTree} (i : Fin cs.length) (v : (cs.get i).VPos) : (PlaneTree.node cs).childCount ↑(PlaneTree.childV i v) = (cs.get i).childCount ↑v

theorem Anderson4D.rdec_root_mem_branchNodes {cs : List PlaneTree} (h : 2 ≤ cs.length) : (PlaneTree.node cs).rootV ∈ (PlaneTree.node cs).BranchNodes

theorem Anderson4D.rdec_childV_mem_leaves {cs : List PlaneTree} (i : Fin cs.length) (v : (cs.get i).VPos) : PlaneTree.childV i v ∈ (PlaneTree.node cs).Leaves ↔ v ∈ (cs.get i).Leaves

theorem Anderson4D.rdec_childV_mem_branchNodes {cs : List PlaneTree} (i : Fin cs.length) (v : (cs.get i).VPos) : PlaneTree.childV i v ∈ (PlaneTree.node cs).BranchNodes ↔ v ∈ (cs.get i).BranchNodes

theorem Anderson4D.rdec_lcaPath_cons_eq (a : ℕ) (p q : List ℕ) : lcaPath (a :: p) (a :: q) = a :: lcaPath p q

theorem Anderson4D.rdec_lcaPath_cons_ne {a b : ℕ} (h : a ≠ b) (p q : List ℕ) : lcaPath (a :: p) (b :: q) = []

theorem Anderson4D.rdec_lcaV_childV {cs : List PlaneTree} (i : Fin cs.length) (v w : (cs.get i).VPos) : lcaV (PlaneTree.childV i v) (PlaneTree.childV i w) = PlaneTree.childV i (lcaV v w)

theorem Anderson4D.rdec_lcaV_childV_ne {cs : List PlaneTree} {i j : Fin cs.length} (hij : i ≠ j) (v : (cs.get i).VPos) (w : (cs.get j).VPos) : lcaV (PlaneTree.childV i v) (PlaneTree.childV j w) = (PlaneTree.node cs).rootV

theorem Anderson4D.rdec_mem_childrenOf_root {cs : List PlaneTree} {w : (PlaneTree.node cs).VPos} : w ∈ childrenOf (PlaneTree.node cs).rootV ↔ ∃ (i : Fin cs.length), w = PlaneTree.childV i (cs.get i).rootV

theorem Anderson4D.rdec_mem_childrenOf_childV {cs : List PlaneTree} {i : Fin cs.length} {u : (cs.get i).VPos} {c : (PlaneTree.node cs).VPos} : c ∈ childrenOf (PlaneTree.childV i u) ↔ ∃ w ∈ childrenOf u, c = PlaneTree.childV i w

Assembling a marking on node cs

def Anderson4D.rdec_nodeNexp {cs : List PlaneTree} (Nms : (i : Fin cs.length) → (cs.get i).HeppMarking) (N : ℕ) : (PlaneTree.node cs).VPos → ℕ

The exponent function on node cs: N at the root, the child's own exponents inside child i.

Equations

• Anderson4D.rdec_nodeNexp Nms N ⟨[], property⟩ = N
• Anderson4D.rdec_nodeNexp Nms N ⟨i :: p, hp⟩ = (Nms ⟨i, ⋯⟩).Nexp ⟨p, ⋯⟩

@[simp]

theorem Anderson4D.rdec_nodeNexp_root {cs : List PlaneTree} (Nms : (i : Fin cs.length) → (cs.get i).HeppMarking) (N : ℕ) : rdec_nodeNexp Nms N (PlaneTree.node cs).rootV = N

@[simp]

theorem Anderson4D.rdec_nodeNexp_childV {cs : List PlaneTree} (Nms : (i : Fin cs.length) → (cs.get i).HeppMarking) (N : ℕ) (i : Fin cs.length) (v : (cs.get i).VPos) : rdec_nodeNexp Nms N (PlaneTree.childV i v) = (Nms i).Nexp v

def Anderson4D.rdec_nodeMarking {cs : List PlaneTree} {N : ℕ} (hN : 1 ≤ N) (Nms : (i : Fin cs.length) → (cs.get i).HeppMarking) (hbelow : ∀ (i : Fin cs.length), ∀ v ∈ (cs.get i).BranchNodes, (Nms i).Nexp v < N) : (PlaneTree.node cs).HeppMarking

The assembled Hepp marking on node cs: root exponent N, child markings inside the children. Requires every child branch exponent < N.

Equations

• Anderson4D.rdec_nodeMarking hN Nms hbelow = { Nexp := Anderson4D.rdec_nodeNexp Nms N, pos := ⋯, parent_gt := ⋯ }

Assembling the leaf embedding on node cs

def Anderson4D.rdec_leafUp {cs : List PlaneTree} (i : Fin cs.length) (w : ↥(cs.get i).Leaves) : ↥(PlaneTree.node cs).Leaves

A leaf of child i, embedded as a leaf of the node.

Equations

• Anderson4D.rdec_leafUp i w = ⟨Anderson4D.PlaneTree.childV i ↑w, ⋯⟩

theorem Anderson4D.rdec_leafUp_surj {cs : List PlaneTree} (hlen : 1 ≤ cs.length) (l : ↥(PlaneTree.node cs).Leaves) : ∃ (i : Fin cs.length) (w : ↥(cs.get i).Leaves), l = rdec_leafUp i w

Every leaf of a nonempty node comes from a child.

def Anderson4D.rdec_nodeEmb {cs : List PlaneTree} (zs : (i : Fin cs.length) → ↥(cs.get i).Leaves → Fin 4 → ℤ) : ↥(PlaneTree.node cs).Leaves → Fin 4 → ℤ

The assembled leaf embedding: on the leaves of child i use zs i (junk value 0 at the impossible root-leaf case).

Equations

• Anderson4D.rdec_nodeEmb zs ⟨⟨[], property⟩, property_1⟩ = 0
• Anderson4D.rdec_nodeEmb zs ⟨⟨i :: p, hp⟩, hl⟩ = zs ⟨i, ⋯⟩ ⟨⟨p, ⋯⟩, ⋯⟩

@[simp]

theorem Anderson4D.rdec_nodeEmb_leafUp {cs : List PlaneTree} (zs : (i : Fin cs.length) → ↥(cs.get i).Leaves → Fin 4 → ℤ) (i : Fin cs.length) (w : ↥(cs.get i).Leaves) : rdec_nodeEmb zs (rdec_leafUp i w) = zs i w

theorem Anderson4D.rdec_leafUp_mem_leavesUnder {cs : List PlaneTree} {i : Fin cs.length} {a : (cs.get i).VPos} {w : ↥(cs.get i).Leaves} (hw : w ∈ leavesUnder a) : rdec_leafUp i w ∈ leavesUnder (PlaneTree.childV i a)

Transport of leavesUnder along rdec_leafUp.

theorem Anderson4D.rdec_scaleN_node_root {cs : List PlaneTree} {N : ℕ} (hN : 1 ≤ N) (Nms : (i : Fin cs.length) → (cs.get i).HeppMarking) (hbelow : ∀ (i : Fin cs.length), ∀ v ∈ (cs.get i).BranchNodes, (Nms i).Nexp v < N) : scaleN (rdec_nodeMarking hN Nms hbelow) (PlaneTree.node cs).rootV = 2 ^ N

theorem Anderson4D.rdec_scaleN_node_childV {cs : List PlaneTree} {N : ℕ} (hN : 1 ≤ N) (Nms : (i : Fin cs.length) → (cs.get i).HeppMarking) (hbelow : ∀ (i : Fin cs.length), ∀ v ∈ (cs.get i).BranchNodes, (Nms i).Nexp v < N) (i : Fin cs.length) (v : (cs.get i).VPos) : scaleN (rdec_nodeMarking hN Nms hbelow) (PlaneTree.childV i v) = scaleN (Nms i) v

theorem Anderson4D.rdec_assemble {M N : ℕ} (hN : 1 ≤ N) (cs : List PlaneTree) (hlen : 2 ≤ cs.length) (Cs : Fin cs.length → Finset (Fin 4 → ℤ)) (hCne : ∀ (i : Fin cs.length), (Cs i).Nonempty) (hdata : ∀ (i : Fin cs.length), (cs.get i).isValid = true ∧ ∃ (Nm : (cs.get i).HeppMarking), Realizes Nm M (Cs i) ∧ (cs.get i).leafCount = (Cs i).card ∧ ∀ v ∈ (cs.get i).BranchNodes, Nm.Nexp v < N) (hdisj : ∀ (i j : Fin cs.length), i ≠ j → Disjoint (Cs i) (Cs j)) (hsep : ∀ (i j : Fin cs.length), i ≠ j → ∀ x ∈ Cs i, ∀ y ∈ Cs j, 2 ^ N / 2 ≤ znorm (x - y)) (hconn : ∀ (i j : Fin cs.length), Relation.ReflTransGen (fun (a b : Fin cs.length) => ∃ x ∈ Cs a, ∃ y ∈ Cs b, znorm (x - y) ≤ 2 ^ N) i j) : rdec_RealizableBelow M (Finset.univ.biUnion Cs) (N + 1)

Assembly step of Lemma 5.5. Nonempty clusters Cs i, realized by valid marked trees with branch exponents < N, pairwise disjoint and 2^N/2-separated, and chain-linked at scale 2^N, are jointly realized by the node of their trees with root exponent N — hence realizable below N + 1.

Single-linkage components of a cluster family

def Anderson4D.rdec_Step (P : Finset (Finset (Fin 4 → ℤ))) (N : ℕ) (C D : Finset (Fin 4 → ℤ)) : Prop

One link between clusters of the family P at scale 2^N.

Equations

• Anderson4D.rdec_Step P N C D = (C ∈ P ∧ D ∈ P ∧ ∃ x ∈ C, ∃ y ∈ D, Anderson4D.znorm (x - y) ≤ 2 ^ N)

def Anderson4D.rdec_Reach (P : Finset (Finset (Fin 4 → ℤ))) (N : ℕ) (C D : Finset (Fin 4 → ℤ)) : Prop

Chain-reachability between clusters of P at scale 2^N.

Equations

• Anderson4D.rdec_Reach P N C D = Relation.ReflTransGen (Anderson4D.rdec_Step P N) C D

theorem Anderson4D.rdec_Step.symm {P : Finset (Finset (Fin 4 → ℤ))} {N : ℕ} {C D : Finset (Fin 4 → ℤ)} (h : rdec_Step P N C D) : rdec_Step P N D C

theorem Anderson4D.rdec_Reach.trans {P : Finset (Finset (Fin 4 → ℤ))} {N : ℕ} {C D E : Finset (Fin 4 → ℤ)} (h1 : rdec_Reach P N C D) (h2 : rdec_Reach P N D E) : rdec_Reach P N C E

theorem Anderson4D.rdec_Reach.symm {P : Finset (Finset (Fin 4 → ℤ))} {N : ℕ} {C D : Finset (Fin 4 → ℤ)} (h : rdec_Reach P N C D) : rdec_Reach P N D C

noncomputable def Anderson4D.rdec_comp (P : Finset (Finset (Fin 4 → ℤ))) (N : ℕ) (C : Finset (Fin 4 → ℤ)) : Finset (Finset (Fin 4 → ℤ))

The single-linkage component of C in the family P at scale 2^N.

Equations

• Anderson4D.rdec_comp P N C = {D ∈ P | Anderson4D.rdec_Reach P N C D}

theorem Anderson4D.rdec_mem_comp {P : Finset (Finset (Fin 4 → ℤ))} {N : ℕ} {C D : Finset (Fin 4 → ℤ)} : D ∈ rdec_comp P N C ↔ D ∈ P ∧ rdec_Reach P N C D

theorem Anderson4D.rdec_self_mem_comp {P : Finset (Finset (Fin 4 → ℤ))} {N : ℕ} {C : Finset (Fin 4 → ℤ)} (hC : C ∈ P) : C ∈ rdec_comp P N C

theorem Anderson4D.rdec_comp_subset {P : Finset (Finset (Fin 4 → ℤ))} {N : ℕ} {C : Finset (Fin 4 → ℤ)} : rdec_comp P N C ⊆ P

theorem Anderson4D.rdec_comp_eq_of_mem {P : Finset (Finset (Fin 4 → ℤ))} {N : ℕ} {C D : Finset (Fin 4 → ℤ)} (hD : D ∈ rdec_comp P N C) : rdec_comp P N D = rdec_comp P N C

theorem Anderson4D.rdec_reach_of_mem_comp {P : Finset (Finset (Fin 4 → ℤ))} {N : ℕ} {C D E : Finset (Fin 4 → ℤ)} (hD : D ∈ rdec_comp P N C) (hE : E ∈ rdec_comp P N C) : rdec_Reach P N D E

Any two members of one component are chain-connected.

theorem Anderson4D.rdec_no_step_of_comp_ne {P : Finset (Finset (Fin 4 → ℤ))} {N : ℕ} {C C' D D' : Finset (Fin 4 → ℤ)} (hD : D ∈ rdec_comp P N C) (hD' : D' ∈ rdec_comp P N C') (hne : rdec_comp P N C ≠ rdec_comp P N C') (hstep : rdec_Step P N D D') : False

Members of distinct components are never directly linked.

theorem Anderson4D.rdec_assemble' {M N : ℕ} (hN : 1 ≤ N) {m : ℕ} (hm : 2 ≤ m) (Cs : Fin m → Finset (Fin 4 → ℤ)) (hCne : ∀ (i : Fin m), (Cs i).Nonempty) (hdata : ∀ (i : Fin m), ∃ (t : PlaneTree), t.isValid = true ∧ ∃ (Nm : t.HeppMarking), Realizes Nm M (Cs i) ∧ t.leafCount = (Cs i).card ∧ ∀ v ∈ t.BranchNodes, Nm.Nexp v < N) (hdisj : ∀ (i j : Fin m), i ≠ j → Disjoint (Cs i) (Cs j)) (hsep : ∀ (i j : Fin m), i ≠ j → ∀ x ∈ Cs i, ∀ y ∈ Cs j, 2 ^ N / 2 ≤ znorm (x - y)) (hconn : ∀ (i j : Fin m), Relation.ReflTransGen (fun (a b : Fin m) => ∃ x ∈ Cs a, ∃ y ∈ Cs b, znorm (x - y) ≤ 2 ^ N) i j) : rdec_RealizableBelow M (Finset.univ.biUnion Cs) (N + 1)

Function-indexed form of the assembly step (hides the List.ofFn plumbing): m ≥ 2 clusters, each realizable below N, pairwise disjoint and 2^N/2-separated, chain-linked at scale 2^N, are jointly realizable below N + 1.

The component family: hypotheses propagate from scale N to N + 1

theorem Anderson4D.rdec_exists_realizing_marked_tree (M : ℕ) (Z : Finset (Fin 4 → ℤ)) (hZ : Z.Nonempty) (hbound : ∀ x ∈ Z, ∀ (i : Fin 4), |x i| ≤ ↑M) : ∃ (t : PlaneTree), t.isValid = true ∧ ∃ (Nm : t.HeppMarking), Realizes Nm M Z ∧ t.leafCount = Z.card

General multi-scale Lemma 5.5 (blueprint node L-5.5, set form): every nonempty finite Z ⊆ [-M, M]⁴ is realized by a valid marked Hepp tree with exactly Z.card leaves. Proof: single-linkage dyadic merging — start from singletons at scale 2, at each scale form chain components of clusters and merge every multi-cluster component under a new root (rdec_assemble), then increase the scale; the box diameter bound 2^{M+1} forces termination.

theorem Anderson4D.exists_realizing_tree (M n : ℕ) (hn : 1 ≤ n) (y : Fin n → Fin 4 → ℤ) (hy : y ∈ rdec_boundedTuples M n) (hrep : ∀ (j : Fin n), 2 ≤ {k : Fin n | y k = y j}.card) : ∃ (t : PlaneTree) (_ : t.isValid = true) (Nm : t.HeppMarking) (mu : t.Multiplicities), y ∈ realizedTuples t Nm mu M n ∧ t.leafCount ≤ n

Structural realization for R-decomp (paper Lemma 5.5, multiplicity form, plus the "fix T" step of (5.6)): every bounded tuple all of whose values occur at least twice belongs to the realization class of some valid marked tree with at most n leaves. The repetition hypothesis hrep is forced by Def 5.1's m_ℓ ≥ 2: a tuple with a once-occurring value lies in no realization class (in the paper such tuples are killed by the expectation of the mean-zero chain before (5.6)).

Finiteness of valid trees with bounded leaf count

(real-carrier port of Combinatorics/TreeCount, paper Lemma 5.2)

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

theorem Anderson4D.rdec_size_add_one_le_of_isValid (t : PlaneTree) : t.isValid = true → t.size + 1 ≤ 2 * t.leafCount

Paper Lemma 5.2, size part, for the real carrier.

theorem Anderson4D.rdec_finite_validTrees (r : ℕ) : {t : PlaneTree | t.isValid = true ∧ t.leafCount ≤ r}.Finite

Paper Lemma 5.2 finiteness, real carrier: valid trees with at most r leaves form a finite set (explicit injection of keys into Fin (4r+1) × (Fin (4r) → Bool), using the stack-decoder key_injective).

@[reducible, inline]

noncomputable abbrev Anderson4D.rdec_treeEnum (n : ℕ) : Finset PlaneTree

The enumeration of valid Hepp trees with at most n leaves, using the quantitative real-carrier implementation of paper Lemma 5.2.

Equations

• Anderson4D.rdec_treeEnum n = Anderson4D.PlaneTree.validTreesAtMost n

@[simp]

theorem Anderson4D.rdec_mem_treeEnum {n : ℕ} {t : PlaneTree} : t ∈ rdec_treeEnum n ↔ t.isValid = true ∧ t.leafCount ≤ n

theorem Anderson4D.rdec_card_treeEnum_le (n : ℕ) : (rdec_treeEnum n).card ≤ 4 ^ (4 * n)

The concrete tree family used by R-decomp has exponentially bounded cardinality, with explicit constant 4^4.

The (5.10)-shaped bridge: chain sum ≤ tree-indexed sum

noncomputable def Anderson4D.rdec_treeRealized (t : PlaneTree) (M n : ℕ) : Finset (Fin n → Fin 4 → ℤ)

Bounded tuples realized by t for some marking and multiplicities: the t-slice of the master decomposition.

Equations

• Anderson4D.rdec_treeRealized t M n = {y ∈ Anderson4D.rdec_boundedTuples M n | ∃ (Nm : t.HeppMarking) (mu : t.Multiplicities), Anderson4D.RealizesTuple t Nm mu M y}

theorem Anderson4D.rdec_mem_treeRealized {t : PlaneTree} {M n : ℕ} {y : Fin n → Fin 4 → ℤ} : y ∈ rdec_treeRealized t M n ↔ y ∈ rdec_boundedTuples M n ∧ ∃ (Nm : t.HeppMarking) (mu : t.Multiplicities), RealizesTuple t Nm mu M y

theorem Anderson4D.rdec_repeatedTuples_subset_treeUnion (M n : ℕ) (hn : 1 ≤ n) : rdec_repeatedTuples M n ⊆ (rdec_treeEnum n).biUnion fun (t : PlaneTree) => rdec_treeRealized t M n

Every bounded repeated tuple occurs in at least one valid-tree slice. This is the finite-cover form of Lemma 5.5 used by the master resummation.

theorem Anderson4D.latticeChainSum_le_treeSum (M n : ℕ) (hn : 1 ≤ n) (F : (Fin n → Fin 4 → ℤ) → ℝ) (hF : ∀ (y : Fin n → Fin 4 → ℤ), 0 ≤ F y) (hzero : ∀ y ∈ rdec_boundedTuples M n, y ∉ rdec_repeatedTuples M n → F y = 0) : latticeChainSum M n F ≤ ∑ t ∈ rdec_treeEnum n, ∑ y ∈ rdec_treeRealized t M n, F y

Weak master bridge for (5.6). If the statistic vanishes on tuples with a once-occurring value (as the mean-zero pairing expansion does), its full bounded lattice sum is dominated by the sum of its valid-tree slices. Slices may overlap, hence the inequality and the nonnegativity hypothesis.

Exact finite-incidence denominator (paper (5.6))

def Anderson4D.realizationFiber {δ : Type u_1} {β : Type u_2} (D : Finset δ) (R : δ → β → Prop) [DecidableRel R] (y : β) : Finset δ

The realization data in D incident to y. In the paper δ is the restricted pair (N_n, m_l); embedding witnesses are deliberately absent.

Equations

• Anderson4D.realizationFiber D R y = {d ∈ D | R d y}

def Anderson4D.symDenom {δ : Type u_1} {β : Type u_2} (D : Finset δ) (R : δ → β → Prop) [DecidableRel R] (y : β) : ℕ

The symmetry denominator in (5.6): the number of realization-data pairs incident to y.

Equations

• Anderson4D.symDenom D R y = (Anderson4D.realizationFiber D R y).card

theorem Anderson4D.symDenom_pos_iff {δ : Type u_1} {β : Type u_2} (D : Finset δ) (R : δ → β → Prop) [DecidableRel R] (y : β) : 0 < symDenom D R y ↔ ∃ d ∈ D, R d y

theorem Anderson4D.symDenom_eq_of_iff {δ : Type u_1} {β : Type u_2} (D : Finset δ) (R : δ → β → Prop) [DecidableRel R] {y y' : β} (h : ∀ d ∈ D, R d y ↔ R d y') : symDenom D R y = symDenom D R y'

The symmetry denominator depends only on the incidence predicate. This is the generic permutation-invariance step used in (5.6)–(5.8).

theorem Anderson4D.sum_eq_sum_incidence_div {δ : Type u_1} {β : Type u_2} (D : Finset δ) (Y : Finset β) (R : δ → β → Prop) [DecidableRel R] (F : β → ℝ) (hcover : ∀ y ∈ Y, ∃ d ∈ D, R d y) : ∑ y ∈ Y, F y = ∑ d ∈ D, ∑ y ∈ Y with (R d) y, F y / ↑(symDenom D R y)

Finite-incidence resummation, paper (5.6). Dividing every incidence by its fiber cardinality counts each covered y exactly once.