RetainedEnergy.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

Integrated estimate for the actual retained dyadic graph

This is the positive Schur step after localization. It uses the two original restricted laws and retains their endpoint symbols on every child. Summing the angular partition introduces no cap-count factor.

theorem OAI.Falconer.retained_dyadic_energy_bound line 18