Dissipation allocation with exact binomial multiplicities.

noncomputable def AVenhance.Infra.Section4.iterateYoungWeight (κ : ℝ) (n j : ℕ) : ℝ

A weight for every actual Leibniz term. Terms at coefficient order j share a geometric budget, divided by their binomial multiplicity.

Equations

• AVenhance.Infra.Section4.iterateYoungWeight κ n j = κ / 16 * (1 / 2) ^ j / ↑(n.choose j)

theorem AVenhance.Infra.Section4.iterateYoungWeight_pos {κ : ℝ} (hκ : 0 < κ) (w : List (Fin 2)) {p : List (Fin 2) × List (Fin 2)} (hp : p ∈ iterateSpatialSplits w) : 0 < iterateYoungWeight κ w.length p.1.length

Every actual split receives a positive dissipation weight.

theorem AVenhance.Infra.Section4.iterateYoungWeight_sum_le {κ : ℝ} (hκ : 0 ≤ κ) (w : List (Fin 2)) : (List.map (fun (p : List (Fin 2) × List (Fin 2)) => iterateYoungWeight κ w.length p.1.length) (iterateSpatialSplits w)).sum ≤ κ / 8

The total allocation absorbs at most one eighth of the dissipation, independently of derivative order and repeated coordinate letters.

theorem AVenhance.Infra.Section4.iterateYoungWeight_reciprocal {κ D : ℝ} (hκ : 0 < κ) (n j : ℕ) (hj : j ≤ n) : D ^ 2 / iterateYoungWeight κ n j = 16 / κ * ↑(n.choose j) * 2 ^ j * D ^ 2

The exact reciprocal weight introduces one binomial factor and a geometric factor 2^j, which cancels against the analytic factorial profile.