Paper-facing permutation-sum statements

This file freezes the statements of Propositions 5.7, 5.9, and 5.10 of Deng--Shen, The four-dimensional Anderson model: a case study for critical SPDEs (arXiv:2607.10105v1). It contains no proof of those estimates.

The left sides use the factorial-ledger normalization paperSum. Thus they are sums over permutations of distinct copies, although their internal carrier is the pure word model of PermSum.Words.

Totalization conventions

• Adjacent positions are represented by AdjacentIndex m; this type is empty when m = 0, so no out-of-range successor is ever read.
• The subtractions in (n - |W|)!, (m - 2|W|)!, and (m - s)! are natural subtraction. In every estimate below the stated tree, multiplicity, and skipped-set hypotheses imply that no truncation occurs. Those inequalities are proof obligations, rather than extra assumptions weakening the paper's propositions.
• Parent scales are read only on non-root branch nodes. Root scales are read only under the explicit hypothesis that the root is a branch node. Hence the junk values of HeppMarking.Nexp away from BranchNodes are never used.
• The compound-leaf set is required to be a subset of Leaves; the junk values of Multiplicities.m away from Leaves are never used.
• Real powers (3/4 and m/2) use mathlib's totalized Real.rpow. Their bases are positive on the stated domains.

Common paper data and weights

@[reducible, inline]

abbrev Anderson4D.HeppLeaf (t : PlaneTree) : Type

The leaf carrier of a Hepp tree.

Equations

• Anderson4D.HeppLeaf t = ↥t.Leaves

def Anderson4D.leafMultiplicity {t : PlaneTree} (mu : t.Multiplicities) : HeppLeaf t → ℕ

The multiplicity function restricted to its meaningful leaf carrier.

Equations

• Anderson4D.leafMultiplicity mu l = mu.m ↑l

def Anderson4D.totalMultiplicity {t : PlaneTree} (mu : t.Multiplicities) : ℕ

Total word length m = ∑_l m_l from Definition 5.3.

Equations

• Anderson4D.totalMultiplicity mu = ∑ l : Anderson4D.HeppLeaf t, Anderson4D.leafMultiplicity mu l

def Anderson4D.nonrootBranches (t : PlaneTree) : Finset t.VPos

The non-root branch nodes. Every parent-scale ratio in (5.15), (5.33), and (5.39) is indexed by this set.

Equations

• Anderson4D.nonrootBranches t = t.BranchNodes.erase t.rootV

def Anderson4D.branchNodesUnder {t : PlaneTree} (v : t.VPos) : Finset t.VPos

Branch nodes in the subtree rooted at v; this is paper notation B_v = {u ∈ B : u ≤ v} from Definition 5.3.

Equations

• Anderson4D.branchNodesUnder v = {u ∈ t.BranchNodes | ↑v <+: ↑u}

def Anderson4D.accumulatedScale {t : PlaneTree} (Nm : t.HeppMarking) (mu : t.Multiplicities) (v : t.VPos) : ℕ

The quantity N'_v = ∑_{u ≤ v} γ_u^∞ N_u used in (5.32) and (5.38).

Equations

• Anderson4D.accumulatedScale Nm mu v = ∑ u ∈ Anderson4D.branchNodesUnder v, Anderson4D.gammaInf mu u * Anderson4D.scaleN Nm u

def Anderson4D.IsSeparatedEmbedding {t : PlaneTree} (Nm : t.HeppMarking) (z : HeppLeaf t → Fin 4 → ℤ) : Prop

Definition 5.4(a), without the unrelated boundedness and linking clauses: the leaf embedding is injective and separated at the LCA scale.

Equations

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

def Anderson4D.SatisfiesSubtreeDiameter {t : PlaneTree} (Nm : t.HeppMarking) (mu : t.Multiplicities) (z : HeppLeaf t → Fin 4 → ℤ) : Prop

Condition (5.32): every pair of leaves below a branch node is at distance at most N'_v.

Equations

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

def Anderson4D.SatisfiesSingleScaleCondition {t : PlaneTree} (Nm : t.HeppMarking) (mu : t.Multiplicities) : Prop

