Construct surgery topology with uniform area evolution
OpenPoincareFormalization.ExtinctionEndgame.exists_area_evolution_surgery_topologyfinite-extinctionwidth
For every closed simply connected topological three-manifold, construct a surgery topology evolution and one nonnegative initial width bound. For each positive horizon with nonempty final slice, supply surgery area-evolution data. The remaining geometric tasks include the admissible sweepout families, their common short-time area estimates, and the actual surgery and radial volume hypotheses. This open construction refines the measured-data input to the active extinction endgame.
Preamble
import Definitions.Def_OpenGA_SurgeryAreaEvolutionData import Definitions.Def_OpenGA_ExtinctionWidthControl set_option autoImplicit false open Set Filter open scoped Topology open OpenGA universe u
Formal statement
theorem PoincareFormalization.ExtinctionEndgame.exists_area_evolution_surgery_topology
(M : ClosedThreeManifold.{u}) [SimplyConnectedSpace M] :
∃ (E : SurgeryTopologyEvolution M) (W : ℝ), 0 ≤ W ∧
∀ T : ℝ, 0 < T → E.components T ≠ [] →
Nonempty (SurgeryAreaEvolutionData W T) := by sorrySource