FullChartRegularGain.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

Pencil-normalized gain for the full bounded point and line chart. The fixed change of slope chart preserves original incidences and pays only the explicitly proved finite thinning and covering losses.

theorem OAI.Falconer.full_chart_regular_fine_gain line 13