CoerciveImpliesRM2Hypothesis
plain-language theorem explainer
CoerciveImpliesRM2Hypothesis supplies a named interface that a coercive L2 bound on radial profile P implies RM2 closure, where closure means finiteness of the log-critical moment for P.A. Navier-Stokes regularity researchers extending the Recognition Science treatment would cite this placeholder to keep downstream developments free of scattered assumptions. The structure is realized as a one-line wrapper around the already-proved rm2Closed_of_coerciveL2Bound lemma.
Claim. For an RM2U radial profile $P$, the hypothesis asserts that the coercive $L^2$ bound on $P$ implies RM2 closure of the coefficient $P.A$, where RM2 closure is defined as finiteness of the log-critical moment.
background
RM2Closed is the placeholder definition RM2Closed A := LogCriticalMomentFinite A, which encodes boundedness of the log-critical $l=2$ tail moment for coefficient A. CoerciveL2Bound P is the L2 control assumption imported from the Core module. The local setting in RM2U.RM2Closure hosts the classical closure steps: coercive $l=2$ control implies finiteness of the shell moment integral |A|/r, which bounds the affine obstruction (RM2).
proof idea
The structure itself is a scaffolding placeholder with no body. Its concrete realization is the one-line wrapper of_proved that applies the proved lemma rm2Closed_of_coerciveL2Bound to construct the hypothesis instance.
why it matters
This declaration earns its place by providing the single named interface hypothesis that downstream Navier-Stokes code can depend on while the file stays axiom-free. It directly fills the placeholder role described in the module documentation for the coercive $l=2$ to RM2 closure steps from navier-dec-12-rewrite.tex. It supports the Recognition Science treatment of fluid equations inside the forcing chain and phi-ladder, with the explicit closure proof still to be supplied.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.