Toy model for the permutation-sum machine (paper (1.14)/(1.15))

Paper: T-toy — (1.14)/(1.15) — the toy estimate

This file formalizes the toy model of arXiv:2607.10105, equations (1.14) and (1.15), which is the model computation behind the §5.4 permutation-sum machine. Points live in Fin 4 → ℝ equipped with the sup (Pi) norm; all constants are norm-dependent and are absorbed into explicit absolute constants.

Main results

• Anderson4D.packing_lemma — the packing/shell bound (1.15): for a τ-separated finite set A and any point x, the sum of ‖x - y‖⁻¹ ^ 2 over the points y ∈ A with τ ≤ ‖x - y‖ is at most packing_const * √#A * τ⁻¹ ^ 2.
• Anderson4D.toy_injTuple_bound — the toy bound (1.14) for sums over injective tuples of points of A: the sum over injective m-tuples of the consecutive inverse-square chain product is at most C ^ n * √(n !) * τ⁻¹ ^ (2 * (m - 1)).
• Anderson4D.toy_permSum_bound — the specialization (1.14) to sums over permutations of n separated points.

def Anderson4D.packing_const : ℝ

The explicit absolute constant in the packing lemma (1.15) for the sup norm on Fin 4 → ℝ. It arises as 256 * 4: shell j contains at most 256 * 16 ^ j points and the dyadic-shell comparison series contributes a factor 4.

Equations

• Anderson4D.packing_const = 1024

theorem Anderson4D.packing_lemma (A : Finset (Fin 4 → ℝ)) {τ : ℝ} (hτ : 0 < τ) (hsep : ∀ a ∈ A, ∀ b ∈ A, a ≠ b → τ ≤ ‖a - b‖) (x : Fin 4 → ℝ) : ∑ y ∈ A with τ ≤ ‖x - y‖, ‖x - y‖⁻¹ ^ 2 ≤ packing_const * √↑A.card * τ⁻¹ ^ 2

Packing lemma, the toy-model estimate (1.15) of arXiv:2607.10105: for a τ-separated finite set A ⊆ Fin 4 → ℝ (sup norm) and any point x, ∑_{y ∈ A, τ ≤ ‖x-y‖} ‖x - y‖⁻² ≤ packing_const · √#A · τ⁻². The proof decomposes the sum into dyadic shells 2^j τ ≤ ‖x - y‖ < 2^{j+1} τ; shell j has at most min (256 · 16^j) #A points, and comparing the resulting series with two geometric series at the crossover 16^j ≈ #A yields √#A.

Sums over injective tuples: the toy bound (1.14)

noncomputable def Anderson4D.injTuples (m : ℕ) (A : Finset (Fin 4 → ℝ)) : Finset (Fin m → Fin 4 → ℝ)

The finite set of injective m-tuples of points of A (as functions Fin m → (Fin 4 → ℝ) with all values in A). Summing the chain weight chainWeight over injTuples n A with #A = n is the paper's sum (1.14) over orderings of the points of A.

Equations

• Anderson4D.injTuples m A = Finset.filter Function.Injective (Fintype.piFinset fun (x : Fin m) => A)

noncomputable def Anderson4D.chainWeight (m : ℕ) (f : Fin m → Fin 4 → ℝ) : ℝ

The consecutive inverse-square chain product ∏_{j<m-1} ‖f j - f (j+1)‖⁻² of a tuple, the summand of (1.14).

Equations

• Anderson4D.chainWeight m f = ∏ j : Fin (m - 1), ‖f ⟨↑j, ⋯⟩ - f ⟨↑j + 1, ⋯⟩‖⁻¹ ^ 2

theorem Anderson4D.chainWeight_nonneg (m : ℕ) (f : Fin m → Fin 4 → ℝ) : 0 ≤ chainWeight m f

theorem Anderson4D.mem_injTuples {m : ℕ} {A : Finset (Fin 4 → ℝ)} {f : Fin m → Fin 4 → ℝ} : f ∈ injTuples m A ↔ (∀ (i : Fin m), f i ∈ A) ∧ Function.Injective f

theorem Anderson4D.toy_injTuple_bound : ∃ (C : ℝ), 1 ≤ C ∧ ∀ (n m : ℕ) (τ : ℝ), 0 < τ → ∀ (A : Finset (Fin 4 → ℝ)), A.card = n → (∀ a ∈ A, ∀ b ∈ A, a ≠ b → τ ≤ ‖a - b‖) → m ≤ n → ∑ f ∈ injTuples m A, chainWeight m f ≤ C ^ n * √↑n.factorial * τ⁻¹ ^ (2 * (m - 1))

Toy theorem (1.14), injective-tuple form. For n τ-separated points in Fin 4 → ℝ (sup norm) and any m ≤ n, the sum over injective m-tuples of the consecutive inverse-square chain product is at most C ^ n · √(n!) · τ^{-2(m-1)} with an absolute constant C. This is the paper's bound (1.14) on the ordering sum, in the form that feeds the §5.4 permutation-sum machine; it follows by iterating the packing lemma (1.15) and the factorial comparison n^n ≤ 4^n n! (giving n^{(n-1)/2} ≤ 2^n √(n!)).

theorem Anderson4D.toy_permSum_bound : ∃ (C : ℝ), 1 ≤ C ∧ ∀ (n : ℕ) (τ : ℝ), 0 < τ → ∀ (x : Fin n → Fin 4 → ℝ), Function.Injective x → (∀ (i j : Fin n), i ≠ j → τ ≤ ‖x i - x j‖) → (∑ π : Equiv.Perm (Fin n), chainWeight n fun (k : Fin n) => x (π k)) ≤ C ^ n * √↑n.factorial * τ⁻¹ ^ (2 * (n - 1))

Toy theorem (1.14), permutation form. For n pairwise τ-separated points x 0, …, x (n-1) in Fin 4 → ℝ (sup norm), the sum over all orderings (permutations π) of the consecutive inverse-square chain product ∏_{j<n-1} ‖x (π j) - x (π (j+1))‖⁻² — here chainWeight n (x ∘ π) — is at most C ^ n · √(n!) · τ^{-2(n-1)}. This is exactly (1.14): the naive bound on the n! orderings would be n! · τ^{-2(n-1)}, and the packing lemma (1.15) upgrades it to √(n!) up to C^n.