HessianTraceEquation.lean`

5 declarations, 0 contain sorry, 0 declared as axioms

Derive the Weyl Hessian trace from Bianchi and the curvature commutator. This removes a separate tensor Laplacian premise from the local weighted square. All contractions use the same concrete quaternion coordinates.

theorem OAI.PositiveEinsteinFour.HighestHessian.rotation_innerSlice_component line 18
theorem OAI.PositiveEinsteinFour.HighestHessian.coupling_innerSlice_component line 25
theorem OAI.PositiveEinsteinFour.HighestHessian.symmetric_bianchi_trace_zero line 37
Source documentation
A derivative-symmetric Bianchi Hessian has zero trace.
```
theorem symmetric_bianchi_trace_zero (X : Hessian)
    (hderiv : ∀ i j, X i j = X j i)
    (hs : ∀ i j, symmetric (X i j))
    (hb : ∀ i r, divergence X i r = 0) : hessianTrace X = 0 := by
…
```
Mentions: OAI.PositiveEinsteinFour.HighestHessian.divergence

theorem OAI.PositiveEinsteinFour.HighestHessian.trace_eq_of_bianchi_commutator line 71

Source documentation

The normalized Weyl trace equation is a consequence of the local curvature commutator and differential Bianchi identity.

theorem trace_eq_of_bianchi_commutator (X : Hessian) (t : Fin 3 → ℝ)
    (ht : ∑ s, t s = 0)
    (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 =
      (1 / 2) * ∑ s, (1 + t s) * quaternionMatrix s i j *
        matrixAction s (Matrix.diagonal t) a b) :
    hessianTrace X = diagonalLaplacianBlock t := by
…

Mentions: OAI.PositiveEinsteinFour.HighestHessian.divergence

theorem OAI.PositiveEinsteinFour.HighestHessian.local_weighted_hessian_square_of_bianchi_commutator line 107

Source documentation

The local weighted square needs no independent Laplacian equation.

theorem local_weighted_hessian_square_of_bianchi_commutator
    (X : Hessian) (t u : Fin 3 → ℝ) (a : Vec) (Z : Tensor)
    (ht : ∑ s, t s = 0)
    (hmatrix : ∀ i j, symmetric (X i j) ∧ traceFree (X i j))
    (hbianchi : ∀ i r, divergence X i r = 0)
    (hcomm : ∀ i j b c, X i j b c - X j i b c =
      (1 / 2) * ∑ s, (1 + t s) * quaternionMatrix s i j *
        matrixAction s (Matrix.diagonal t) b c)
    (x y m : ℝ) (hm : 0 < m)
    (htx : ∀ s, -x ≤ t s) (huy : ∀ s, -y ≤ u s) (hxy : x + y ≤ 2) :
    0 ≤ (m / 6) * curvaturePairing t u (hessianRemainder X t) (hessianRemainder X t) +
      curvaturePairing t u (hessianRemainder X t) (weightTensor a Z) / 6 +
…

Mentions: OAI.PositiveEinsteinFour.HighestHessian.divergence, OAI.PositiveEinsteinFour.HighestHessian.curvaturePairing, OAI.PositiveEinsteinFour.HighestHessian.hessianRemainder, OAI.PositiveEinsteinFour.HighestHessian.weightTensor