The combined main theorem from the no-selection statement

anomalous_dissipation_full_of_noSelection: for α < 1/3 choose β, the ingredients I with a large Λ, the stream sequence and its limit φ, and κ_j = ε_{j+1}^p; then the three parts follow from a0Core_contract, uniformHolder_contract and the no-selection statement.

theorem AVenhance.Infra.FullTheorem.FullAssembly.exists_beta (α : ℝ) (hα₀ : 0 < α) (hα₁ : α < 1 / 3) : ∃ (β : ℝ), 6 / 5 ≤ β ∧ α < β - 1 ∧ β < 4 / 3 ∧ 1 < β

Numerical choice of the exponent β.

theorem AVenhance.Infra.FullTheorem.anomalous_dissipation_full_of_noSelection (hNS : ∀ (β C₀ : ℝ), NoSelectionContract β C₀) : AnomalousDissipationFullStatement

The combined main theorem from the no-selection input.