rm2Closed_of_bet3
plain-language theorem explainer
Any RM2URadialProfile obeying the Bet 3 coercive L2 hypothesis produces a closed RM2 system on its A component. Navier-Stokes workers in the Recognition Science program cite this to connect the direct inheritance assumption to the RM2 target without deriving tail-flux vanishing. The proof is a one-line wrapper that extracts the coercive field and feeds it to the coerciveL2Bound closure lemma.
Claim. Let $P$ be an RM2URadialProfile. If $P$ satisfies the Bet 3 coercive $L^2$ bound hypothesis, then the RM2 system is closed for the component $P.A$.
background
The RM2U.NonParasitism module isolates non-parasitism as the single hard gate: the tail-flux boundary term at infinity vanishes for the relevant ell=2 coefficient, written TailFluxVanish P.A P.A'. Bet3CoerciveL2Hypothesis is the structure that directly assumes CoerciveL2Bound P, bypassing derivation of the flux condition. This keeps the RM2U to RM2 pipeline clean and checkable once the missing tailFlux to coercive step is supplied as an interface in EnergyIdentity.
proof idea
The proof is a one-line wrapper that applies rm2Closed_of_coerciveL2Bound from RM2U, substituting the coercive field extracted from the Bet3CoerciveL2Hypothesis structure.
why it matters
This theorem completes the Bet 3 inheritance route to RM2Closed and supplies one of the end-to-end closure wrappers in the module. It addresses the non-parasitism gate in the Navier-Stokes translation of Recognition Science, where the tail-flux vanishing is the key hypothesis. It leaves open the derivation of the coercive bound from the underlying RS forcing chain rather than assuming it outright.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.