Construct measured surgery data from a hypothetical counterexample

Open

PoincareFormalization.measured_surgery_data_of_not_homeomorph_sphere

by Xinze-Li-Moqian · Sep 10, 2026 · Mathlib 0df444a (Lean v4.33.1)

bishop-gromovgeometric-analysispoincare-conjecture

For a compact simply connected Hausdorff topological three-manifold $M$ hypothetically not homeomorphic to $S^3$ , construct one $W\ge0$ such that for every $T>0$ there are measured surgery comparison data on $[0,T]$ . This is an Open geometric construction. It must supply the reference ball and measure, the uniform radial lower bound at every event, density comparison, removed-region containment, a total volume budget, and scalar/sweepout profiles. The intended application must identify the abstract measure with geometric volume. Smoothing, Ricci flow with surgery, and the Colding–Minicozzi estimates remain to be developed.

Preamble

import Definitions.Def_OpenGA_MeasuredSurgeryComparisonData
import Mathlib.Geometry.Manifold.ChartedSpace
import Mathlib.Analysis.InnerProductSpace.PiL2
import Mathlib.AlgebraicTopology.FundamentalGroupoid.SimplyConnected
import Definitions.Def_OpenGA_SurgeryComparisonProcess
import Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic
import Mathlib.MeasureTheory.Integral.Lebesgue.Add
import Mathlib.Data.Finset.Sort
import Mathlib.Data.Set.Finite.Basic
import Mathlib.Algebra.Order.Archimedean.Basic
import Mathlib.Algebra.Order.BigOperators.Group.Finset
import Mathlib.Tactic.Linarith

set_option autoImplicit false
open MeasureTheory Set Filter
open scoped ENNReal BigOperators Topology
open DifferentialGeometry.Geometry.Riemannian.VolumeComparison

Formal statement

theorem PoincareFormalization.measured_surgery_data_of_not_homeomorph_sphere
    (M : Type*) [TopologicalSpace M] [T2Space M]
    [ChartedSpace (EuclideanSpace ℝ (Fin 3)) M]
    [SimplyConnectedSpace M] [CompactSpace M]
    (hnot : ¬ Nonempty (M ≃ₜ ↥(Metric.sphere (0 : EuclideanSpace ℝ (Fin (3 + 1))) 1))) :
    ∃ initialWidth : ℝ, 0 ≤ initialWidth ∧ ∀ finalTime : ℝ, 0 < finalTime →
      Nonempty (OpenGA.MeasuredSurgeryComparisonData initialWidth finalTime) := by sorry

Source

https://github.com/MathNetwork/OpenGA/blob/feat/prove2me-differential-geometry/OpenGALib/ComparisonGeometry/MeasuredSurgery.lean

View graph