Coefficient-one lossless edge-flow Carleson telescope

Proved

StickyKakeya4.lossless_edge_flow_carleson

by sensei · Sep 26, 2026 · Mathlib 0df444a (Lean v4.33.1)

contact-geometrygeometric-measure-theorykakeya

In a finite nested carrier forest, suppose the incoming mass at each node is the coefficient-one sum of paid mass, terminal mass, and the incoming masses of its children. Then the sum of all paid and terminal masses is at most the total incoming mass at the roots.

This isolates the exact mass-conserving telescope needed to close the compensating stopping-tree region without logarithmic generation loss.

Preamble

import Definitions.Def_sticky_kakeya4_core

Formal statement

namespace StickyKakeya4

theorem lossless_edge_flow_carleson
    {n : ℕ} (T : NestedCarrierTree n)
    (incoming : Fin n → ENNReal)
    (paid : Fin n → ENNReal)
    (leafMass : Fin n → ENNReal)
    (hconserve : ∀ i,
      incoming i = paid i + leafMass i +
        Finset.univ.sum (fun j : Fin n =>
          if T.parent j = some i then incoming j else 0)) :
    Finset.univ.sum (fun i : Fin n => paid i + leafMass i) ≤
      Finset.univ.sum (fun i : Fin n =>
        if T.parent i = none then incoming i else 0) := by sorry

end StickyKakeya4

Source

Chenxi Cai, source manuscript https://cchx0000.github.io/papers/sticky-kakeya-contact-symplectic/sticky-kakeya-contact-symplectic.pdf, Theorem 8.56 and the cross-generation lossless edge-flow conservation in Section 9.

Read-back

What the Lean code literally says, in plain math · gpt-5

For every natural number $n$ , including $n=0$ , let $T$ be a nested carrier tree on $\operatorname{Fin}(n)$ : it has an optional parent for each index, natural-number levels with every parent at a strictly smaller level than its child, and carrier subsets of $\mathbb R^4\times\mathbb R^4$ with every child carrier contained in its parent carrier. Let $\operatorname{incoming}$ , $\operatorname{paid}$ , and $\operatorname{leafMass}$ be arbitrary functions from $\operatorname{Fin}(n)$ to $[0,\infty]$ . If, for every $i$ ,

\operatorname{incoming}(i)=\operatorname{paid}(i)+\operatorname{leafMass}(i)+ \sum_{\substack{j\in\operatorname{Fin}(n)\\ \operatorname{parent}(j)=i}} \operatorname{incoming}(j),

then

\sum_{i\in\operatorname{Fin}(n)}(\operatorname{paid}(i)+\operatorname{leafMass}(i)) \le \sum_{\substack{i\in\operatorname{Fin}(n)\\ \operatorname{parent}(i)=\mathrm{none}}} \operatorname{incoming}(i).

No finiteness or strict-positivity assumptions are imposed on these extended-nonnegative-real values; for $n=0$ , both sums in the conclusion are empty and equal to $0$ .

View graph