Moments.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

The integer reduction in the balanced-Weyl-moment argument. Volume is normalized so that the Euler identity is 2 + n + m = volume * (1 + P + Q).

theorem OAI.PositiveEinsteinFour.ordered_harmonic_counts line 15

Source documentation

The characteristic identities, two gaps, and upper volume estimate leave only the ordered exceptional pair (n₊, n₋) = (2, 1) if the counts differ.

theorem ordered_harmonic_counts (n m : ℕ) (P Q volume : ℝ)
    (hP : 1 ≤ P) (hQ : 1 ≤ Q) (horder : Q ≤ P) (hsum : P + Q < 4)
    (hvolume : 0 < volume)
    (hupper : volume ≤ 2 * (1 - 3 / 40 * (P + Q)))
    (heuler : 2 + (n : ℝ) + (m : ℝ) = volume * (1 + P + Q))
    (hsignature : (n : ℝ) - (m : ℝ) = 2 / 3 * volume * (P - Q)) :
    n = m ∨ n = 2 ∧ m = 1 := by
…

theorem OAI.PositiveEinsteinFour.exceptional_moment_relation line 51
Source documentation
In the exceptional count pair, the larger second moment is fixed by the smaller one. This is the exact 13/7 relation used before the two-moment obstruction.
```
theorem exceptional_moment_relation (P Q volume : ℝ)
    (heuler : 5 = volume * (1 + P + Q))
    (hsignature : 1 = 2 / 3 * volume * (P - Q)) :
    P = (13 * Q + 3) / 7 := by
…
```
theorem OAI.PositiveEinsteinFour.exceptional_moment_constraint line 65
Source documentation
Integrating v² ≤ (2-b)² with the exceptional relation yields the second constraint of the scalar moment obstruction. mean is the mean of b.
```
theorem exceptional_moment_constraint (P Q mean : ℝ)
    (hrelation : P = (13 * Q + 3) / 7)
    (hpointwise_integral : P ≤ 4 - 4 * mean + Q) :
    28 * mean + 6 * Q ≤ 25 := by
…
```