Small inputs of the no-selection argument, proved

• twoDiffusivity_contract: comparison of two diffusivities with the same drift;
• cosineDatum_contract: facts about the cosine data;
• velGrad_contract: gradient bound on the drift of the stream sequence;
• a0Core_contract: the main theorem at ingredient level (for the given limit field).

theorem AVenhance.Infra.FullTheorem.Contracts.twoDiffusivity_contract : TwoDiffusivityContract

theorem AVenhance.Infra.FullTheorem.Contracts.cosineDatum_contract : CosineDatumContract

theorem AVenhance.Infra.FullTheorem.Contracts.velGrad_contract (β C₀ : ℝ) : VelGradContract β C₀

theorem AVenhance.Infra.FullTheorem.Contracts.a0Core_contract (β C₀ : ℝ) (hβ : 6 / 5 ≤ β) : A0CoreContract β C₀