CoupledCasimir.lean`

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

The plus spectral polynomial on the actual highest-Hessian space.

def OAI.PositiveEinsteinFour.HighestHessian.rawSlice line 15
def OAI.PositiveEinsteinFour.HighestHessian.outerAction line 18
def OAI.PositiveEinsteinFour.HighestHessian.innerAction line 21
theorem OAI.PositiveEinsteinFour.HighestHessian.outerAction_add line 24
theorem OAI.PositiveEinsteinFour.HighestHessian.innerAction_add line 30
theorem OAI.PositiveEinsteinFour.HighestHessian.outerAction_square line 36
theorem OAI.PositiveEinsteinFour.HighestHessian.innerAction_outerAction line 43
theorem OAI.PositiveEinsteinFour.HighestHessian.totalPlus_inner_outer line 51
theorem OAI.PositiveEinsteinFour.HighestHessian.coupledOperator_outer_inner line 61
theorem OAI.PositiveEinsteinFour.HighestHessian.totalPlus_casimir_split line 87
Source documentation
The total Casimir separates into the two actual tensor factors.
```
theorem totalPlus_casimir_split (X : Hessian) :
    (∑ s : Fin 3, totalPlus s (totalPlus s X)) =
      (-3 : ℝ) • X + (∑ s : Fin 3, innerAction s (innerAction s X)) +
        (2 : ℝ) • coupledOperator X := by
…
```
Mentions: OAI.PositiveEinsteinFour.HighestHessian.totalPlus, OAI.PositiveEinsteinFour.HighestHessian.innerAction, OAI.PositiveEinsteinFour.HighestHessian.coupledOperator
theorem OAI.PositiveEinsteinFour.HighestHessian.innerAction_rawSlice line 102
theorem OAI.PositiveEinsteinFour.HighestHessian.innerAction_casimir_of_condition line 114
Source documentation
The inner Casimir acts on the actual Bianchi slices.
```
theorem innerAction_casimir_of_condition (X : Hessian) (hX : condition X) :
    (∑ s : Fin 3, innerAction s (innerAction s X)) = (-35 : ℝ) • X := by
…
```
Mentions: OAI.PositiveEinsteinFour.HighestHessian.condition, OAI.PositiveEinsteinFour.HighestHessian.innerAction
theorem OAI.PositiveEinsteinFour.HighestHessian.coupledOperator_of_condition line 133
Source documentation
The spectral value is derived from the three already computed Casimirs.
```
theorem coupledOperator_of_condition (X : Hessian) (hX : condition X) :
    coupledOperator X = (-5 : ℝ) • X := by
…
```
Mentions: OAI.PositiveEinsteinFour.HighestHessian.condition, OAI.PositiveEinsteinFour.HighestHessian.coupledOperator
theorem OAI.PositiveEinsteinFour.HighestHessian.plusPolynomial_of_condition line 147
Source documentation
The explicit polynomial fixes the concrete highest-Hessian subspace.
```
theorem plusPolynomial_of_condition (X : Hessian) (hX : condition X) :
    plusPolynomial X = X := by
…
```
Mentions: OAI.PositiveEinsteinFour.HighestHessian.condition, OAI.PositiveEinsteinFour.HighestHessian.plusPolynomial
theorem OAI.PositiveEinsteinFour.HighestHessian.plusPolynomial_pairing line 154
Source documentation
The real polynomial preserves pairings with every highest tensor.
```
theorem plusPolynomial_pairing (L Y : Hessian) (hY : condition Y) :
    hessianPairing (plusPolynomial L) Y = hessianPairing L Y := by
…
```
Mentions: OAI.PositiveEinsteinFour.HighestHessian.condition, OAI.PositiveEinsteinFour.HighestHessian.plusPolynomial
theorem OAI.PositiveEinsteinFour.HighestHessian.highestProjection_plusPolynomial line 171
Source documentation
The constructed highest projection factors through the real polynomial.
```
theorem highestProjection_plusPolynomial (L : Hessian) :
    highestProjection (plusPolynomial L) = highestProjection L := by
…
```
Mentions: OAI.PositiveEinsteinFour.HighestHessian.highestProjection, OAI.PositiveEinsteinFour.HighestHessian.plusPolynomial