Coupling.lean`

24 declarations, 0 contain sorry, 0 declared as axioms

Algebra and integration in the one-block vanishing argument

The scalar one-block vanishing argument in Section 8 of Positively curved Einstein four-manifolds (23 September 2026).

def OAI.PositiveEinsteinFour.couplingCoefficient line 19
Source documentation
The coefficient c in the paper's equation (15).
```
def couplingCoefficient (v b : ℝ) : ℝ := 2 / 5 - 3 / 10 * v * b
```
theorem OAI.PositiveEinsteinFour.couplingCoefficient_lower line 21
def OAI.PositiveEinsteinFour.normWeight line 30
Source documentation
The rational weight R_v in equation (15).
```
def normWeight (v : ℝ) : ℝ := 4 * (1 + v) / (1 + 6 * v + v ^ 2)
```
theorem OAI.PositiveEinsteinFour.weight_denominator_pos line 32
theorem OAI.PositiveEinsteinFour.normWeight_nonneg line 35
theorem OAI.PositiveEinsteinFour.weight_defect_identity line 40
Source documentation
The fourth power identity supplies the sharp weight comparison.
```
theorem weight_defect_identity (z : ℝ) :
    1 + 6 * z ^ 2 + (z ^ 2) ^ 2 - 4 * z * (1 + z ^ 2) = (z - 1) ^ 4 := by
…
```
theorem OAI.PositiveEinsteinFour.normWeight_mul_sqrt_le line 44
theorem OAI.PositiveEinsteinFour.normWeight_mul_sqrt_lt line 56
theorem OAI.PositiveEinsteinFour.normWeight_le_inv_sqrt line 73
theorem OAI.PositiveEinsteinFour.normWeight_lt_inv_sqrt line 78
theorem OAI.PositiveEinsteinFour.weighted_square_le line 84
Source documentation
Weighted two-term Cauchy--Schwarz, without any square-root denominators.
```
theorem weighted_square_le {a b s t : ℝ} (ha : 0 ≤ a) (hb : 0 ≤ b) :
    (s * a + t * b) ^ 2 ≤ (a + b) * (s ^ 2 * a + t ^ 2 * b) := by
…
```
theorem OAI.PositiveEinsteinFour.inv_sqrt_sq line 88

theorem OAI.PositiveEinsteinFour.radial_cost_bound line 94

Source documentation

Two-term Cauchy--Schwarz with the zero-denominator convention used in the paper. The energies p and q stand for squared gradient norms.

theorem radial_cost_bound {v b p q : ℝ}
    (hv : 0 ≤ v) (hb : 0 ≤ b) (hp : 0 ≤ p) (hq : 0 ≤ q)
    (hpzero : v = 0 → p = 0) (hqzero : b = 0 → q = 0) :
    (normWeight v * p + normWeight b * q) ^ 2 ≤
      (p + q) * (p / v + q / b) := by
…

Mentions: OAI.PositiveEinsteinFour.normWeight

theorem OAI.PositiveEinsteinFour.radial_cost_strict_of_pos line 121
Source documentation
Away from the norm-one level set, an active gradient makes the radial cost comparison strict. Level-set gradient vanishing is supplied separately by the geometric application.
```
theorem radial_cost_strict_of_pos {v b p q : ℝ}
    (hv : 0 < v) (hb : 0 < b) (hp : 0 ≤ p) (hq : 0 ≤ q)
    (hactive : (0 < p ∧ v ≠ 1) ∨ (0 < q ∧ b ≠ 1)) :
    (normWeight v * p + normWeight b * q) ^ 2 <
      (p + q) * (p / v + q / b) := by
…
```
Mentions: OAI.PositiveEinsteinFour.normWeight
theorem OAI.PositiveEinsteinFour.radial_cost_strict line 145
theorem OAI.PositiveEinsteinFour.not_two_constant_blocks line 180
Source documentation
The final numerical contradiction once both nonzero norms are constant and the published Weyl gaps have been applied.
```
theorem not_two_constant_blocks {v b : ℝ} (hv : 0 ≤ v) (hb : 0 ≤ b)
    (hvGap : 1 ≤ v ^ 2) (hbGap : 1 ≤ b ^ 2) : ¬ v + b < 2 := by
