MetricDoubleCover.lean`

12 declarations, 0 contain sorry, 0 declared as axioms

The metric and Euler reductions for an actual two-sheeted cover. The raw metric facts are the pullback/local-isometry and geodesic-lifting consequences of Petersen, §1.3.3 and Proposition 5.6.3. The minimum-distance formula, two-point fiber count, antipodal quotient and parity obstruction are derived here.

structure OAI.PositiveEinsteinFour.MetricDoubleCover line 30
Source documentation
Raw data of a Riemannian two-sheeted cover. distance_lift is the endpoint of a lift of a minimizing base geodesic from the specified point; the other distance inequality is length preservation under projection.
```
structure MetricDoubleCover (g : SmoothMetric M) (h : SmoothMetric N) where
…
```
theorem OAI.PositiveEinsteinFour.MetricDoubleCover.projection_deck line 48
theorem OAI.PositiveEinsteinFour.MetricDoubleCover.fiber_card line 52
Source documentation
Freeness and the explicit deck fibers give the actual sheet number.
```
theorem fiber_card (y : M) : Nat.card {x : N // C.projection x = y} = 2 := by
…
```
theorem OAI.PositiveEinsteinFour.MetricDoubleCover.quotient_distance_one line 79
theorem OAI.PositiveEinsteinFour.MetricDoubleCover.scaled_distance line 92
theorem OAI.PositiveEinsteinFour.MetricDoubleCover.deck_distance_scaled line 96
theorem OAI.PositiveEinsteinFour.MetricDoubleCover.quotient_distance line 100
theorem OAI.PositiveEinsteinFour.MetricDoubleCover.classified_of_round line 110
Source documentation
The round branch is the existing concrete projective quotient theorem, after transporting the deck action through the given sphere identification.
```
theorem classified_of_round (a : ℝ) (ha : 0 < a)
    (hround : ScaledIsometricTo h a roundDistance) : Classified g := by
…
```
Mentions: OAI.PositiveEinsteinFour.Classified
def OAI.PositiveEinsteinFour.HatcherDoubleEulerInput line 131
Source documentation
Hatcher, Chapter 2, Exercise 22, specialized to the actual two-sheeted cover of closed smooth four-manifolds. The finite-CW comparison and Hatcher 3.26(c) identify the Euler characteristic with Topology.eulerFour.
```
def HatcherDoubleEulerInput : Prop :=
…
```
def OAI.PositiveEinsteinFour.HatcherProjectiveBettiInput line 140
Source documentation
The degree-zero through degree-four consequence of Hatcher 3.19 for a manifold identified with CP², using the ordinary isometry/homeomorphism and singular-homology invariance. No curvature classification is assumed.
```
def HatcherProjectiveBettiInput (h : SmoothMetric N) : Prop :=
…
```
theorem OAI.PositiveEinsteinFour.eulerThree_of_projective_betti line 144
theorem OAI.PositiveEinsteinFour.MetricDoubleCover.classified_of_two_models line 151