GrowthContradiction.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

The scalar contradiction in the branching argument

At the end of Section 9 of the supplied manuscript, the mass in the moving box is bounded below by 3^n * m₀ and above by C * (1 + (1+a)^n * t₀)^4. The following argument proves that those estimates cannot both hold when (1+a)^4 < 3. It assumes no kinetic equation, branching kernel, or existence statement.

theorem OAI.BoltzmannNonuniqueness.GrowthContradiction.fourth_power_cap_le line 28
Source documentation
The fourth-power cap along a geometric sequence of times is itself bounded by a geometric sequence, with growth ratio r^4.
```
theorem fourth_power_cap_le {r t₀ : ℝ} (hr : 1 ≤ r) (ht₀ : 0 ≤ t₀) (n : ℕ) :
    (1 + r ^ n * t₀) ^ 4 ≤ (1 + t₀) ^ 4 * (r ^ 4) ^ n := by
…
```

theorem OAI.BoltzmannNonuniqueness.GrowthContradiction.no_uniform_branching_cap line 41

Source documentation

The simultaneous branching lower bound and fourth-power cap bound are impossible.

theorem no_uniform_branching_cap {a t₀ m₀ C : ℝ}
    (ha : 0 < a) (ht₀ : 0 < t₀) (hm₀ : 0 < m₀) (hC : 0 ≤ C)
    (hgrowth : (1 + a) ^ 4 < 3) :
    ¬ ∀ n : ℕ, (3 : ℝ) ^ n * m₀ ≤ C * (1 + (1 + a) ^ n * t₀) ^ 4 := by
…

theorem OAI.BoltzmannNonuniqueness.GrowthContradiction.exists_generation_exceeding_cap line 70

Source documentation

Consequently some generation has branching mass strictly larger than the cap permits.

theorem exists_generation_exceeding_cap {a t₀ m₀ C : ℝ}
    (ha : 0 < a) (ht₀ : 0 < t₀) (hm₀ : 0 < m₀) (hC : 0 ≤ C)
    (hgrowth : (1 + a) ^ 4 < 3) :
    ∃ n : ℕ, C * (1 + (1 + a) ^ n * t₀) ^ 4 < (3 : ℝ) ^ n * m₀ := by
…