BianchiCubic.lean`

6 declarations, 0 contain sorry, 0 declared as axioms

The sharp cubic contraction in a normalized diagonal frame

The contraction is defined from the actual symmetric matrix of four-vectors. The displayed diagonal-frame hypothesis is the pointwise spectral-frame condition used in the curvature calculation, and is not a differential-geometric input.

def OAI.PositiveEinsteinFour.Bianchi.normalizedCurvatureForm line 19
theorem OAI.PositiveEinsteinFour.Bianchi.distinguished_component_bound line 25
Source documentation
The distinguished tangent component loses one fifth of its energy in this quadratic contraction. The other components retain the full bound.
```
theorem distinguished_component_bound (S : Shape) (a p k l : Vec) (ν : ℝ)
    (ha : ‖a‖ = 1) (hap : inner ℝ a p = ν) (hak : inner ℝ a k = 0) :
    |normalizedCurvatureForm S p k l| ≤
      (5 / 3) * ‖p‖ ^ 2 + 5 * ‖k‖ ^ 2 + ‖l‖ ^ 2 - ν ^ 2 / 3 := by
…
```
Mentions: OAI.PositiveEinsteinFour.Bianchi.Shape, OAI.PositiveEinsteinFour.Bianchi.Vec, OAI.PositiveEinsteinFour.Bianchi.normalizedCurvatureForm
def OAI.PositiveEinsteinFour.Bianchi.cubicContraction line 61
Source documentation
The literal matrix contraction tr(Z_a Σ_j Z_j²)/6. Each inner product contracts the derivative (four-vector) index.
```
def cubicContraction (a : Vec) (T : Tensor) : ℝ :=
…
```
Mentions: OAI.PositiveEinsteinFour.Bianchi.Vec, OAI.PositiveEinsteinFour.Bianchi.Tensor
theorem OAI.PositiveEinsteinFour.Bianchi.cubicContraction_diagonal line 67
Source documentation
In the diagonalizing frame for Z_a, the cubic contraction is the normalized matrix-slot quadratic contraction times its scale.
```
theorem cubicContraction_diagonal (S : Shape) (a : Vec) (T : Tensor) (ν : ℝ)
    (hdiag : ∀ i j, inner ℝ a (T.matrix i j) = if i = j then ν * S.s i else 0) :
    cubicContraction a T = ν * curvatureContraction S 1 T := by
…
```
Mentions: OAI.PositiveEinsteinFour.Bianchi.Shape, OAI.PositiveEinsteinFour.Bianchi.Vec, OAI.PositiveEinsteinFour.Bianchi.Tensor, OAI.PositiveEinsteinFour.Bianchi.cubicContraction, OAI.PositiveEinsteinFour.Bianchi.curvatureContraction
theorem OAI.PositiveEinsteinFour.Bianchi.diagonal_parameter_components line 92
Source documentation
The diagonal-frame condition determines the radial and orthogonal components along the chosen tangent direction.
```
theorem diagonal_parameter_components (S : Shape) (a p k l : Vec) (ν : ℝ)
    (hdiag : ∀ i j, inner ℝ a ((parameters S p k l).matrix i j) =
      if i = j then ν * S.s i else 0) :
    inner ℝ a p = ν ∧ inner ℝ a k = 0 := by
…
```
Mentions: OAI.PositiveEinsteinFour.Bianchi.Shape, OAI.PositiveEinsteinFour.Bianchi.Vec, OAI.PositiveEinsteinFour.Bianchi.parameters

theorem OAI.PositiveEinsteinFour.Bianchi.cubicContraction_sharp_diagonal line 123

Source documentation

The sharp constant in (13), proved from the actual tensor contraction in any normalized diagonal frame for the distinguished derivative.

theorem cubicContraction_sharp_diagonal (S : Shape) (a p k l : Vec) {ν : ℝ}
    (ha : ‖a‖ = 1) (hν : 0 ≤ ν)
    (hdiag : ∀ i j, inner ℝ a ((parameters S p k l).matrix i j) =
      if i = j then ν * S.s i else 0) :
    |cubicContraction a (parameters S p k l)| ≤
      (4 / 5) * Real.sqrt (3 / 5) * ((parameters S p k l).squaredNorm / 6) *
        Real.sqrt ((parameters S p k l).squaredNorm / 6) := by
…

Mentions: OAI.PositiveEinsteinFour.Bianchi.Shape, OAI.PositiveEinsteinFour.Bianchi.Vec, OAI.PositiveEinsteinFour.Bianchi.parameters, OAI.PositiveEinsteinFour.Bianchi.cubicContraction