Construct measured surgery comparison from area evolution
ProvedOpenGA.nonempty_measuredSurgeryComparisonData_of_areaEvolutionfinite-extinctionwidth
At every time in each event-free interval, integrate the uniform area derivative estimates to construct the required width comparison datum. Preserve all volume, scalar, continuity, initial-value and jump conditions. This is a proved analytic adapter, not a construction of a Ricci flow with surgery.
Preamble
import Definitions.Def_OpenGA_SurgeryAreaEvolutionData set_option autoImplicit false open Set Filter open scoped Topology open OpenGA
Formal statement
theorem OpenGA.nonempty_measuredSurgeryComparisonData_of_areaEvolution {W T : ℝ}
(D : SurgeryAreaEvolutionData W T) : Nonempty (MeasuredSurgeryComparisonData W T) := by sorrySource