RicciGradient.lean`

6 declarations, 0 contain sorry, 0 declared as axioms

The algebraic part of the Ricci-commuted gradient equation, retaining an arbitrary Bianchi test tensor. The raw operator is the sum of the differentiated Weyl equation, Ricci curvature, and bundle curvature.

def OAI.PositiveEinsteinFour.Bianchi.mixedGradient line 16
theorem OAI.PositiveEinsteinFour.Bianchi.mixedGradient_pairing line 19
theorem OAI.PositiveEinsteinFour.Bianchi.sum_mixedGradient line 24
def OAI.PositiveEinsteinFour.Bianchi.ricciGradient line 33
Source documentation
This is the uncompressed right side after applying Ricci commutation and divergence freedom, with Ricci normalized to 3g. Its coefficients are 6 + 3, -12, and the full bundle action -(1+t_s) I_s Σ_s.
```
def ricciGradient (t : Fin 3 → ℝ) (Z : Tensor) : RawGradient :=
…
```
Mentions: OAI.PositiveEinsteinFour.Bianchi.Tensor, OAI.PositiveEinsteinFour.Bianchi.RawGradient
theorem OAI.PositiveEinsteinFour.Bianchi.ricciGradient_pairing line 39
Source documentation
The coefficient 20 follows from bilinear compression of the actual bundle action. No compressed differential equation is assumed.
```
theorem ricciGradient_pairing (t : Fin 3 → ℝ) (ht : ∑ s, t s = 0)
    (Z W : Tensor) (hz : Z.traceFree) (hbz : Z.bianchi)
    (hw : W.traceFree) (hbw : W.bianchi) :
    rawPairing (ricciGradient t Z) W.matrix =
      13 * rawPairing Z.matrix W.matrix -
        20 * rawPairing (rawMatrixCurvature t Z) W.matrix := by
…
```
Mentions: OAI.PositiveEinsteinFour.Bianchi.Tensor, OAI.PositiveEinsteinFour.Bianchi.rawPairing, OAI.PositiveEinsteinFour.Bianchi.ricciGradient, OAI.PositiveEinsteinFour.Bianchi.rawMatrixCurvature
theorem OAI.PositiveEinsteinFour.Bianchi.ricciGradient_compressed_pairing line 58
Source documentation
The bilinear identity is precisely the concrete orthogonal compression used by the squared-gradient and matrix-slot Green formulas.
```
theorem ricciGradient_compressed_pairing (S : Shape) (v : ℝ) (p k l : Vec)
    (W : Tensor) (hw : W.traceFree) (hbw : W.bianchi) :
    rawPairing (ricciGradient (fun s => v * S.s s) (parameters S p k l)) W.matrix =
      rawPairing ((13 : ℝ) • (parameters S p k l).matrix -
        (20 : ℝ) • (curvatureAction S v p k l).matrix) W.matrix := by
…
```
Mentions: OAI.PositiveEinsteinFour.Bianchi.Shape, OAI.PositiveEinsteinFour.Bianchi.Vec, OAI.PositiveEinsteinFour.Bianchi.Tensor, OAI.PositiveEinsteinFour.Bianchi.rawPairing, OAI.PositiveEinsteinFour.Bianchi.ricciGradient, OAI.PositiveEinsteinFour.Bianchi.parameters, OAI.PositiveEinsteinFour.Bianchi.curvatureAction