WeylGeometry.lean`

26 declarations, 0 contain sorry, 0 declared as axioms

Concrete orthonormal frames and curvature blocks of the metric in the classification statement, defined from its chart curvature.

abbrev OAI.PositiveEinsteinFour.Geometry.Mat4 line 20
Also declared: ComparatorChallenges/EinsteinFour.lean:107 (same declaration text).
abbrev OAI.PositiveEinsteinFour.Geometry.Mat3 line 21
def OAI.PositiveEinsteinFour.Geometry.chartMetric line 23
Also declared: ComparatorChallenges/EinsteinFour.lean:109 (same declaration text).
def OAI.PositiveEinsteinFour.Geometry.chartRicci line 26
structure OAI.PositiveEinsteinFour.Geometry.OrthonormalFrame line 31
Source documentation
Columns are the coordinates of an orthonormal tangent frame in the same chart as the concrete metric and curvature used by ClassificationOn.
Also declared: ComparatorChallenges/EinsteinFour.lean:112 (same declaration text).
```
structure OrthonormalFrame (g : SmoothMetric M) (c : M) where
…
```
theorem OAI.PositiveEinsteinFour.Geometry.OrthonormalFrame.det_ne_zero line 39
def OAI.PositiveEinsteinFour.Geometry.OrthonormalFrame.map line 46
Source documentation
The actual linear change from frame coordinates to chart coordinates.
Distinct definitions of this name: ComparatorChallenges/EinsteinFour.lean:116 (different declaration text). Qualify references as OAI.PositiveEinsteinFour.Geometry.OrthonormalFrame.map@path.
```
def map : FourSpace →ₗ[ℝ] FourSpace :=
…
```
theorem OAI.PositiveEinsteinFour.Geometry.OrthonormalFrame.map_apply line 50
theorem OAI.PositiveEinsteinFour.Geometry.OrthonormalFrame.map_injective line 53
def OAI.PositiveEinsteinFour.Geometry.OrthonormalFrame.vector line 59
Distinct definitions of this name: ComparatorChallenges/EinsteinFour.lean:121 (different declaration text). Qualify references as OAI.PositiveEinsteinFour.Geometry.OrthonormalFrame.vector@path.
theorem OAI.PositiveEinsteinFour.Geometry.OrthonormalFrame.vector_apply line 61
def OAI.PositiveEinsteinFour.Geometry.OrthonormalFrame.ricci line 64
Source documentation
Pullback of the actual chart Ricci tensor.
```
def ricci : Mat4 := e.matrixᵀ * chartRicci g c * e.matrix
```
Mentions: OAI.PositiveEinsteinFour.Geometry.Mat4, OAI.PositiveEinsteinFour.Geometry.chartRicci
theorem OAI.PositiveEinsteinFour.Geometry.OrthonormalFrame.ricci_eq_three_one line 67
Source documentation
Normalization of Ricci transfers to every orthonormal frame.
```
theorem ricci_eq_three_one
    (hRic : chartRicci g c = (3 : ℝ) • chartMetric g c) :
    e.ricci = (3 : ℝ) • (1 : Mat4) := by
…
```
Mentions: OAI.PositiveEinsteinFour.Geometry.chartRicci, OAI.PositiveEinsteinFour.Geometry.chartMetric, OAI.PositiveEinsteinFour.Geometry.Mat4
theorem OAI.PositiveEinsteinFour.Geometry.OrthonormalFrame.sectional_pos line 75
Source documentation
Positivity in chart coordinates is preserved by the actual invertible frame change. This uses the sectional-curvature predicate in the target.
```
theorem sectional_pos (hsec : HasPositiveSectionalCurvature g)
    (u v : FourSpace) (huv : LinearIndependent ℝ ![u, v]) :
    0 < sectionalNumerator g c (chartAt FourSpace c c) (e.map u) (e.map v) := by
…
```
def OAI.PositiveEinsteinFour.Geometry.frameCurvature line 89
Source documentation
The Riemann tensor evaluated on an actual orthonormal frame. Its slots are <R(e_i,e_j)e_k,e_l>, matching sectionalNumerator.
```
def frameCurvature (g : SmoothMetric M) (c : M) (e : OrthonormalFrame g c)
    (i j k l : Fin 4) : ℝ :=