…
```
theorem OAI.PositiveEinsteinFour.coupled_square_identity line 186
theorem OAI.PositiveEinsteinFour.coupled_nonpositive line 192
theorem OAI.PositiveEinsteinFour.coupled_strictly_negative line 201

theorem OAI.PositiveEinsteinFour.ae_equality_of_coupled_bound line 213

Source documentation

The measure-theoretic closing step: a nonnegative integral forces equality in the pointwise Cauchy--Schwarz bound. No integrability of the separate possibly singular summands is needed here beyond integrability of I.

theorem ae_equality_of_coupled_bound {X : Type*} [MeasurableSpace X]
    {μ : Measure X} {I c θ r j : X → ℝ}
    (hIi : Integrable I μ) (hIntegral : 0 ≤ ∫ x, I x ∂μ)
    (hc : ∀ᵐ x ∂μ, 0 < c x) (hj : ∀ᵐ x ∂μ, r x ^ 2 ≤ j x)
    (hI : ∀ᵐ x ∂μ,
      I x ≤ -c x * j x + 2 * θ x * r x - θ x ^ 2 / c x) :
    ∀ᵐ x ∂μ, j x = r x ^ 2 := by
…

theorem OAI.PositiveEinsteinFour.zero_energies_of_radial_equality line 239

Source documentation

Equality in the radial bound annihilates both gradient energies. The assumptions concerning level sets are exactly the scalar level-set fact used in the manuscript, and are kept separate from the new coupled bound.

theorem zero_energies_of_radial_equality {v b p q : ℝ}
    (hv : 0 ≤ v) (hb : 0 ≤ b) (hp : 0 ≤ p) (hq : 0 ≤ q)
    (hpzero : v = 0 → p = 0) (hqzero : b = 0 → q = 0)
    (hpone : v = 1 → p = 0) (hqone : b = 1 → q = 0)
    (heq : (p + q) * (p / v + q / b) =
      (normWeight v * p + normWeight b * q) ^ 2) : p = 0 ∧ q = 0 := by
…

Mentions: OAI.PositiveEinsteinFour.normWeight

theorem OAI.PositiveEinsteinFour.ae_zero_energies_of_coupled_bound line 264

Source documentation

The first conclusion of the one-block vanishing argument, including zero sets. The new geometric estimate on I is an explicit premise of this scalar reduction, not an assumed published theorem or a claim that the geometric estimate has already been proved.

theorem ae_zero_energies_of_coupled_bound {X : Type*} [MeasurableSpace X]
    {μ : Measure X} {I θ v b p q : X → ℝ}
    (hIi : Integrable I μ) (hIntegral : 0 ≤ ∫ x, I x ∂μ)
    (hv : ∀ᵐ x ∂μ, 0 ≤ v x) (hb : ∀ᵐ x ∂μ, 0 ≤ b x)
    (hsum : ∀ᵐ x ∂μ, v x + b x ≤ 2)
    (hp : ∀ᵐ x ∂μ, 0 ≤ p x) (hq : ∀ᵐ x ∂μ, 0 ≤ q x)
    (hsupport : ∀ᵐ x ∂μ,
      (v x = 0 → p x = 0) ∧ (b x = 0 → q x = 0) ∧
      (v x = 1 → p x = 0) ∧ (b x = 1 → q x = 0))
    (hI : ∀ᵐ x ∂μ,
      I x ≤ -couplingCoefficient (v x) (b x) *
        ((p x + q x) * (p x / v x + q x / b x)) +
…

Mentions: OAI.PositiveEinsteinFour.couplingCoefficient

theorem OAI.PositiveEinsteinFour.ae_eq_mean_of_zero_energy line 295

Source documentation

A variance bound turns a vanishing gradient energy into an almost-everywhere constant. The mean is left explicit so the lemma does not require a particular normalization of the measure.

theorem ae_eq_mean_of_zero_energy {X : Type*} [MeasurableSpace X]
    {μ : Measure X} {v p : X → ℝ}
    (hi : Integrable (fun x => (v x - ∫ y, v y ∂μ) ^ 2) μ)
    (hvariance : (∫ x, (v x - ∫ y, v y ∂μ) ^ 2 ∂μ) ≤ ∫ x, p x ∂μ)
    (hp : p =ᵐ[μ] 0) : v =ᵐ[μ] fun _ => ∫ x, v x ∂μ := by
…

theorem OAI.PositiveEinsteinFour.one_block_vanishes_of_coupled_bound line 312

Source documentation

The full scalar one-block vanishing step of Section 8. The combined integrand estimate is a premise, and remains a separate geometric obligation; this theorem does not identify it as a published result. The variance and gap premises have exactly the normalizations needed in the closing argument.

theorem one_block_vanishes_of_coupled_bound {X : Type*} [MeasurableSpace X]
    {μ : Measure X} [IsProbabilityMeasure μ] {I θ v b p q : X → ℝ}
    (hIi : Integrable I μ) (hIntegral : 0 ≤ ∫ x, I x ∂μ)
    (hv : ∀ᵐ x ∂μ, 0 ≤ v x) (hb : ∀ᵐ x ∂μ, 0 ≤ b x)
    (hsum : ∀ᵐ x ∂μ, v x + b x < 2)
    (hp : ∀ᵐ x ∂μ, 0 ≤ p x) (hq : ∀ᵐ x ∂μ, 0 ≤ q x)
    (hsupport : ∀ᵐ x ∂μ,
      (v x = 0 → p x = 0) ∧ (b x = 0 → q x = 0) ∧
      (v x = 1 → p x = 0) ∧ (b x = 1 → q x = 0))
    (hI : ∀ᵐ x ∂μ,
      I x ≤ -couplingCoefficient (v x) (b x) *
        ((p x + q x) * (p x / v x + q x / b x)) +
…

Mentions: OAI.PositiveEinsteinFour.couplingCoefficient