A parent-function substitute for the weighted Cayley identity

Paper (5.24)--(5.25) needs only an upper bound for a weighted sum over labelled link trees. We do not formalize the stronger weighted Cayley identity used in the paper. Instead, after choosing a root, orient every edge toward it and encode each of the other q - 1 vertices by its parent. This injects the relevant trees into

ParentCode q = (Fin (q - 1) → Fin q).

The sum over all parent functions factorizes exactly. With parent weights 1 + w i it is

(q + ∑ i, w i) ^ (q - 1).

Thus any injectively parent-encoded tree family whose tree weight is bounded by its code weight satisfies the inequality required at (5.24). This is a documented proof substitution: the conclusion is weaker than the paper's exact weighted Cayley formula, but is precisely the estimate consumed by Proposition 5.6.

All statements below include q = 0 and q = 1. In both cases the parent slot type is empty and the empty product is 1; explicit endpoint lemmas are provided at the end.

@[reducible, inline]

abbrev Anderson4D.ParentCode (q : ℕ) : Type

A rooted parent-function code on q labels: one parent choice for each of the q - 1 non-root slots.

Equations

• Anderson4D.ParentCode q = (Fin (q - 1) → Fin q)

def Anderson4D.parentCodeWeight {R : Type u_1} [CommMonoid R] {q : ℕ} (a : Fin q → R) (p : ParentCode q) : R

Multiplicative weight of a parent-function code.

Equations

• Anderson4D.parentCodeWeight a p = ∏ j : Fin (q - 1), a (p j)

theorem Anderson4D.sum_parentCodeWeight {R : Type u_1} [CommSemiring R] (q : ℕ) (a : Fin q → R) : ∑ p : ParentCode q, parentCodeWeight a p = (∑ i : Fin q, a i) ^ (q - 1)

Exact factorization of the sum over all parent functions.

Natural weights

theorem Anderson4D.sum_parentCodeWeight_subset_nat (q : ℕ) (a : Fin q → ℕ) (P : Finset (ParentCode q)) : ∑ p ∈ P, parentCodeWeight a p ≤ (∑ i : Fin q, a i) ^ (q - 1)

For natural weights, restricting to any finite set of parent functions can only decrease the total weight.

theorem Anderson4D.sum_parentCodeWeight_one_add_nat (q : ℕ) (w : Fin q → ℕ) : ∑ p : ParentCode q, parentCodeWeight (fun (i : Fin q) => 1 + w i) p = (q + ∑ i : Fin q, w i) ^ (q - 1)

Exact all-parent-functions formula with the paper's natural weights 1 + w i.

theorem Anderson4D.parentCode_one_add_bound_nat (q : ℕ) (w : Fin q → ℕ) (P : Finset (ParentCode q)) : ∑ p ∈ P, parentCodeWeight (fun (i : Fin q) => 1 + w i) p ≤ (q + ∑ i : Fin q, w i) ^ (q - 1)

Parent-function upper bound with natural weights, in the exact form used by the proof substitution for paper (5.24)--(5.25).

Nonnegative real weights

theorem Anderson4D.parentCodeWeight_nonneg_real {q : ℕ} {a : Fin q → ℝ} (ha : ∀ (i : Fin q), 0 ≤ a i) (p : ParentCode q) : 0 ≤ parentCodeWeight a p

theorem Anderson4D.sum_parentCodeWeight_subset_real (q : ℕ) (a : Fin q → ℝ) (ha : ∀ (i : Fin q), 0 ≤ a i) (P : Finset (ParentCode q)) : ∑ p ∈ P, parentCodeWeight a p ≤ (∑ i : Fin q, a i) ^ (q - 1)

For nonnegative real weights, restricting to a finite set of parent functions can only decrease the total weight.

theorem Anderson4D.sum_parentCodeWeight_one_add_real (q : ℕ) (w : Fin q → ℝ) : ∑ p : ParentCode q, parentCodeWeight (fun (i : Fin q) => 1 + w i) p = (↑q + ∑ i : Fin q, w i) ^ (q - 1)

Exact all-parent-functions formula with nonnegative real weights 1 + w i. Nonnegativity is not needed for the identity itself.