…
```
Mentions: OAI.PositiveEinsteinFour.Geometry.OrthonormalFrame
theorem OAI.PositiveEinsteinFour.Geometry.frameCurvature_sectional line 95
def OAI.PositiveEinsteinFour.Geometry.oppositeQuaternion line 102
Source documentation
The second quaternion triple is obtained by reversing the first frame axis. This exchanges the two Hodge-star eigenspaces.
```
def oppositeQuaternion (s : Fin 3) (i j : Fin 4) : ℝ :=
…
```
def OAI.PositiveEinsteinFour.Geometry.curvaturePairing line 107
Source documentation
Curvature as a bilinear form on two-form coordinates.
```
def curvaturePairing (g : SmoothMetric M) (c : M) (e : OrthonormalFrame g c)
    (p q : Fin 4 × Fin 4) : ℝ := frameCurvature g c e p.1 p.2 q.2 q.1
```
Mentions: OAI.PositiveEinsteinFour.Geometry.OrthonormalFrame, OAI.PositiveEinsteinFour.Geometry.frameCurvature
def OAI.PositiveEinsteinFour.Geometry.curvatureBlock line 112
Source documentation
The factor 1/8 accounts for antisymmetric coordinate pairs and the 1/sqrt(2) normalization of the quaternionic two-form basis.
```
def curvatureBlock (R : (Fin 4 × Fin 4) → (Fin 4 × Fin 4) → ℝ)
    (Q : Fin 3 → Mat4) : Mat3 := fun s t =>
…
```
Mentions: OAI.PositiveEinsteinFour.Geometry.Mat4, OAI.PositiveEinsteinFour.Geometry.Mat3
def OAI.PositiveEinsteinFour.Geometry.plusWeyl line 117
Source documentation
The self-dual Weyl block in the normalized Ricci=3g convention.
```
def plusWeyl (g : SmoothMetric M) (c : M) (e : OrthonormalFrame g c) : Mat3 :=
…
```
Mentions: OAI.PositiveEinsteinFour.Geometry.OrthonormalFrame, OAI.PositiveEinsteinFour.Geometry.Mat3
def OAI.PositiveEinsteinFour.Geometry.minusWeyl line 121
Source documentation
The anti-self-dual Weyl block in the same concrete frame.
```
def minusWeyl (g : SmoothMetric M) (c : M) (e : OrthonormalFrame g c) : Mat3 :=
…
```
Mentions: OAI.PositiveEinsteinFour.Geometry.OrthonormalFrame, OAI.PositiveEinsteinFour.Geometry.Mat3
def OAI.PositiveEinsteinFour.Geometry.normalizedBlockNorm line 125
Source documentation
The normalized Weyl norm, written without a choice of eigenvectors.
```
def normalizedBlockNorm (T : Mat3) : ℝ :=
…
```
Mentions: OAI.PositiveEinsteinFour.Geometry.Mat3
theorem OAI.PositiveEinsteinFour.Geometry.normalizedBlockNorm_nonneg line 128
theorem OAI.PositiveEinsteinFour.Geometry.normalizedBlockNorm_sq line 131
theorem OAI.PositiveEinsteinFour.Geometry.normalizedBlockNorm_eq_zero_iff line 138
Source documentation
Vanishing of the normalized norm is exactly vanishing of the concrete curvature block.
```
theorem normalizedBlockNorm_eq_zero_iff (T : Mat3) :
    normalizedBlockNorm T = 0 ↔ T = 0 := by
…
```
Mentions: OAI.PositiveEinsteinFour.Geometry.Mat3, OAI.PositiveEinsteinFour.Geometry.normalizedBlockNorm
theorem OAI.PositiveEinsteinFour.Geometry.curvatureBlock_symmetric line 158
Source documentation
Pair symmetry of curvature implies symmetry of its actual block.
```
theorem curvatureBlock_symmetric
    {R : (Fin 4 × Fin 4) → (Fin 4 × Fin 4) → ℝ}
    (hR : ∀ p q, R p q = R q p) (Q : Fin 3 → Mat4) :
    (curvatureBlock R Q)ᵀ = curvatureBlock R Q := by
…
```
Mentions: OAI.PositiveEinsteinFour.Geometry.Mat4, OAI.PositiveEinsteinFour.Geometry.curvatureBlock