Condition (5.38)(a): N_{v⁺} ≤ 8 N'_v for every non-root branch node.

Equations

• Anderson4D.SatisfiesSingleScaleCondition Nm mu = ∀ v ∈ Anderson4D.nonrootBranches t, Anderson4D.scaleN Nm (Anderson4D.PlaneTree.parentV v) ≤ 8 * Anderson4D.accumulatedScale Nm mu v

def Anderson4D.IsDyadicNat (R : ℕ) : Prop

Natural dyadic numbers, used for the scale R in Proposition 5.10.

Equations

• Anderson4D.IsDyadicNat R = ∃ (k : ℕ), R = 2 ^ k

@[reducible, inline]

abbrev Anderson4D.AdjacentIndex (m : ℕ) : Type

Positions having a successor. This is the zero-based version of the paper's index set {1, ..., m-1}.

Equations

• Anderson4D.AdjacentIndex m = { j : Fin m // ↑j + 1 < m }

def Anderson4D.adjacentSucc {m : ℕ} (j : AdjacentIndex m) : Fin m

The position immediately to the right of an adjacency index.

Equations

• Anderson4D.adjacentSucc j = ⟨↑↑j + 1, ⋯⟩

noncomputable def Anderson4D.latticeEdgeWeight (x y : Fin 4 → ℤ) : ℝ

The exact factor ⟨x-y⟩⁻² = (1 + |x-y|²)⁻¹ in (5.15), (5.33), and (5.39), using the project's fixed lattice sup norm.

Equations

• Anderson4D.latticeEdgeWeight x y = (1 + Anderson4D.znorm (x - y) ^ 2)⁻¹

noncomputable def Anderson4D.heppChainWeight {t : PlaneTree} {m : ℕ} (z : HeppLeaf t → Fin 4 → ℤ) (w : Fin m → HeppLeaf t) : ℝ

Product of all adjacent edge weights in a word.

Equations

• Anderson4D.heppChainWeight z w = ∏ j : Anderson4D.AdjacentIndex m, Anderson4D.latticeEdgeWeight (z (w ↑j)) (z (w (Anderson4D.adjacentSucc j)))

noncomputable def Anderson4D.heppChainWeightExcept {t : PlaneTree} {m : ℕ} (z : HeppLeaf t → Fin 4 → ℤ) (O : Finset (AdjacentIndex m)) (w : Fin m → HeppLeaf t) : ℝ

Product in (5.39), omitting exactly the adjacency indices in O.

Equations

• Anderson4D.heppChainWeightExcept z O w = ∏ j : Anderson4D.AdjacentIndex m, if j ∈ O then 1 else Anderson4D.latticeEdgeWeight (z (w ↑j)) (z (w (Anderson4D.adjacentSucc j)))

def Anderson4D.NoAdjacentOutside {α : Type u_1} {m : ℕ} [DecidableEq α] (O : Finset (AdjacentIndex m)) (w : Fin m → α) : Prop

Proposition 5.10's adjacency condition: equal consecutive leaves are forbidden outside the skipped set O; no primitivity is imposed.

Equations

• Anderson4D.NoAdjacentOutside O w = ∀ j ∉ O, w ↑j ≠ w (Anderson4D.adjacentSucc j)

@[implicit_reducible]

instance Anderson4D.instDecidableNoAdjacentOutside {α : Type u_1} {m : ℕ} [DecidableEq α] (O : Finset (AdjacentIndex m)) (w : Fin m → α) : Decidable (NoAdjacentOutside O w)

Equations

• Anderson4D.instDecidableNoAdjacentOutside O w = Anderson4D.instDecidableNoAdjacentOutside._aux_1 O w

noncomputable def Anderson4D.primitiveChainWeight {t : PlaneTree} {m : ℕ} (z : HeppLeaf t → Fin 4 → ℤ) (w : Fin m → HeppLeaf t) : ℝ

The (5.15) summand, including precisely the word-level primitivity condition (5.11)(c).

Equations

• Anderson4D.primitiveChainWeight z w = if Anderson4D.NoProperLeafBlock w then Anderson4D.heppChainWeight z w else 0

noncomputable def Anderson4D.primitiveSeparatedChainWeight {t : PlaneTree} {m : ℕ} (z : HeppLeaf t → Fin 4 → ℤ) (w : Fin m → HeppLeaf t) : ℝ

The (5.33) summand: primitivity together with no adjacent equal leaves.

Equations

• Anderson4D.primitiveSeparatedChainWeight z w = if Anderson4D.NoProperLeafBlock w ∧ Anderson4D.NoAdjacentEqual w then Anderson4D.heppChainWeight z w else 0

noncomputable def Anderson4D.singleScaleChainWeight {t : PlaneTree} {m : ℕ} (z : HeppLeaf t → Fin 4 → ℤ) (O : Finset (AdjacentIndex m)) (w : Fin m → HeppLeaf t) : ℝ

The (5.39) summand: omitted factors at O, the adjacency restriction outside O, and deliberately no primitivity condition.

Equations

• Anderson4D.singleScaleChainWeight z O w = if Anderson4D.NoAdjacentOutside O w then Anderson4D.heppChainWeightExcept z O w else 0

noncomputable def Anderson4D.sqrtFactorial (k : ℕ) : ℝ

(k!)^{1/2} in the paper.

Equations

• Anderson4D.sqrtFactorial k = √↑k.factorial

noncomputable def Anderson4D.factorialThreeQuarters (k : ℕ) : ℝ

(k!)^{3/4} in the paper, represented by Real.rpow.

Equations

• Anderson4D.factorialThreeQuarters k = ↑k.factorial ^ (3 / 4)

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

The scale ratio N_v / N_{v⁺}, used only for non-root branch nodes.

Equations

• Anderson4D.parentScaleRatio Nm v = ↑(Anderson4D.scaleN Nm v) / ↑(Anderson4D.scaleN Nm (Anderson4D.PlaneTree.parentV v))

Proposition 5.7, equation (5.15)

noncomputable def Anderson4D.permSumRHS (C : ℝ) (n : ℕ) (t : PlaneTree) (Nm : t.HeppMarking) (mu : t.Multiplicities) : ℝ

The right-hand side of (5.15), with W ranging over subsets of the non-root branch nodes.

Equations

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

def Anderson4D.PermSumEstimate (C : ℝ) : Prop

Proposition 5.7 / (5.15), frozen statement.

C is the single absolute constant. The hypotheses spell out the ambient n ≥ 2 context, a valid nontrivial Hepp tree, even leaf multiplicities of total 2n, and realization by a fully admissible embedding.

Equations

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

Proposition 5.9, equations (5.32)--(5.33)

noncomputable def Anderson4D.inductiveRHS (C0 D : ℝ) (m : ℕ) (t : PlaneTree) (Nm : t.HeppMarking) (mu : t.Multiplicities) (compound : Finset t.VPos) : ℝ

The right-hand side of (5.33). compound is exactly the set L_C; simpleLeaves t compound is L_S.

Equations

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

def Anderson4D.InductiveEstimate (C0 D : ℝ) : Prop

Proposition 5.9 / (5.32)--(5.33), frozen statement.

The named constants remain parameters with the literal hypotheses C0 > 1000 and D = exp(C0^10). Compound multiplicities need not be even. The left side retains both primitivity and the no-adjacent-equal restriction.

Equations

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

Proposition 5.10, equations (5.38)--(5.39)

noncomputable def Anderson4D.singleScaleRHS (C0 : ℝ) (m s R : ℕ) (t : PlaneTree) (Nm : t.HeppMarking) (mu : t.Multiplicities) (compound : Finset t.VPos) : ℝ

The right-hand side of (5.39). The exponent m/2 on C0 is a real half-power, not natural-number division.

Equations

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

def Anderson4D.SingleScaleEstimate (C0 : ℝ) : Prop

Proposition 5.10 / (5.38)--(5.39), frozen statement.

R is explicitly dyadic and dominates N'_r; O is a set of adjacency indices with |O| = s. The left side has no primitivity restriction.

Equations

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