of_proved
plain-language theorem explainer
The declaration supplies a named interface hypothesis asserting that coercive ell-two control on a radial profile implies RM2 closure. Analysts extending the RM2U model for Navier-Stokes regularity would reference it to centralize assumptions. Its proof is a direct term construction from the prior Cauchy-Schwarz lemma on integrability.
Claim. Let $P$ be a radial profile with coefficient function $A$. Then coercive $ell=2$ control on $P$ implies that $A$ satisfies the RM2 closure condition.
background
The RM2U closure module hosts steps converting coercive ell-two bounds into RM2 statements for radial profiles. A radial profile consists of a function $A$ together with its first and second derivatives satisfying the appropriate differentiability conditions on $(1,infty)$. The interface hypothesis is defined as the proposition that any coercive L2 bound on the profile yields RM2 closure for $A$. Upstream, the key lemma establishes this implication via a Cauchy-Schwarz argument showing that L2 integrability of $A$ forces L1 integrability of $A/r$.
proof idea
The proof applies the established implication lemma directly to the given profile, packaging the result into the interface structure. This is a one-line term-mode construction that invokes the Cauchy-Schwarz integrability step without additional tactics.
why it matters
This result occupies the interface layer of the RM2U closure, providing a single named placeholder for the coercive ell-two to RM2 step described in the manuscript. It ensures downstream developments remain free of scattered axioms. The construction mirrors the one-line argument that L2 control on $A$ implies absolute convergence of the log-critical shell moment integral of $|A|/r$.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.