ProfileGraphEstimate.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

The graph estimate with the two actual regularized profiles

This applies the proved oscillatory localization and graph bound, then inserts the actual occupied-cell counts and integer parallel-test degrees. The analytic error remains explicit for the separate arbitrary-power budget.

theorem OAI.Falconer.dyadic_profile_graph_energy_step line 17