CurvatureContraction.lean`

22 declarations, 0 contain sorry, 0 declared as axioms

Quaternion contractions in the derivative-slot Green formula.

def OAI.PositiveEinsteinFour.CurvatureContraction.blockCoefficient line 16
Source documentation
Curvature coefficients with the final two slots in covector order.
```
def blockCoefficient (Q : Fin 3 → Geometry.Mat4) (t : Fin 3 → ℝ)
    (i k j l : Fin 4) : ℝ :=
…
```
Mentions: OAI.PositiveEinsteinFour.Geometry.Mat4
def OAI.PositiveEinsteinFour.CurvatureContraction.plusCoefficient line 20
def OAI.PositiveEinsteinFour.CurvatureContraction.minusCoefficient line 22
def OAI.PositiveEinsteinFour.CurvatureContraction.einsteinCoefficient line 24
theorem OAI.PositiveEinsteinFour.CurvatureContraction.einsteinCoefficient_eq_tensor line 30
Source documentation
These coefficients are the actual Einstein curvature decomposition, with the last two entries reversed to act on a covector slot.
```
theorem einsteinCoefficient_eq_tensor (t u : Fin 3 → ℝ) (i k j l : Fin 4) :
    einsteinCoefficient t u i k j l =
      einsteinCurvatureTensor (Matrix.diagonal t) (Matrix.diagonal u) i k l j := by
…
```
Mentions: OAI.PositiveEinsteinFour.CurvatureContraction.einsteinCoefficient
theorem OAI.PositiveEinsteinFour.CurvatureContraction.plus_twoForm_pairing line 43
Source documentation
Orthogonality includes the normalization of the curvature two-forms.
```
theorem plus_twoForm_pairing (s r : Fin 3) :
    (∑ i, ∑ k, quaternionMatrix s i k * quaternionMatrix r i k) =
      if s = r then (4 : ℝ) else 0 := by
…
```
theorem OAI.PositiveEinsteinFour.CurvatureContraction.opposite_twoForm_pairing line 49
theorem OAI.PositiveEinsteinFour.CurvatureContraction.mixed_twoForm_pairing line 55
theorem OAI.PositiveEinsteinFour.CurvatureContraction.block_pairing line 61
theorem OAI.PositiveEinsteinFour.CurvatureContraction.plus_block_pairing line 110
Source documentation
Contracting two self-dual curvature blocks retains the product of their three eigenvalues, with no missing two-form normalization.
```
theorem plus_block_pairing (a b : Fin 3 → ℝ) (j l h n : Fin 4) :
    (∑ i, ∑ k, plusCoefficient a i k j l * plusCoefficient b i k h n) =
      ∑ s, a s * b s * quaternionMatrix s j l * quaternionMatrix s h n := by
…
```
Mentions: OAI.PositiveEinsteinFour.CurvatureContraction.plusCoefficient
theorem OAI.PositiveEinsteinFour.CurvatureContraction.mixed_block_pairing line 123
Source documentation
The mixed block contraction is zero before pairing against any tensor.
```
theorem mixed_block_pairing (a b : Fin 3 → ℝ) (j l h n : Fin 4) :
    (∑ i, ∑ k, plusCoefficient a i k j l * minusCoefficient b i k h n) = 0 := by
…
```
Mentions: OAI.PositiveEinsteinFour.CurvatureContraction.plusCoefficient, OAI.PositiveEinsteinFour.CurvatureContraction.minusCoefficient
theorem OAI.PositiveEinsteinFour.CurvatureContraction.block_oneForm_pairing line 129
theorem OAI.PositiveEinsteinFour.CurvatureContraction.plus_oneForm_pairing line 153
Source documentation
The matrix-slot curvature contraction retains precisely the matching self-dual generator.
```
theorem plus_oneForm_pairing (a : Fin 3 → ℝ) (s : Fin 3) (j l : Fin 4) :
    (∑ i, ∑ k, plusCoefficient a i k j l * quaternionMatrix s i k) =
      2 * a s * quaternionMatrix s j l := by
