ConditionalUnoriented.lean`

5 declarations, 0 contain sorry, 0 declared as axioms

The topological reduction from the oriented two-model theorem to the unoriented three-model theorem uses the orientation cover, its pullback metric and the Euler/Betti identities from Hatcher.

structure OAI.PositiveEinsteinFour.ClosedOrientedMetricFour line 23
Source documentation
A closed connected oriented Riemannian four-manifold, with its genuine smooth manifold structure. The measurable structure can be installed as the Borel structure when applying the analytic theorem.
Distinct definitions of this name: ComparatorChallenges/EinsteinFour.lean:156 (same statement text; different proof or body). Qualify references as OAI.PositiveEinsteinFour.ClosedOrientedMetricFour@path.
```
structure ClosedOrientedMetricFour where
…
```
structure OAI.PositiveEinsteinFour.OrientationMetricDoubleCover line 42
Source documentation
Hatcher's connected orientation cover, equipped with the pullback metric. Preservation of Einstein and positive sectional curvature is the local-isometry specialization in Petersen §1.3.3.
```
structure OrientationMetricDoubleCover (g : SmoothMetric M) where
…
```
def OAI.PositiveEinsteinFour.HatcherOrientationCoverInput line 51
Source documentation
Hatcher, Proposition 3.25 and Theorem 3.26(c), together with smooth metric pullback: either an orientation exists, or its connected two-sheeted cover has the displayed actual geometric data.
```
def HatcherOrientationCoverInput (g : SmoothMetric M) : Prop :=
…
```
structure OAI.PositiveEinsteinFour.UnorientedPublishedInputs line 57
Source documentation
The precise covering/topological inputs needed after the oriented classification. The Euler and Betti statements concern the actual cover manifold; the antipodal quotient is proved from its metric data.
```
structure UnorientedPublishedInputs (g : SmoothMetric M) : Prop where
…
```

theorem OAI.PositiveEinsteinFour.classified_of_oriented_models line 70

Source documentation

The oriented analytic classification, once supplied for every closed oriented metric, implies the full unoriented classification. The sphere cover descends through a proved free-involution quotient; the CP² cover contradicts the proved odd Euler obstruction.

theorem classified_of_oriented_models (g : SmoothMetric M)
    (hpublished : UnorientedPublishedInputs g)
    (hmodels : ∀ X : ClosedOrientedMetricFour.{u},
      IsEinstein X.metric → HasPositiveSectionalCurvature X.metric →
        ∃ a : ℝ, 0 < a ∧ (ScaledIsometricTo X.metric a roundDistance ∨
          ScaledIsometricTo X.metric a fubiniStudyDistance))
    (hEinstein : IsEinstein g) (hpositive : HasPositiveSectionalCurvature g) :
    Classified g := by
…

Mentions: OAI.PositiveEinsteinFour.UnorientedPublishedInputs, OAI.PositiveEinsteinFour.Classified