TraceCurvature.lean`

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

The curvature commutator retained by the complete trace component.

def OAI.PositiveEinsteinFour.TraceHessian.diagonalSquareBlock line 14
Source documentation
The actual trace-free square of a diagonal Weyl block.
```
def diagonalSquareBlock (t : Fin 3 → ℝ) : Mat :=
…
```
Mentions: OAI.PositiveEinsteinFour.TraceHessian.Mat
def OAI.PositiveEinsteinFour.TraceHessian.diagonalLaplacianBlock line 18
Source documentation
The normalized weak Weyl equation in a diagonal frame.
```
def diagonalLaplacianBlock (t : Fin 3 → ℝ) : Mat :=
…
```
Mentions: OAI.PositiveEinsteinFour.TraceHessian.Mat
theorem OAI.PositiveEinsteinFour.TraceHessian.matrixAction_diagonalSquare line 22
Source documentation
The scalar trace term disappears from the infinitesimal matrix action.
```
theorem matrixAction_diagonalSquare (t : Fin 3 → ℝ) (ht : ∑ s, t s = 0)
    (s : Fin 3) :
    matrixAction s (diagonalSquareBlock t) =
      (-t s) • matrixAction s (Matrix.diagonal t) := by
…
```
Mentions: OAI.PositiveEinsteinFour.TraceHessian.matrixAction, OAI.PositiveEinsteinFour.TraceHessian.diagonalSquareBlock
theorem OAI.PositiveEinsteinFour.TraceHessian.matrixAction_diagonalLaplacian line 38
theorem OAI.PositiveEinsteinFour.TraceHessian.traceComponent_skew line 55
Source documentation
The trace component retains its complete skew derivative part.
```
theorem traceComponent_skew (M : Mat) (i j : Fin 4) (a b : Fin 3) :
    traceComponent M i j a b - traceComponent M j i a b =
      (1 / 12) * ∑ s, quaternionMatrix s i j * matrixAction s M a b := by
…
```
Mentions: OAI.PositiveEinsteinFour.TraceHessian.Mat, OAI.PositiveEinsteinFour.TraceHessian.traceComponent, OAI.PositiveEinsteinFour.TraceHessian.quaternionMatrix, OAI.PositiveEinsteinFour.TraceHessian.matrixAction
theorem OAI.PositiveEinsteinFour.TraceHessian.traceComponent_diagonalLaplacian_skew line 72
Source documentation
The trace component's skew part is exactly the Einstein curvature commutator once the weak Weyl equation supplies its trace.
```
theorem traceComponent_diagonalLaplacian_skew (t : Fin 3 → ℝ)
    (ht : ∑ s, t s = 0) (i j : Fin 4) (a b : Fin 3) :
    traceComponent (diagonalLaplacianBlock t) i j a b -
      traceComponent (diagonalLaplacianBlock t) j i a b =
      (1 / 2) * ∑ s, (1 + t s) * quaternionMatrix s i j *
        matrixAction s (Matrix.diagonal t) a b := by
…
```
Mentions: OAI.PositiveEinsteinFour.TraceHessian.traceComponent, OAI.PositiveEinsteinFour.TraceHessian.diagonalLaplacianBlock, OAI.PositiveEinsteinFour.TraceHessian.quaternionMatrix, OAI.PositiveEinsteinFour.TraceHessian.matrixAction
theorem OAI.PositiveEinsteinFour.TraceHessian.trace_subtracted_symmetric line 90
Source documentation
Subtracting the prescribed trace component removes the actual curvature commutator; derivative symmetry is a consequence, not an extra type premise.
```
theorem trace_subtracted_symmetric (X : Hessian) (t : Fin 3 → ℝ)
    (ht : ∑ s, t s = 0)
    (hcomm : ∀ i j a b, X i j a b - X j i a b =
      (1 / 2) * ∑ s, (1 + t s) * quaternionMatrix s i j *
        matrixAction s (Matrix.diagonal t) a b) :
    ∀ i j, (X - traceComponent (diagonalLaplacianBlock t)) i j =
      (X - traceComponent (diagonalLaplacianBlock t)) j i := by
…
```
Mentions: OAI.PositiveEinsteinFour.TraceHessian.Hessian, OAI.PositiveEinsteinFour.TraceHessian.quaternionMatrix, OAI.PositiveEinsteinFour.TraceHessian.matrixAction, OAI.PositiveEinsteinFour.TraceHessian.traceComponent, OAI.PositiveEinsteinFour.TraceHessian.diagonalLaplacianBlock