WeylLaplacian.lean`

9 declarations, 0 contain sorry, 0 declared as axioms

The scalar contraction of the commuted Weyl equation. The compression coefficient is derived on the actual Bianchi tensor, not taken from a representation label or assumed as the manuscript's differential equation.

def OAI.PositiveEinsteinFour.Bianchi.totalGradientTensor line 17
theorem OAI.PositiveEinsteinFour.Bianchi.totalGradientTensor_coordinates line 21
theorem OAI.PositiveEinsteinFour.Bianchi.totalGradientTensor_matrix line 33
theorem OAI.PositiveEinsteinFour.Bianchi.totalGradientTensor_bianchi line 39
def OAI.PositiveEinsteinFour.Bianchi.mixedCouplingForm line 45
def OAI.PositiveEinsteinFour.Bianchi.diagonalGradientForm line 48
theorem OAI.PositiveEinsteinFour.Bianchi.mixedCouplingForm_eq line 53
Source documentation
The single-generator compression follows from the actual Bianchi projector and the preserved gradient tensor.
```
theorem mixedCouplingForm_eq (s : Fin 3) (Z : Tensor)
    (hz : Z.traceFree) (hb : Z.bianchi) :
    mixedCouplingForm s Z = Z.squaredNorm -
      (1 / 5 : ℝ) * (∑ a, ∑ b, ‖rawGradientGenerator s Z.matrix a b‖ ^ 2) := by
…
```
Mentions: OAI.PositiveEinsteinFour.Bianchi.Tensor, OAI.PositiveEinsteinFour.Bianchi.mixedCouplingForm, OAI.PositiveEinsteinFour.Bianchi.rawGradientGenerator
theorem OAI.PositiveEinsteinFour.Bianchi.weighted_mixedCouplingForm line 75
Source documentation
Exact weighted mixed compression with no spectral-theory premise.
```
theorem weighted_mixedCouplingForm (t : Fin 3 → ℝ) (ht : ∑ s, t s = 0)
    (Z : Tensor) (hz : Z.traceFree) (hb : Z.bianchi) :
    (∑ s, t s * mixedCouplingForm s Z) = 8 * diagonalGradientForm t Z := by
…
```
Mentions: OAI.PositiveEinsteinFour.Bianchi.Tensor, OAI.PositiveEinsteinFour.Bianchi.mixedCouplingForm, OAI.PositiveEinsteinFour.Bianchi.diagonalGradientForm
theorem OAI.PositiveEinsteinFour.Bianchi.commuted_laplacian_contraction line 97
Source documentation
Contract the raw Ricci-commuted equation against the Bianchi gradient. The four scalar terms are respectively the derivative of the Weyl equation, Ricci, the constant coupling, and the curvature-dependent coupling.
```
theorem commuted_laplacian_contraction (t : Fin 3 → ℝ) (ht : ∑ s, t s = 0)
    (Z : Tensor) (hz : Z.traceFree) (hb : Z.bianchi) (L : ℝ)
    (hraw : L = 6 * Z.squaredNorm - 12 * diagonalGradientForm t Z +
      3 * Z.squaredNorm + 4 * Z.squaredNorm - ∑ s, t s * mixedCouplingForm s Z) :
    L = 13 * Z.squaredNorm - 20 * diagonalGradientForm t Z := by
…
```
Mentions: OAI.PositiveEinsteinFour.Bianchi.Tensor, OAI.PositiveEinsteinFour.Bianchi.diagonalGradientForm, OAI.PositiveEinsteinFour.Bianchi.mixedCouplingForm