Algebra.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

Algebraic final steps for positively curved Einstein four-manifolds

These are the linear-algebra and characteristic-number deductions used in Sections 1 and 8 of Positively curved Einstein four-manifolds (2026). The geometric hypotheses needed to apply them are kept explicit.

theorem OAI.PositiveEinsteinFour.linear_involution_eq_neg_id line 21
Source documentation
An involution with no nonzero fixed vector is the antipodal linear map. The proof uses the fixed vector A x + x; orthogonality and a spectral theorem are unnecessary once the sphere action has been linearized.
```
theorem linear_involution_eq_neg_id
    {V : Type*} [AddCommGroup V] [Module ℝ V]
    (A : V →ₗ[ℝ] V)
    (hinvolution : ∀ x, A (A x) = x)
    (hfixed : ∀ x, A x = x → x = 0) :
    A = -LinearMap.id := by
…
```

theorem OAI.PositiveEinsteinFour.linear_involution_eq_neg_id_of_sphere_free line 34

Source documentation

A linear involution acting freely on the unit sphere is antipodal.

theorem linear_involution_eq_neg_id_of_sphere_free
    {V : Type*} [NormedAddCommGroup V] [NormedSpace ℝ V]
    (A : V →ₗ[ℝ] V)
    (hinvolution : ∀ x, A (A x) = x)
    (hfree : ∀ x, ‖x‖ = 1 → A x ≠ x) :
    A = -LinearMap.id := by
…

theorem OAI.PositiveEinsteinFour.remaining_harmonic_count line 50
Source documentation
The characteristic identities, the Weyl gap, and the strict lower volume bound in the exceptional moment-three case force the sole surviving harmonic count to be one. Volume is divided by π²; moment denotes the normalized second moment of the nonzero block. This is Proposition 8.2's numerical step.
```
theorem remaining_harmonic_count
    (n : ℕ) (volume moment : ℝ)
    (hvolume_pos : 0 < volume)
    (hgap : 1 ≤ moment)
    (hmoment_lt : moment < 4)
    (hcharacteristic : volume = (8 - 2 * (n : ℝ)) / 3)
    (hsignature : moment * volume = 2 * (n : ℝ))
    (hvolume_exceptional : moment = 3 → 4 / 3 < volume) :
    n = 1 ∧ moment = 1 ∧ volume = 2 := by
…
```
theorem OAI.PositiveEinsteinFour.normalized_eigenvalue_parameter line 87
Source documentation
The normalized eigenvalues of a trace-free symmetric three-by-three matrix have the parameter range and cubic invariant used in Section 2. Here -r is the least eigenvalue and the squared Hilbert--Schmidt norm is six. This elementary form needs neither eigenvector choices nor a square root.
```
theorem normalized_eigenvalue_parameter
    (r s t : ℝ)
    (htrace : -r + s + t = 0)
    (hnorm : r ^ 2 + s ^ 2 + t ^ 2 = 6)
    (hs : -r ≤ s) (ht : -r ≤ t) :
    1 ≤ r ∧ r ≤ 2 ∧ s * t = r ^ 2 - 3 ∧
      ((-r) ^ 3 + s ^ 3 + t ^ 3) / 6 = (3 * r - r ^ 3) / 2 := by
…
```