CurvatureTensors00.lean`

16 declarations, 0 contain sorry, 0 declared as axioms

The axial reduction of the quadratic coupling terms

The exact matrix certificate (21) implies the full three-variable quadratic inequality. The proof multiplies by the positive P0 * v and applies the closed two-by-two determinant criterion, so it also covers the axial endpoint.

theorem OAI.PositiveEinsteinFour.spectral_schur_nonneg line 24

Source documentation

The spectral Schur completion, including σ = 1.

theorem spectral_schur_nonneg
    (v P σ ρ D W p : ℝ)
    (hv : 0 < v) (hP : 0 < P)
    (hσlower : -1 ≤ σ) (hσupper : σ ≤ 1)
    (hcircle : ρ ^ 2 = 1 - σ ^ 2)
    (hA : 0 ≤ P * v * D - (1 + σ) * v ^ 2 * W ^ 2) :
    0 ≤ (1 - σ) * v * P / 3 * p ^ 2 -
      2 * v * ρ / Real.sqrt 3 * p * W + D := by
…

def OAI.PositiveEinsteinFour.lowerBlock line 60
Source documentation
The pure non-axial block in the quadratic part of the plus Weyl estimate.
```
def lowerBlock (v b σ k l : ℝ) : ℝ :=
…
```

theorem OAI.PositiveEinsteinFour.spectral_matrix_as_schur line 65

Source documentation

Polynomial-matrix form (21) is the numerator of the Schur complement.

theorem spectral_matrix_as_schur (v b σ k l : ℝ) (hv : v ≠ 0) :
    A11 v b σ * k ^ 2 + 2 * A12 v b σ * k * l + A22 v b σ * l ^ 2 =
      P0 v b * v * lowerBlock v b σ k l -
        (1 + σ) * v ^ 2 * (Pk v b * k + Pl v b * l) ^ 2 := by
…

Mentions: OAI.PositiveEinsteinFour.lowerBlock

theorem OAI.PositiveEinsteinFour.axial_reduction_nonneg line 76

Source documentation

The loss from moving off the axial spectral shape is nonnegative, for all first-derivative variables. This is the quadratic axial reduction in Section 6. The closed domain and σ = 1 are included.

theorem axial_reduction_nonneg
    {v b σ ρ : ℝ} (hv : 0 < v) (hb : 0 ≤ b) (hsum : v + b ≤ 2)
    (hσlower : -1 ≤ σ) (hσupper : σ ≤ 1) (hcircle : ρ ^ 2 = 1 - σ ^ 2)
    (p k l : ℝ) :
    0 ≤ (1 - σ) * v * P0 v b / 3 * p ^ 2 -
      2 * v * ρ / Real.sqrt 3 * p * (Pk v b * k + Pl v b * l) +
        lowerBlock v b σ k l := by
…

Mentions: OAI.PositiveEinsteinFour.lowerBlock

def OAI.PositiveEinsteinFour.Bianchi.axialLoss line 109
theorem OAI.PositiveEinsteinFour.Bianchi.axialLoss_nonneg line 119
Source documentation
Sum the scalar Schur certificate over the actual tangent coordinates. All inner products retain their signs.
```
theorem axialLoss_nonneg {v b σ ρ : ℝ}
    (hv : 0 < v) (hb : 0 ≤ b) (hsum : v + b ≤ 2)
    (hσlower : -1 ≤ σ) (hσupper : σ ≤ 1)
    (hcircle : ρ ^ 2 = 1 - σ ^ 2) (p k l : Vec) :
    0 ≤ axialLoss v b σ ρ p k l := by
…
```
Mentions: OAI.PositiveEinsteinFour.Bianchi.Vec, OAI.PositiveEinsteinFour.Bianchi.axialLoss
def OAI.PositiveEinsteinFour.Bianchi.blockQuadratic line 138
Source documentation
The plus part of the genuine quadratic integrand before the scalar derivatives of κ and the variance correction are added.
```
def blockQuadratic (S : Shape) (v b τ : ℝ) (p k l : Vec) : ℝ :=
…
```
Mentions: OAI.PositiveEinsteinFour.Bianchi.Shape, OAI.PositiveEinsteinFour.Bianchi.Vec
theorem OAI.PositiveEinsteinFour.Bianchi.blockQuadratic_gap line 148
Source documentation
Exact collection of the gap from the axial value. The only additional term is the nonnegative loss from the opposite block's nonaxial spectrum.
```
theorem blockQuadratic_gap (S : Shape) (v b τ : ℝ) (hv : v ≠ 0) (p k l : Vec) :
    (axialCoefficient v b + 2 * kappa v b / (3 * v)) * ‖p‖ ^ 2 -
        blockQuadratic S v b τ p k l =
      axialLoss v b S.sigma S.rho p k l +
        (51 / 5 : ℝ) * (1 - τ) * b ^ 2 *
          ((parameters S p k l).squaredNorm / 6) := by
