Main theorem from the two remaining estimates, step-down and classical well-posedness

Stream-function estimates (AVenhance.limit_field_regular) is proved, so its literal-statement hypothesis of anomalous_dissipation_of_keystones is discharged by the theorem itself. Only step-down and classical well-posedness remain, as literal hypotheses.

theorem AVenhance.Infra.Section5.Integration.anomalous_dissipation_of_A8_A1c (hA8 : ∀ (β C₀ : ℝ), IndyStepDownContract β C₀) (hA1c : ClassicalWellposedContract) : AnomalousDissipationStatement

Main theorem from the literal step-down and classical well-posedness statements (stream-function estimates is proved).