…
```
Mentions: OAI.PositiveEinsteinFour.CurvatureContraction.plusCoefficient
theorem OAI.PositiveEinsteinFour.CurvatureContraction.minus_oneForm_pairing line 164
Source documentation
The anti-self-dual curvature has no matrix-slot action on a plus Weyl block: the two-form contraction vanishes before any Bianchi constraint.
```
theorem minus_oneForm_pairing (a : Fin 3 → ℝ) (s : Fin 3) (j l : Fin 4) :
    (∑ i, ∑ k, minusCoefficient a i k j l * quaternionMatrix s i k) = 0 := by
…
```
Mentions: OAI.PositiveEinsteinFour.CurvatureContraction.minusCoefficient
theorem OAI.PositiveEinsteinFour.CurvatureContraction.opposite_column_pairing line 172
theorem OAI.PositiveEinsteinFour.CurvatureContraction.minus_block_pairing line 179
theorem OAI.PositiveEinsteinFour.CurvatureContraction.minus_plus_block_pairing line 191
theorem OAI.PositiveEinsteinFour.CurvatureContraction.quaternion_column_pairing line 202
theorem OAI.PositiveEinsteinFour.CurvatureContraction.plus_ricci_contraction line 211
Source documentation
The derivative-slot Ricci contraction contributes 3*v^2 when sum t_s^2 = 6*v^2.
```
theorem plus_ricci_contraction (t u : Fin 3 → ℝ) (ht : ∑ s, t s = 0)
    (l h : Fin 4) :
    (1 / 2 : ℝ) * (∑ j, ∑ i, ∑ k,
      plusCoefficient t i k j l * einsteinCoefficient t u i k j h) =
        ((∑ s, t s ^ 2) / 2) * (if l = h then 1 else 0) := by
…
```
Mentions: OAI.PositiveEinsteinFour.CurvatureContraction.plusCoefficient, OAI.PositiveEinsteinFour.CurvatureContraction.einsteinCoefficient
theorem OAI.PositiveEinsteinFour.CurvatureContraction.minus_ricci_contraction line 235
Source documentation
The anti-self-dual block has the same derivative-slot Ricci term.
```
theorem minus_ricci_contraction (t u : Fin 3 → ℝ) (hu : ∑ s, u s = 0)
    (l h : Fin 4) :
    (1 / 2 : ℝ) * (∑ j, ∑ i, ∑ k,
      minusCoefficient u i k j l * einsteinCoefficient t u i k j h) =
        ((∑ s, u s ^ 2) / 2) * (if l = h then 1 else 0) := by
…
```
Mentions: OAI.PositiveEinsteinFour.CurvatureContraction.minusCoefficient, OAI.PositiveEinsteinFour.CurvatureContraction.einsteinCoefficient
theorem OAI.PositiveEinsteinFour.CurvatureContraction.sum_mixedCouplingForm line 259
Source documentation
Total Bianchi coupling, used for the scalar part of the squared block.
```
theorem sum_mixedCouplingForm (Z : Tensor) (hb : Z.bianchi) :
    (∑ s, mixedCouplingForm s Z) = -4 * Z.squaredNorm := by
…
```

theorem OAI.PositiveEinsteinFour.CurvatureContraction.plus_commutator_scalar line 274

Source documentation

The matrix-slot part of the commutator plus its derivative-slot Ricci part gives exactly the polynomial in equation (11).

theorem plus_commutator_scalar (t : Fin 3 → ℝ) (ht : ∑ s, t s = 0)
    (Z : Tensor) (hz : Z.traceFree) (hb : Z.bianchi) :
    ((∑ s, t s ^ 2) / 2) * Z.squaredNorm -
      (1 / 2 : ℝ) * (∑ s, t s * (1 + t s) * mixedCouplingForm s Z) =
        (7 / 6 : ℝ) * (∑ s, t s ^ 2) * Z.squaredNorm -
          4 * diagonalGradientForm t Z -
          4 * diagonalGradientForm (fun s => t s ^ 2 - (∑ r, t r ^ 2) / 3) Z := by
…