WeylMatrixEquation.lean`

12 declarations, 0 contain sorry, 0 declared as axioms

The Weyl matrix equation in an arbitrary orthonormal frame. This derivation uses the actual Bianchi Hessian and curvature commutator, so no eigenframe is differentiated.

def OAI.PositiveEinsteinFour.TraceHessian.traceFreeSquare line 18
def OAI.PositiveEinsteinFour.TraceHessian.weylLaplacian line 21
theorem OAI.PositiveEinsteinFour.TraceHessian.traceFreeSquare_symmetric line 23
theorem OAI.PositiveEinsteinFour.TraceHessian.traceFreeSquare_traceFree line 32
theorem OAI.PositiveEinsteinFour.TraceHessian.weylLaplacian_symmetric line 38
theorem OAI.PositiveEinsteinFour.TraceHessian.weylLaplacian_traceFree line 45
theorem OAI.PositiveEinsteinFour.TraceHessian.matrixAction_square_coordinates line 51
theorem OAI.PositiveEinsteinFour.TraceHessian.matrixAction_traceFreeSquare line 63
Source documentation
The infinitesimal rotation of the trace-free square is computed without a diagonalization hypothesis.
```
theorem matrixAction_traceFreeSquare (M : Mat) (hs : symmetric M) (ht : traceFree M)
    (r : Fin 3) :
    matrixAction r (traceFreeSquare M) = -(∑ s, M r s • matrixAction s M) := by
…
```
Mentions: OAI.PositiveEinsteinFour.TraceHessian.Mat, OAI.PositiveEinsteinFour.TraceHessian.symmetric, OAI.PositiveEinsteinFour.TraceHessian.traceFree, OAI.PositiveEinsteinFour.TraceHessian.matrixAction, OAI.PositiveEinsteinFour.TraceHessian.traceFreeSquare
theorem OAI.PositiveEinsteinFour.TraceHessian.matrixAction_weylLaplacian line 69
def OAI.PositiveEinsteinFour.TraceHessian.bundleCurvatureAction line 83
Source documentation
Curvature acting on the matrix bundle in the Ric=3g normalization. The row M r s is the Weyl block in the same fixed frame.
```
def bundleCurvatureAction (M : Mat) (i j : Fin 4) (N : Mat) : Mat :=
…
```
Mentions: OAI.PositiveEinsteinFour.TraceHessian.Mat
theorem OAI.PositiveEinsteinFour.TraceHessian.traceComponent_weylLaplacian_skew line 87
theorem OAI.PositiveEinsteinFour.TraceHessian.weyl_trace_eq_of_bianchi_commutator line 104
Source documentation
The full matrix Weyl equation is forced by differential Bianchi and the classical curvature commutator. It holds in an arbitrary frame.
```
theorem weyl_trace_eq_of_bianchi_commutator (M : Mat) (hs : symmetric M) (ht : traceFree M)
    (X : Hessian) (hm : ∀ i j, symmetric (X i j) ∧ traceFree (X i j))
    (hb : ∀ i r, divergence X i r = 0)
    (hc : ∀ i j a b, X i j a b - X j i a b = bundleCurvatureAction M i j M a b) :
    hessianTrace X = weylLaplacian M := by
…
```
Mentions: OAI.PositiveEinsteinFour.TraceHessian.Mat, OAI.PositiveEinsteinFour.TraceHessian.symmetric, OAI.PositiveEinsteinFour.TraceHessian.traceFree, OAI.PositiveEinsteinFour.TraceHessian.Hessian, OAI.PositiveEinsteinFour.TraceHessian.bundleCurvatureAction, OAI.PositiveEinsteinFour.TraceHessian.hessianTrace, OAI.PositiveEinsteinFour.TraceHessian.weylLaplacian