theorem Anderson4D.parentCode_one_add_bound_real (q : ℕ) (w : Fin q → ℝ) (hw : ∀ (i : Fin q), 0 ≤ w i) (P : Finset (ParentCode q)) : ∑ p ∈ P, parentCodeWeight (fun (i : Fin q) => 1 + w i) p ≤ (↑q + ∑ i : Fin q, w i) ^ (q - 1)

Parent-function upper bound for nonnegative real weights, in the exact form consumed by paper (5.24)--(5.25).

Injectively encoded finite tree families

theorem Anderson4D.weightedCayley_le_of_parent_injection {τ : Type u_1} [DecidableEq τ] (q : ℕ) (trees : Finset τ) (encode : τ → ParentCode q) (hencode : Set.InjOn encode ↑trees) (degree : τ → Fin q → ℕ) (w : Fin q → ℝ) (hw : ∀ (i : Fin q), 0 ≤ w i) (hweight : ∀ T ∈ trees, ∏ i : Fin q, (1 + w i) ^ (degree T i - 1) ≤ parentCodeWeight (fun (i : Fin q) => 1 + w i) (encode T)) : ∑ T ∈ trees, ∏ i : Fin q, (1 + w i) ^ (degree T i - 1) ≤ (↑q + ∑ i : Fin q, w i) ^ (q - 1)

Parent-function proof substitution for weighted Cayley.

Let trees be any finite family, encode an injection from that family into rooted parent functions, and degree its degree data. If the intended tree weight ∏ i, (1 + w i) ^ (degree T i - 1) is bounded by the corresponding parent-code weight (the missing root factor is ≥ 1), then the weighted tree sum is at most (q + ∑ i, w i)^(q-1).

This is the directly reusable interface for Proposition 5.6, Step 5; the caller supplies only the combinatorial encoding and its pointwise weight comparison.

theorem Anderson4D.weightedCayley_le_of_parent_injection_nat {τ : Type u_1} [DecidableEq τ] (q : ℕ) (trees : Finset τ) (encode : τ → ParentCode q) (hencode : Set.InjOn encode ↑trees) (degree : τ → Fin q → ℕ) (w : Fin q → ℕ) (hweight : ∀ T ∈ trees, ∏ i : Fin q, (1 + w i) ^ (degree T i - 1) ≤ parentCodeWeight (fun (i : Fin q) => 1 + w i) (encode T)) : ∑ T ∈ trees, ∏ i : Fin q, (1 + w i) ^ (degree T i - 1) ≤ (q + ∑ i : Fin q, w i) ^ (q - 1)

Natural-weight analogue of weightedCayley_le_of_parent_injection.

Explicit small-cardinality endpoints

@[simp]

theorem Anderson4D.parentCodeWeight_zero {R : Type u_1} [CommMonoid R] (a : Fin 0 → R) (p : ParentCode 0) : parentCodeWeight a p = 1

@[simp]

theorem Anderson4D.parentCodeWeight_one {R : Type u_1} [CommMonoid R] (a : Fin 1 → R) (p : ParentCode 1) : parentCodeWeight a p = 1

theorem Anderson4D.parentCode_one_add_bound_nat_zero (w : Fin 0 → ℕ) (P : Finset (ParentCode 0)) : ∑ p ∈ P, parentCodeWeight (fun (i : Fin 0) => 1 + w i) p ≤ 1

Natural-weight endpoint at q = 0.

theorem Anderson4D.parentCode_one_add_bound_nat_one (w : Fin 1 → ℕ) (P : Finset (ParentCode 1)) : ∑ p ∈ P, parentCodeWeight (fun (i : Fin 1) => 1 + w i) p ≤ 1

Natural-weight endpoint at q = 1.

theorem Anderson4D.parentCode_one_add_bound_real_zero (w : Fin 0 → ℝ) (P : Finset (ParentCode 0)) : ∑ p ∈ P, parentCodeWeight (fun (i : Fin 0) => 1 + w i) p ≤ 1

At q = 0, every subset of parent codes has total real weight at most the empty-product value 1.

theorem Anderson4D.parentCode_one_add_bound_real_one (w : Fin 1 → ℝ) (hw : ∀ (i : Fin 1), 0 ≤ w i) (P : Finset (ParentCode 1)) : ∑ p ∈ P, parentCodeWeight (fun (i : Fin 1) => 1 + w i) p ≤ 1

At q = 1, there are no parent slots, so every subset of parent codes has total real weight at most 1.