HighestAction.lean`

7 declarations, 0 contain sorry, 0 declared as axioms

The plus Casimir energy and curvature bound on actual highest Hessians.

theorem OAI.PositiveEinsteinFour.HighestHessian.totalPlus_casimir line 16
Source documentation
The Casimir identity for four-slot tensors.
```
theorem totalPlus_casimir (c : Fin 21 → ℝ) :
    totalPlus 0 (totalPlus 0 (highest c)) +
      totalPlus 1 (totalPlus 1 (highest c)) +
      totalPlus 2 (totalPlus 2 (highest c)) = (-48 : ℝ) • highest c := by
…
```
Mentions: OAI.PositiveEinsteinFour.HighestHessian.totalPlus, OAI.PositiveEinsteinFour.HighestHessian.highest
theorem OAI.PositiveEinsteinFour.HighestHessian.totalPlus_coordinates line 24
Source documentation
Entrywise identification with the four-slot Kronecker-sum matrix.
```
theorem totalPlus_coordinates (s : Fin 3) (X : Hessian) (p : TensorIndex) :
    tensorCoordinates (totalPlus s X) p =
      ∑ q : TensorIndex, plusKernel s p q * tensorCoordinates X q := by
…
```
Mentions: OAI.PositiveEinsteinFour.HighestHessian.totalPlus
theorem OAI.PositiveEinsteinFour.HighestHessian.totalPlus_skew line 33
Source documentation
The actual total generator is skew-adjoint for the Frobenius pairing.
```
theorem totalPlus_skew (s : Fin 3) (X Y : Hessian) :
    hessianPairing (totalPlus s X) Y = -hessianPairing X (totalPlus s Y) := by
…
```
Mentions: OAI.PositiveEinsteinFour.HighestHessian.totalPlus
theorem OAI.PositiveEinsteinFour.HighestHessian.totalPlus_energy line 42
Source documentation
Exact energy Casimir on the genuine twenty-one-dimensional tensors.
```
theorem totalPlus_energy (c : Fin 21 → ℝ) :
    hessianNormSq (totalPlus 0 (highest c)) +
      hessianNormSq (totalPlus 1 (highest c)) +
      hessianNormSq (totalPlus 2 (highest c)) = 48 * hessianNormSq (highest c) := by
…
```
Mentions: OAI.PositiveEinsteinFour.HighestHessian.totalPlus, OAI.PositiveEinsteinFour.HighestHessian.highest

theorem OAI.PositiveEinsteinFour.HighestHessian.plus_energy_bound line 57

Source documentation

The sharp plus-curvature coefficient follows directly from the energy Casimir and the three lower eigenvalue bounds.

theorem plus_energy_bound (c : Fin 21 → ℝ) (t : Fin 3 → ℝ) (x : ℝ)
    (ht : ∀ s, -x ≤ t s) :
    -(t 0 * hessianNormSq (totalPlus 0 (highest c)) +
      t 1 * hessianNormSq (totalPlus 1 (highest c)) +
      t 2 * hessianNormSq (totalPlus 2 (highest c))) / 60 ≤
      (4 / 5) * x * hessianNormSq (highest c) := by
…

Mentions: OAI.PositiveEinsteinFour.HighestHessian.totalPlus, OAI.PositiveEinsteinFour.HighestHessian.highest

theorem OAI.PositiveEinsteinFour.HighestHessian.totalPlus_energy_of_condition line 75
Source documentation
The energy identity applies to any tensor satisfying the actual local symmetry, trace and differentiated Bianchi conditions.
```
theorem totalPlus_energy_of_condition (X : Hessian) (hX : condition X) :
    hessianNormSq (totalPlus 0 X) + hessianNormSq (totalPlus 1 X) +
      hessianNormSq (totalPlus 2 X) = 48 * hessianNormSq X := by
…
```
Mentions: OAI.PositiveEinsteinFour.HighestHessian.condition, OAI.PositiveEinsteinFour.HighestHessian.totalPlus
theorem OAI.PositiveEinsteinFour.HighestHessian.plus_energy_bound_of_condition line 81