QuarticClosed.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

The quartic estimate at vanishing Weyl blocks, with totalized division.

def OAI.PositiveEinsteinFour.QuarticClosed.axisEnergy line 15
Source documentation
The surviving part of (19) when the first block and its energy vanish. This expression has no division by the norm of that vanished block.
```
def axisEnergy (x b τ χ d f : ℝ) : ℝ :=
…
```
theorem OAI.PositiveEinsteinFour.QuarticClosed.quarticEnergy_axis line 25
Source documentation
Cancellation at a vanished first block is exact under Lean's totalized field division, including at zero norm.
```
theorem quarticEnergy_axis (x b τ χ d f g H : ℝ) :
    quarticEnergy x b 0 ((5 / 3) * d) g (projectionCoefficient b x τ χ)
      H (defectCoefficient b x) 0 f = axisEnergy x b τ χ d f := by
…
```
Mentions: OAI.PositiveEinsteinFour.QuarticClosed.axisEnergy
theorem OAI.PositiveEinsteinFour.QuarticClosed.quartic_axis_bound line 35
Source documentation
The quartic bound on a single surviving block. A continuous approach through positive two-block data supplies the endpoint, including maximal spectral curvature. No division by the vanished block is used.
```
theorem quartic_axis_bound
    {b s τ χ d f : ℝ} (hb : 0 < b) (hs : 1 ≤ s) (hs2 : s ≤ 2)
    (hbs : b * s ≤ 2) (hτ : τ = (3 * s - s ^ 3) / 2)
    (hχ : χ ^ 2 = 1 - τ ^ 2) (hd : 0 ≤ d) (hf : (5 / 3) * d ≤ f) :
    axisEnergy 0 b τ χ d f ≤ -(2 / 5 : ℝ) * d * (d / b) := by
…
```
Mentions: OAI.PositiveEinsteinFour.QuarticClosed.axisEnergy

theorem OAI.PositiveEinsteinFour.QuarticClosed.quartic_energy_bound_closed line 73

Source documentation

The quartic estimate on the closed spectral domain. The two zero-set hypotheses encode exactly that a vanished curvature block has zero derivative energy there; they remove every singular divided term by its zero numerator.

theorem quartic_energy_bound_closed
    {v b r s σ τ ρ χ a d e f : ℝ}
    (hv : 0 ≤ v) (hb : 0 ≤ b)
    (hr : 1 ≤ r) (hr2 : r ≤ 2) (hs : 1 ≤ s) (hs2 : s ≤ 2)
    (hspectral : v * r + b * s ≤ 2)
    (hσ : σ = (3 * r - r ^ 3) / 2) (hρ : ρ ^ 2 = 1 - σ ^ 2)
    (hτ : τ = (3 * s - s ^ 3) / 2) (hχ : χ ^ 2 = 1 - τ ^ 2)
    (ha : 0 ≤ a) (hd : 0 ≤ d) (he : (5 / 3) * a ≤ e) (hf : (5 / 3) * d ≤ f)
    (hve : v = 0 → e = 0) (hbf : b = 0 → f = 0) :
    quarticEnergy v b ((5 / 3) * a) ((5 / 3) * d)
      (projectionCoefficient v (b * s) σ ρ) (projectionCoefficient b (v * r) τ χ)
      (defectCoefficient v (b * s)) (defectCoefficient b (v * r)) e f ≤
…