ActualModelIdentification.lean`

5 declarations, 0 contain sorry, 0 declared as axioms

Actual half-conformally-flat model identification. All analytic, index, injectivity, and metric-model inputs are supplied by proved geometry.

theorem OAI.PositiveEinsteinFour.Geometry.actual_halfFlat_positive_harmonic_dimension_one line 18
theorem OAI.PositiveEinsteinFour.Geometry.actual_halfFlat_models line 26
theorem OAI.PositiveEinsteinFour.Geometry.actual_derdzinski_hitchin line 40
theorem OAI.PositiveEinsteinFour.orientedClassification line 63
Source documentation
Every connected closed oriented positively curved Einstein four-manifold is, up to positive scaling and isometry, the round S4 or Fubini–Study CP2.
Distinct definitions of this name: ComparatorChallenges/EinsteinFour.lean:190 (same statement text; different proof or body). Qualify references as OAI.PositiveEinsteinFour.orientedClassification@path.
```
theorem orientedClassification (X : ClosedOrientedMetricFour.{u})
    (hEinstein : IsEinstein X.metric) (hpositive : HasPositiveSectionalCurvature X.metric) :
    ∃ a : ℝ, 0 < a ∧ (ScaledIsometricTo X.metric a roundDistance ∨
      ScaledIsometricTo X.metric a fubiniStudyDistance) := by
…
```
theorem OAI.PositiveEinsteinFour.classificationOn line 78
Source documentation
Every closed connected positively curved Einstein four-manifold is, up to positive scaling and isometry, standard S4, CP2, or RP4.
Distinct definitions of this name: ComparatorChallenges/EinsteinFour.lean:202 (same statement text; different proof or body). Qualify references as OAI.PositiveEinsteinFour.classificationOn@path.
```
theorem classificationOn : ClassificationOn M := by
…
```
Mentions: OAI.PositiveEinsteinFour.ClassificationOn