Counting sequences with geometric-decay weights

Paper: L-5.13 — (5.55)/(5.56) — sequence counting

Formalization of Lemma 5.13 of Deng–Shen (arXiv:2607.10105), PAPER_MAP node L-5.13: the bounds (5.55) and (5.56), plus a variant of (5.55) where an exception set of at most B consecutive-pair positions is omitted from the product.

• Anderson4D.sum_min_two_rpow_le — paper (5.55): for θ > 0 there is C = C(θ) ≥ 1 such that for all m + 1 ≤ n, summing over tuples z : Fin (m+1) → Fin n the products ∏ⱼ min 1 (2 ^ (−θ(z_j − z_{j+1}))) over consecutive pairs gives at most C ^ n.
• Anderson4D.sum_min_two_rpow_skip_le — (5.55) with the product restricted to univ \ E for an exception set E with E.card ≤ B; C = C(θ, B).
• Anderson4D.sum_min_ratio_pow_le — paper (5.56): for n + 1 distinct dyadics P_k = 2 ^ (e k) (with e injective), summing over all maps x : Fin (n+1) → Fin (n+1) the products ∏ⱼ min 1 ((P_{x(j+1)} / P_{x(j)}) ^ θ) gives at most C ^ (n+1).
• Anderson4D.sum_min_ratio_pow_skip_le_rect — the rectangular, bounded-skip form used in Step 3 of Proposition 5.10, where the sequence may be longer than the family of distinct dyadic values.

Representation choices. Tuples of length m + 1 with the product over j : Fin m via Fin.castSucc/Fin.succ replace the paper's length-m tuples with m - 1 consecutive pairs (avoiding truncated subtraction in the index type). The paper's 2 ^ (−θ(z_j − z_{j+1})) has a real exponent, so it is a real power (rpow) of an integer-valued difference; in (5.56) the dyadics 2 ^ (e k) are integer powers (zpow) and the outer exponent θ is again rpow.

theorem Anderson4D.sum_min_two_rpow_le (θ : ℝ) (hθ : 0 < θ) : ∃ (C : ℝ), 1 ≤ C ∧ ∀ (m n : ℕ), m + 1 ≤ n → ∑ z : Fin (m + 1) → Fin n, ∏ j : Fin m, min 1 (2 ^ (-(θ * ↑(↑↑(z j.castSucc) - ↑↑(z j.succ))))) ≤ C ^ n

Paper (5.55), Lemma 5.13 (node L-5.13). For θ > 0 there is C = C(θ) ≥ 1 such that for all m, n with m + 1 ≤ n, ∑_{z : Fin (m+1) → Fin n} ∏_{j} min 1 (2 ^ (−θ(z_j − z_{j+1}))) ≤ C ^ n, the product running over the m consecutive pairs and the difference z_j − z_{j+1} being integer-valued (the power is rpow).

theorem Anderson4D.sum_min_two_rpow_skip_le (θ : ℝ) (hθ : 0 < θ) (B : ℕ) : ∃ (C : ℝ), 1 ≤ C ∧ ∀ (m n : ℕ), m + 1 ≤ n → ∀ (E : Finset (Fin m)), E.card ≤ B → ∑ z : Fin (m + 1) → Fin n, ∏ j ∈ Finset.univ \ E, min 1 (2 ^ (-(θ * ↑(↑↑(z j.castSucc) - ↑↑(z j.succ))))) ≤ C ^ n

Skip variant of paper (5.55), Lemma 5.13. The (5.55)-bound with the product over consecutive pairs outside an exception set E of size at most B; the constant depends only on θ and B.

theorem Anderson4D.sum_min_ratio_pow_skip_le_rect (θ : ℝ) (hθ : 0 < θ) (B : ℕ) : ∃ (C : ℝ), 1 ≤ C ∧ ∀ (m ν : ℕ) (e : Fin ν → ℤ), ν ≤ m + 1 → Function.Injective e → ∀ (E : Finset (Fin m)), E.card ≤ B → ∑ x : Fin (m + 1) → Fin ν, ∏ j ∈ Finset.univ \ E, min 1 ((2 ^ e (x j.succ) / 2 ^ e (x j.castSucc)) ^ θ) ≤ C ^ (m + 1)

Rectangular bounded-skip form of paper (5.56), Lemma 5.13.

The paper applies (5.56) to a sequence whose length is the total multiplicity, while its entries belong to a possibly smaller finite family of distinct dyadic values. This theorem records that exact reindexing: if ν ≤ m + 1, an injective exponent family e : Fin ν → ℤ may be ranked inside Fin (m + 1), and the resulting sum is bounded by C ^ (m + 1). The product may omit a set E of at most B adjacent pairs.

theorem Anderson4D.sum_min_ratio_pow_le (θ : ℝ) (hθ : 0 < θ) : ∃ (C : ℝ), 1 ≤ C ∧ ∀ (n : ℕ) (e : Fin (n + 1) → ℤ), Function.Injective e → ∑ x : Fin (n + 1) → Fin (n + 1), ∏ j : Fin n, min 1 ((2 ^ e (x j.succ) / 2 ^ e (x j.castSucc)) ^ θ) ≤ C ^ (n + 1)

Paper (5.56), Lemma 5.13 (node L-5.13). For θ > 0 there is C = C(θ) ≥ 1 with the following property: for every n and every injective exponent family e : Fin (n+1) → ℤ — encoding n + 1 distinct dyadics P_k = 2 ^ (e k) — summing over all maps x : Fin (n+1) → Fin (n+1) the products ∏ⱼ min 1 ((P_{x(j+1)} / P_{x(j)}) ^ θ) over the n consecutive pairs gives at most C ^ (n+1). The dyadics are integer powers (zpow) of 2; the outer exponent θ is a real power (rpow). Proof: replace the e-values by their ranks (rank_sub_rank_le) and compose with the injection x ↦ rank ∘ x into the (5.55)-sum.

theorem Anderson4D.sum_min_ratio_pow_le_of_strictMono (θ : ℝ) (hθ : 0 < θ) : ∃ (C : ℝ), 1 ≤ C ∧ ∀ (n : ℕ) (e : Fin (n + 1) → ℤ), StrictMono e → ∑ x : Fin (n + 1) → Fin (n + 1), ∏ j : Fin n, min 1 ((2 ^ e (x j.succ) / 2 ^ e (x j.castSucc)) ^ θ) ≤ C ^ (n + 1)

Paper (5.56), Lemma 5.13 — sorted form. The bound of sum_min_ratio_pow_le for strictly increasing exponent families.