…
```
Mentions: OAI.PositiveEinsteinFour.Bianchi.Shape, OAI.PositiveEinsteinFour.Bianchi.Vec, OAI.PositiveEinsteinFour.Bianchi.blockQuadratic, OAI.PositiveEinsteinFour.Bianchi.axialLoss, OAI.PositiveEinsteinFour.Bianchi.parameters
theorem OAI.PositiveEinsteinFour.Bianchi.blockQuadratic_le_axial line 166
Source documentation
Equation (21) bounds the complete plus quadratic contribution by its axial value, including the true Bianchi energy and all tangent pairings.
```
theorem blockQuadratic_le_axial (S : Shape) {v b τ : ℝ}
    (hv : 0 < v) (hb : 0 ≤ b) (hsum : v + b ≤ 2) (hτ : τ ≤ 1)
    (p k l : Vec) :
    blockQuadratic S v b τ p k l ≤
      (axialCoefficient v b + 2 * kappa v b / (3 * v)) * ‖p‖ ^ 2 := by
…
```
Mentions: OAI.PositiveEinsteinFour.Bianchi.Shape, OAI.PositiveEinsteinFour.Bianchi.Vec, OAI.PositiveEinsteinFour.Bianchi.blockQuadratic

theorem OAI.PositiveEinsteinFour.axial_reduction_vectors line 201

Source documentation

Equation (21) controls the complete tangent-vector quadratic form.

theorem axial_reduction_vectors
    {v b σ ρ : ℝ} (hv : 0 < v) (hb : 0 ≤ b) (hsum : v + b ≤ 2)
    (hσlower : -1 ≤ σ) (hσupper : σ ≤ 1) (hcircle : ρ ^ 2 = 1 - σ ^ 2)
    (p k l : Vec) :
    0 ≤ (1 - σ) * v * P0 v b / 3 * ‖p‖ ^ 2 -
      2 * v * ρ / Real.sqrt 3 *
        (Pk v b * inner ℝ p k + Pl v b * inner ℝ p l) +
      (K1 v b σ - 5 * kappa v b / v) * ‖k‖ ^ 2 +
      2 * K12 v b σ * inner ℝ k l +
      (K2 v b σ - kappa v b / v) * ‖l‖ ^ 2 := by
…

def OAI.PositiveEinsteinFour.hessianQuadraticContribution line 232
Source documentation
The complete plus-block quadratic contribution before axial reduction. The opposite cubic invariant is kept as τ.
```
def hessianQuadraticContribution (S : Shape) (v b τ : ℝ) (p k l : Vec) : ℝ :=
…
```
theorem OAI.PositiveEinsteinFour.hessian_quadratic_axial_identity line 240

theorem OAI.PositiveEinsteinFour.hessian_quadratic_axial_bound line 263

Source documentation

The full quadratic contribution is bounded by its axial value, with all three derivative variables still actual tangent vectors.

theorem hessian_quadratic_axial_bound (S : Shape) {v b τ : ℝ}
    (hv : 0 < v) (hb : 0 ≤ b) (hsum : v + b ≤ 2) (hτ : τ ≤ 1)
    (p k l : Vec) :
    hessianQuadraticContribution S v b τ p k l ≤
      (axialCoefficient v b + 2 * kappa v b / (3 * v)) * ‖p‖ ^ 2 := by
…

Mentions: OAI.PositiveEinsteinFour.hessianQuadraticContribution

def OAI.PositiveEinsteinFour.Bianchi.coupledQuadratic line 303
Source documentation
Both block contributions, the differentiated scalar multipliers, and the derivative term of the variance correction.
```
def coupledQuadratic (S T : Shape) (v b : ℝ) (p k l q kb lb : Vec) : ℝ :=
…
```
Mentions: OAI.PositiveEinsteinFour.Bianchi.Shape, OAI.PositiveEinsteinFour.Bianchi.Vec
theorem OAI.PositiveEinsteinFour.Bianchi.coupledQuadratic_le_matrix line 309
theorem OAI.PositiveEinsteinFour.Bianchi.coupledQuadratic_bound line 339
Source documentation
The full quadratic piece of the coupled integrand satisfies the target bound, with the original fixed block labels and tangent pairing.
```
theorem coupledQuadratic_bound (S T : Shape) {v b : ℝ}
    (hv : 0 < v) (hb : 0 < b) (hsum : v + b ≤ 2) (p k l q kb lb : Vec) :
    coupledQuadratic S T v b p k l q kb lb ≤
      2 * theta v b * (normWeight v * ‖p‖ ^ 2 + normWeight b * ‖q‖ ^ 2) := by
…
```
Mentions: OAI.PositiveEinsteinFour.Bianchi.Shape, OAI.PositiveEinsteinFour.Bianchi.Vec, OAI.PositiveEinsteinFour.Bianchi.coupledQuadratic, OAI.PositiveEinsteinFour.normWeight